[Haskell] Correct interpretation of the curry-howard isomorphism

[oleg at pobox.com]

> 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"