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