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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
