The Comonad.Reader

Description
Anamorphisms are generalizations of Haskell's unfoldr. A anamorphism builds a data structure with an F-coalgebra by recursively unrolling a seed.

History
The name anamorphism comes from the Greek 'ανα-' meaning "upwards". [1,2]

Notation
An anamorphism for some F-coalgebra is denoted with "lenses" . When the functor F can be determined unambiguously, it is usually written or ana .

Implementation

 
ana :: Functor f => Coalgebra f a -> a -> FixF f
ana g = InF . fmap (ana g) . g
 

Alternate implementations

 
ana g = hylo InF g
 

Duality

An anamorphism is the categorical dual of a catamorphism.

Derivation
If is the final -coalgebra for some endofunctor and is an -coalgebra, then there is a unique -coalgebra homomorphism from to which we denote .

That is to say, the following diagram commutes:

Laws

Rule	Haskell
ana-charn	fmap x . psi = outF . x x = ana psi
ana-self	fmap (ana psi) . psi = outF . ana psi
ana-id	id = ana outF
ana-uniq	fmap x . psi = outF . x fmap y . psi = outF . y => x = y
ana-fusion	fmap x . phi = psi . x => ana phi = ana psi . x
ana-compose	e :: f :~> g => ana (e . outF) . ana phi = ana (e . phi)

Examples

 
data StreamF a x = a :> x
type Stream a = FixF (StreamF a)
 
instance Functor (StreamF a) where
    fmap f (a :> as) = a :> f as
 
repeat :: a -> Stream a
repeat = ana psi where
    psi n = n :> n
 
from :: Num a => a -> Stream a
from = ana psi where
    psi n = n :> (n + 1)
 

Links
[Haddock] [Source] [Field Guide]

References

[1] E. Meijer, M. Fokkinga, R. Paterson. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Proceedings, 5th ACM Conference on Functional Programming Languages and Computer Architecture.
[2] M. Fokkinga. Law and Order in Algorithmics. PhD Thesis. 1992

I'm off to MSFP'08 (which is colocated with ICALP) and should have a day or two spare on either side of the workshop to let me find stuff to do in Iceland and meet people.

I'd love to get a chance to meet folks in person.

If anyone else is planning on being in the area, please feel free to drop me a line.

[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) ]

Description
A paramorphism is used when a catamorphism won't quite do because you need not only the result of recursing with the F-algebra over the tail of a structure, but you also need the tail itself. This is another way to say that you call in a paramorphism when you need the power of primitive recursion.

History
Lambert Meertens coined the name paramorphism [1]. The name comes from the greek παρα meaning "alongside", the root of parallel.

Notation
A paramorphisms defined in terms of an --Algebra are commonly denoted using "barbed wire" as or as para f. Uustalu and Vene [2] use the notation so that apomorphisms, the categorical dual of paramorphisms, can have a symmetric notation.

Implementation

 
type Para f = (,) (FixF f)
-- para :: Functor f => GAlgebra f (Para f) a -> FixF f -> a
para :: Functor f => (f (FixF f,a) -> a) -> FixF f -> a
para f = f . fmap (id &&& para f) . outF -- from para-cancel
 

Alternate Implementations

 
para f = snd . cata (InF . fmap fst &&& f) -- para-def
para = zygo InF
 

Laws

Derivation

For any two morphisms and we have . [2, p9, Lemma 2]

In other words, if we define , the following diagram commutes:

Example

 
data NatF a = S a | Z deriving (Eq,Show)
type Nat = FixF NatF
 
instance Functor NatF where
     fmap f Z = Z
     fmap f (S z) = S (f z)
 
plus :: Nat -> Nat -> Nat
plus n = cata phi where
     phi Z = n
     phi (S m) = s m
 
times :: Nat -> Nat -> Nat
times n = cata phi where
     phi Z = z
     phi (S m) = plus n m
 
z :: Nat
z = InF Z
 
s :: Nat -> Nat
s = InF . S
 
fac :: Nat -> Nat
fac = para phi where
     phi Z = s z
     phi (S (n,f)) = times f (s n)
 

