[Haskell] Correct interpretation of the curry-howard isomorphism
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