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.
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@cl.cam.ac.uk