Links
[Haddock] [Source] [Field Guide]

References

[1] L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413-424, 1992.
[2] T. Uustalu and V. Vene. Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically. Informatica, 1999 Vol. 10, No. 1, 1-0

Description
Catamorphisms are generalizations of Haskell's foldr. A catamorphism deconstructs a data structure with an F-algebra.

History
The name catamorphism appears to have been chosen by Lambert Meertens [1]. The category theoretic machinery behind these was resolved by Grant Malcolm [2,3], and they were popularized by Meijer, Fokkinga and Paterson [4,5]. The name comes from the Greek 'κατα-' meaning "downward or according to". A useful mnemonic is to think of a catastrophe destroying something.

Notation
A catamorphism for some F-algebra is denoted . When the functor F can be determined unambiguously, it is usually written or cata .

Implementation

 
cata :: Functor f => Algebra f a -> FixF f -> a
cata f = f . fmap (cata f) . outF
 

Alternate implementations

 
cata f = hylo f outF
cata f = para (f . fmap fst)
 

Duality

A catamorphism is the categorical dual of an anamorphism.

Derivation
If is the initial -algebra for some endofunctor and is an -algebra, then there is a unique -algebra homomorphism from to which we denote .

That is to say, the following diagram commutes:

Laws

Rule	Categorically	Haskell
cata-cancel		cata phi . InF = phi . fmap (cata phi)
cata-refl		cata InF = id
cata-fusion		f . phi = phi . fmap f => f . cata phi = cata phi
cata-compose		eps :: f :~> g => cata phi . cata (In . eps) = cata (phi . eps)

Examples

 
data StrF x = Cons Char x | Nil
type Str = FixF StrF
 
instance Functor StrF where
    fmap f (Cons a as) = Cons a (f as)
    fmap f Nil = Nil
 
length :: Str -> Int
length = cata phi where
    phi (Cons a b) = 1 + b
    phi Nil = 0
 
data NatF a = S a | Z deriving (Eq,Show)
type Nat = FixF NatF
 
instance Functor NatF where
     fmap f Z = Z
     fmap f (S z) = S (f z)
 
plus :: Nat -> Nat -> Nat
plus n = cata phi where
     phi Z = n
     phi (S m) = s m
 
times :: Nat -> Nat -> Nat
times n = cata phi where
     phi Z = z
     phi (S m) = plus n m
 
z :: Nat
z = InF Z
 
s :: Nat -> Nat
s = InF . S
 

Links
[Haddock] [Source] [Field Guide]

References

[1] L. Meertens. First Steps towards the theory of Rose Trees. Draft Report, CWI, Amsterdam, 1987.
[2] G. Malcolm. PhD Thesis. University of Gronigen, 1990.
[3] G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255--279, 1990.
[4] E. Meijer. Calculating Compilers, Ph.D thesis, Utrecht State University 1992.
[5] E. Meijer, M. Fokkinga, R. Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Proceedings, 5th ACM Conference on Functional Programming Languages and Computer Architecture.

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.

* 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 .

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 :

 
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 lacks coexponentials -- with good reason! If 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 is said to be representable by an object if it is naturally isomorphic to .

We can translate that into Haskell, letting play the role of 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 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 with a left adjoint 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 can play the role of as we did above. For , 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 , and end of is a pair where is an object of and omega is a dinatural transformation from e to S such that given any other dinatural transformation to S from another object x in , there exists a unique morphism , such that for every in .

We usually choose to write ends as , and abuse terminology calling the end of .

Note this uses a dinatural transformation from an object in , which we can choose to represent an arbitrary dinatural transformation from an object to a functor 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 = 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 = 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 or to denote a -> b. Similarly we use 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 along in terms of ends.

Working by rote, we note that is just c -> K m as noted above, and that 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 the function 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 along as a coend:

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 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 and consists of a pair of functors , and and a natural isomorphism:

We call the left adjoint functor, and the right adjoint functor and an adjoint pair, and write this relationship as

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 = leftAdjunct and = rightAdjunct. [haddock]

 
class &