[Haskell-cafe] Very freaky

[Jonathan Cast]

On Tuesday 10 July 2007, Andrew Coppin wrote:
> OK, so technically it's got nothing to do with Haskell itself, but...

Actually, it does: the basic technologies underlying Haskell (combinatory 
logic and the Hindley-Milner type system) were originally invented in the 
course of this stream of research.

> I was reading some utterly incomprehensible article in Wikipedia. It was
> saying something about categories of recursive sets or some nonesense
> like that, and then it said something utterly astonishing.
>
> By playing with the lambda calculus, you can come up with functions
> having all sorts of types. For example,
>
>   identity :: x -> x
>
>   add :: x -> x -> x
>
>   apply :: (x -> y) -> (y -> z) -> (x -> z)
>
> However - and I noticed this myself a while ago - it is quite impossible
> to write a (working) function such as
>
>   foo :: x -> y
>
> 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.

> but they seem to be  
> asserting that a type can be interpreted as a logic theorum, and that
> you can only write a function with a specific type is the corresponding
> theorum is true. (Conversly, if you have a function with a given type,
> the corresponding theorum *must* be true.)
>
> For example, the type for "identity" presumably reads as "given that x
> is true, we know that x is true". Well, duh!
>
> Moving on, "add" tells as that "if x is true and x is true, then x is
> true". Again, duh.
>
> Now "apply" seems to say that "if we know that x implies y, and we know
> that y implies z, then it follows that x implies z". Which is
> nontrivial, but certainly looks correct to me.
>
> On the other hand, the type for "foo" says "given that some random
> statement x happens to be true, we know that some utterly unrelated
> statement y is also true". Which is obviously nucking futs.
>
> Taking this further, we have "($) :: (x -> y) -> x -> y", which seems to
> read "given that x implies y, and that x is true, it follows that y is
> true". Which, again, seems to compute.
>
> 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.

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.

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs