[Haskell] Correct interpretation of the curry-howard isomorphism

[JP Bernardy]

Hi,

--- Bruno Oliveira <bruno.oliveira at comlab.ox.ac.uk>
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 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.

Cheers,
JP.



	
		
__________________________________
Do you Yahoo!?
Yahoo! Photos: High-quality 4x6 digital prints for 25¢
http://photos.yahoo.com/ph/print_splash