On Fri, 23 Apr 2004, Bruno Oliveira wrote:
and haskell type system is sound
then we cannot write coerce.
Which as been shown in the last emails that it is not true.
So, either the interpretation of the isomorphism is wrong, or Haskell type system is in fact unsound. Right ? They cannot be both true!
_|_ is an element of all types in Haskell because any function can fail to terminate as far as the type system's concerned. You can't write a coercion that doesn't do one of: return _|_, return a conversion (which can't be done for a->b) or return a constant (also not doable in the general case with the exception of _|_). AIUI (I'm no logician), that's just going to amount to something akin to "given a proof everything's true" or similar. Don't look at me for soundness, mind! -- flippa@flippac.org