[Haskell-cafe] Re: Re: is proof by testing possible?
Joe Fredette
jfredett at gmail.com
Mon Oct 12 17:14:19 EDT 2009
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
More information about the Haskell-Cafe
mailing list