[Haskell] Correct interpretation of the curry-howard isomorphism

[Bruno Oliveira]

Hi Frank!

But then I have a paradox ...

>>>> 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.
>>
>>> This is the part of your email which frightens me the most. Of
>>> course Haskell's type system is unsound! What factors lead you to
>>> this kind of assumption?
>>
>> Clearly a misconception of mine.

>I'm afraid the misconception is Conor's.

>Haskell's type system is (so far as we know) sound: this means programs 
>will not crash.

If this interpretation of the curry-howard isomorphism is true:

----------------------------------
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.
----------------------------------

and haskell type system is sound 

then we cannot write coerce. 

Which as been shown in the last emails that it is not true.

So, either the interpretation of the isomorphism is wrong, or Haskell type system is in fact unsound. Right ?
They cannot be both true!

Well, the other possibility is, there are two different meanings for soundness :)

Best regards,

Bruno Oliveira