[Haskell] Correct interpretation of the curry-howard isomorphism

[Andre Pang]

On 23/04/2004, at 10:56 PM, Bruno Oliveira wrote:

>>> 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.
>>
>> 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.
> Is it a good excuse that people told me that (or I misunderstood them) 
> :) ?

I'm no expert on this, but I would think that 'undefined' is a property 
of the dynamic semantics, not static semantics: i.e. although you will 
get a run-time error when you run the thing, it is still sound with 
respect to the type system.

This is probably the same situation as if you had:

     coerce :: a -> b
     coerce x = error "Foo"

Both error (i.e. _|_) and undefined are not ill-typed here, but 
IANATT[1].

1.  I Am Not A Type Theorist


-- 
% Andre Pang : trust.in.love.to.save