[Haskell] Correct interpretation of the curry-howard isomorphism
Conor T McBride
c.t.mcbride at durham.ac.uk
Sat Apr 24 12:32:06 EDT 2004
Bruno Oliveira wrote:
> Hi Frank!
> But then I have a paradox ...
>>>Clearly a misconception of mine.
>>I'm afraid the misconception is Conor's.
Frank, does it make sense to you to call a logical system `sound' if you
can use it to prove things which aren't true?
I did seek to be clear that I was interpreting `soundness' as
consistency, which seemed to be the appropriate notion when considering
the Curry-Howard correspondence. My mistake.
Haskell is not a `logical system' (why not?), so perhaps you can
call it `sound' with weaker justification, such as
>>Haskell's type system is (so far as we know) sound: this means programs
>>will not crash.
This, I referred to as `type safety'. I happen to think that such a
weak notion doesn't deserve the designation `soundness', but it seems
that this is a misconception. Fair enough. It feels good to be sound,
> Well, the other possibility is, there are two different meanings for
Only two? If we redesignate segmentation-fault-core-dumped a `value',
perhaps we can convince ourselves that C's type system is `sound'.
Such a scenario would provide even greater scope for violent
agreement than we currently enjoy.
But perhaps, in the interests of avoiding further misconception, we had
better follow the Duchess's dictum:
Take care of the sense, and the sounds will take care of themselves.
More information about the Haskell