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]:

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:T ₁ . t ₂

, x:T ₁ ⊢ t ₂ : T ₂

T = T ₁ T ₂

By the induction hypothesis, , for some M ₂ with , x:T ₁ ⊢ M ₂ <: T ₂ - i.e., with ⊢ M ₂ <: T ₂ , 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, ⊢ T ₁ M ₂ <: T ₁ T ₂ .

Case T-APP :

t = t ₁ t ₂

⊢ t ₁ : T ₁₁ T ₁₂

T = T ₁₂

⊢ t ₂ : T ₁₁

From the induction hypothesis, we obtain and , with ⊢ M ₁ <: T ₁₁ T ₁₂ and ⊢ M ₂ <: T ₁₁ . Let N ₁ be the least nonvariable supertype of M ₁ - i.e., ⊢ M ₁ ⇑ N ₁ . By part (2) of Lemma 28.1.1, ⊢ N ₁ <: T ₁₁ T ₁₂ . Since we know that N ₁ is not a variable, the inversion lemma for the subtype relation (26.4.10) tells us that N ₁ = N ₁₁ N ₁₂ , with ⊢ T ₁₁ <: N ₁₁ and ⊢ N ₁₂ <: T ₁₂ . By transitivity, ⊢ M ₂ <: N ₁₁ , so rule TA-APP applies to give us , which satisfies the requirements.

Case T-TABS :

t = λX<:T ₁ . t ₂

, X<:T ₁ ⊢ t ₂ : T ₂

T = " X<:T ₁ .T ₂

By the induction hypothesis, for some M ₂ with , X<:T ₁ ⊢ M ₂ <: T ₂ . By TA-TABS, . By S-ALL, ⊢ " X<:T ₁ .M ₂ <: " X<:T ₁ .T ₂ .

Case T-TAPP :	t = t ₁ [T ₂ ]	⊢ t ₁ : " X<:T ₁₁ .T ₁₂
	T = [ X ↦ T ₂ ] T ₁₂	⊢ T ₂ <: T ₁₁

By the induction hypothesis, we have , with ⊢ M ₁ <: " X<:T ₁₁ . T ₁₂ . Let N ₁ be the least nonvariable supertype of M ₁ - i.e., ⊢ M ₁ ⇑ N ₁ . By the exposure lemma (28.1.1), ⊢ N ₁ <: " X<:T ₁₁ . T ₁₂ . But we know that N ₁ is not a variable, so the inversion lemma for the subtype relation (26.4.10) tells us that N ₁ = " X<:T ₁₁ .N ₁₂ , with , X<:T ₁₁ ⊢ N ₁₂ <: T ₁₂ . Rule TA-TAPP gives us , and the preservation of subtyping under substitution (Lemma 26.4.8) yields ⊢ [X ↦ T ₂ ]N ₁₂ <: [X ↦ T ₂ ]T ₁₂ = 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.