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

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:T 1 . t 2 , x:T 1 ⊢ t 2 : T 2 T = T 1 T 2

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

 Case T-APP : t = t 1 t 2 ⊢ t 1 : T 11 T 12 T = T 12 ⊢ t 2 : T 11

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

 Case T-TABS : t = λX<:T 1 . t 2 , X<:T 1 ⊢ t 2 : T 2 T = " X<:T 1 .T 2

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

 Case T-TAPP : t = t 1 [T 2 ] ⊢ t 1 : " X<:T 11 .T 12 T = [ X ↦ T 2 ] T 12 ⊢ T 2 <: T 11

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