Haskell


[Edit: My apologies to mfp of eigenclass; my original analysis was flawed. I've restructured this to serve as an introduction to difference lists.]

Recently there was a post on eigenclass that was picked up by programming.reddit wherein the author performed an analysis of the classic Haskell quicksort example.

Bowing to Lennart's biases I'll admit the Haskell quicksort is not exactly the same thing and refer to it as "quicksort" in somewhat patronizing quotes hereafter.

 
import Data.List (partition)
 
qsort :: Ord a => [a] -> [a]
qsort [] = []
qsort (a:as) = qsort ls ++ [a] ++ qsort rs where
    (ls,rs) = partition (< = a) as
 

I've slightly modified the above to use partition rather than use filter twice, but its the same thing just with a single traversal -- unfortunately my blog inserts a space in the <=.

Profiling the following will see $\mathcal{O}(n^2)$ performance.

 
reverse (a:as) = reverse as ++ [a]
reverse [] = []
 
 
T(0) = 1
T(n) = T(n - 1) + n - 1 + 1 = T (n - 1) + n
T(n) = O(n^2)
 

It is also fairly well known that you can convert the naive reverse to a tail recursive form and get a linear time list reversal.

 
reverse as = reverse' as [] where
    reverse' (a:as) xs = reverse' as (a:xs)
    reverse' [] xs = xs
 

Here we can clearly see that we pattern match once and cons once per time through reverse'.

 
T(0) = 2
T(n) = T(n - 1) + 2
T(n) = O(n)
 

One way to think about this implementation is to think about it in terms of a difference list. Don Stewart has a nice library for difference lists, which uses a newtype but I'll stick to a type here to avoid syntactic noise.

 
type DList a = [a] -> [a]
 

To see that connection, lets rewrite this point-free and highlight the result type by applying the above type alias.

 
reverse as = reverse' as [] where
    reverse' :: [a] -> ([a] -> [a])
    reverse' (a:as) = reverse' as . (a:)
    reverse' [] = id
 

With the above we can see that:

 
reverse' :: [a] -> DList a
 

Motivated by the above, we can see that a difference list is just a function that accepts a list which it will use as its tail. So a difference list is a slightly constrained type of function from [a] -> [a].

Now, if we look at the type of

 
singleton :: a -> DList a
singleton = (:)
 

we can see that (a:) is already difference list. However, [] is not.

We can represent the empty list as a difference list with:

 
nil :: DList a
nil = id
 

Now in this representation we can append difference lists by just using (.):

 
append :: DList a -> DList a -> DList a
append = (.)
 

and you can convert from a difference list to a list by just applying it to [].

So if these are so good, why don't we use them everywhere?

1. Well, the amortization schedule for the costs you incur while tearing down a difference list is different than for a traditional list, so you pay prices at different times.
2. The type is 'too large' in that it doesn't adequately capture the constraint that the function must use the list its given and must append it to its output and can't use the list in any other ways.
3. Difference lists do not generate thunks that remember their contents after being forced the first time. However, if all you are going to do when you are done is convert the overall result back to a normal list, then you can get that list to get the memoization-like thunking effect from the result list.

So with these in hand, we can easily see reverse' as taking a list and returning a difference list, and then we are just converting it back to a normal list using the fairly standard worker/wrapper pattern.

 
reverse as = reverse' as [] where
    reverse' :: [a] -> DList a
    reverse' (a:as) = reverse' as `append` singleton a
    reverse' [] = nil
 

Ok. So recalling qsort,

 
qsort [] = []
qsort (a:as) = qsort ls ++ [a] ++ qsort rs where
    (ls,rs) = partition (< =a) as
 

Lets apply the same transformation that we applied to reverse to the well known quicksort example, transforming its output to a difference list.

 
qsort' :: Ord a => [a] -> DList a
qsort' [] = nil
qsort' (a:as) = qsort' ls `append` singleton a `append` qsort' rs where
    (ls,rs) = partition (< =a) as
 

And after inlining the very succinct definitions and transforming the output back to a list we get a visibly similar worker/wrapper combo:

 
qsort :: Ord a => [a] -> [a]
qsort as = qsort' as [] where
    qsort' [] = id
    qsort' (a:as) = qsort' ls . (a:) . qsort' rs where
        (ls,rs) = partition (< =a) as
 

However, we now get better performance.

Performance

Green is the time taken by the difference list version. Blue is the traditional Haskell qsort.


[Link]

To embed the Haskell Café on a web page:

<iframe src='http://embed.lively.com/iframe?rid=-4485567674160322075'
    width='460' height='400'
    marginwidth='0' marginheight='0'
    frameborder='0' scrolling='no'>
</iframe>

[Edit: re-introduced the domain function]

Recently Andy Gill posted a nice use of data families to memoize a narrow range of values to optimize Conal Elliott's functional linear maps.

I've tweaked Andy's definition slightly below to use a type family for D e instead of a data family, which avoids some of the syntactic noise of the domain function when D e = e, and lets it this be used transparently in some places. This change lacks substance however, and the source code links at the bottom include the code with and without this change.

Since I'm using data and type families, you'll need GHC 6.9.

 
class Applicative ((:~*) e) => NarrowMemo e where
        data (:~*) e :: * -> *
        type D e :: *
        apply :: (e :~* r) -> D e -> r
        memo :: (D e -> r) -> (e :~* r)
        domain :: D e -> e
 
instance NarrowMemo Bool where
        data Bool :~* a = MemoBool a a
        type D Bool = Bool
        apply (MemoBool o1 o2) True = o1
        apply (MemoBool o1 o2) False = o2
        memo f = MemoBool (f True) (f False)
        domain = id
 

We can quickly add in the missing bits for the Bool demo he supplied:

 
instance Functor ((:~*) Bool) where
        fmap f (MemoBool a b) = MemoBool (f a) (f b)
 
instance Applicative ((:~*) Bool) where
        pure x = MemoBool x x
        MemoBool f g  < *> MemoBool a b = MemoBool (f a) (g b)
 

And we can automatically generate an instance of Monad for (:~*)e if we really want to:

 
instance NarrowMemo e => Monad ((:~*) e) where
        return = pure
        m >>= k = memo $ apply (fmap k m) >>= apply -- in (->)e
 

And we can drop in a couple more instances to make it interesting. The tensor product:

 
instance (NarrowMemo a, NarrowMemo b) =>
    NarrowMemo (a,b) where
        data (a,b) :~* e = MemoBoth (a :~* (b :~* e))
        type D (a,b) = (D a, D b)
        apply (MemoBoth f) = uncurry (apply . apply f)
        memo f = MemoBoth $ memo $ \a -> memo (f . (,) a)
        domain = domain *** domain
 
instance (NarrowMemo a, NarrowMemo b) =>
    Functor ((:~*) (a,b)) where
        fmap f (MemoBoth g) = MemoBoth (fmap (fmap f) g)
 
instance (NarrowMemo a, NarrowMemo b) =>
    Applicative ((:~*) (a,b)) where
        pure = MemoBoth . pure . pure
        f < *> a = MemoBoth $
                memo $ \da ->
                memo $ \db ->
                let e = (da, db) in
                apply f e (apply a e)
 

and a disjoint sum, if only so we have some more memo tables to play with.

 
instance (NarrowMemo a, NarrowMemo b) =>
    NarrowMemo (Either a b) where
        data Either a b :~* e = MemoEither (a :~* e) (b :~* e)
        type D (Either a b) = Either (D a) (D b)
        apply (MemoEither l _) (Left a) = apply l a
        apply (MemoEither _ r) (Right b) = apply r b
        memo f = MemoEither (memo (f . Left)) (memo (f . Right))
        domain = domain +++ domain
 
instance (NarrowMemo a, NarrowMemo b) =>
    Functor ((:~*) (Either a b)) where
        fmap f (MemoEither a b) = MemoEither (fmap f a) (fmap f b)
 
instance (NarrowMemo a, NarrowMemo b) =>
    Applicative ((:~*) (Either a b)) where
        pure f = MemoEither (pure f) (pure f)
        MemoEither f g < *> MemoEither a b = MemoEither (f < *> a) (g < *> b)
 

Now, the reason I wanted to play with this was I hacked up a memoizing state-in-context comonad a couple of weeks back using unsafePerformIO and a memo table, but using Andy's trick we can build up a pure memoizing context comonad for smaller or more regular domains.

Recall the state-in-context comonad from category-extras.

 
class Comonad w => ComonadContext s w | w -> s where
        getC :: w a -> s
        modifyC :: (s -> s) -> w a -> a
 
data Context s a = Context (s -> a) s
 
instance ComonadContext s (Context s) where
        getC (Context _ s) = s
        modifyC m (Context f c) = f (m c)
 
instance Functor (Context s) where
        fmap f (Context f' s) = Context (f . f') s
 
instance Copointed (Context s) where
        extract   (Context f a) = f a
 
instance Comonad (Context s) where
        duplicate (Context f a) = Context (Context f) a
 

We can modify the definition to replace (->) with the version above of Andy's (:~*) to obtain a narrowly memoized version:

 
data NarrowContext e a = NarrowContext (e :~* a) (D e)
 
instance NarrowMemo e => Functor (NarrowContext e) where
        fmap f (NarrowContext t d) = NarrowContext (memo (f . apply t)) d
 
instance NarrowMemo e => Copointed (NarrowContext e) where
        extract (NarrowContext t d) = apply t d
 
instance NarrowMemo e => Comonad (NarrowContext e) where
        duplicate (NarrowContext f a) =
                NarrowContext (memo (NarrowContext f)) a
 
instance NarrowMemo e => ComonadContext (D e) (NarrowContext e a) where
        getC (NarrowContext _ e) = e
        modifyC f (NarrowContext g e) = apply g (f e)
 

Now any computation done in this modified state-in-context comonad is memoized and compositions of those computations are also memoized and built up from the memoized intermediate steps.

We should be able to play similar games with a lot of other (co)monads that use exponentials as well.

For instance (:~*) itself can play the role of a narrowly-memoized anonymous exponential comonad.

 
instance (NarrowMemo e, Monoid (D e)) => Copointed ((:~*) e) where
        extract t = apply t mempty
 
instance (NarrowMemo e, Monoid (D e)) => Comonad ((:~*) e) where
        duplicate f = memo $ m -> memo (apply f . mappend m)
 

[ Source Code (using data families only) ]
[ Source Code (using data and type families) ]

I talk an awful lot about different recursion schemes in this blog.

What I want to do for the next few posts is taxonomize a list of the general recursion schemes I have seen, cite the original references for them where available, and provide a concise implementation of each and try to motivate the connections between them. I'll likely go back through and add more information or post motivating examples for each as I work.

The following recursion schemes can be found in category-extras, along with variations on the underlying themes, so this should work as a punch-list. I'll update this post with links as I go.

Folds
Scheme Code Description
catamorphism Cata tears down a structure level by level
paramorphism*† Para tears down a structure with primitive recursion
zygomorphism*† Zygo tears down a structure with the aid of a helper function
histomorphism† Histo tears down a structure with the aid of the previous answers it has given.
prepromorphism*† Prepro tears down a structure after repeatedly transforming it
Unfolds
Scheme Code Description
anamorphism Ana builds up a structure level by level
apomorphism*† Apo builds up a structure opting to return a single level or an entire branch at each point
futumorphism† Futu builds up a structure multiple levels at a time
postpromorphism*† Postpro builds up a structure and repeatedly transforms it
Refolds
Scheme Code Description
hylomorphism† Hylo builds up and tears down a virtual structure
chronomorphism† Chrono builds up a virtual structure with a futumorphism and tears it down with a histomorphism
synchromorphism Synchro a high level transformation between data structures using a third data structure to queue intermediate results
exomorphism Exo a high level transformation between data structures from a trialgebra to a bialgebra
metamorphism Erwig a hylomorphism expressed in terms of bialgebras
metamorphism Gibbons A fold followed by an unfold; change of representation
dynamorphism† Dyna builds up a virtual structure with an anamorphism and tears it down with a histomorphism
Elgot algebra Elgot builds up a structure and tears it down but may shortcircuit the process during construction
Elgot coalgebra Elgot builds up a structure and tears it down but may shortcircuit the process during deconstruction

* This gives rise to a family of related recursion schemes, modeled in category-extras with distributive law combinators.
† The scheme can be generalized to accept one or more F-distributive (co)monads.

(more...)

As you may recall, every functor in Haskell is strong, in the sense that if you provided an instance of Monad for that functor the following definition would satisfy the requirements mentioned here:

 
strength :: Functor f => a -> f b -> f (a,b)
strength = fmap . (,)
 

In an earlier post about the cofree comonad and the expression problem, I used a typeclass defining a form of duality that enables you to let two functors annihilate each other, letting one select the path whenever the other offered up multiple options. To have a shared set of conventions with the material in Zipping and Unzipping Functors, I have since remodeled that class slightly:

 
class Zap f g | f -> g, g -> f where
	zapWith :: (a -> b -> c) -> f a -> g b -> c
	zap :: f (a -> b) -> g a -> b
	zap = zapWith id
 

Interestingly, we can use the fact that every functor in Haskell is strong to derive not only one instance of Zap, but two, given any Adjunction $f \dashv g$.

I'll give one instance here:

 
zapWithAdjunctionGF :: Adjunction g f =>
    (a -> b -> c) -> f a -> g b -> c
zapWithAdjunctionGF f a b =
    uncurry (flip f) . counit . fmap (uncurry (flip strength)) $
    strength a b
 

And I'll leave the substantially similar derivation of the following to the reader:

 
zapWithAdjunctionFG :: Adjunction f g => (a -> b -> c) -> f a -> g b -> c
 

Now, we would like to do the same thing we did with Representable last time, and just require the user of the Adjunction class to provide us with more instances, something like:

 
class (Zap f g, Zap g f, Representable g (f Void), Functor f) =>
    Adjunction f g | f -> g, g -> f where
        ...
 

But there is a problem: Adjunction composition.

If you will recall from before, we were able to define an instance for an Adjunction for a composition of two adjunctions:

 
newtype O f g a = Compose { decompose :: f (g a) }
 
instance (Functor f, Functor g) => Functor (f `O` g) where
        fmap f = Compose . fmap (fmap f) . decompose
 
instance (Adjunction f1 g1, Adjunction f2 g2) =>
    Adjunction (f2 `O` f1) (g1 `O` g2) where
        counit =
               counit .
               fmap (counit . fmap decompose) .
               decompose
        unit =
               Compose .
               fmap (fmap Compose . unit) .
               unit
 

The problem is that we have three different ways to build an instance of Zap for this composition and we would need to define two of them that conflict!

We would need both of these, which would lead to ambiguous instance heads:

 
instance (Adjunction f1 g1, Adjunction f2 g2) =>
    Zap (f2 `O` f1) (g1 `O` g2) where
        zapWith = zapWithAdjunctionFG
instance (Adjunction f1 g1, Adjunction f2 g2) =>
    Zap (g1 `O` g2) (f2 `O` f1) where
        zapWith = zapWithAdjunctionGF
 

Furthermore, we can also define a third instance of Zap over composition, which doesn't even care about Adjunction, which also conflicts with the above:

 
instance (Zap f g, Zap h k) => Zap (f `O` h) (g `O` k) where
    zapWith f a b =
        zapWith (zapWith f) (decompose a) (decompose b)
 

We could use the standard Haskell trick of making different compositions based on which instance of Zap you want to support, but the combinatorial explosion of constructors here when combined with the other reasons you may want to compose a pair of functors leads to a bit of absurdity, especially since I'm using it to capture a relationship no one cares about.

Consequently, category-extras does not capture this constraint.

Cozapping

As a final aside, we noted previously that Traversable functors were costrong. If a strong Adjunction gives rise to a couple of instances of Zap, we'd expect a similar relationship between a notion of Cozap and a costrong Adjunction.

But what would cozapping be?

First lets take a step back and break down zipWith into a couple of steps. If we note that zapWith (,) looks like:

 
prezapAdjunctionGF :: Adjunction g f => f a -> g b -> (a,b)
prezapAdjunctionGF a b =
    swap . counit . fmap (uncurry strength . swap) $ strength a b
    where swap ~(a,b) = (b,a)
 

Whereupon we can run the output through the canonical eval morphism for exponentials in $\mathbf{Hask}$:

 
eval :: (a -> b, a) -> b
eval (f,a) = f a
 

We can run everything backwards (modulo the noise caused by currying) in the first definition above and get:

 
precozapAdjunctionFG ::
    (Adjunction f g, Traversable f, Traversable g) =>
    Either a b -> Either (f a) (g b)
precozapAdjunctionFG =
    costrength . fmap (swap . costrength) . unit . swap
 

However, we lack a coeval morphism for coexponentials, since $\mathbf{Hask}$ lacks coexponentials -- with good reason! If $\mathbf{Hask}$ was a co-CCC then it would degenerate to a rather boring poset.

But that said, even getting this far, how many adjunctions are there between Traversable functors in Haskell, really?

I've had a few people ask me questions about Adjunctions since my recent post and a request for some more introductory material, so I figured I would take a couple of short posts to tie Adjunctions to some other concepts.

Representable Functors

A covariant functor $F : \mathcal{C} -> \mathbf{Set}$ is said to be representable by an object $x \in \mathcal{C}$ if it is naturally isomorphic to $\mathbf{Hom}_C(x,-)$.

We can translate that into Haskell, letting $\mathbf{Hask}$ play the role of $\mathbf{Set}$ with:

 
class Functor f => Representable f x where
    rep :: (x -> a) -> f a
    unrep :: f a -> (x -> a)
 
{-# RULES
"rep/unrep" rep . unrep = id
"unrep/rep" unrep . rep = id
 #-}
 

It is trivial to show that any two representations of a given functor must be isomorphic, and that there is a natural isomorphism between any two functors with the same representation, so we could strengthen the signature of the type class above by adding a pair of functional dependencies: f -> x, x -> f, but lets work without this straightjacket for now.

Example

We can represent the anonymous reader monad with its environment.

 
instance Representable ((->)x) x where
    rep = id
    unrep = id
 

Example

We could adopt the pleasant fiction that () has a single inhabitant to avoid bringing in an empty type, but lets do this correctly. Clearly the Identity functor needs no extra information from its representation.

 
data Void {- you'll need EmptyDataDecls -}
 
instance Representable Identity Void where
    rep f = Identity (f undefined)
    unrep = const . runIdentity
 

Adjunctions

If you recall the definition of Adjunctions over $\mathbf{Hask}$ from before:

 
class (Functor f, Functor g) =>
    Adjunction f g | f -> g, g -> f where
        unit   :: a -> g (f a)
        counit :: f (g a) -> a
        leftAdjunct  :: (f a -> b) -> a -> g b
        rightAdjunct :: (a -> g b) -> f a -> b
 
        unit = leftAdjunct id
        counit = rightAdjunct id
        leftAdjunct f = fmap f . unit
        rightAdjunct f = counit . fmap f
 

We can generate a lot of representable functors, by turning to the theorem mentioned in the Wikipedia article about the representability of a right adjoint in terms of its left adjoint wrapped around a singleton element:

Any functor $K : \mathcal{C} -> \mathbf{Set}$ with a left adjoint $F : \mathbf{Set} -> \mathcal{C}$ is represented by (FX, ηX(•)) where X = {•} is a singleton set and η is the unit of the adjunction.

Well, earlier we defined a singleton set, Void, and $\mathbf{Hask}$ can play the role of $\mathbf{Set}$ as we did above. For $\mathcal{C} = \mathbf{Hask}$, we can translate the remainder quite easily:

 
repAdjunction :: Adjunction f g => (f Void -> a) -> g a
repAdjunction f = leftAdjunct f undefined
 
unrepAdjunction :: Adjunction f g => g a -> (f Void -> a)
unrepAdjunction = rightAdjunct . const
 

Now, as usual the way type class inference works in Haskell requires us to reason somewhat backwards.

You'd like to say:

 
instance Adjunction f g => Representable g (f Void) where
        rep = repAdjunction;
        unrep = unrepAdjunction
 

But if you do so, you can't define any other instances for Representable, you'll have used up the instance head, so the previous definitions couldn't be made.

On the other hand, you can create the obligation for an appropriate instance of Representable by changing the signature of Adjunction:

 
class (Representable g (f Void), Functor f) =>
    Adjunction f g | f -> g, g -> f where
        ...
 

Then the definitions for repAdjunction and unrepAdjunction can be used by any would-be Adjunction to automatically generate the corresponding Representable instance, just like liftM can alwyas be used to make a Haskell Monad into a Functor.

We can also go the other way and define an Adjunction given a representation for the right adjoint, but I'll leave that as an exercise for the reader. (Hint: you'll probably want to weaken the signature for Adjunction to remove the fundeps, so you can test some simple cases). You may also want to take a look at the section on Adjunctions as Kan extensions portion of the earlier post.

I have since modified category-extras definition of Adjunction to require the instance for Representable motivated above.

Haddock:
[Control.Functor.Adjunction]
[Control.Functor.Representable]

Grant B. asked me to post the derivation for the right and left Kan extension formula used in previous Kan Extension posts (1,2). For that we can turn to the definition of Kan extensions in terms of ends, but first we need to take a couple of steps back to find a way to represent (co)ends in Haskell.

Dinatural Transformations

Rather than repeat the definition here, we'll just note we can define a dinatural transformation in Haskell letting polymorphism represent the family of morphisms.

 
type Dinatural f g = forall a. f a a -> g a a
 

Ends

So what is an end?

An end is a universal dinatural transformation from some object e to some functor s.

Diving into the formal definition:

Given a functor $F : \mathcal{C}^{op} \times \mathcal{C} -> \mathcal{D}$, and end of $F$ is a pair $(e,\omega)$ where $e$ is an object of $\mathcal{D}$ and omega is a dinatural transformation from e to S such that given any other dinatural transformation $\beta$ to S from another object x in $\mathcal{D}$, there exists a unique morphism $h : x -> e$, such that $\beta_a = \omega_a \cdot h$ for every $a$ in $\mathcal{C}$.

We usually choose to write ends as $e = \int_c S(c,c)$, and abuse terminology calling $e$ the end of $S$.

Note this uses a dinatural transformation from an object $x$ in $\mathcal{D}$, which we can choose to represent an arbitrary dinatural transformation from an object $x$ to a functor $S$ in terms of a dinatural transformation from the constant bifunctor:

 
newtype Const x a b = Const { runConst :: x }
 

This leaves us with the definition of a dinatural transformation from an object as:

 
Dinatural (Const x) s ~ forall a. Const x a a -> s a a
 

but the universal quantification over the Const term is rather useless and the Const bifunctor is supplying no information so we can just specialize that down to:

 
type DinaturalFromObject x s = x -> forall a. s a a
 

Now, clearly for any such transformation, we could rewrite it trivially using the definition:

 
type End s = forall a. s a a
 

with $\omega$ = id.

 
type DinaturalFromObject x s = x -> End s
 

And so End above fully complies with the definition for an end, and we just say e = End s abusing the terminology as earlier. The function $\omega$ = id is implicit.

For End to be a proper end, we assume that s is contravariant in its first argument and covariant in its second argument.

Example: Hom

A good example of this is (->) in Haskell, which is as category theory types would call it the Hom functor for Hask. Then End (->) = forall a. a -> a which has just one inhabitant id if you discard cheating inhabitants involving fix or undefined.

We write $\mathcal{C}(a,b)$ or $\mathrm{Hom}_\mathcal{C}(a,b)$ to denote a -> b. Similarly we use b^a to denote an exponential object within a category, and since in Haskell we have first class functions using the same syntax this also translates to a -> b. We'll need these later.

Example: Natural Transformations

If we define:

 
newtype HomFG f g a b =
        HomFG { runHomFG :: f a -> g b }
 

then we could of course choose to define natural transformations in terms of End as:

 
type Nat f g = End (HomFG f g) -- forall a. f a -> g a
 

Right Kan Extension as an End

Turning to Wikipedia or Categories for the Working Mathematician you can find the following definition for right Kan extension of $T$ along $K$ in terms of ends.

$(\mathrm{Ran}_KT)c=\int_m Tm^{\mathbf{C}(c,Km)}$

Working by rote, we note that $\mathbf{C}(c,Km)$ is just c -> K m as noted above, and that $(Tm)^{\mathbf{C}(c,Km)}$ is then just (c -> K m) -> T m'. So now we just have to take the end over that, and read off:

 
newtype RanT f g c m m' = (c -> K m) -> T m'
type Ran f g c = End (RanT f g c)
 

Which, modulo newtype noise is the same as the type previously supplied type:

 
newtype Ran f g c = Ran { runRan :: forall m. (c -> f m) -> g m }
 

Coends

The derivation for the left Kan extension follows similarly from defining coends over Hask in terms of existential quantification and copowers as products.

The coend derivation is complicated slightly by Haskell's semantics. Disposing of the constant bifunctor as before we get:

 
type DinaturalToObject s c = forall a. (s a a -> c)
 

Which since we want to be able to box up the s a a term separately, we need to use existential quantification.

 
(forall a. s a a -> c) ~ (exists a. s a a) -> c
 

We cannot represent this directly in terms of a type annotation in Haskell, but we can do so with a data type:

 
data Coend f = forall a. Coend (f a a)
 

Recall that in Haskell, existential quantification is represented by using universal quantification outside of the type constructor.

The main difference is that in our coend $(e,\zeta)$ the function $\zeta$ is now runCoend instead of id, because we have a Coend data constructor around the existential. Technicalities make it a little more complicated than that even, because you can't define a well-typed runCoend and have to use pattern matching on the Coend data constructor to avoid having an existentially quantified type escape the current scope, but the idea is the same.

Left Kan Extension as a Coend

Then given the definition for the left Kan extension of $T$ along $K$ as a coend:

$(\mathrm{Lan}_KT)c=\int^m \mathbf{C}(Km,c)\cdot Tm$

we can read off:

 
data LanT k t c m m' = LanT (k m -> c) (t m)
type Lan k t c = Coend (LanT k t c)
 

Which is almost isomorphic to the previously supplied type:

 
data Lan k t c = forall m. Lan (k m -> c) (t m)
 

except for the fact that we had to use two layers of data declarations when using the separate Coend data type, so we introduced an extra place for a $\perp$ to hide.

A newtype isn't allowed to use existential quantification in Haskell, so this form forces a spurious case analysis that we'd prefer to do without. This motivates why category-extras uses a separate definition for Lan rather than the more elaborate definition in terms of Coend.

I want to spend some more time talking about Kan extensions, composition of Kan extensions, and the relationship between a monad and the monad generated by a monad.

But first, I want to take a moment to recall adjunctions and show how they relate to some standard (co)monads, before tying them back to Kan extensions.

Adjunctions 101

An adjunction between categories $\mathcal{C}$ and $\mathcal{D}$ consists of a pair of functors $F : \mathcal{C} -> \mathcal{D}$, and $G : \mathcal{D} -> \mathcal{C}$ and a natural isomorphism:

$\phi : \mathrm{Hom}_\mathcal{D} (F-, =) -> \mathrm{Hom}_\mathcal{C} (-, G=)$

We call $F$ the left adjoint functor, and $G$ the right adjoint functor and $(F,G)$ an adjoint pair, and write this relationship as $F \dashv G$

Borrowing a Haskell definition from Dave Menendez, an adjunction from the category of Haskell types (Hask) to Hask given by a pair of Haskell Functor instances can be defined as follows, where phi is witnessed by $\phi$ = leftAdjunct and $\phi^{-1}$ = rightAdjunct. [haddock]

 
class (Functor f, Functor g) =>
    Adjunction f g | f -> g, g -> f where
        unit   :: a -> g (f a)
        counit :: f (g a) -> a
        leftAdjunct  :: (f a -> b) -> a -> g b
        rightAdjunct :: (a -> g b) -> f a -> b
 
        unit = leftAdjunct id
        counit = rightAdjunct id
        leftAdjunct f = fmap f . unit
        rightAdjunct f = counit . fmap f
 

Currying and Uncurrying

The most well known adjunction to a Haskell programmer is between the functors given by ((,)e) and ((->)e). (Recall that you can read ((,)e) as (e,) and ((->)e) as (e->); however, the latter syntax isn't valid Haskell as you aren't allowed to make (,) and (->) sections. We use this adjunction most every day in the form of the functions curry and uncurry.

 
curry :: ((a, b) -> c) -> a -> b -> c
curry f x y = f (x,y)
 
uncurry :: (a -> b -> c) -> (a, b) -> c
uncurry f ~(x,y) = f x y
 

However the arguments are unfortunately slightly flipped around when we go to define this as an adjunction.

 
instance Adjunction ((,)e) ((->)e) where
        leftAdjunct f a e  = f (e,a)
        rightAdjunct f ~(e,a) = f a e
 

This adjunction defines the relationship between the anonymous reader monad and the anonymous reader comonad (aka the product comonad).

All Readers are the Same

As an aside, if you look at the reader arrow, reader monad and reader comonad all side by side you can see that they are all basically the same thing. Kleisli arrows for the anonymous reader monad have the form a -> e -> b. The Reader arrow takes the form arr (a, e) b, which when arr is (->) this reads as (a,e) -> b, which is just a curried Kleisli arrow for the Reader monad. On the other hand the reader comonad is ((,)e), and its CoKleisli arrows have the form (e,a) -> b. So, putting these side by side:

 
a -> e -> b
(a , e) -> b
(e , a) -> b
 

You can clearly see these are all the same thing!

State and Composing Adjunctions

Once we define functor composition:

 
newtype O f g a = Compose { decompose :: f (g a) }
instance (Functor f, Functor g) => Functor (f `O` g) where
        fmap f = Compose . fmap (fmap f) . decompose
 

We can see that every adjunction gives rise to a monad:

 
instance Adjunction f g => Monad (g `O` f) where
        return = Compose . unit
        m >>= f =
             Compose .