Data.Functor.Linear

Linear Data Functors should be thought of as containers holding values of type a over which you are able to apply a linear function of type a %1-> b on each value of type a in the functor and consume a given functor of type f a.

Replace all occurances of b with the given a and consume the functor f b.

Discard a consumable value stored in a data functor.

Data Applicative-s can be seen as containers which can be zipped together. A prime example of data Applicative are vectors of known length (ZipLists would be, if it were not for the fact that zipping them together drops values, which we are not allowed to do in a linear container).

In fact, an applicative functor is precisely a functor equipped with (pure and) liftA2 :: (a %1-> b %1-> c) -> f a %1-> f b %1-> f c. In the case where f = [], the signature of liftA2 would specialise to that of zipWith.

Intuitively, the type of liftA2 means that Applicatives can be seen as containers whose "number" of elements is known at compile-time. This includes vectors of known length but excludes Maybe, since this may contain either zero or one value. Similarly, ((->) r) forms a Data Applicative, since this is a (possibly infinitary) container indexed by r, while lists do not, since they may contain any number of elements.

Remarks for the mathematically inclined

An Applicative is, as in the restricted case, a lax monoidal endofunctor of the category of linear types. That is, it is equipped with

• a (linear) function () %1-> f ()

• a (linear) natural transformation (f a, f b) %1-> f (a, b)

It is a simple exercise to verify that these are equivalent to the definition of Applicative. Hence that the choice of linearity of the various arrow is indeed natural.

The Const functor.

Examples

>>> fmap (++ "World") (Const "Hello")Const "Hello"

Because we ignore the second type parameter to Const, the Applicative instance, which has (<*>) :: Monoid m => Const m (a -> b) -> Const m a -> Const m b essentially turns into Monoid m => m -> m -> m, which is (<>)

>>> Const [1, 2, 3] <*> Const [4, 5, 6]Const [1,2,3,4,5,6]

A linear data traversible is a functor of type t a where you can apply a linear effectful action of type a %1-> f b on each value of type a and compose this to perform an action on the whole functor, resulting in a value of type f (t b).

To learn more about Traversable, see here:

• "Applicative Programming with Effects", by Conor McBride and Ross Paterson, Journal of Functional Programming 18:1 (2008) 1-13, online at http://www.soi.city.ac.uk/~ross/papers/Applicative.html.

• "The Essence of the Iterator Pattern", by Jeremy Gibbons and Bruno Oliveira, in Mathematically-Structured Functional Programming, 2006, online at http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/#iterator.

• "An Investigation of the Laws of Traversals", by Mauro Jaskelioff and Ondrej Rypacek, in Mathematically-Structured Functional Programming, 2012, online at http://arxiv.org/pdf/1202.2919.

Implementation of traverse for types which derive (linear) Generic1.

### Performance note

At present, this function does not perform well for recursive types like lists; it will not specialize to either

### Example

data T
$(deriveGeneric1 ''T)

instance Traversable T where
  traverse = genericTraverse

Note that, contrary to many other classes in linear-base, we can't define `Traversable T` using deriving via, because the role of t, in the type of traverse, is nominal.

This type class derives the definition of genericTraverse by induction on the generic representation of a type.