Linear types - additive conjunction via linear record projections?

[Jashweii]

https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst #111 #91
"Projections take an unrestricted record as argument: f1 :: R -> A1 (because otherwise the other fields would not be consumed)"
"we didn't consider additive pairs to be useful enough to justify a dedicated implementation and syntax."

Wouldn't it be possible to use restricted records/data type projections for additive conjunction with minimal extra syntax?
I personally have very little idea about linear logic outside of messing with linear types in GHC, and really don't know if it would work with the theory of LinearHaskell.

-- Additive pair, pseudo syntax. The multiplicity is the multiplicity of the record parameter in projections, 
-- i.e. (&) a b %1 -> a, (&) a b %1 -> b
data (&) a b = AP %1 { fst :: a, snd :: b } 
f :: Handle %1 -> Handle & Handle
f h = AP { fst = h, snd = h } -- Ok, these are distinct branches. A consumer can only take one of them
g :: Handle %1 -> (Handle, Handle) & ()
g h = AP { fst = (h, h), snd = () } -- Bad on both sides, in one branch we duplicate h in the other we drop it
pi1 :: (a & b) %1 -> a
pi1 AP{fst=a} = a -- Ok, pattern is complete because extracting fst consumes the additive pair
pi12 :: (a & b) %1 -> (a, b)
pi12 AP{fst=a, snd=b} = (a, b) -- Bad, doesn't typecheck, duplicating the a. pair
pi0 :: (a & b) %1 -> ()
pi0 AP{} = () -- Likewise, dropping the a. pair

With OverloadedRecordDot and RebindableSyntax (or multiplicity polymorphic HasField):

data Server 
  = Server %1 
  { route1 :: Server
  , route2 :: Int -> Server
  , route3 :: Server
  , route4 :: Int
  }
f :: Server %1 -> Int -> Int
f s a =  (s.route1.route2 a).route3.route4

Exactly the same as the non linear version, except linear in the server.
This would also let you write two one new unit type:

data A = A %'Many
data B = B %'One -- Is this one ()?

Maybe this could also be done for sum types?

[Jashweii]

Having thought about this some more it is not quite as simple when it comes to pattern matching, and this similarly is affected by laziness.
In terms of semantics I imagined them behaving as regular records aside from typing rules - internally it would duplicate resources between the fields but these duplicates would be guarded by the premise that exactly one such field is used.
First, you can have AP{fst} and AP{snd} in separate branches, but you have to take sequencing into account for lifted fields

dubious, ok, ok2 :: Bool -> () & () %1 -> ()
-- This function could only be accepted if the bool was guaranteed to be sequenced first.
dubious False AP{fst=()} = ()
dubious True AP{snd=x} = x
-- Make explicit the sequencing.
ok False = \AP{fst=()} -> ()
ok True = snd
-- There is no subsequent case (and this is a complete match).
ok2 _ AP{fst=()} = ()

Second, only taking one is overly restrictive if the usages are themselves separated, for example:

bimap :: (a %1 -> a') & (b %1 -> b') %1 -> (a & b) %1 -> (a' & b')
bimap AP{fst=f, snd=g} AP{fst=x, snd=y} = AP{fst=f x,snd=g y}

I think it is sound to rule out a mix of Record %1 -> Field1 and Record %'Many -> Field2 which would imply per field annotations, because then you have to decide how to combine the additive and multiplicative parts anyway.

I also made sense out of the new unit I was having trouble understanding. It is a possibly fatal downside to using constructor %m - the units are backwards. data () = () %1, the unit of non-empty multiplicative records (which would be %Many with the same syntax). How it behaves:

