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