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