[Haskell-cafe] Re: Re: is proof by testing possible?

[Ben Franksen]

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