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*?! >_<