&, T tensor

[Jashweii]

Is there a reason this isn't present in linear-base? I know you can't make & (co)datatypes directly in Haskell and have to encode them, but it seems like it's worth having. I think I read somewhere the main motivation for not having it was that it doesn't include effects in the choice (aside from places where linearity is used to do allocations etc) but couldn't you just have an effect element and sequence it?

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

-- a or b, consumer choice
newtype a & b = With (forall c . Y a b c -> c)

-- dupable - easily created (Top ()) and cannot observe difference, not consumable (contains linear resource)
data Top = forall a . Top a

Seems like a fruitful place to look

• Binary operator & representing exclusive consumer choice
• Unit ⊤ (or Top) (exclusive consumer choice of 0 things), this is also useful for a type that accumulates all linear resources and cannot be consumed
• N-ary vector of choices (lazy vector since Ur (a & b) is (a, b))
• Dependent choice (parameterise Y a b)
• Various & analogues of classes of functors (monoidal functors, distribution laws, contravariant versions)
• Optics (e.g. strong wrt &) identifying a choice that can be made within a structure
  Some of this stuff might find use for protocols.

[Jashweii]

Not sure how many interesting classes of functors working with this tensor there are, from some experimenting:

• It distributes outside of any linear control functor since it's rep[x] -> x
• It probably distributes inside linear distributables for the same reason
• You could maybe have a class with a method choose :: f a & f b %1 -> f (Either a b) indicating f makes choices
• Cosemigroups on &

This is the general pattern I'm working with

-- family of destructors
type family Destructor a :: Type -> Type

-- Eliminate a codata type
class Codata a where
  π :: Destructor a b %1 -> a %1 -> b

-- left assoc for chaining
(·) :: Codata a => a %1 -> Destructor a b %1 -> b
a · f = π f a
{-# INLINE (·) #-}

-- Construct a codata type by copattern matching
--   co\case
--     ⋮ ⋯ → ⋯
class Codata a => Cofree a where
  -- π h (co f) = h f
  -- co (`π` a) = a
  co :: (forall b . Destructor a b %1 -> b) %1 -> a

-- cofree codata / dependent consumer exclusive choice marked by f
newtype Co f = Co (forall a . f a %1 -> a)
type instance Destructor (Co f) = f

For suitable choices of Destructor you can

-- lift outside of linear control functors
data DestructorF a f b where
  DestructorF :: Destructor a b %1 -> DestructorF a f (f b)
-- represent &
data Y a b c where
  L :: Y a b a
  R :: Y a b b
-- represent ⊤
data V a where
-- represent functions
data Arg a b c where
  Arg :: a %1 -> Arg a b b
-- codata instance for pair projections
data Selector a b c where
  Fst :: Consumable b => Selector a b a
  Snd :: Consumable a => Selector a b b

Example representing servers with the same class

data ServerF a b where
  Query :: String -> ServerF a (a, Bool)
  Feed :: Int -> ServerF a a
  Request :: ServerF a (a, Int)
  Exit :: b %1 -> ServerF a b

newtype Server = Server (Co (ServerF Server))
  deriving newtype (Codata, Cofree)
type instance Destructor Server = ServerF Server

server :: [String] -> Int -> Server
server keys tot = co\case
  Query s -> (server keys tot, elem s keys)
  Feed i -> server keys (tot + i)
  Request -> (server keys tot, tot)
  Exit a -> a

client :: Server %1 -> Maybe Int
client s = 
  case s·Query "a" of
    (s, b) ->
      case b of
        True -> 
          case s·Feed 1·Feed 2·Request of
            (s, i) -> s·Exit (Just i)
        False -> s · Exit Nothing

[Jashweii]

In terms of optics

• Optic (Strong (&) Top) s t a b says there is some choosable branch a(b) inside s(t)
• Linear forget (as used to linearly view) is strong over &/T - this gives s %1 -> a which makes the choice identified by the optic.
• It's also strong over FUN 'One (modify the alternative without taking it), and probably some other things.

[aspiwack]

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).

