[Haskell] Correct interpretation of the curry-howard isomorphism

Andre Pang ozone at algorithm.com.au
Sat Apr 24 01:15:03 EDT 2004

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 

1.  I Am Not A Type Theorist

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

More information about the Haskell mailing list