[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Derek Elkins]

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.