28.2 Minimal Typing

 < Free Open Study > 



28.2 Minimal Typing

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).

28.2.1 Theorem [Minimal Typing]:

  1. If , then Г t : T.

  2. 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.

28.2.2 Corollary [Decidability of Typing]:

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.

28.2.3 Exercise [⋆⋆]:

Where do the proofs above need to be changed for full F<:?



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net