[Haskell] Correct interpretation of the curry-howard isomorphism
franka at cs.uu.nl
Fri Apr 23 19:21:05 EDT 2004
>>> coerce :: a -> b
>>> coerce x = undefined
>>> As an obvious consequence, Haskell type system would be unsound.
>>> So, I assumed that this would be a wrong interpretation.
>> This is the part of your email which frightens me the most. Of
>> course Haskell's type system is unsound! What factors lead you to
>> this kind of assumption?
> Clearly a misconception of mine.
I'm afraid the misconception is Conor's.
Haskell's type system is (so far as we know) sound: this means programs
will not crash.
It is also complete: every computable function is definable.
However, the type system is _inconsistent_: that is, every type is
inhabited (by, at least, bottom).
Recall Goedel: no consistent logic can be both sound and complete
w.r.t. computationally adequate models. For Haskell to qualify as a
programming language, we need it to be complete. In order that Haskell
programs never "go wrong", we need it to be sound. So, it cannot be
More information about the Haskell