-- By analogy against the function encoding of an additive pair - empty set of fields
data Void :: UnliftedType
newtype T = T (forall x . Void %1 -> x)
-- Easy to construct
t :: T
t = T \case{}
-- Appears to consume everything linearly
hide :: a %1 -> T %1 -> T
hide a (T f) = T (\case{} f a)
-- But can't be linearly consumed. 
-- drop :: T %1 -> ()
-- drop (T f) = -- I have to use f. That means calling it with a Void. (I'm not 100% on what it would do for a lifted type)
-- Another present way of writing it.
data T = forall a . T a 
t  = T ()
hide a (T x) = T (a, x) -- gets bigger unfortunately
-- drop (T a) = -- Need (forall a . a %1 -> ()) to use a
-- As a primitive
data T = T %'Many -- With the idea in this thread, because projecting uses it many times
t = T
hide _ _ = T -- Producing T allows me to ignore the argument linearly, because T itself can't be used linearly.

[goldfirere]

I'm intrigued by this possibility -- in particular the simple syntax you include (a linear annotation that applies to the whole record-field blob).

But I actually don't understand the drawbacks you list in your second post. Could you work out one specific example showing what can go wrong?

[Jashweii]

I've realised you can't actually currently type the constructor (much like linear if then else without encoding that via a function). I think that's what LinearHaskell relies on currently for multiplicative records, maybe it would work if fully applied?
Essentially (APair a b) needs to be typed like if _ then a else b should be. I don't see a simple way of assigning it a type that doesn't involve at least existentials (since the multiplicity is decided after the value is made, we only know that exactly one of the fields is consumed).

I think the way I originally put it (the multiplicity of projections) is ambiguous in the unit/empty record case (there are no projections), which is probably why I got confused and was suspicious about it - it's likely an arbitrary choice of syntax.
Really all you need is a way of distinguishing additive and multiplicative conjunction for records (e.g. by putting %1 on the constructor - or any other sort of annotation).
If there isn't a better syntax for it, %1 for additive unit as I originally thought before "correcting" myself would probably be more sensible.
This way records today are %'Many (regardless of if they are empty) and it specifies additive vs multiplicative independent of if there are no fields, and the unit is naturally the empty record with the same % annotation.
In practice you would make the %1 projections multiplicity polymorphic like those on newtypes are planned to be (there is no difference between additive/multiplicative for a single field).

With the part about seq, I am thinking of what would normally be side effects in thunks made invisible via linear types.
This is more ergonomic and less of a wart than () ->, for a concrete example similar to the server type above:

data Summater
  = Summater %1
  { result :: Int
  , add :: Int -> Summater
  , so_far :: (Int -> Summater) %1 -> Summater
  }

summatePure :: Int -> Summater
summatePure n = Summater { result = n, add = summatePure . (+ n), so_far = ($ n) }

summateRef :: Int -> (Summater %1 -> Ur b) %1 -> Ur b
summateRef n f = 
 -- create a reference to an int with initial value n
 -- return f a where
 --   result a = (current value of ref)
 --   so_far a = \f -> f (current value of ref)
 --   add    a = \n -> add n to ref `seq` a

Note that both cases are visibly pure, and use the same type (modulo the signature of summateRef itself since it produces something that needs using uniquely).
This doesn't work if you can seq a field linearly without using it.

[Jashweii]

Having read MMH: High-level programming with the Mu-Mu-Tilde-calculus this now makes far more sense to me than it did when I wrote this. Essentially this is just about codata.

-- Multiplicative conjunction
data (a, b) where
  (,) :: a %1 -> b %1 -> (a, b)
-- Additive conjunction (reads similarly to additive disjunction i.e. Either)
codata a & b where
  L :: a & b %1 -> a
  R :: a & b %1 -> b
-- Additive disjunction
data Either a b where
  Left :: a %1 -> Either a b
  Right :: b %1 -> Either a b
-- Multiplicative disjunction*
codata a ⅋ b where
  (⅋) :: a ⅋ b %1 -> Either a b 
  -- Not certain this is a faithful translation

Without LinearTypes, the two types of conjunction are essentially isomorphic (esp. as Haskell is lazy).

-- Embedding of codata parameterised over observation GADT
newtype Co f = Co (forall a . f a -> a)
data Y a b ab where
  L :: Y a b a
  R :: Y a b b
type a & b = Co (Y a b)

to :: (a, b) -> a & b
to (a, b) = Co \case
  L -> a
  R -> b

fro :: a & b -> (a, b)
fro (Co h) = (h L, h R)

But with LinearTypes, they are not. In either branch to only uses one of the pair components (dropping one), fro tries to get both & branches (duplicating one). So I suppose if someone wanted a real proposal for this, it would be add user-defined codata. I'm not aware of any other benefit of adding them to Haskell, aside from the neatness of a user being able to define -> as a co-datatype, or introducing co-patterns.

[Jashweii]

The general case makes the correspondance between records and co-data noticed in this issue more obvious

codata T a1...an where
  K1 :: forall b11 ... b1n . C1 => A11 %M11 ... -> A1N %M1N -> (T a1...an %1 -> X1)
  ...
  KN :: forall bN1 ... bNn . CN => AN1 %MN1 ... -> ANN %MNN -> (T a1...an %1 -> XN)

vs (ignoring linearity differences of the overall record and whether the type is the first or last arg)

data T a1...an = T 
  { k1 :: {- T a1..an -> -} forall b11 ... b1n . C1 => A11 %M11 ... -> A1N %M1N -> X1
  ...
  , kn ::                   forall bN1 ... bNn . CN => AN1 %MN1 ... -> ANN %MNN -> XN
  }

\cocase
  K1 @b11 ... @b1n {- given C1 -} a11 ... a1n -> e1 : X1
  ...
  KN @bN1 ... @bNn {- given CN -} aN1 ... aNn -> eN : XN

vs (ignoring linearity differences of the overall record)

T 
  { k1 = \@b11 ... @b1n {- given C1 -} a11 ... a1n -> e1 : X1
  ...
  , kN = \@bN1 ... @bNn {- given CN -} aN1 ... aNn -> eN : XN }

(this would be nicer if you could define record fields like top-level/let/where/\cases bindings, i.e. T { k1 True ... = ..., k1 False ... = ..., ... })

The new unit is ⊤

codata (⊤) where {}
(⊤) :: (⊤)
(⊤) = \cocase {}
-- today, (exists a. a)
data (⊤) = forall a . (:⊤) a
(⊤) :: (⊤)
(⊤) = (:⊤) ()

Again without LinearTypes this is indistinguishable from (), but with LinearTypes you cannot consume it linearly.
As codata: has no destructors to call.
As data: cannot linearly consume arbitrary type.
This is a unit for & but not (,) aka ⊗

f :: ⊤ & a %1 -> a
f = R -- choose right branch never producing ⊤
g :: a %1 -> ⊤ & a
g a = \cocase
  L -> ⊤ a -- can dump arbitrary resources into ⊤
  R -> a

A general case of this can be seen with heterogeneous lists

data a ∈ as where
  EZ :: a ∈ (a ': as)
  ES :: !(a ∈ as) -> (a ∈ (b ': as))
-- not concerned with linearity of ∈

data HL as where
  HZ :: HL '[]
  HS :: a %1 -> HL as %1 -> HL (a ': as)

data HL' as = HL' (forall a . a ∈ as -> a)

Without LinearTypes, HL and HL' are the same aside from performance, laziness, and determining the length of the type-level list. With LinearTypes, HL is foldr ⊗ 1 but HL' is foldr & ⊤. If you are taking them linearly, you must use every field of HL but exactly one field of HL'.

This covers destructors that take no arguments, I think you can just make the results of other destructors into functions similar to the record syntax example above. (Of course if you were defining -> itself you couldn't do this.)

The paper mentioned focuses on a proof language for sequent calculus, where data constructors/codata destructors take coterm parameters. The way I'm interpreting this for something based on the lambda calculus is to produce a function from the codatatype (same as taking a co-term parameter/exit continuation for the result). Non-GADT syntax isn't obvious in this case - maybe you would have to add -> result type to each destructor (but then record constructor syntax would mean something else to the above interpretation).

With all this said it is still conceivable (but less clean) to add an indicator to a single constructor datatype to say to interpret it as foldr & ⊤ instead of introducing codata. Essentially the arguments would be checked as branches instead, and a single field access would be %1 usage. There would probably be some questions about where strictness is allowed also kind of like the existing limitations of linear types. The earlier idea of working with multiple branches at once would be far more work to implement (probably not worth it), kind of like or patterns but combined with "or bodies". Like the earlier example

bimap :: (a %1 -> a') & (b %1 -> b') %1 -> (a & b) %1 -> (a' & b')
-- bimap AP{fst=f, snd=g} AP{fst=x, snd=y} = AP{fst=f x,snd=g y}
bimap fg xy = AP
  { fst=fst fg (fst xy)
  , snd=snd fg (snd xy) }