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 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
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
