Introduce basic & (additive conjunction) and possibly ⊤ (top - additive conjunctive unit) types

Start by reviewing the proposed encodings in this issue and the referenced issues #474 and #405; the payload names no implementation files or tests. Determine whether the project should add additive conjunction alone or also top, then validate an accepted design against the stated linearity and laziness concerns. Done means an agreed API and implementation scope, followed by the relevant project tests.

This is split off from https://github.com/tweag/linear-base/issues/474, but this is much more focused and trimmed down, and specifically concerned with & and (maybe) ⊤ which I think are well behaved. I'm not suggesting any of the dependent co-data in that thread be added, nor ⅋ and ⊥ which I am still unsure about and think are problematic. I don't think & has similar issues (I hope to justify this at the end) - my only concern is if optimisations could break the encoding described at the bottom but then maybe they'd be a problem for other unsafe linear implementations? There are some mentions of unsafety of laziness and I use a lazy pair for the suggested representation, I'm not sure if this is actually a problem or not, it's not a lazy match.

I checked the examples in 9.14.1, but had a lot of extensions enabled.

Preamble (if you know what & is skip this paragraph)
& is a tensor much like (,) and Either. In regular Haskell, it is the same as (,). LinearTypes distinguishes the two (and the corresponding units ⊤, and () aka 1). & represents additive conjunction - consumer choice. Like (,) (multiplicative conjunction) there are two resources the producer might supply, but like Either (additive disjunction) only one of those resources is ever given and must be handled. Unlike Either, the consumer chooses which is produced. These are generally linear resources that are produced in separate branches.

-- Safe straw-man encoding, a & b = ¬(¬a + ¬b)
-- Notice: no unrestricted fields or functions
newtype a & b = With (forall r . Either (a %1 -> r) (b %1 -> r) %1 -> r)
-- The projections really are linear without the data being unrestricted
-- This is the consumer side difference between (,) and (&)
fst :: a & b %1 -> a
snd :: a & b %1 -> b
-- proof
fst (With h) = h (Left (\x -> x))
snd (With h) = h (Right (\x -> x))

Example uses:

• Affine types a & () that can either be used once or not (but you can't use this to discard other as)
• Linear eliminator for either:

  either :: (a %1 -> r) & (b %1 -> r) %1 -> Either a b %1 -> r
  either ab (Left a) = fst ab a
  either ab (Right a) = snd ab a
  

• Servers that have multiple exclusive routes - you must choose exactly one
• Alternative to #405

I previously gave an example using a GADT - this encoding is equivalent (seemingly - less room for laziness/more efficient).

data Y a b c where
  L :: Y a b a
  R :: Y a b b

newtype WithY a b = WithY (forall c . Y a b c -> c)

withToY :: a & b %1 -> WithY a b
withToY (With h) = WithY (\case
  L -> h (Left (\x -> x))
  R -> h (Right (\x -> x)))

yToWith :: WithY a b %1 -> a & b
yToWith (WithY h) = With (\case
  Left f -> f (h L)
  Right f -> f (h R))

In response to @aspiwack's previous comment about adding it https://github.com/tweag/linear-base/issues/474#issuecomment-1938225850.

You touch upon one reason why additive product isn't in linear-base: negatives aren't preserved by effects; yet it feels that they are most useful in presence of effects. We could parameterise by the effect, something like

newtype With m a b = With (forall c . Y a b c -> m c)
Though this feels awkward (plus it doesn't actually associate, I believe, so we'd probably have to conceive of an n-ary version instead).

This can be represented by m a & m b in the non-m encoding but this version forces you to shove an m in there e.g. Identity. I think there are legitimate uses outside of monadic contexts and not any reason to impose it on the type unless you want a new transformer type (if there's even a co/monad out of this... maybe there is).

Another reason is that there are quite a few potential encodings. Besides the one you're proposing, I can think of

newtype With a b = With (forall k. (Either (a %1 -> k) (b %1 -> k)) %1 -> k)
and

data With a b where
With :: x %1 -> (x %1 -> a) -> (x %1 -> b) -> With a b
(note: the two projection functions are unrestricted, the rest of the arrows are linear)

The former is equivalent to the Y version as demonstrated above (but potentially with more laziness due to Either and extra functions). The latter I don't believe is truly an encoding of & as it requires unrestricted eliminators. The usage of the eliminators should also be & - you will use choose to use exactly one of them exactly once. (I'm not a category theory person but I think this is a yoneda encoding or something like that.)

data WithMap a b where
  -- no more unrestricted arguments
  WithMap :: x %1 -> (x %1 -> a) & (x %1 -> b) %1 -> WithMap a b

-- equivalent to & straw-man at the top

withMap :: a & b -> WithMap a b
withMap a = WithMap a (With (\case
  Left f -> f fst
  Right f -> f snd))

mapWith :: WithMap a b %1 -> a & b
mapWith (WithMap x fg) = With (\case
  Left f -> f (fst fg x)
  Right f -> f (snd fg x))

The point of having data types in a standard library is to serve as a synchronisation point, but I couldn't decide which of the many choices available were best. I should also say that I have a feeling that, because additive conjunction isn't native to data type fields, it's often better to define your own custom with-like type (maybe it's ternary, maybe it's recursive, …) than to use a prebuilt one (which you'll rightly counter by saying that this doesn't cover the definition of optics).

Note for context - in the other thread I was suggesting some far more general ideas, I'm not suggesting those here.
I think just the pair by itself (and maybe its unit) is useful. If you are not concerned with efficiency, you can use it for N-ary cases - it's only as inefficient as the standard inductive HList definition. This doesn't include a dependent version, but then neither does base contain a dependent (,) or Either. I haven't really considered recursion in detail but I don't see why it wouldn't work with a recursive case, the same way you can use (,) and Either recursively.

Insofar as Haskell does not have native codatatypes, I think this is unambiguously the best possible implementation of & for linear-base if there are no optimisation problems:

data a & b = UnsafeMkWith a b

fst :: a & b %1 -> a
fst (UnsafeMkWith !a b) = unsafeConst a b

snd :: a & b %1 -> b
snd (UnsafeMkWith a !b) = unsafeConst b a

with :: (forall r . Either (a %1 -> r) (b %1 -> r) %1 -> r) %1 -> a & b
with = unsafeCoerce unsafeWith

unsafeWith :: (forall r . Either (a %1 -> r) (b %1 -> r) %1 -> r) -> a & b
-- this should be lazy in both fields, so the given function is only called when a field is requested
-- and only one field should be requested if a & b is used linearly, otherwise it's already unrestricted
-- which should make & and (,) equivalent
unsafeWith f = UnsafeMkWith (f (Left (\x -> x))) (f (Right (\x -> x)))

-- Internal
unsafeConst :: a %1 -> b %1 -> a
unsafeConst = Unsafe.toLinear2 const

This piggybacks off of Haskell's laziness. Both fields in the pair are lazy and so can store linear thunks that would mutate the same thing in conflicting ways. Only one should ever be sequenced (if used linearly, if not you shouldn't have such thunks to begin with) - assuming issues caused by optimisation. There's no additional laziness (beyond the overall type and any within its arguments, a practical necessity). It is an efficient representation (at least as far as lazy pairs go).

