[Haskell-cafe] Tutorial: Curry-Howard Correspondence
derek.a.elkins at gmail.com
Sun Oct 21 21:48:50 EDT 2007
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.
More information about the Haskell-Cafe