Re: [Haskell] Correct interpretation of the curry-howard isomorphism
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
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 IANATT[1]. 1. I Am Not A Type Theorist -- % Andre Pang : trust.in.love.to.save
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.
I'm afraid the misconception is Conor's. Haskell's type system is (so far as we know) sound: this means programs will not crash. It is also complete: every computable function is definable. However, the type system is _inconsistent_: that is, every type is inhabited (by, at least, bottom). Recall Goedel: no consistent logic can be both sound and complete w.r.t. computationally adequate models. For Haskell to qualify as a programming language, we need it to be complete. In order that Haskell programs never "go wrong", we need it to be sound. So, it cannot be consistent. Regards, Frank
Hi Frank! But then I have a paradox ...
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.
I'm afraid the misconception is Conor's.
Haskell's type system is (so far as we know) sound: this means programs will not crash.
If this interpretation of the curry-howard isomorphism is true: ---------------------------------- if we can write a function: coerce :: a -> b then, this would mean (by the curry-howard isomorphism) that the type system is not sound. ---------------------------------- and haskell type system is sound then we cannot write coerce. Which as been shown in the last emails that it is not true. So, either the interpretation of the isomorphism is wrong, or Haskell type system is in fact unsound. Right ? They cannot be both true! Well, the other possibility is, there are two different meanings for soundness :) Best regards, Bruno Oliveira
On Fri, 23 Apr 2004, Bruno Oliveira wrote:
and haskell type system is sound
then we cannot write coerce.
Which as been shown in the last emails that it is not true.
So, either the interpretation of the isomorphism is wrong, or Haskell type system is in fact unsound. Right ? They cannot be both true!
_|_ is an element of all types in Haskell because any function can fail to terminate as far as the type system's concerned. You can't write a coercion that doesn't do one of: return _|_, return a conversion (which can't be done for a->b) or return a constant (also not doable in the general case with the exception of _|_). AIUI (I'm no logician), that's just going to amount to something akin to "given a proof everything's true" or similar. Don't look at me for soundness, mind! -- flippa@flippac.org
So, either the interpretation of the isomorphism is wrong, or Haskell type syste m is in fact unsound. Right ? They cannot be both true!
Let us indeed examine what exactly it means for a type system to be sound. The soundness of a type system is usually proved as a theorem of a form: If an expression E is (statically) assigned a type T, *AND* if the evaluation of the expression E terminates and yields a value V of type T', then T = T' (if the type system supports subtyping, then the theorem says that T' is a subtype of T). Please note the second IF. In Haskell, if we don't use unsafePerformIO [1], the theorem holds (certainly for the large subset of Haskell that is described by the HM type system). Regarding Curry-Howard isomorphism: it has two parts: - a term is an encoding of a proof of a formula that is its type - proof normalization corresponds to term normalization (Thanks to Ken Shan for explaining this). Let us concentrate on the first part (which we would call Curry-Howard correspondence). First of all, why it can hold. Judgments of a type system may be considered axioms and inference rules. A formula is a theorem if we can point out a proof, that is, a tree of axioms and rules that lead to that formula. We also note that a type judgment is associated with a term of a particular structure. So, we can encode a tree of type judgments as an abstract syntax tree. That is, a term is an encoding of a proof tree. I guess it is easy to explain with an example: In the following, s, t, u would be type variables (aka variables in our logical system), x, y, z would be term variables. Greek letters stand for meta-variables in axiom schemas and rules. Gamma is a (perhaps empty) set of formulas. -> stands for a logical implication and the functional arrow. Let us attempt to prove the first-order logical formula (s->((s->t)->t)) where -> stands for logical implication. One can construct a truth table to see that the formula is a tautology. We will prove it in the Sequent Calculus LK. We actually need only a subset of the calculus' axioms and inference rules: A: Gamma, alpha ---> alpha C1: Gamma, alpha ---> beta ===> Gamma ---> alpha -> beta C2: Gamma ---> alpha -> beta ===> Gamma, alpha ---> beta Here ---> separates the antecedent and the succedent of a sequent, ===> separates the premise and the conclusion of a rule. C1 and C2 are actually the same rule: in LK, rules can be applied either way. Here's the proof: A: s->t ---> s->t C2: s->t ---> s->t ===> C1: s, (s->t) ---> t ===> C1: s ---> (s->t)->t ===> ---> s->((s->t)->t) Now, we can introduce terms: exp ::= variable | \variable -> exp | exp exp and annotate inference rules with terms: C1: Gamma, x::alpha ---> exp::beta ===> Gamma ---> (\x->exp)::(alpha -> beta) C2: Gamma ---> exp::(alpha -> beta) ===> Gamma, exp2::alpha ---> (exp exp2)::beta Now we can encode the above proof as a term (\x->\f->(f x)). Indeed, the syntactic form of a term uniquely determines the rule to apply. So the abstract syntax tree of a term is proof tree (for the type of a term). We can enter :type \x -> (\f -> f x) in Hugs or GHCi and see that the term has indeed the desired type. Haskell terms and Haskell types are of course more complex. In particular, Haskell includes the following axioms and rules: ---> [] :: alpha ---> id :: alpha -> alpha Gamma ---> x::[alpha] ===> Gamma ---> (head x)::alpha Gamma ---> x::(alpha->alpha) ===> Gamma ---> (fix x) :: alpha Using these rules, one can easily derive that ---> (head []) :: alpha ---> (fix id) :: alpha Indeed, if we ask a Haskell system ":type head []" or ":type fix id" we see the result "forall a. a". That is, we can derive everything and anything at all. The world is trivial. However, the above reasoning had a flaw: the rules for 'head' and 'fix' actually had side conditions. For example, the rule for 'head' applies only if the argument of 'head' is a non-empty list. That condition was implicit -- but it had to be verified for our proof to be valid. Similarly, the rule for 'fix' applies only if 'fix x' terminates. It is slighty cumbersome to express this side condition formally. Therefore, when applied to Haskell, the Curry-Howard correspondence has to be modified. Terms may encode invalid proofs. Only terms that are values or that can be reduced to values in finite number of steps encode valid proofs. Thus: a type (==formula) is proven if there is a program (term) that evaluates to a value of that type. [1] Given unsafePerformIO, it is possible to implement "coerce:: a ->b" that is a terminating, total function. Here it is, for easy reference. coerce:: a->b coerce a = let ref = unsafePerformIO (newIORef undefined) in unsafePerformIO ((writeIORef ref a) >> readIORef ref) In a sense, a language with unsafePerformIO is akin to a theorem prover with a primitive "trustMe"
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
participants (6)
-
Andre Pang -
Bruno Oliveira -
Conor T McBride -
Frank Atanassow -
oleg＠pobox.com -
Philippa Cowderoy