---

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 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).

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?

[Jashweii]

#474 (comment)
It's not that particularly I have any real use case, and linear types are pretty exploratory for me. The example I came up with was just on the spot. It's more that & is the sort of thing I would expect in linear-base, since it's a sort of basic building block, and it might well end up being useful even in typing other parts of linear-base.
I don't think the encoding is that big of a deal, to some degree it is an implementation detail and doesn't need to be exposed. The GADT version has worse type inference at least, I'm not sure if there's a non implementation detail in the usage of the consumers - you might expect (a %1 -> a') & (b %1 -> b') %1 -> (a & b %1 -> a' & b'). The simplest implementation would be a hidden (a, b) with a bunch of unsafe linears.
W.r.t my example and optics, that is actually one use for &. I can create an optic

requesting :: Optic (LD.Strong (&) Top) Server Server (Server, Int) (Server, Int)

out of an iso with & some-c that lets me modify that branch that could be taken, or view it to take that branch (linear in s). To some degree I suppose & itself not always being that useful is kind of the same as for (,), often a datatype is more natural than to use pairs everywhere, and writing a custom elimination type is more like defining a codatatype.

Considering effects, is there a reason to use (With m a b) over With (m a) (m b)? When it comes back to something more purpose built you can always have the result be M something to begin with. In my example I could also change one of the ServerF constructors to return IO something, or write some generic wrapper CoT m f. I think as a basic primitive the version without a monad fused into it is more natural, assuming it is the same and there's not some issue I've not seen like the sequencing of choosing the branch and performing whatever effects.

[Jashweii]

Relatedly to this, ⅋, #450, destination arrays and https://www.reddit.com/r/haskell/comments/126oqt3/linear_haskell_linearbase_and_linear_logic is it would be useful to have a double elimination primitive ¬¬a -> a. With this you can then convert between functions and ⅋, and presumably have an ⅋ optic that accesses parallel resources. One way this works is with a %1 -> () and creating and writing to a reference (e.g. the destination array) but I don't know nearly enough about LL or GHC to know if there's some better way that could be done as a GHC primitive, how it relates to laziness, or if it could use a ⊥ type instead of ().

[aspiwack]

I've been thinking about this on and off, indeed. More than allowing to convert between functions and ⅋, I think it would legitimately create ⅋. Thank you for point out the link to optics.

To answer your questions:

• I don't think laziness interacts in any interesting way with such a primitive.
• I believe that, due Linear Haksell's quirks, ⊥ and () are the same.
• I believe that the state passing and the, more usual, continuation passing implementation of this functions are essentially the same thing, but I've never had the opportunity to explore this idea further.

[Jashweii]

Since without linearity the tensors are the same as (,) and Either, I'm wondering if ⅋ could be unsafely implemented as Either (lazy in the choice) like (&) can be as (,) (lazy in the parts).

I can internally go between the two representations with unsafeLinear, but then can't guarantee it's faithful. i.e. ⅋_Either to ¬(¬a, ¬b) is just either and (unsafely) only using one of the supplied eliminators, ¬(¬a, ¬b) to ⅋_Either is using the double elimination primitive to consume a ¬(⅋_Either a b) by contramapping with Left/Right to ¬a and ¬b to pass to the ¬(¬a, ¬b) function (unsafely duplicating the ¬(⅋_Either a b)).

Another encoding I've found is as one of its eliminators ¬a -> b (¬¬a ⅋ b). Swapping it (to get ¬b -> a) needs double elimination. This also helps give some intuition about it - you tell it how to use up one part, and it gives you the other part, showing that it's multiplicative (both parts need using) but ensuring the two parts (e.g. function input and output) are kept separate.

[Jashweii]

