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

[Joe Fredette]

I read about differentiating and differences for types, that was  
awesome, but when I read the seemingly-impossible post the first time,  
I didn't have enough background in topology to understand what was  
going on. Differentiating types is usually how I introduce the power  
of haskell's type system to the other students in my Math department.  
I actually showed my algebra professor how non-recursive datatypes in  
n-variables are just multinomials over a commutative (up to  
isomorphism) ring and how you can use that to reason about  
equivalences between types based on the polynomial they're isomorphic  
too. My Algebra Professor, who does not program and knows very little  
about it,  sat back in his chair and say,

"So that's what all the fuss is about? Programming is easy!"

Really, all this goes to show that a rich, algebraic type system like  
Haskell's is invaluable because it harnesses the power of mathematics  
that we've been working at for years. Free Theorems indeed!

On Oct 12, 2009, at 4:45 PM, Ben Franksen wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe