> {-# LANGUAGE Rank2Types,ExistentialQuantification #-}

Pick a type. Let's call it

`X`. Now consider the type

forall a . (a -> X,a) -> X

What can we say about elements of this type? There's an obvious example of such a function,

`eval`that applies the first element of the pair to the second.

> eval (f,x) = f x

It's also easy to construct others. What property do they all share? Well there's a nice way to answer this question. We can use Janis Voigtländer's Free Theorem Generator. After a bit of simplification it tells us that if

`f`is in

forall a . (a -> X,a) -> X

then for any compatible

`g`

f (x,g y) = f (x . g,y)

We can apply any function we like to the second argument and we get exactly the same result by pre-composing with the first argument.

This is a pretty strong property - it puts a big constraint on what

`f`can do. It holds because any function of type

`forall a . (a -> X,a) -> X`maps to a type

`X`that makes no reference to the quantified

`a`. It can't let any information about the type

`a`escape. And this means that

`f`has to somehow eliminate an element of

`a`and and element of

`a->X`. There's only one non-trivial way to do that: provide the former to the latter as a function argument. So

`f`must factor as

`h . eval`for some function

`h`. The free theorem comes from the fact that

`eval (x,g y) = eval (x.g,y)`. Or,

`f`could be the constant function, but that still factors in the same way.

Let's try something slightly more complex. Consider the type

forall a . (a -> X,[a]) -> X

Again we can ask the free theorem generator to give us a property. We're told that if

`f`is of this type, then for any compatible

`g`

f(x,map g y) = f(x . g,y)

The crucial point this time is that in order to eliminate the

`[a]`we have to use

`fmap`to apply the function of type

`a -> X`. So any function of this type must factor through

`fmap`, and that's why the free theorem follows.

Now it's time to put this in a more general framework. We can write both of the above examples as elements of type

`forall a . S a a -> X`where

`S`is some type constructor. In both cases we also have that

`S a`is a functor. But it's also a cofunctor in its first argument. Intuitively this says that

`S a b`contains or produces

`b`'s but consumes

`a`'s. Here's a class to express this:

> class Difunctor h where

> lmap :: (b -> a) -> h a c -> h b c

> rmap :: (c -> d) -> h a c -> h a d

(I made up the word Difunctor.)

For (co)functoriality we insist on the laws

lmap (f . g) = lmap g . lmap f

rmap (f . g) = rmap f . rmap g

We can make both of the examples above instances:

> data Ex1 x a b = Ex1 (a -> x) b

> instance Difunctor (Ex1 x) where

> lmap f (Ex1 g x) = Ex1 (g . f) x

> rmap f (Ex1 g x) = Ex1 g (f x)

> data Ex2 x a b = Ex2 (a -> x) [b]

> instance Difunctor (Ex2 x) where

> lmap f (Ex2 g x) = Ex2 (g . f) x

> rmap f (Ex2 g x) = Ex2 g (map f x)

Our free theorems were essentially about this type:

> type DiNatural s x = forall a . (s a a -> x)

and in both cases the free theorem could be written as

f . lmap g == f . rmap g

This is a highly non-trivial result. Look at the preconditions for this theorem: they say something about each of the arguments to

`s`individually. And yet we deduce that the two arguments are in fact intimately connected. We can apply

`g`using either

`lmap`or

`rmap`and get the same result. This property is known as dinaturality. More precisely, if for some

`X`,

`f :: s a a -> X`, where

`s`is a difunctor, then

`f`is dinatural if for all compatible

`g`,

f . lmap g == f . rmap g

We have this theorem: if

`s`is an instance of the

`Difunctor`class (obeying its laws) then for any

`X`, elements of

`DiNatural s X`are dinatural.

(Compare with the definition of naturality:

`f . fmap g = fmap g . f`.)

I'm tempted to call this "Dinaturality for Free" but there's already a paper by that name and I don't know what it's about. And note that I only claim it's a theorem. I don't actually know how to prove this uniformly for all difunctors, but I'd stake a beer on it. At least as long as we don't do any weird haskell coding (so our free theorems are always valid) and as long as we restrict ourselves to functions that always terminate.

In the examples I gave above the reason why this holds is related to the fact that any function of the given type can be factored as something following an evaluation type function. More generally, if

`s`is a dinatural then if there is a single

`Y`, and function

`i :: s a a -> Y`, such that every function

`f :: s a a -> X`, for any

`X`, can be factored as

`f = h . i`, then

`Y`is said to be the coend of

`s`.

There are different approaches to computing a coend. Above I've used inspection. The coend of

`(a -> X,a)`is

`X`. But there's also a kind of cheating approach where we can use an existential type to get the type uniformly for all dinaturals:

> data Coend s = forall a . Coend (s a a)

For an explanation of why that works, see Edward Kmett's post on Kan Extensions. For this example, this means we expect the types

`t`and

`Coend (Ex1 t)`to be isomorphic. Here is the isomorphism and its inverse:

> iso :: Coend (Ex1 t) -> t

> iso (Coend (Ex1 f x)) = f x

> iso' :: t -> Coend (Ex1 t)

> iso' x = Coend (Ex1 (const x) ())

I'll leave the proof that

`iso`and

`iso'`are mutual inverses to you.

I hope that gives some idea of what a coend is. Informally it captures the method by which a dinatural transformation of type

`forall a . s a a -> X`is able to eliminate the quantified

`a`. If you look through the Haskell libraries you'll find many dinaturals (or at least things that can be made dinatural through the use of

`uncurry`).

