22.5 Principal Types

---

22.5 Principal Types

We remarked above that if there is some way to instantiate the type variables in a term so that it becomes typable, then there is a most general or principal way of doing so. We now formalize this observation.

22.5.1 Definition

A principal solution for (Г, t,S, C) is a solution (σ, T) such that, whenever (σ′, T′) is also a solution for (Г, t, S, C), we have σ ⊑ σ′. When (σ, T) is a principal solution, we call T a principal type of t under Г.^[4]

22.5.2 Exercise [⋆ ↛]

Find a principal type for λx:X. λy:Y. λz:Z. (x z) (y z).

22.5.3 Theorem [Principal Types]

If (Г t, S, C) has any solution, then it has a principal one. The unification algorithm in Figure 22-2 can be used to determine whether (Г, t, S, C) has a solution and, if so, to calculate a principal one.

Proof: By the definition of a solution for (Г, t, S, C) and the properties of unification.

22.5.4 Corollary

It is decidable whether (Г, t) has a solution.

Proof: By Corollary 22.3.8 and Theorem 22.5.3.

22.5.5 Exercise [Recommended, ⋆⋆⋆ ↛]

Combine the constraint generation and unification algorithms from Exercises 22.3.10 and 22.4.6 to build a type-checker that calculates principal types, taking the reconbase checker as a starting point. A typical interaction with your typechecker might look like:

   λx:X. x; ▸ <fun> : X → X   λz:ZZ. λy:YY. z (y true); ▸ <fun> : (?X0→?X1) → (Bool→?X0) → ?X1   λw:W. if true then false else w false; ▸ <fun> : (Bool→Bool) → Bool 

Type variables with names like ?X₀ are automatically generated.

22.5.6 Exercise [⋆⋆⋆]

What difficulties arise in extending the definitions above (22.3.2, etc.) to deal with records? How might they be addressed?

The idea of principal types can be used to build a type reconstruction algorithm that works more incrementally than the one we have developed here. Instead of generating all the constraints first and then trying to solve them, we can interleave generation and solving, so that the type reconstruction algorithm actually returns a principal type at each step. The fact that the types are always principal ensures that the algorithm never needs to re-analyze a subterm: it makes only the minimum commitments needed to achieve typability at each step. One major advantage of such an algorithm is that it can pinpoint errors in the user's program much more precisely.

22.5.7 Exercise [⋆⋆⋆ ↛]

Modify your solution to Exercise 22.5.5 so that it performs unification incrementally and returns principal types.

^[4]Principal types should not be confused with principal typings. See page 337.

---