| < Free Open Study > |
|
The algorithm for calculating minimal types is now built along the same lines as the one for the simply typed lambda-calculus with subtyping, with one additional twist: when we typecheck an application, we calculate the minimal type of the left-hand side and then expose this type to obtain an arrow type, as shown in Figure 28-2. If the exposure of the left-hand side does not yield an arrow type, then rule TA-APP does not apply and the application is ill-typed. Similarly, we typecheck a type application by exposing its left-hand side to obtain a quantified type.
Figure 28-2: Algorithmic Typing for F<:
The soundness and completeness of this algorithm with respect to the original typing rules are easy to show. We give the proof for kernel F<: (the argument for full F<: is similar; cf. Exercise 28.2.3).
If , then Г ⊢ t : T.
If Г ⊢ t : T, then with Г ⊢ M <: T.
Proof: Part (1) is a straightforward induction on algorithmic derivations, using part (1) of Lemma 28.1.1 for the application cases. Part (2) goes by induction on a derivation of Г ⊢ t : T, with a case analysis on the final rule used in the derivation. The most interesting cases are those for T-APP and T-TAPP.
Case T-VAR: | t = x | x:T Î Г |
By TA-VAR, . By S-REFL, Г ⊢ T <: T.
Case T-ABS: | t = λx:T1 . t2 | Г, x:T1 ⊢ t2 : T2 | T = T1 → T2 |
By the induction hypothesis, Г, for some M2 with Г, x:T1 ⊢ M2 <: T2-i.e., with Г ⊢ M2 <: T2, since subtyping does not depend on term variable bindings in the context (Lemma 26.4.4). By TA-ABS, . By S-REFL and S-ARROW, Г ⊢ T1 → M2 <: T1 → T2.
Case T-APP: | t = t1 t2 | Г ⊢ t1 : T11 → T12 | T = T12 | Г ⊢ t2 : T11 |
From the induction hypothesis, we obtain and , with Г ⊢ M1 <: T11 → T12 and Г ⊢ M2 <: T11. Let N1 be the least nonvariable supertype of M1-i.e., Г ⊢ M1 ⇑ N1. By part (2) of Lemma 28.1.1, Г ⊢ N1 <: T11 → T12. Since we know that N1 is not a variable, the inversion lemma for the subtype relation (26.4.10) tells us that N1 = N11 → N12, with Г ⊢ T11 <: N11 and Г ⊢ N12 <: T12. By transitivity, Г ⊢ M2 <: N11, so rule TA-APP applies to give us , which satisfies the requirements.
Case T-TABS: | t = λX<:T1 . t2 | Г, X<:T1 ⊢ t2 : T2 | T = "X<:T1 .T2 |
By the induction hypothesis, for some M2 with Г, X<:T1 ⊢ M2 <: T2. By TA-TABS, . By S-ALL, Г ⊢ "X<:T1.M2 <: "X<:T1 .T2.
Case T-TAPP: | t = t1 [T2] | Г ⊢ t1 : "X<:T11 .T12 |
T = [X ↦ T2]T12 | Г ⊢ T2 <: T11 |
By the induction hypothesis, we have , with Г ⊢ M1 <: "X<:T11 . T12. Let N1 be the least nonvariable supertype of M1-i.e., Г ⊢ M1 ⇑ N1. By the exposure lemma (28.1.1), Г ⊢ N1 <: "X<:T11 . T12. But we know that N1 is not a variable, so the inversion lemma for the subtype relation (26.4.10) tells us that N1 = "X<:T11.N12, with Г, X<:T11 ⊢ N12 <: T12. Rule TA-TAPP gives us , and the preservation of subtyping under substitution (Lemma 26.4.8) yields Г ⊢ [X ↦ T2]N12 <: [X ↦ T2]T12 = T.
Case T-SUB: | Г ⊢ t : S | Г ⊢ S <: T |
By the induction hypothesis, with Г ⊢ M <: S. By transitivity, Г ⊢ M <: T.
The kernel F<: typing relation is decidable, given a decision procedure for the subtype relation.
Proof: For any Г and t, we can check whether there is some T such that Г ⊢ t : T by using the algorithmic typing rules to generate a proof of . If we succeed, then this T is also a type for t in the original typing relation, by part (1) of 28.2.1. If not, then part (2) of 28.2.1 implies that t has no type in the original typing relation. Finally, note that the algorithmic typing rules correspond to a terminating algorithm, since they are syntax directed (at most one applies to a given term t) and they always reduce the size of t when read from bottom to top.
Where do the proofs above need to be changed for full F<:?
| < Free Open Study > |
|