This code and description was inspired by the discussion at nLab.

## 8 comments:

Is there a result of the form: every counit of a comonad is dinatural?

I'm thinking of generalizations of the counit of the context comonad.

By definition, the counit is natural. 'cobind', or whatever you want to call it, is (probably) dinatural though.

uncurry cobind :: (w a -> b,w a) -> w b

I don't know how to prove uniformly that everything of this type is dinatural, but the free theorem for every example I've tried says it is.

If uncurry cobind is dinatural, why wouldn't uncurry bind also be so?

uncurry bind :: (a -> m b, m a) -> m b

As for the context comonad, I'm thinking of this:

counit :: (forall a. (a->x,a)) -> x

which is basically your

iso :: Coend (Ex1 t) -> t.

uncurry bind is also dinatural.

Your counit isn't.

The signature of a dinatural transformation (the kind we're talking about anyway) is

f :: forall a . (s a a -> X)

for some X.

I've put in parentheses to make the quantification clear. f is actually a family of functions, one for each a, mapping form s a a to X, as per the textbook definition of dinatural.

Your counit is of the form

counit :: A -> B

where A = forall a.(a->x,a)

(forgetting about the quantification over x for now). The quantification over a is contained completely in the domain.

In other words counit isn't a family of functions, it's a single function from an existential type. So it's a completely different kind of entity.

I'm pretty sure, but have not proven, that free theorems are equivalent to the (general) dinaturality conditions (plus some general properties of dinatural transformations.) I believe this has always been the case for any examples that correspond to natural transformations and for the examples that wouldn't correspond to natural transformations, the free theorems have at least implied the dinaturality condition.

Another interesting example of a dinatural transformation is (a -> a) -> a.

You say: "if s is a dinatural then if there is a single Y, and function i :: s a a -> Y, such that every function f :: s a a -> X, for any X, can be factored as f = h . i, then Y is said to be the coend of s."

I'm not sure, but I think you mean: "if s is a difunctor then if there is a single Y, and function i :: s a a -> Y, such that every dinatural function f :: s a a -> X, for any X, can be factored as f = h . i, then Y is said to be the coend of s."

Also, this concept of a morphism that factors another class of morphisms uniquely reminds me of fibred categories: is i :: s a a -> Y cartesian with respect to some fibration?

I think what you call a difunctor is what everyone else calls a profunctor.

Post a Comment