[Haskell] Correct interpretation of the curry-howard isomorphism

JP Bernardy jyp_7 at yahoo.com
Fri Apr 23 04:29:12 EDT 2004


--- Bruno Oliveira <bruno.oliveira at comlab.ox.ac.uk>

> 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 true (in place of a
real proof -- another function).

Of course, this makes "corece = undefined" rather
uninteresting as a proof.

> So, I assumed that this would be a wrong
> interpretation. Would the following be more correct?
> ------------------------------------------
> if we can write a function:
> coerce :: a -> b
> without calling any other function or primitive
> (that is, just with making use of the type system),
> then this would 
> mean that the type system is unsound.

I'd say, check what any primitive 'proves' before
using it. Besides that, calling other functions is ok.


Do you Yahoo!?
Yahoo! Photos: High-quality 4x6 digital prints for 25¢

More information about the Haskell mailing list