Jonathan Cast wrote:
On Tuesday 10 July 2007, Andrew Coppin wrote:
OK, so technically it's got nothing to do with Haskell itself, but...
Actually, it does
I rephrase: This isn't *specifically* unique to Haskell, as such.
Now, Wikipedia seems to be suggesting something really remarkable. The
text is very poorly worded and hard to comprehend,
Nothing is ever absolutely so --- except the incomprehensibility of
Wikipedia's math articles. They're still better than MathWorld, though.
Ah, MathWorld... If you want to look up a formula or identity, it's
practically guaranteed to be there. If you want to *learn* stuff...
forget it!
So is this all a huge coincidence? Or have I actually suceeded in
comprehending Wikipedia?
Yes, you have. In the (pure, non-recursive) typed lambda calculus, there is
an isomorphism between (intuitionistic) propositions and types, and between
(constructive) proofs and terms, such that a term exists with a given type
iff a (corresponding) (constructive) proof exists of the corresponding
(intuitionistic) theorem. This is called the Curry-Howard isomorphism, after
Haskell Curry (he whom our language is named for), and whatever computer
scientist independently re-discovered it due to not having figured out to
read the type theory literature before doing type theoretic research.
...let us not even go into what constitutes "intuitionistic
propositions" (hell, I can't even *pronounce* that!) or what a
"constructive" proof is...
Once functional programming language designers realized that the
generalization of this to the fragments of intuitionistic logic with logical
connectives `and' (corresponds to products/record types) and `or'
(corresponds to sums/union types) holds, as well, the prejudice that
innovations in type systems should be driven by finding an isomorphism with
some fragment of intuitionistic logic set in, which gave us existential types
and rank-N types, btw. So this is really good research to be doing.
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript / Delphi / VisualBasic / Perl / Python thing seems so boring.)
On the other hand... WHAT THE HECK DOES ALL THAT TEXT *MEAN*?! >_<
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
