I kept meaning to follow up on my earlier post about the Yoneda lemma by working out if each of the three examples I considered were Theorems for Free! But it's tedious work to decrypt the free theorem as it is generated by the procedure in Wadler's paper. But then I suddenly realised that lambdabot could do the work for me. I looked at all three examples that I gave, but I'll just spell out the details for the last one here. Consider machines of type

`forall b. (A -> b) -> C -> b`. What free theorem do we get from that? If you don't have lambdabot you can see here. But first I need to point out either a limitation in that free theorem prover, or a limitation of my understanding of it. It seems to attach a

`forall`for every free variable. But I want to have A and C fixed, but unknown. It makes a difference. In the end a cheated by considering the type

`(Float -> b) -> Char -> b`

The free theorem is

h1 (f1 x2) = g1 x2) => h1 (t1 f1 x1) = t1 g1 x1

where

`t1 :: forall b. (Float -> b) -> Char -> b`. With a tiny bit of work we can deduce

t1 h1 = h1 . t1 id.

Using my earlier notation, that is essentially

`check3 . uncheck3 = id`. Similar results followed for the other examples. So I conjecture that for functors F, the free theorems for

`(a -> b) -> F b`are just proofs of the Yoneda lemma (well, the less trivial direction at least). I'm guessing this is all blindingly obvious to type theorists but it's all new to me.

Anyway, a couple of thoughts come to mind. This stuff is all about parametricty, and part of what makes this work is that any polymorphic function (with the same restrictions in Theorems for Free!) that looks like a natural transformation

*is*a natural transformation in the category of Haskell types. But Theorems for Free! also talks about functions that

*don't*look like natural transformations. For example consider the type

`(a->a)->(a->a)`. The free theorem reflects the fact that any such function must simply raise its argument to some non-negative integer power. But it seems to me that when the free theorem is written in point-free style, then functions (ie. functions that map objects to arrows like the way natural transformations do) in a general category that satisfy this theorem are also in some sense 'natural'. So is there a wider sense of 'natural' in a category that I should know about?

What I find interesting here isn't necessarily the type theory in itself. What I think

*is*interesting is that the type theory provides nice intuition for other applications for the Yoneda lemma, and indeed other parts of category theory. Up to now, my spare time reading of computer science hasn't really fed back back into my understanding of other branches of mathematics. But this time it has. Even though the category of Haskell types and functions looks a lot like

**Set**, it has nice properties of its own that deepen your understanding of categories in general.

Anyway, while I'm on the subject of things Yonedic, here's an application of category theory to the composition of music. The author s claim the Yoneda lemma has applications in this field. Yes, you read that correctly. No, it's not April 1. In fact, I discovered this by doing a google code search on yoneda.

One last thing. I should credit augustss for getting me to think about the mathematical significance of parametricity in the first place. That was 6 months ago. Trying to do mathematics when you only have a couple of hours free a week is slow going.

BTW I'm in Mexico on vacation for the next week and a half. On the plane I'll be reading (at least) the papers on cake cutting and Venn diagrams mentioned here: Ars Mathematica.

## 3 comments:

I really enjoy reading your blog. I was wondering if you would consider writing something for the recently revived Monad.Reader. A lot of your blog posts could make great articles with a bit of polishing! Get in touch if you're interested,

Wouter Swierstra

PS - As far as variable substitution is concerned, you might be interested in free monads - which are basically the same construction you described in your blog post. For some reason, they aren't very well-known in the functional programming community.

For what it's worth, you can work out free theorems for arbitrary functors using the other one in lambdabot. It goes to a lot of trouble to make the theorems as point-free as possible.

So in your example:

h1 (f1 x2) = g1 x2 => h1 (t1 f1 x1) = t1 g1 x1can be simplified by noting that the "if" part of the implication merely says that

g1 = h1 . f1. And so, dropping the 1's:h . t f = t (h . f)Setting

f = idgives you the theorem.The free theorem for

test :: (C -> a) -> F ais:fmap f . test = test . (.) fThis should be unsurprising, because

(.) fisfmap fin the functor((->) C). Once again, all this says is thattestis a natural transformation.Applying

idto both sides gives:fmap f (test id) = test . fAnd a little rearrangement gives you the result you're after.

As to your second question, about

(a->a) -> (a->a), it's not a mapping between functors, but it is a mapping between natural transformations! I haven't looked too hard into it, but I suspect that the free theorem for this is a consequence of whatever the obvious mapping property of these "supernatural transformations" would look be.There's another way to look at it, but you'll have to read my article in the next Monad.Reader to find out.

But Theorems for Free! also talks about functions that don't look like natural transformations. For example consider the type (a->a)->(a->a). The free theorem reflects the fact that any such function must simply raise its argument to some non-negative integer power. But it seems to me that when the free theorem is written in point-free style, then functions (ie. functions that map objects to arrows like the way natural transformations do) in a general category that satisfy this theorem are also in some sense 'natural'. So is there a wider sense of 'natural' in a category that I should know about?Since the type variable occurs both covariantly and contravariantly a natural transformation is inappropriate (the functors would have to be both covariant and contravariant at the same time). Instead you may want to look at dinaturality, Basic Concepts of Enriched Categories is the best source of information (online) about them I'm aware of. It also covers indexed (co)limits, an unreasonably under-represented tool (and also (co)ends).

Dinaturality, or perhaps a special case of it, is often referred to as extraordinary naturality.

Post a Comment