[Haskell] Correct interpretation of the curry-howard isomorphism

[Conor T McBride]

Hi

Bruno Oliveira wrote:
 > Hi Frank!
 >
 > But then I have a paradox ...

 >>>Clearly a misconception of mine.
 >

Frank:
 >>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,
doesn't it?

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

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.

Cheers

Conor