Joe Fredette wrote:
That has got to be the single awesomest thing I have ever seen ever...
I was dumbfounded, too, when I first read about this. BTW, and completely off-topic: if you like this, you might have fun too with Conor McBride's discovery that data types can be differentiated, and the result is even useful: it corresponds to what is known (to some) as a Zipper: http://www.cs.nott.ac.uk/~ctm/diff.pdf Moreover, we can also give a sensible and useful interpretation to finite difference quotients of types: http://blog.sigfpe.com/2009/09/finite-differences-of-types.html which McBride calls "dissections" and discusses in some depth here: http://strictlypositive.org/CJ.pdf What is most astonishing to me is that these constructions work even though there is neither subtraction nor division defined on data types, only addition and multiplication (there are neutral elements for both, but not necessarily inverses). Cheers Ben