Algebra of Types as it relates to Zippers

[Jim Snavely <ludflu@gmail.com>]

This post has been going around my Google+ Functional programmers circle.

For those of you who read the Zipper paper last fall, this is pretty
interesting.

It turns out that the zipper construct is not just a clever trick for
updating purely functional data structures,
but also has very interesting theoretical underpinnings in the type system.

http://blog.lab49.com/archives/3011

The upshot is that if you treat type systems as a algebraic system, a
zipper (aka, a "one-hole context")
is equivalent to the derivative of the type of the data structure
you're building a zipper for.
Yes, that kind of derivative, i.e.  I should brush up on my neglected
calculus skills.

This seems to be derived from a Connor McBride paper, which is way over my head.

http://strictlypositive.org/diff.pdf

If you're mind is not sufficiently blown by all that check out this
related Stackoverflow.com post
http://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work

-- 
--Jim