[Haskell-cafe] Very freaky

[Andrew Coppin]

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