Presented by Richard C. Cobbe
Transcribed by Vasileios Koutavas
Used a categorical proof technique to prove the soundness of polymorphic type inference for the functional core of ML.
Some of the domains that he used:
V: domain of tagged values (disjoint union)
B0: Boolean Domain
Types:
i0, i1, ... : ground types
t -> t : function types
Relation: u "has type" t
|= u: t
bottom has every type
WRONG has no type
* The relation |= looks like a logical relation. It relates the type meaning of the term to its actual meaning.
Environments:
r: semantic environment
G: type environment
Relation between environments (compatible environments, or
"r respects G"):
for all x in dom(r),
|= r(x): G(x)
This can also be written:
|= r: G
Soundness Theorem:
If |= r: G and G |- e: t, then |= E[[e]] r: t
Proof: structural induction
one case of the induction:
G |- e = if e1 then e2 else e3 : t
v1 = E[[e1]] r
- v1 = WRONG, then not typable
- v1 = bottom, bottom has all types => well typed
- v1 = B0 (boolean), then pick e1 or e2
* This was the first paper that introduced type soundness.
Extended the proof technique for imperative languages. It resulted to a very complicated categorical proof that it was difficult to follow and verify.
s, r |- e \Downarrow v, s'
Proof method:
Step 1:
If |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then |= v: t
problem: not enough information. There is no store information
Step 2: Add store in the typing relations
If s |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then s |= v: t
problem: There is no store type information.
e.g. This scenario is allowed:
s = { a -> nil }
r = { x -> a, y -> a }
G = { x -> (int list) ref, y -> (bool list) ref }
e = x := [7]; !y
Step 3: Add store typing ST: loc -> types
Soundness Theorem:
If s: ST |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then
there exists ST' s.t. s': ST' |= v: t
The definition of the relation s: ST |= r: G is not trivial. Because of possible cycles in the store an inductive definition is not well-founded. We need a co-inductive set for the definition of this relation (Maximal fixpoint):
We have to find a set of values and prove that this set is consistent with the function F(Q): Q subset or equal to F(Q). (definition of function in the paper)
s: ST |= v: t ==> s': ST' |= v: t
where:
s' = s + { a0 -> v0 }
ST' = ST + { a0 -> t0 }
let Q = { (s': ST' |= v: t) | s: ST |= v: t }
We have to show that: Q subset or equal to F(Q) (Q is F-consistent)
* Co-induction seems easier than categorical proof, but it has the difficulty to
guess the initial set Q.
* Advantage of this method over Milner's: It avoids the complicated domain construction.
Soundness Theorem:
If |- e: t then e diverges or e |->> v and |- v: t
where |->> is the transitive closure of small-step reduction (->), inside a context.
Proof:
It is undecidable if a term will get stuck. Therefore we use a conservative approximation for
stuck terms, called Faulty Terms:
(c v) s.t delta(c, v) is undefined
The proof is based on three lemmas:
Lemma 1: Subject Reduction (Preservation)
If G |- e1: t and e1 -> e2 then G |- e2: t1
Proof: case analysis on the form of small step reduction (->)
Corollary:
If G |- e1: t and e1 |->> e2 then G |- e2: t1
Lemma 2: Uniform Evaluation (not Progress)
For closed e, if there is no faulty e' s.t. e |->> e' then e diverges or e |->> v
Lemma 3: Faulty terms are untypable.
Proof: straight forward case analysis on delta(c, v)
From lemmas 1,2,3 we get the proof of the soundness theorem.
Extensibility of the proof:
In the paper the language is extended with references. The new soundness proof reuses the
cases of the old proof an adds only the new cases in the three lemmas.
Also we have to add the new faulty terms (they expand quadratically):
(! v) when v is not a reference
(:= v) when v is not a reference
(\ro \theta <x, v>. (x v))
Q: Why is Wright & Felleisen's technique better?
- Milner's technique: difficult domain construction
- Tofte's technique: difficult co-induction
- Wright & Felleisen's technique: (a) straight forward induction, (b) extensible.