[Haskell-cafe] Haskell Zippers on Wikibooks: teasing! :)

[wren ng thornton]

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