Data.Functor.Linear.Internal.Applicative

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.