[Haskell-cafe] Re: Re: is proof by testing possible?
Ben Franksen
ben.franksen at online.de
Mon Oct 12 16:45:44 EDT 2009
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
More information about the Haskell-Cafe
mailing list