I've been thinking some more. The either encoding is probably wrong due to the non-use.
One possible alternative for ⊥ is Haskell's ⊥ (i.e. any exception or non-termination). Not sure if there's any problem with this choice. Unlike () this always blows up when seq-d.
1^⊥ = ⊥ = 1 ⊸ ⊥

newtype Bot = Bot Bot

If you take a ⅋ b = (A^⊥ ⊗ B^⊥)^⊥ i.e.

newtype Not a = Not (a %1 -> Bot)
newtype a ⅋ b = Par (Not a %1 -> Not b %1 -> Bot)

you could evaluate the parts in parallel, with independent failure for ⊥ (but then you might have to worry about thread safety with your Not destination variables). You can also implement ? with not,
(?A)^⊥ = !(A^⊥)
?A = (!(A^⊥))^⊥
= !(A ⊸ Bot) ⊸ Bot
= (A ⊸ Bot) → Bot

newtype WhyNot a = WhyNot (Not a -> Bot)

With all this said I wonder if there could be a more efficient Not as a write only variable or if it needs to have some post-write evaluation (kind of like the pre-return evaluation of laziness or function results). If it was a write only variable then maybe this stuff could be related to the threading via MVars or something. This would also probably relate to WhyNot. Not sure what the best way to implement all of this is for performance.

The parallelism, exceptions, ⊥ semantics are worth thinking about. The rest (e.g. & as wrapped unsafe (,)) is not a big deal since the API would probably remain the same, e.g.

-- ¬¬a = a
nn :: Iso' a (Not (Not a))

doesn't matter how Not is implemented.

[Jashweii]

Took some inspiration from double elimination and made this treating Bot as the elimination type and unsafely coercing for the knowledge that the elimination type is the input type (tested in ghc 9.10). So potentially you don't even need a mutable destination variable. Needs further testing.

import Unsafe.Coerce (unsafeEqualityProof, UnsafeEquality(..))

-- 0
data Zero

-- 1
data One = One

-- ⊤
data Top = forall a . Top a

-- ⊥ abstract, (lack of) constructors hidden
data Bot

-- unsafe primitive
doubleElim :: forall a . ((a %1 -> Bot) %1 -> Bot) %1 -> a
doubleElim =
  case unsafeEqualityProof @a @Bot of
    UnsafeRefl -> \k -> k (\x -> x)

-- ¬
newtype (¬) a = Not (a %1 -> Bot)

-- !
data (!) a where
  Ur :: a -> (!) a

newtype (?) a = WhyNot ((¬) a -> Bot) -- ¬!¬

-- ¬(¬a ⛒ ¬b)
newtype a ⅋ b = Par ((¬) a %1 -> (¬) b %1 -> Bot)

-- ¬(¬ a ⊕ ¬b)
newtype a & b = With (Either ((¬) a) ((¬) b) %1 -> Bot)

type (⛒) = (,)

type (⊕) = Either

contradict :: (¬) a %1 -> a %1 -> Bot
contradict (Not k) = k

notNot1 :: (¬) ((¬) a) %1 -> a
notNot1 k = doubleElim (\a -> contradict k (Not a)) 

notNot2 :: a %1 -> (¬) ((¬) a)
notNot2 a = Not (`contradict` a)

notOne1 :: (¬) One %1 -> Bot
notOne1 = (`contradict` One)

notOne2 :: Bot %1 -> (¬) One
notOne2 b = Not (\One -> b)

notBot1 :: (¬) Bot %1 -> One
notBot1 k = notNot1 (Not (\f -> contradict k (contradict f One)))

notBot2 :: One %1 -> (¬) Bot
notBot2 One = Not (\x -> x)

notZero1 :: (¬) Zero %1 -> Top
notZero1 = Top

notZero2 :: Top %1 -> (¬) Zero
notZero2 t = Not (\x -> (case x of {}) t)

notTop1 :: (¬) Top %1 -> Zero
notTop1 k = notNot1 (Not (\f -> contradict k (Top (contradict f))))

