Hi, --- Bruno Oliveira <bruno.oliveira@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