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

[Jon Fairbairn]

Derek Elkins <derek.a.elkins at gmail.com> writes:

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

I wouldn't say that that was all that could 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).

in particular, one can say interesting things about
Haskell's type system in the absence of dubious constants
like fix and unsafePerformIO. For example, if an expression
doesn't contain fix (and doesn't contain ... and possibly
other conditions to do with features the consequences of
which I've lost track), then we know that evaluation of the
expression will terminate.

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk