Hi,
--- Bruno Oliveira [EMAIL PROTECTED]
wrote:
coerce :: a - b
coerce x = undefined
As an obvious consequence, Haskell type system would
be unsound.
Actually, in the isomrphism, undefined is a proof
that any theorem is correct. Somehow it can represent
an assumption that a subtheorem is
JP Bernardy wrote:
I'd say, check what any primitive 'proves' before
using it. Besides that, calling other functions is ok.
Except for general recursion.
coerce :: a - b
coerce = coerce
-- Lennart
___
Haskell mailing list
[EMAIL PROTECTED]
Hi!
Thanks Connor, I enjoyed your answer, it was very illustrative.
but then, it would be too easy to write this in haskell:
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.
On 23/04/2004, at 10:56 PM, Bruno Oliveira wrote:
but then, it would be too easy to write this in haskell:
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
