> 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" _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell