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
_______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
