[Haskell] Correct interpretation of the curry-howard isomorphism

[Bruno Oliveira]

Hi!

Thanks Connor, I enjoyed your answer, it was very illustrative.

>> 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) :) ?


>The type system does not become a logic until you populate some of
>the types (hopefully only those corresponding to true propositions)
>with the terms which describe the construction of proofs. You can't
>pretend that Haskell is sound just by hoping that Curry and Howard
>(when properly interpreted) won't be able to see the broken bits.

>It's nonetheless an interesting question which bits you need to
>throw away to get a sound language. You'll have to get rid of

>   y :: (p -> p) -> p
>   unJust :: Maybe wmd -> wmd

>and hence the programming language features which enable them to
>be constructed, in particular, pattern matching with incomplete
>coverings, and general recursion.

Yes, I thought about those implications, that's why I also thought (incorrectly) that it would be too limiting and therefore probably wrongly interpreted.

It is also, not too hard to see, as you said, that general recursion would validate that interpretation (even without using any other primitives or functions):

coerce :: a -> b
coerce = coerce

or even

coerce :: a -> b
coerce x = let y = y in y

Then, even if we ignored the primitives, Haskell would still be unsound! 
Moreover, we could then say that most of the functional languages (which have a similar type system) are unsound.

Right ? Is it "Charity" an exception on this?


>There's an interesting paper `Elementary Strong Functional
>Programming' by David Turner, in which he proposes such a language.
>He suggests that, at least for paedagogical purposes, a functional
>language which gave up completeness for consistency might be no
>bad thing. I'm inclined to agree with him.

I will take a look on it.

>So I won't make any foolish and portentous pronouncements about
>dependent types being the only way to save us from damnation. I'll
>merely observe that we often use the unsound parts of programming
>languages as the best approximations available to the programs
>we really mean: we don't intend recursion to loop infinitely,
>we just have no means to explain in the program why it doesn't;
>we don't intend to apply unJust to Nothing, we just have no means
>to explain in the program why this can't happen. Dependent types
>support a higher level of articulacy about what is really going on,
>reducing, but not removing entirely the need to work outside the
>consistent fragment of the language. They do not save us from Satan
>but from Wittgenstein. Whereon you know something, thereon speak!

Dependent types definitely seem an advance to me. I saw recently a presentation
of a very impressive tool (epigram - I wonder if you have heard about it :P).

I'll be definitely take a better look on it as soon as I finish some work with more priority.

Best Regards,

Bruno