I think Top is slightly more ambiguous. If we are not concerned with having garbage collected what was put into it, an empty datatype might do (but again, effects). I am not concerned with which (or whether) top is added, but it would be nice to have a general tensor interface and it gives you things like applicative/traversable/optics analogues for a different tensor. (I may need to consider laziness here also.)

-- existential version
data Top = forall a . Top a
-- Void eliminator version
data Void
newtype Top2 = Top2 (forall a . Void -> a)
-- equivalent
top2 :: Top %1 -> Top2
top2 (Top x) = Top2 (\y -> case y of {} x)

twoTop :: Top2 %1 -> Top
twoTop = Top

Now, as someone who wants negative type combinators in the library, indeed the first such someone, you have your say in what will go inside. So let's talk some more. Your server example doesn't look like it'd benefit from additive conjunction directly, would it? But what I'm reading is that you were doing something and were somewhat annoyed by not having additive conjunction available. What was that something you wanted additive conjunction for?

I'm not saying it's the best implementation, and I haven't double checked this, but I believe you could implement the server example with something like the following:

newtype Server a = Server (
  (String -> (Server a, Bool)) &
  (Int -> Server a) &
  (Server a, Int) &
  ()) -- instead of impredicative type

then expose the individual accessors as separate linear functions.
Though the GADT version is saner and maybe you would just cheat with a record like I'm suggesting for &.

I didn't have a particular case where I wanted to use &, really I'm more just interested in linear types generally and think & would be useful. I think having something in a standard(ish) library is a bit of a two-way street in Haskell, on the one hand things used a lot get added but on the other hand things added get used a lot more. So if this doesn't seem worth it feel free to ignore it.

As for co-data types in general and ⅋, here is my opinion on why & is reasonable. The eliminators for & have a single destination/negative argument, much like functions. This is why I think they introduce no problems in Haskell (which is based on natural deduction, not sequent calculus). Lazy pairs already behave much like them (excluding construction). ⅋ does not (by definition as codata it should be given take two continuations). All of the (safe) encodings of & and ⊤ I've been able to convert between. I still have no clue as to a proper encoding of ⅋ or negation, perhaps all of the things have actually been proper but simply aren't equivalent in Haskell outside of a double elimination context.

I've also been able to do all of the expected tensor operations (at least with & and Top) but perhaps need to look into laziness in case there's any room for error. I don't think there is beyond possibly representing additional laziness (which (,) and Either already do).

-- using safe encoding
data Top = forall a . Top a

-- inverse: fst
inL :: a %1 -> a & Top
inL x = With (\case
  Left f -> f x -- fst: calls with Left id, giving back x
  Right f -> f (Top x))

swap :: a & b %1 -> b & a
swap (With h) = With (\case
 -- clearly symmetric
  Left f -> h (Right f)
  Right f -> h (Left f))

assocL :: a & (b & c) %1 -> (a & b) & c
assocL h = With (\case
  -- assocR is similar
  Left f -> f (With (\case
    Left f -> f (fst h)
    Right f -> f (fst (snd h))))
  Right f -> f (snd (snd h)))

map :: (a %1 -> a') & (b %1 -> b') %1 -> (a & b) %1 -> (a' & b')
map fg ab = With (\case
  Left f -> f (fst fg (fst ab))
  Right f -> f (snd fg (snd ab)))