[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

Derek and Lennart,

Thank you both for your clarifications. Tutorials (and blogs) of the C-H 
correspondence and the naive (i.e. set-theoretic) categorical 
descriptions of Haskell are so eager to get to the insights you mention 
that they gloss too easily over the important role of _|_, a term I have 
been learning to give more respect to every time I (re)read about the 
differences between sets and CPOs.

If types correspond to theorems and terms correspond to proofs, then I 
guess program transformations correspond to rules of inference (e.g. 
function application flip ($) :: p -> (p -> q) -> q corresponding to 
modus ponens), and what causes the inconsistency is an extra rule of 
inference implied by non-strict function application when applied to 
bottom allowing the proof \_ -> undefined :: p -> q

What slightly bemuses me is that I would have thought this makes the 
proof procedure unsound, and consequently the insights into "the logic 
Haskell's type system corresponds to" not terribly insightful when 
analogized to intuitionist logic unless there were some computational 
way of restricting the proof system to a sound subset, which is what I 
was trying to get at by proposing to accept only proofs that terminated. 
Obviously, I've got a bit more reading to do before I can really 
understand all this.

Dan

Derek Elkins wrote:
> On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote:
>> There's nothing wrong with Haskell types.  It's the terms that make
>> Haskell types an inconsistent logic.
> 
> Logics are what are consistent or not, so saying the logic Haskell's
> type system corresponds to is inconsistent is all that can be said.
> Somewhere there is an axiom in it that makes forall a.(a -> a) -> a
> hold.  Usually, we just take that directly as the axiom (i.e. the
> existence of fix).
> 
>> But that doesn't mean that the C-H correspondence doesn't have any
>> insight to offer.
> 
> Which is certainly not what I said at all.
> 
> 
> 
> 
>