# [Haskell-cafe] Tutorial: Curry-Howard Correspondence

Dan Weston westondan at imageworks.com
Mon Oct 22 15:31:31 EDT 2007

```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.
>
>
>
>
>

```