doesn't make much sense to me yet, although I suspect I can read the mu as a lambda on types?

Not really. The mu has more to do with recursion. Matthias.

Peter Verswyvelen wrote:

After my colleague explained me about zippers and how one could derive the datatype using differential rules, I had to read about it.

So I started reading http://en.wikibooks.org/wiki/Haskell/Zippers#Mechanical_Differentiation

This page contains the sentence: *"For a systematic construction, we need to calculate with types. The basics of structural calculations with types are outlined in a separate chapter **Generic Programming*http://en.wikibooks.org/w/index.php?title=Haskell/Generic_Programming&action=edit&redlink=1 * and we will heavily rely on this material"* * * However, the generic programming link does not exist yet :-)

A clear case of laziness on the author's part... wait, that would be me. :-O In any case, contributions to the wikibook would be most welcome. ;-) For now, I'd recommend Generic Programming: An introduction http://www.cse.chalmers.se/~patrikj/poly/afp98/ It's a bit verbose at times, but you only need the first few chapters to get an idea about polynomial functors (sums and pairs) and mu . Regards, apfelmus -- http://apfelmus.nfshost.com

Peter Verswyvelen wrote:

After my colleague explained me about zippers and how one could derive the datatype using differential rules, I had to read about it.

So I started reading http://en.wikibooks.org/wiki/Haskell/Zippers#Mechanical_Differentiation

This page contains the sentence: *"For a systematic construction, we need to calculate with types. The basics of structural calculations with types are outlined in a separate chapter **Generic Programming*http://en.wikibooks.org/w/index.php?title=Haskell/Generic_Programming&action=edit&redlink=1 * and we will heavily rely on this material"* * * However, the generic programming link does not exist yet :-)

So although I now have a rough idea about it, I don't understand the details yet, e.g. notation like

[image: \mathit{Node}\,A = \mu X.\,\mathit{NodeF}_A\,X]

doesn't make much sense to me yet, although I suspect I can read the mu as a lambda on types?

|\mu X. T| can be interpreted as |fix (\lambda X. T)| on types (where fix is the function returning the least fixed point of its argument), so you're close. To figure out what this interpretation means, you can just think of it as tying the knot, where the X is the name we give to the recursive type; thus: data List x = Nil | Cons x (List x) == data List x = \mu xs -> Nil | Cons x xs -- i.e. "xs" = \mu xs -> Nil | Cons x xs ==> data ListF x xs = Nil | Cons x xs type List x = \mu xs -> ListF x xs ... The full details are a bit more complex because we should distinguish between \mu (least fixed point) and \nu (greatest fixed point). For Haskell data types these two fixed points happen to coincide, but that's not the case in general. -- Live well, ~wren