search

tweag / linear-base

Standard library for linear types in Haskell.
MIT License
333 stars 37 forks source link

Polymorphism big plans for Data and Control functor hierarchy #27

Open aspiwack opened 5 years ago

aspiwack commented 5 years ago

Currently, data functors and control functors have type

fmap :: (a ->. b) -> f a ->. f b

and

fmap :: (a ->. b) ->. f a ->. f b

respectively. (that is data functors are regular functors and control functors are enriched functors).

But with polymorphism, it seem that we may want to split them further. Based more on how they are used (data functors are data containers of sorts, which control functors are effect-bearing computations).

My thoughts are the following: just like for lists the type of data functor's fmap would become

fmap :: (a # p -> b) -> f a # p -> f b

(it specialises to linear data functor when p ~ One and to regular (unrestricted) functor when p ~ Omega). It is not equivalent, but it seems to make sense. The only downside, though, is that it may be a bit weird for types which are always linear in the context (like a pure mutable array, for instance). An alternative is to do:

class Functor (p :: Multiplicity) f where
  fmap :: (a # p -> b) -> f a # p -> f b

This way we have polymorphism without the weirdness.

On the other hand, for control functors, we care about linearity of the control, but not linearity of the data. Therefore, we can the multiplicity of the data variable, like IO in the paper.

class Functor (f :: Multiplicity -> * -> *) where
  fmap :: (a ->. b) ->. f p a ->. f p b

(maybe a variant of type (a # p ->. b) ->. f q a ->. f (p * q)? Really the general form would be (a #p ->. Mult q b) ->. f p a ->. f q b).

The bottom-line is that control functors become functors from the category where objects are pairs (a, p) of an object and a type, and maps from (a, p) to (b, q) are a # p ->. Mult q b, to the category of types and linear functions (enriched in the category of types and linear functions).

This is not a restriction because you can always compose your old-style control functor with Mult p to obtain a new one. It also extends to a notion of monad (more precisely, of relative monad).

Which is the whole point of the change: it will make do notation much more pleasant, with the ability to return linear or unrestricted values.

sjoerdvisscher commented 3 years ago

I think for data functors the domain and codomain should be allowed to differ? So:

fmap :: (a %p -> b) -> f a %q -> f b