&, 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]

https://github.com/tweag/linear-base/issues/474#issuecomment-1938225850 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.