[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


Moreover, we can also give a sensible and useful interpretation to finite
difference quotients of types:


which McBride calls "dissections" and discusses in some depth here:


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).


More information about the Haskell-Cafe mailing list