[Haskell] Correct interpretation of the curry-howard isomorphism

[Frank Atanassow]

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

Regards,
Frank