[Haskell] Correct interpretation of the curry-howard isomorphism

[Philippa Cowderoy]

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