[Haskell] Correct interpretation of the curry-howard isomorphism

Philippa Cowderoy flippa at flippac.org
Fri Apr 23 19:23:53 EDT 2004

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 at flippac.org

More information about the Haskell mailing list