notTop2 :: Zero %1 -> (¬) Top
notTop2 x = case x of {}

notBang1 :: (¬) ((!) a) %1 -> (?) ((¬) a)
notBang1 k = WhyNot (\k' -> contradict k (Ur (notNot1 k')))

notBang2 :: (?) ((¬) a) %1 -> (¬) ((!) a)
notBang2 (WhyNot f) = Not (\(Ur a) -> f (Not (`contradict` a)))

notWhyNot1 :: (¬) ((?) a) %1 -> (!) ((¬) a)
notWhyNot1 k = notNot1 (Not (\x -> contradict k (WhyNot (\f -> contradict x (Ur f)))))

notWhyNot2 :: (!) ((¬) a) %1 -> (¬) ((?) a)
notWhyNot2 (Ur a) = Not (\(WhyNot h) -> h a)

notConj1 :: (¬) (a ⛒ b) %1 -> (¬) a ⅋ (¬) b
notConj1 k = Par (\ka kb -> contradict k (notNot1 ka, notNot1 kb))

notConj2 :: (¬) a ⅋ (¬) b %1 -> (¬) (a ⛒ b)
notConj2 (Par h) = Not (\(ka, kb) -> h (notNot2 ka) (notNot2 kb))

notPar1 :: (¬) (a ⅋ b) %1 -> (¬) a ⛒ (¬) b
notPar1 k = notNot1 (Not (\a -> contradict k (Par (\x y -> contradict a (x, y)))))

notPar2 :: (¬) a ⛒ (¬) b %1 -> (¬) (a ⅋ b)
notPar2 (ka, kb) = Not (\(Par h) -> h ka kb)

notDisj1 :: (¬) (a ⊕ b) %1 -> (¬) a & (¬) b
notDisj1 k = With (\ab' -> case ab' of
  Left x -> contradict k (Left (notNot1 x))
  Right x -> contradict k (Right (notNot1 x)))

notDisj2 :: (¬) a & (¬) b %1 -> (¬) (a ⊕ b)
notDisj2 (With ab) = Not (\ab' -> case ab' of
  Left  k -> ab (Left  (notNot2 k))
  Right k -> ab (Right (notNot2 k)))

notWith1 :: (¬) (a & b) %1 -> (¬) a ⊕ (¬) b
notWith1 k = notNot1 (Not (\f -> contradict k (With (contradict f))))

notWith2 :: (¬) a ⊕ (¬) b %1 -> (¬) (a & b)
notWith2 k = Not (\(With ab) -> ab k)

[Jashweii]

The fully general

doubleElim :: forall a r . ((a %1 -> r) %1 -> r) %1 -> a

is unsound because the function does not need to call its function argument.

• r = 0 %_ -> _
  use case{} on it to use the function (essentially just adding to a closure)
• r = ⊤
  Just add the function to the ⊤ (again adding to a closure)

(Similar to existing linear base functions that require something movable.)
However I think an abstract ⊥ is fine. You can't empty case it (if nobody can see its set of constructors) so you can't consume it.
You can also use this encoding

-- ⊥ = ¬ 1 = 1 ⊸ ⊥
newtype Bot = Bot Bot
-- not sure if there's a need for the extra laziness or if newtype is fine but the point is this is like representing () -> a as a.
-- scratch that I think this *has* to be a newtype in order to guarantee the only (_ -> Bot) is id or the passed in function (which is also id)

so only a non-terminating function could consume it.
Proof the general one is unsound:

-- ⊥ cannot be Void %_ -> _
unsafe_1 :: a
unsafe_1 = doubleElim (\f x -> case (x :: Void) of {} f)

-- ⊥ cannot be Top
unsafe_2 :: a
unsafe_2 = doubleElim Top

data Void
data One = One
data Top = forall a . Top a
newtype Bot = Bot Bot