[Haskell] Correct interpretation of the curry-howard isomorphism
Bruno Oliveira
bruno.oliveira at comlab.ox.ac.uk
Thu Apr 22 23:59:39 EDT 2004
Hi all!
I would like to know what is the right interpretation of one of the consequences of the curry-howard isomorphism.
I know that there is a relation between being able to implement coerse :: a -> b, and the fact that a type system is sound.
I thought this would be the right consequence:
------------------------------------------
if we can write a function:
coerce :: a -> b
then, this would mean (by the curry-howard isomorphism) that the type system is not sound.
------------------------------------------
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. 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 would appreciate if someone could provide me with the right interpretation.
Thanks, in advance!
Best Regards,
Bruno Oliveira
More information about the Haskell
mailing list