Lower bounds on type inference with subtypes

My Hoang^{∗} and John C. Mitchell^{∗} Computer Science Department

Stanford University Stanford, CA 94305

{hoang, mitchell}@cs.stanford.edu

Abstract

We investigate type inference for programming languages with subtypes. As described in previous work, there are several type inference problems for any given expression language, depending on the form of the subtype partial order and the ability to define new subtypes in programs. Our first main result is that for any specific subtype partial order, the problem of determining whether a lambda term is typable is algorithmically (polynomial-time) equivalent to a form of satisfiability problem over the same partial order. This gives the first exact characterization of the problem that is independent of the syntax of expressions. In addition, since this form of satisfiability problem is pspace-hard over certain partial orders, this equivalence strengthens the previous lower bound of np-hard to pspace-hard. Our second main result is a lower bound on the length of most general types when the subtype hierarchy may change as a result of additional type declarations within the program. More specifically, given any input expression, a type inference algorithm tries to find a most general (or principal) typing. The property of a most general typing is that it has all other possible typings as instances. However, there are several sound notions of instance in the presence of subtyping. Our lower bound is that no sound definition of instance would allow the set of additional subtyping hypotheses about a term to grow less than linearly in the size of the term.

1 Introduction

Subtyping is a basic feature of typed object-oriented languages. The main importance of subtyping is that it allows substitutivity: if A is a subtype of B, then elements of type A can be used anywhere that an element of type B is required. Among the many implications for staticallytyped languages, this allows data structures such as heterogeneous lists, where elements of the list come from arbitrary subtypes of some given type. This paper studies the problem of type inference in the presence of subtyping. Type inference, used in languages such as ML [GMW79, Mil85], Haskell [HF92, H^{+} 92] and Miranda [Tur85], is the process of inferring type information that has been omitted from expressions. Type inference allows type errors to be detected at compile time, without forcing programmers to include type annotations in programs.

Although an algorithm for type inference with subtyping was published in 1984 [Mit84, Mit91b], this algorithm has seen little if any practical use. Apart from the fact that languages which could take advantage of this algorithm are only now emerging, the main problems seem to be that the algorithm is inefficient and the output, even for relatively simple input expressions, appears excessively long and cumbersome to read. Some attempts to make the algorithm more practical appear in [FM89, FM90]; some studies of the inherent difficulty of the problem are [WO89, LM92, Tiu92, Ben94]. The previous studies show that some simplifications can be made to the output of the algorithm, the problem is at least np-hard in the general case (even assuming that the basic operations that occur in programs have relatively simple types) but some special cases could be solved more efficiently.

Our first main result is the algorithmic equivalence between typability with subtyping and a satisfiability problem over partial orders. In particular, for any subtype partial order, deciding whether an expression has any typing at all is equivalent to determining whether a form of satisfiability problem is solvable over this partial order. This gives us a characterization of the decision problem for typing in the presence of subtypes that is independent of the syntax of expressions. One reason why this is important is that, when considering programming languages with particular restrictions on the subtype partial order, we can focus on the satisfiability problem and rest assured that any satisfiability problem could arise in practice. Since this particular satisfiability problem over partial orders has been shown pspace-hard, over partial orders in general or certain fixed partial orders, our equivalence also strengthens the best previous lower bound of np-hard to pspace-hard. As noted in [LM92] the naive upper bound is exponential time.

Our equivalence between typability and partial order satisfiability holds even with very restricted assumptions about the types of basic symbols that appear in program expressions. More specifically, it is shown in [LM92] that it is np-hard to decide whether a lambda term has a type even if all term constants are restricted to having only atomic types. This is done by showing how the satisfaction of inequalities of the form b ≤ t, s ≤ t over a partial order can be represented as typability of terms using constants only of atomic type. (We use b for an element of the partial order of types and s and t for type variables.) In this paper, we show how arbitrary inequalities of the form s ≤ t → u and s ≥ t → u also arise in typing lambda terms using only constants of atomic types. Using earlier results on the complexity of the satisfaction of subtype inequalities [Tiu92], we can use this equivalence to show that the typability problem is pspace-hard, even when all constants in expressions have only atomic types.

∗ Supported in part by NSF Grant CCR-9303099 and the TRW Foundation.

Our equivalence clearly implies that the only way to devise a practical, polynomial-time type inference algorithm in the presence of subtyping is to restrict the programming language so that only certain forms of subtype partial orders are definable. This is in fact reasonable since, for example, single inheritance always results in forests of trees. In [Ben94], it is claimed that the satisfiability problem is solvable in polynomial time for this case. Therefore, if most programs use only single inheritance, we might expect polynomialtime behavior in practice. However, a practical type inference algorithm must print more than a simple yes/no answer in response to an input language expression. This is particularly important when a program may declare additional types and subtypes. Since a function declared at the top of the program may be called in several different lower contexts, the initial type-checking of the function must tell the programmer which uses of the function will be type correct and which will be erroneous. Otherwise, it will be very difficult to determine, when the type checker rejects a later application of this function, whether the problem lies in the function declaration or its use. Unfortunately, an efficient satisfiability algorithm for special partial orders still does not help us optimize the output of a type inference algorithm.

Given any input expression, a type inference algorithm tries to find a most general (or principal) typing. The property of a most general typing is that it has all other possible typings as instances. Without subtyping, “instance” boils down to “substitution instance.” A consequence is that the most general typing of any given expression is also the syntactically shortest, since no substitution can decrease the size of an expression. However, with subtyping, “instance” involves both substitution and entailment of subtyping hypotheses. Since substitution can render a set of subtyping hypotheses tautologous, a most general typing that involves any subtyping hypotheses about type variables will never be the shortest typing for the expression.

Given a fixed notion of instance, there may be most general typings of different lengths. In [FM89, FM90], an attempt is made to optimize the algorithm from [Mit84] so that the shortest most general typing is produced. However, simple examples given in Section 5 of the present paper show that this is not the best one can do. Specifically, by adopting a more powerful notion of instance than used in previous studies, we can reduce the length of the shortest most general type. In fact, for some expressions, we can eliminate subtyping hypotheses altogether from their most general types. If we were able to do this for all expressions, this would dramatically simplify the output of the type inference algorithm. However, we show that no sound definition of instance would allow the set of additional subtyping hypotheses about a term to grow less than linearly in the size of the term.

The rest of the paper is organized as follows. In Section 2, we define the type system incorporating subtyping. Besides establishing notation, this allows us to define the decision problems of typability and subtype inequality satisfiability. Section 3 and Section 4 are devoted to proving the polynomial-time equivalence of these two decision problems. In Section 5, we investigate the size of most general typings of terms with respect to any sensible definition of instance. Finally, we end with some directions for future work in Section 6.

2 Preliminaries

We study a type system for typing untyped lambda terms, possibly containing constant symbols. The set of untyped lambda-terms are generated by the following grammar

M : : = x | c | λx. M | M M

where x may be any variable and c a constant symbol.

The types of lambda terms are formed using type variables and type constants. Let B be a set of base types (int, bool, …). Then the set of types over B is generated by the following grammar

σ : : = b | t | σ → σ

where t is a type variable and b ∈ B. We let T ype^{B} be the set of types over B with no type variables. These are also called the set of ground types over B.

Given a set of base types B, a subtype assertion or containment is a formula of the form σ ⪯ τ, where σ, τ are types over B. A subtype assertion σ ⪯ τ is said to be atomic if σ and τ are either type variables or base types. Let ≤_{B} be a partial order on B. Intuitively, this ordering indicates the subtype ordering on base types in B. Let C be a set of subtype assertions. The following proof system defines the relation C ⊢ σ ⪯ τ which can be read, “σ is a subtype of τ under the additional subtype assumptions of C ”. If C, C′ are sets of subtype assertions, we use C ⊢ C′ to denote that C ⊢ σ ⪯ τ for every subtype assertion σ ⪯ τ ∈ C′.

(asmp)  C ⊢ σ ⪯ τ if σ ⪯ τ ∈ C or σ ≤_{B} τ
(ref )  C ⊢ σ ⪯ σ

(trans)  \frac{C ⊢ σ_{1} ⪯ σ_{2}  C ⊢ σ_{2} ⪯ σ_{3}}{C ⊢ σ_{1} ⪯ σ_{3}}

(→)  \frac{C ⊢ σ_{2} ⪯ σ_{1}  C ⊢ τ_{1} ⪯ τ_{2}}{C ⊢ σ_{1} → τ_{1} ⪯ σ_{2} → τ_{2}}

Given a partial order ⟨B, ≤_{B}⟩ on a set of base types B, we define the partial order ⪯_{B} on the set of types over B, as σ ⪯_{B} τ iff ϕ ⊢ σ ⪯ τ. We call the relation ⪯_{B} the subtyping relation induced by ≤_{B}. This is the subtyping relation without additional subtyping hypotheses.

We are now ready to define the problem of satisfaction of subtype inequalities. A system of inequalities over a partial order B = ⟨B, ≤_{B}⟩ is a finite set of formulas of the form σ_{1} ≤ σ_{2} , where σ_{1} and σ_{2} are types over B. Let V be the set of type variables that appear in a system of inequalities, I. We say that I is satisfiable in the partial order B if there is a substitution φ: V → T ype^{B} such that φ(σ_{1}) ⪯_{B} φ(σ_{2}) for every inequality σ_{1} ≤ σ_{2} in I. We then have the following decision problems for satisfiability of subtype inequalities (abbreviated SSI):

(SSI) Given a finite partial order B and a system I of inequalities, is I satisfiable in B?

(B -SSI) Given a system I of inequalities, is I satisfable in a fixed partial order B?

The difference between the two problems is that in (SSI), a problem instance is a pair ⟨B, I⟩, while an instance of (B - SSI) is a set I of inequalities to be satisfied over the fixed partial order B. In other words, there is a problem (B -SSI) for each partial order B.

To be able to type lambda terms, we need to know types for the term constants. And, to incorporate subtyping, we also need to know the subtype ordering on base types. A signature Σ = ⟨B, ≤_{B}, T ⟩ consists of a set B of base types, a partial order ≤_{B} on B, and a set T of pairs of the form ⟨c, σ⟩ with c a term constant and σ ∈ T ype^{B}. A typing judgement is a formula C, Γ ▷ M: σ where C is a set of atomic subtype assertions and Γ is a set of assumptions of the form x: σ, with x a variable. Intuitively, the context Γ represents the type declarations of the free variables used in a program and the coercion set C reflects the additional subtyping declarations that may appear in a program. The following proof system is used to identify the set of welltyped terms.

(var)  C, Γ ▷ x: σ  if x: σ ∈ Γ
(const)  C, Γ ▷ c: σ  if ⟨c, σ⟩ ∈ T

(abs)  \frac{C, Γ [x: σ] ▷ M: τ}{Γ ▷ λx. M: σ → τ}

(app)  \frac{C, Γ ▷ M: σ → τ  C, Γ ▷ N: σ}{C, Γ ▷ M N: τ}

(subtp)  \frac{C, Γ ▷ M: σ}{C, Γ ▷ M: τ}  if C ⊢ σ ⪯ τ

In the (abs) rule, we use Γ [x: σ] to denote the context given by Γ [x: σ] = (Γ − {x: τ}) ∪ {x: σ} if x: τ ∈ Γ, and Γ [x: σ] = Γ ∪ {x: σ}, otherwise. We call the above proof system ST_{⪯}, for simply-typed λ-calculus with subtyping. We use Σ ⊢_{ST_{⪯}} C, Γ▷M: σ to denote that the typing judgement C, Γ ▷ M: σ is derivable over signature Σ. The reason for including a set C of containments not given by the signature, and allowing type variables, is to represent sets of possible typings. For example, if a signature has int ⪯ real and char ⪯ string, then typing s ⪯ t, ϕ ▷ λx. x: s → t will have both λx. x: int → real and λx. x: char → string as instances, according to the definition we give in Section 5. We say that a term M is typable or well-typed (over a given signature Σ) if there exists a context Γ and type σ such that Σ ⊢_{ST_{⪯}} ϕ, Γ ▷ M: σ. As a notational convenience, we often drop the coercion set C from typing judgements if it is empty, i.e., we use Γ▷M: σ for the judgement ϕ, Γ▷M: σ. Just as for SSI, we have the following two decision problems for type inference in the presence of subtyping (abbreviated TIS):

(TIS) Given a signature Σ and a term M, is M typable over the signature Σ?

(Σ-TIS) Given a term M, is M typable over a fixed signature Σ?

The difference between the two problems is that in (TIS), a problem instance is a pair ⟨Σ, M⟩, while an instance of (Σ-TIS) is a typability problem over the fixed signature Σ. In other words, there is a problem (Σ-TIS) for each signature Σ.

As in [Mit91b], we can prove that the type of an expression M only depends on the type assumptions about its free variables. We use the notation Γ(x) to denote the unique σ such that x: σ ∈ Γ.

Lemma 2.1 Assume that ⊢_{ST_{⪯}} C, Γ ▷ M: σ. Suppose Γ′ is a context such that for all variables x that are free in M, Γ′(x) = Γ(x). Then ⊢_{ST_{⪯}} C, Γ′ ▷ M: σ.

A useful consequence of restricting the assertions in the coercion set of typing judgements to be atomic is the following property which states that one may normalize proofs in ST_{⪯} so that the only uses of (subtp) rule occur immediately after (var) and (const).

Lemma 2.2 For every provable typing statement C, Γ▷M: σ, there is a proof in which rule (subtp) is only used immediately after the typing axioms (var) and (const).

3 Type Inference Reduced to Inequality Satisfaction

It is well-known that the typability problem for simply-typed λ-calculus can be reduced to unification [ASU86, Wan87]. In this section we show that the analagous constraint satisfaction problem for typability in the presence of subtying is the satisfiability of subtype inequalities. More precisely, we exhibit a polynomial time reduction from TIS to SSI in which the poset constructed only depends on the signature. This reduction was implicit in [Mit91b] and [Tiu92].

In the rest of the paper we will use formulas of the form σ = τ, when defining a system of inequalities, as an abbreviation for the pair of inequalities σ ≤ τ and τ ≤ σ. Since ⪯_{B} is a partial order (as opposed to a preorder) the equation σ = τ is satisfiable iff σ ≤ τ and τ ≤ σ are satisfiable.

If Σ = ⟨B, ≤_{B}, T ⟩ is a signature with subtyping, then we define the partial order P_{Σ} to be ⟨B, ≤_{B}⟩.

Lemma 3.1 Given a signature (with subtyping) Σ, the decision problem for typability over Σ is polynomial time reducible to the satisfiability problem for subtype inequalities over P_{Σ} , i.e., Σ-TIS ≤_{m} P_{Σ} -SSI.

Proof Let Σ = ⟨B, ≤_{B}, T ⟩ be a signature. For any term M and a context A such that A(x) is a type variable for every x ∈ Dom(A), we define SI (M, A) = ⟨t, I⟩ by induction on the structure of M as follows, with t a type variable and I a system of inequalities.

SI (x, A) = ⟨t, {A(x) ≤ t}⟩

where t is a fresh type variable not in A.

SI (c, A) = ⟨t, {σ ≤ t}⟩

where ⟨c, σ⟩ ∈ C and t is fresh.

SI (MN, A) = let ⟨t_{1}, I_{1}⟩ = SI (M, A)

⟨t_{2}, I_{2}⟩ = SI (N, A) in

⟨t, I_{1} ∪ I_{2} ∪ {t_{1} = t_{2} → t}⟩, t is fresh.

SI (λx. M, A) = let ⟨t_{1}, I_{1}⟩ = SI (M, A ∪ {x: s})

where s is fresh in

⟨t, I_{1} ∪ {t = s → t_{1}}⟩ where t is fresh The reduction from Σ-TIS to P_{Σ} -SSI can then be given as follows. For any term M, we produce the set of inequalities I, where SI (M, A) = ⟨t, I⟩ with A a context that maps each variable x, free in M, to a distinct type variable. Using Lemma 2.2 it can be easily seen that this is a reduction. Since each inductive clause in the definition of SI adds only two new inequalities (a constant number) |I| ≤ c |M|, and this is a polynomial time reduction.

Corollary 3.2 The problem of deciding whether a given term is typable over a given signature, with subtyping, is polynomial time reducible to the satisfiability of subtype inequalities problem, i.e., TIS ≤_{m} SSI.

In the next section we will focus attention on systems of inequalities in which all formulas are of the form b ≤ t, s ≤ t, s ≤ t → u, or t → u ≤ s where s, t, u ∈ V , and b ∈ B. We call the satisfiability problem for this restricted system of inequalities SSI_{restr}. If the signature Σ = ⟨B, ≤_{B}, T ⟩ is such that all constants have atomic types, i.e., for all ⟨c, σ⟩ ∈ T , σ ∈ B, we call the TIS problem for such input signature TIS_{atom}. Note that Σ-TIS_{atom} really restricts the signature Σ rather than instances of the problem.

Corollary 3.3 The decision problem for typability over a signature Σ in which all constants have atomic types is polynomial time reducible to the satisfiability problem for restricted systems of subtype inequalities over P_{Σ} , i.e., Σ-TIS_{atom} ≤_{m} P_{Σ} -SSI_{restr}. Hence, TIS_{atom} ≤_{m} SSI_{restr}.

Proof The inequalities added in the inductive cases of SI when the term is an application or λ-abstraction are of the form s = t → u. When the term is a variable the inequality is of the form s ≤ t. When the term is a constant the inequality added is σ ≤ t which is of the form b ≤ t when σ is atomic.

4 Reducing Inequality Satisfaction to Typability

In Section 3, we showed how a solution to the type-inference problem in the presence of subtypes can be obtained from a solution to the problem of satisfaction of subtype inequalities. In this section, we establish the converse reduction, namely, we prove that SSI is polynomial time reducible to TIS. As corollaries of this reduction, we are able to translate lower-bound results about SSI to TIS. Together with results in Section 3, this shows the equivalence of the two problems TIS and SSI. When there are no subtype assumptions on base types, type-checking for simply-typed lambda calculus with subtyping reduces to that of simply-typed lambda calculus. And satisfaction of subtype inequalities over a discrete partial order is the same as unification. This gives the well known equivalence between type inference for simplytyped lambda calculus and unification [Tys88, Mit91a, Wan87] as a consequence of our results.

Although interest in type inference with subtypes gave rise to the earlier studies of satisfaction of subtype inequalities over partial orders [PT91, Tiu91, Tiu92], the precise connection between the two problems was not previously understood. In fact, comments in [Tiu92] suggest the belief that the satisfaction of inequalities would turn out to be algorithmically more complex. This suggests some of the subtlety of our proof that the two problems are in fact polynomial-time equivalent.

4.1 SSI_{restr} reduced to TIS_{atom}

We begin by showing how inequalities of the restricted form can be simulated by corresponding terms. More precisely, we will exhibit a polynomial time reduction from SSI_{restr} to TIS_{atom} . Before doing that, we state two lemmas that we will need in the proof of correctness of the reduction.

Lemma 4.1 Suppose D is a derivation of Γ▷M: σ in ST_{⪯}. Let φ be any substitution. Define the derivation φ(D) to be the one obtained by replacing every line of the form Γ′ ▷ M′: σ′ by φ(Γ′)▷M′: φ(σ′). Then φ(D) is a valid derivation in ST_{⪯}.

Proof We can prove by induction on τ_{1} that if τ_{1} ⪯_{B} τ_{2} then for any substitution φ, φ(τ_{1}) ⪯_{B} φ(τ_{2}). The lemma now easily follows by inspection of each axiom and inference rule of ST_{⪯}.

In particular by choosing φ to be a ground substitution, i.e., one that maps all variables to ground types, Lemma 4.1 shows that if any term M is typable then it has a typing derivation in which all type occurrences are ground types. Furthermore, by Lemma 2.2 we can assume that the derivation uses (subtp) only after (var) or (const).

The following lemma shows that typing an application term forces certain subtype inequalities to be satisfied. This is an easy consequence of Lemma 2.2.

Lemma 4.2 Let Σ = ⟨B, ⪯_{B}, C⟩ be a signature, suppose Σ ⊢_{ST_{⪯}} Γ ▷ xy: σ. Then Γ(x) = ρ_{1} → τ_{1} , Γ(y) = ρ_{2} with ρ_{2} ⪯_{B} ρ_{1} and τ_{1} ⪯_{B} σ.

Proof Consider any derivation of Γ▷xy: σ of the form given by Lemma 2.2

\frac{Γ ▷ x: δ_{1} → σ Γ ▷ y: δ_{1}}{Γ ▷ xy: σ}

with Γ(x) ⪯_{B} δ_{1} → σ and Γ(y) ⪯_{B} δ_{1} . Then Γ(x) = ρ_{1} → τ_{1} and with δ_{1} ⪯_{B} ρ_{1} and τ_{1} ⪯_{B} σ which gives us the statement of the lemma.

Let P = ⟨P, ≤_{P} ⟩ be any poset. Define the signature Σatom_{P} = ⟨P, ≤_{P} , T ⟩ where T = {c_{p}: p | p ∈ P }, i.e., for each element of the partial order, we define a constant of that type. Note that Σatom_{P} assigns atomic types to all constants. We are now ready to establish the converse to Corollary 3.3.

Lemma 4.3 The satisfiability problem for restricted systems of subtype inequalities over a poset P is polynomial time reducible to the typability problem over the atomic signature Σatom_{P}, i.e., P -SSI_{restr} ≤_{m} Σatom_{P} -TIS.

The reduction and the proof of its correctness appear in the Appendix.

Corollary 4.4 The satisfiability problem for restricted system of inequalities is polynomial time reducible to the problem of deciding whether a given term is typable over a given signature in which all constants have atomic types, i.e., SSI_{restr} ≤_{m} TIS_{atom} .

Corollary 4.5 There exists a signature Σ which maps constants to atomic types such that Σ-TIS_{atom} is pspace-hard. Hence, the problem TIS_{atom} is also pspace-hard.

Proof By results in [Tiu92], there exists a poset P for which P -SSI_{restr} is pspace-hard. Lemma 4.3 translates this result to TIS_{atom} .

4.2 SSI reduced to TIS

We now generalize the reduction described in Section 4.1 to show how satisfiability of a set of arbitrary inequalities can be simulated by typability of a term. To simulate inequalities that are not necessarily of a restricted form, we no longer have the requirement that the signature give only atomic types to constants.

Let P = ⟨P, ≤_{P} ⟩ be any poset. We define the signature Σ_{P} = ⟨P, ≤_{P} , T ⟩ where T = {⟨c_{p}^{l}, p → p⟩ | p ∈ P } ∪ {⟨c_{p}^{u}, p⟩ | p ∈ P }. Note that the signature Σ_{P} is not atomic. The following lemma generalizes the reduction of P -SSI_{restr} to Σatom_{P} -TIS and shows how arbitrary inequalities can be simulated by terms in the signature Σ_{P} using the constants c_{p}^{l} ’s of functional type.

Lemma 4.6

(i) The satisfiability problem for subtype inequalities over a poset P is polynomial time reducible to the typability problem over a signature Σ_{P}, i.e., P -SSI ≤_{m} Σ_{P} - TIS.

(ii) The satisfiability of subtype inequalities problem is polynomial time reducible to the typability problem, i.e., SSI ≤_{m} TIS.

Proof

(i) For any type σ over P , we define a term M_{σ} and a context C_{σ} [ ] with one hole simultaneously by induction σ. Intuitively, M_{σ} is defined so that σ is a subtype of any type of M_{σ}, and C_{σ} [ ] is defined so that for any term N, a typing of C_{σ} [N] constrains the type of N to be a subtype of σ. If σ is a type over variable set V = {t_{1}, …, t_{n}} then M_{σ} and C_{σ} [ ] have free variables u_{1}, v_{1}, …, u_{n}, v_{n}.

• M_{t_{i}} = v_{i} u_{i} C_{t_{i}} [ ] = v_{i} [ ]

• M_{p} = c_{p}^{u} C_{p} [ ] = c_{p}^{l} [ ]

• M_{σ → τ} = λx. K M_{τ} C_{σ} [x] C_{σ → τ} [ ] = C_{τ} [ [ ] M_{σ}]

where K is the combinator (λx. (λy. x)). Given an arbitrary inequality σ_{1} ≤ σ_{2} , we can now define the term [σ_{1} ≤ σ_{2}] as follows:

[σ_{1} ≤ σ_{2}] = C_{σ_{2}} [M_{σ_{1}}]

As in lemma 4.3, for any system I of inequalities, we produce the following term

M = λu_{1} … λu_{n}.

(λv_{1} … λv_{n}. (λx. [i_{1}])((λx. [i_{2}])(⋯ ((λx. [i_{m−1}])[i_{m}]) ⋯))

) \underbrace{(λx. x) ⋯ (λx. x)}_{n times}

where I = {i_{1}, …, i_{m}}

(ii) The signature Σ_{P} can be produced from the partial order P in polynomial time.

From Corollaries 3.2, 3.3, 4.4, and Lemma 4.6, we have the following theorem.

Theorem 4.7

(i) The satisfiability problem for restricted system of subtype inequalities (SSI_{restr} ) and the typability problem over a signature in which all constants have atomic types (TIS_{atom} ) are polynomial time equivalent.

(ii) The satisfiability of subtype inequalities (SSI) and the typability problems (TIS) are polynomial time equivalent.

5 Most General Typings

In this section we investigate a general theory of instances and most-general typing judgements for the type system ST_{⪯}. While the typability problems we considered before were with respect to the given fixed subtype ordering on base types, we will now study most general tyings for typing judgements with additional subtype assumptions. One reason for allowing additional subtype hypotheses is that, in general, this is the only way to obtain most general types. A second justification is that from the most general typing for an expression which includes additional subtype assumptions, it is possible to decide whether the expression is typable with respect to any fixed subtype ordering.

Intuitively, a most general typing judgement for a term is one which characterizes all possible typings for it. In more detail, if C, Γ▷M: σ is a most general typing for M, then all other derivable typings C′, Γ′ ▷ M: σ′ can be obtained from it. The precise manner in which C′, Γ′ ▷ M: σ′ is obtained from the most general typing C, Γ ▷ M: σ is via a definition of instance, a binary relation on typing judgements. Then a most general typing for a term M is a derivable typing judgement such that all other derivable typings for M are instances of it. Thus, most general typings are crucially related to the notion of instance that one uses. In [Mit91b], the following definition of instance is given:

Definition 5.1 A typing statement C′, Γ′ ▷ M: σ′ is an instance of C, Γ ▷ M: σ if there exists a substitution S such that:

(i) C′ ⊢ S C,

(ii) σ′ = S σ,

(iii) ∀x ∈ Dom(Γ), Γ′(x) = S Γ(x).

[Mit91b] also gives an algorithm GA which infers a most general typing for any term with respect to the stated definition of instance. Unfortunately, the size of the coercion set in the most general typing produced by GA can become exponential in the size of the term. Since an important aspect of any type-inference algorithm is the size and readability of its output, there has been previous work on optimizing the type inference algorithm to produce the shortest most general typings [FM89, FM90]. However, there is an intrinsic limit to the shortest most general typings that can be produced if we adhere to Definition 5.1 of instance. To give a relatively simple example, there are typings for terms which cannot be instances of any typing with empty coercion set.

Example 5.2 Let M = λf. λx. λy. K (f x) (f y). Using type s for x and type t for y, a derivable typing for M is:

{s ⪯ u, t ⪯ u, v ⪯ w}, ϕ ▷ M: (u → v) → s → t → w (1)

A typing for the term M with empty coercion set is:

ϕ, ϕ ▷ M: (s → t) → s → s → t  (2)

However, the typing (2) with empty coercion set cannot have the typing (1) as an instance, using Definition 5.1. For, there can be no substitution S such that Sσ = σ′, where σ = (s → t) → s → s → t and σ′ = (u → v) → s → t → w.

Since the problem in Example 5.2 arises from the definition of instance that one has chosen, a natural object of interest is an alternative formulation of the notion of instance which would permit most general typings with succinct set of subtype assumptions. It would be particularly good, if for example, one can obtain most general typings in which the subtype assumption set is always empty. The following more general definition of instance allows the typing (1) to be an instance of (2), and thus allows a most general typing of M from Example 5.2 with an empty coercion set.

Definition 5.3 A typing statement C′, Γ′ ▷ M: σ′ is an instance of C, Γ ▷ M: σ if there exists a substitution S such that:

(i) C′ ⊢ S C,

(ii) C′ ⊢ S σ ⪯ σ′,

(iii) ∀x ∈ Dom(Γ), C′ ⊢ Γ′(x) ⪯ S Γ(x).

We can see that the typing (2) has (1) as an instance, by Definition 5.3, using the the substitution S defined by S(s) = u and S(t) = v. Unfortunately, even this more powerful notion of instance does not allow typings with empty coercion sets to be more general than all other derivable typings for arbitrary terms.

Example 5.4 Take M = f(f x). Consider any derivable typing for M, ϕ, Γ ▷ M: σ, with empty coercion set. Then we must have Γ(x) = σ, Γ(f) = σ → σ. We can see that this typing with empty coercion set cannot have the following typing for M as an instance.

{s ⪯ t, u ⪯ v, u ⪯ t}, {f: t → u, x: s} ▷ f(f x): v

For consider any substitution S. By condition (ii) of Definition 5.3, we must have C′ ⊢ S(σ) ⪯ v, where C′ = {s ⪯ t, u ⪯ v, u ⪯ t}. By inspection of C′, this implies that S(σ) = u or S(σ) = v. In either case, we cannot satisfy condition (iii) for the variable x, since C′ ⊬ s ⪯ u and C′ ⊬ s ⪯ v.

Investigation of other plausible notions of instance by the authors also failed to allow typings with empty coercion sets to be most general. It was therefore a natural question whether there could be any definition of instance that would permit such elegant most general typings. In this section, we show that this is impossible. The main result of this section is that there is no suitable definition of instance for which there is a bound on the size of the coercion set in most general typings of terms. Thus we need to allow arbitrarily many subtype assumptions in giving the most general types of terms, in general.

We begin with a formalization of the properties of any suitable definition of instance. An instance relation , ≻, is a binary relation on typing judgements. Intuitively, C, Γ ▷ M: σ ≻ C, Γ′ ▷ M: σ′ means that the typing judgement C, Γ ▷ M: σ is more general than C′, Γ′ ▷ M: σ′. A definition of instance usually does not depend on the term M appearing in the judgements. Further, a basic property that one requires of any definition of instance, is the closure of derivability under instantiation. These two properties are captured in the following definition. Since all the properties in this section are proved for pure λ-terms, i.e., without any term constants, we omit mentioning any signature in the following definition and the rest of this section.

Definition 5.5 Let ≻ be a definition of instance on typing judgements. Then ≻ is a sound definition of instance if:

(i) C, Γ ▷ M: σ ≻ C′, Γ′ ▷ M: σ′ iff C, Γ ▷ N: σ ≻ C′, Γ′ ▷ N: σ′, for all terms N.

(ii) If C, Γ ▷ M: σ ≻ C′, Γ′ ▷ M: σ′ and ⊢_{ST_{⪯}} C, Γ ▷ M: σ then ⊢_{ST_{⪯}} C′, Γ′ ▷ M: σ′.

Given a definition of instance, ≻, a typing judgement C, Γ▷ M: σ is a most general typing for term M if

• The typing judgement C, Γ ▷ M: σ is derivable.

• For all derivable typing judgements C, Γ′ ▷ M: σ′, we have C, Γ ▷ M: σ ≻ C, Γ′ ▷ M: σ′.

We can now show that the term f(f x) cannot have a most general typing, under any sound definition of instance, in which the coercion set is empty. This is a special case of a more general theorem that we will prove later, but its proof is illustrative in understanding the proof of the more general theorem.

Lemma 5.6 Let M = f(f x) and ≻ be any sound definition of instance. Then M does not have a most general typing in which the coercion set is empty.

Proof Consider any derivable typing ϕ, Γ▷M: σ with empty coercion set. Then we must have x: σ, f: σ → σ ∈ Γ. We will show that ϕ, Γ ▷ M: σ cannot be a most general typing for M.

Let C′ = {s ⪯ t, u ⪯ t, u ⪯ v}, Γ′ = {x: s, f: t → u}, σ′ = v. Clearly, ⊢_{ST_{⪯}} C′, Γ′ ▷ M: σ′. Consider the term N = x. Since x: σ ∈ Γ, we have ⊢_{ST_{⪯}} ϕ, Γ ▷ N: σ. But since C′ ⊬ s ⪯ v, we have ⊬_{ST_{⪯}} C′, Γ′ ▷ N: σ′. By property (ii) of a sound definition of instance,

ϕ, Γ ▷ N: σ ⊁ C′, Γ′ ▷ N: σ′

Hence, by property (i) of a sound definition of instance,

ϕ, Γ ▷ M: σ ⊁ C′, Γ′ ▷ M: σ′

We will now generalize Lemma 5.6 to show that no bound on the size of the coercion set will suffice to express most general typings of all terms. For any atomic coercion set C and set of type variables T , define the coercion set C_{↾T} to be the set

{s ⪯ t ∈ C | s ∈ T or t ∈ T }

We say that an atomic coercion set C is closed if for any non-trivial atomic subtyping assertion, s ⪯ t with s ≠ t, C ⊢ s ⪯ t iff s ⪯ t ∈ C. For any atomic coercion set C, define its closure as the atomic coercion set defined by

Clos(C) = {s ⪯ t | s ≠ t, C ⊢ s ⪯ t}

We use F T V (C) to denote the type variables appearing in the coercion set C, and use F T V (σ), F T V (Γ) for a type σ and context Γ, similarly. We now state without proofs some technical lemmas involving free type variables in coercion sets which will be useful in the proof of our main theorem.

Lemma 5.7 For any atomic coercion set C,

(i) Clos(C) is closed.

(ii) F T V (Clos(C)) ⊆ F T V (C).

Lemma 5.8 Let C be an atomic coercion set.

(i) If C ⊢ σ ⪯ τ then Clos(C) ⊢ σ ⪯ τ.

(ii) If ⊢_{ST_{⪯}} C, Γ ▷ M: σ then ⊢_{ST_{⪯}} Clos(C), Γ ▷ M: σ.

Lemma 5.9 Suppose C is a closed atomic coercion set.

(i) If C ⊢ σ ⪯ τ and F T V (σ) ⊆ T or F T V (τ) ⊆ T then C_{↾T} ⊢ σ ⪯ τ.

(ii) If ⊢_{ST_{⪯}} C, Γ▷M: σ and M has no λ-abstractions then ⊢_{⪯} C_{↾F T V (Γ)}, Γ ▷ M: σ.

We are now ready to show that we cannot bound the size of the coercion set of most general typings. As in Lemma 5.6, we will use terms of the form f(f x) in proving our result. More precisely, we show that the term

M = z f_{1}(f_{1} x_{1}) ⋯ f_{k+1}(f_{k+1} x_{k+1})

cannot have a most general typing which uses at most k subtype assumptions. Roughly, the argument is as follows. If there are no subtype assumptions involving the types in one of the subterms f_{i}(f_{i} x_{i}) then this subterm has been typed using an empty coercion set and hence by an argument similar to Lemma 5.6, this typing cannot be most general. Otherwise, a typing which uses at most k subtype assumptions must relate the types used in two subterms f_{i}(f_{i} x_{i}) and f_{j}(f_{j} x_{j}). Since this is a constraint that does not have to be enforced in typing M, such a typing must not be more general than a typing in which the type assumptions used in typing the subterms f_{i}(f_{i} x_{i}) and f_{j}(f_{j} x_{j}) are completely unrelated. All this is made more precise, using Lemmas 5.7, 5.8, 5.9, in the proof of the following theorem which is given in the Appendix.

Theorem 5.10 Let ≻ be any sound definition of instance. For every k there is a term M_{k} with |M_{k}| = O(k) such that the most general typing of M_{k} requires a coercion set with at least k + 1 elements, i.e., the size of the coercion set grows at least linearly in the size of the term.

6 Conclusion

This paper contains two results on type inference with subtyping. The first shows that typability of a term in the presence of a fixed subtype ordering is equivalent to satisfiability of subtype inequalities over the same subtype ordering. A natural special case of typability arises when all program constants only have atomic types. This special case is equivalent to satisfiability of a certain restricted form of subtype inequalities. Since this restricted satisfiability problem has been shown previously to be pspace-hard, our equivalence gives a pspace lower bound on the algorithmic problem of typability with either general or atomic types. The second main result is concerned with most general typings, which are the typical output of a type-inference algorithm. Instead of working with a particular notion of instance, we have given a general lower bound that is independent of the notion of instance one may chose. Our lower bound is that for any sound notion of instance, the number of subtype assumptions in the most general typing grows linearly in the length of the term.

One important investigation is a precise characterization of the structural complexity of the problem of typability. The equivalences shown here demonstrate the importance of the problem of subtype inequality satisfaction and the importance of inequalities of the restricted form. One open problem is to find the complexity-theoretic relationship between satisfiability with arbitrary subtype inequalities and satisfiability with inequalities of the restricted form. Another problem is to give matching upper bounds and lower bounds for each problem.

The lower bounds in this paper suggest the importance of finding more tractable subproblems. This would have important consequences for programming language design. Both the algorithmic complexity of typability and the lack of succinct most general typings appear to arise due to particular partial orders that may not arise in practice. It is therefore important to identify classes of subtype orderings that lead to reasonably flexible programming languages and, at the same time, yield tractable type inference problems.

References

[ASU86] A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: principles, techniques, tools. Addison-Wesley, 1986.

[Ben94] M. Benke. Efficient type reconstruction in the presence of inheritance. Manuscript, 1994.

[FM89] Y. Fuh and P. Mishra. Polymorphic subtype inference: closing the theory-practice gap. In Proc. Theory and Practice of Software Development, pages 167–184, March 1989.

[FM90] Y. Fuh and P. Mishra. Type inference with subtypes. Theor. Computer Science, 73, 1990.

[GMW79] M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Springer LNCS 78, Berlin, 1979.

[H^{+} 92] P. Hudak et al. Report on the programming language Haskell. SIGPLAN Notices, 27(5):Section R, 1992.

[HF92] P. Hudak and J. Fasel. A gentle introduction to Haskell. SIGPLAN Notices, 27(5):Section T, 1992.

[LM92] P.D. Lincoln and J.C. Mitchell. Algorithmic aspects of type inference with subtypes. In Proc. 19th ACM Symp. on Principles of Programming Languages, pages 293–304, January 1992.

[Mil85] R. Milner. The Standard ML core language. Polymorphism, 2(2), 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.

[Mit84] J.C. Mitchell. Coercion and type inference (summary). In Proc. 11th ACM Symp. on Principles of Programming Languages, pages 175–185, January 1984.

[Mit91a] J.C. Mitchell. A simple reduction of unification to typa-

         bility. Message to types@theory.lcs.mit.edu,

June 28 1991.

[Mit91b] J.C. Mitchell. Type inference with simple subtypes. J. Functional Programming, 1(3):245–286, 1991.

[PT91] V. Pratt and J. Tiuryn. Satisfiability of inequations in a poset. Manuscript, October 1991.

[Tiu91] J. Tiuryn. Solving term inequalities is pspacehard. Manuscript, October 1991.

[Tiu92] J. Tiuryn. Subtype inequalities. In Proc. IEEE Symp. on Logic in Computer Science, pages 308– 315, 1992.

[Tur85] D.A. Turner. Miranda: a non-strict functional language with polymorphic types. In IFIP Int’l Conf. on Functional Programming and Computer Architecture, Nancy, Berlin, 1985. Springer LNCS 201.

[Tys88] J. Tyszkiewicz. Complexity of type inference in finitely typed lambda calculus. Master’s thesis, University of Warsaw, 1988.

[Wan87] M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, 10:115–122, 1987.

[WO89] M. Wand and P. O’Keefe. On the complexity of type inference with coercion. In Proc. ACM Conf. Functional Programming and Computer Architecture, pages 293–298, 1989.

A Appendix

Proof of Lemma 4.3 Suppose P = ⟨P, ≤_{P} ⟩. Let I be a restricted system of inequalities over P, with type variables from a finite set V = {t_{1}, …, t_{n}}. For any inequality i ∈ I, we will define a term [i] over Σatom_{P} with free variables u_{1}, v_{1}, …, u_{n}, v_{n}. In defining the terms [i], the variables v_{i} should be understood as having function types σ_{i} → τ_{i} with σ_{i} serving as a lower bound on any satisfying substitution for the type variable t_{i}, and τ_{i} serving as an upper bound. Thus, the application of v_{i} to u_{i} yields a term whose type has to be a supertype of the substitution for t_{i}, while the application of v_{i} to a term N, forces the type of N to be a subtype of the substitution of t_{i}. Using these two ideas, the terms [i] are then so defined as to enforce the subtype relations implied by the inequality i.

\begin{aligned}[p ≤ t_{i}] & = & v_{i} c_{p} \\ [t_{i} ≤ t_{j}] & = & v_{j} (v_{i} u_{i}) \\ [t_{i} ≤ t_{j} → t_{k}] & = & v_{k} ((v_{i} u_{i}) (v_{j} u_{j})) \\ [t_{j} → t_{k} ≤ t_{i}] & = & v_{i} (λx. K(v_{k} u_{k}) (v_{j} x)) \end{aligned}

where K is the combinator (λx. (λy. x)). Finally, we produce the following term

M = λu_{1} … λu_{n}.

(λv_{1} … λv_{n}.

(λx. [i_{1}])((λx. [i_{2}])(⋯ ((λx. [i_{m−1}])[i_{m}]) ⋯))

) \underbrace{(λx. x) ⋯ (λx. x)}_{n times}

Abstracting the variables v_{i} and applying to the identity functions λx. x forces each variable v_{i} to be of the desired function type that was assumed in the construction of the terms [i].

We now prove that M is typable iff I is satisfiable. If I is satisfiable by substitution φ_{I}, it can be easily seen that M can be typed by using type φ_{I}(t_{j}) for u_{j} and φ_{I}(t_{j}) → φ_{I}(t_{j}) for v_{j}.

For the converse, assume that M is typable. By our previous comments, consider a derivation D of M in which all type occurrences are ground types and in which (subtp) is used only after (var) and (const).

Note that if ⊢_{ST_{⪯}} Γ ▷ λx. x: τ then τ = τ_{l} → τ_{r} where τ_{l} ⪯_{P} τ_{r}. By the following derivation fragment in which there are no (subtp) occurrences after (app) or (abs)

⋯, v: τ ▷ ( ): σ
⋯ ▷ λv. ( ): τ → σ  ⋯ ▷ λx. x: τ
⋯ ▷ (λv. ( ))(λx. x): σ

it follows by constructing D backwards that D must have a line of the form

Γ_{uv} ▷ (λx. [i_{1}])((λx. [i_{2}]) ⋯): σ

where Γ_{uv} = {u_{1}: ρ_{1}, …, u_{n}: ρ_{n}, v_{1}: σ_{1} → τ_{1}, …, v_{n}: σ_{n} → τ_{n}} for some types ρ_{1}, …, ρ_{n}, σ_{1}, …, σ_{n}, τ_{1}, …, τ_{n} with σ_{i} ⪯_{P} τ_{i} and σ_{i}, τ_{i} ∈ T_{P} . Take φ to be any substitution with σ_{i} ⪯_{P} φ(x_{i}) ⪯_{P} τ_{i}, such a φ exists since σ_{i}, τ_{i} ∈ T_{P} . We prove that φ is a satisfying substitution for I. By constructing D backwards we also see that Γ_{uv} ▷ [i_{l}]: σ′_{l} for some σ′_{l}. We prove that φ as defined above will then satisfy i_{l}. We only show two representative cases:

Case i_{l} ≡ t_{i} ≤ t_{j} → t_{k}: Then [i_{l}] = (v_{k} ((v_{i} u_{i}) (v_{j} u_{j}))). Since Γ_{uv} ▷ [i_{l}]: σ′_{l}, we must have occurring in D

Γ_{uv} ▷ v_{k}: δ_{2} → σ′_{l}  (3)
Γ_{uv} ▷ ((v_{i} u_{i})(v_{j} u_{j})): δ_{2}  (4)

from (4) we must have that

Γ_{uv} ▷ (v_{i} u_{i}): δ_{1} → δ_{2}  (5)
Γ_{uv} ▷ (v_{j} u_{j}): δ_{1}  (6)

By Lemma 4.2, τ_{i} ⪯_{P} δ_{1} → δ_{2} , τ_{j} ⪯_{P} δ_{1} . Thus τ_{i} = s_{i} → w_{i} and δ_{1} ⪯_{P} s_{i} and w_{i} ⪯_{P} δ_{2} . Since Γ(v_{k}) = σ_{k} → τ_{k} it follows that σ_{k} → τ_{k} ⪯_{P} δ_{2} → σ′_{l}, i.e., δ_{2} ⪯_{P} σ_{k}. Thus τ_{i} = s_{i} → w_{i} with τ_{j} ⪯_{P} s_{i} and w_{i} ⪯_{P} σ_{k}, i.e., φ(t_{i}) ⪯_{P} τ_{i} ⪯_{P} τ_{j} → σ_{k} ⪯_{P} φ(t_{j}) → φ(t_{k}). Hence, φ(t_{i}) ⪯_{P} φ(t_{j} → t_{k}).

Case i_{l} ≡ t_{j} → t_{k} ≤ t_{i}: Then [i_{l}] = v_{i}N, where N = (λx. K(v_{k} u_{k}) (v_{j} x)). Then we must have occurring in D

Γ_{uv}, x: σ_{x} ▷ v_{k} u_{k}: δ_{1}  (7)
Γ_{uv}, x: σ_{x} ▷ v_{j} x: δ_{2}  (8)
Γ_{uv} ▷ N: σ_{x} → δ_{3}  (9)

where δ_{1} ⪯_{P} δ_{3} , since if ⊢_{ST_{⪯}} Γ ▷ K: τ then τ = τ_{l} → τ′_{l} → τ_{r} with τ_{l} ⪯_{P} τ_{r}. By Lemma 4.2, from (8) we get that σ_{x} ⪯_{P} σ_{j} and from (7) we get that τ_{k} ⪯_{P} δ_{1} . Then by similar reasoning as before since ⊢_{ST_{⪯}} Γ_{uv} ▷ v_{i}N: ⋯ we get that σ_{x} → δ_{3} ⪯_{P} σ_{i}, i.e.,

φ(t_{j} → t_{k}) = φ(t_{j}) → φ(t_{j})
⪯_{P} σ_{j} → τ_{k}
⪯_{P} σ_{x} → δ_{1}
⪯_{P} σ_{x} → δ_{3}
⪯_{P} σ_{i}
⪯_{P} φ(t_{i})

Proof of Theorem 5.10 Consider any k ≥ 0. Take

M = z f_{1}(f_{1} x_{1}) ⋯ f_{k+1}(f_{k+1} x_{k+1})

We will prove that M cannot have a most general typing whose coercion set has at most k elements. Consider any provable typing C, Γ ▷ M: σ with |C| ≤ k. We will exhibit a provable typing C′, Γ′ ▷ M: σ′ such that C, Γ ▷ M: σ ⊁ C′, Γ′ ▷ M: σ′.

Let ρ_{i} and ρ′_{i} be the typing assumptions for x_{i} and f_{i} respectively, in Γ, i.e., let ρ_{i} = Γ(x_{i}), ρ′_{i} = Γ(f_{i}) for i = 1, …, k + 1. Then, define

\begin{aligned}Γ_{i} & = & \{x_{i}: ρ_{i}, f_{i}: ρ′_{i}\}, & i = 1, …, k + 1 \\ S_{i} & = & F T V (C) ∩ F T V (Γ_{i}), & i = 1, …, k + 1 \end{aligned}

Case I: For some j, 1 ≤ j ≤ k + 1, S_{j} = ϕ. Take

C′ = ⋃_{1≤i≤k+1}{s_{i} ⪯ t_{i}, u_{i} ⪯ t_{i}, u_{i} ⪯ v_{i}}
Γ′ = {z: v_{1} → v_{2} → ⋯ → v_{k+1} → w} ∪

⋃_{1≤i≤k+1}{x_{i}: s_{i}, f_{i}: t_{i} → u_{i}}

σ′ = w

Since ⊢_{ST_{⪯}} C, Γ▷M: σ and C is atomic, using Lemma 2.2 there is a proof D as in Table 1. Suppose that S_{j} = ϕ. From the proof D, we have that ⊢_{ST_{⪯}} C, Γ ▷ f_{j}(f_{j} x_{j}): σ_{j}. Using Lemma 2.1, we have that ⊢_{ST_{⪯}} C, Γ_{j}▷f_{j}(f_{j} x_{j}): σ_{j}. By Lemma 5.8(ii), ⊢_{ST_{⪯}} Clos(C), Γ_{j} ▷f_{j}(f_{j} x_{j}): σ_{j}. By Lemma 5.7(i) and Lemma 5.9(ii),

⊢_{ST_{⪯}} Clos(C)_{↾F T V (Γ_{j})}, Γ_{j} ▷ f_{j}(f_{j} x_{j}): σ_{j}.

Now

Clos(C)_{↾F T V (Γ_{j})} = Clos(C)_{↾F T V (Γ_{j})∩F T V (Clos(C))}

By Lemma 5.7(ii),

F T V (Γ_{j}) ∩ F T V (Clos(C)) = ϕ.

Hence,

Clos(C)_{↾F T V (Γ_{j})} = ϕ.

Thus,

⊢_{ST_{⪯}} ϕ, Γ_{j} ▷ f_{j}(f_{j} x_{j}): σ_{j}

Hence, it must be that

ρ_{j} = σ_{j}, ρ′_{j} = σ_{j} → σ_{j}  (10)

Consider the term

N = z (f_{1}(f_{1} x_{1})) ⋯
(f_{j−1}(f_{j−1} x_{j−1})) x_{j} ⋯
(f_{k+1}(f_{k+1} x_{k+1}))

From (10), we know that ⊢_{ST_{⪯}} C, Γ ▷ x_{j}: σ_{j}. Plugging this proof instead of C, Γ ▷ f_{j}(f_{j} x_{j}): σ_{j} in the derivation D, we get that ⊢_{ST_{⪯}} C, Γ ▷ N: σ. But, we cannot have that ⊢_{ST_{⪯}} C′, Γ′ ▷ N: σ′ since C′ ⊬ s_{j} ⪯ v_{j} and thus N is not typable under assumptions C′, Γ′. Thus, ⊬_{ST_{⪯}} C′, Γ′ ▷ N: σ′. Since ≻ is sound,

\begin{aligned}& C, Γ ▷ N: σ ⊁ C′, Γ′ ▷ N: σ′ \\ ⇒ & C, Γ ▷ M: σ ⊁ C′, Γ′ ▷ M: σ′ \end{aligned}

Case II: S_{j} ≠ ϕ, for j = 1, …, k + 1. Consider

C′ = ϕ
Γ′ = {z: p_{1} → p_{2} → ⋯ → p_{k+1} → w} ∪

⋃_{1≤i≤k+1}{x_{i}: p_{i}, f_{i}: p_{i} → p_{i}}

σ′ = w

Consider the sets C_{↾S_{1}}, …, C_{↾S_{k+1}} . Then they cannot all be pairwise disjoint. For, if they were, we have

|C_{↾S_{1}} ∪ ⋯ ∪ C_{↾S_{k+1}}| = |C_{↾S_{1}}| + ⋯ + |C_{↾S_{k+1}}|
≥ 1 + ⋯ + 1  (S_{i} ≠ ϕ)
= k + 1

But, C_{↾S_{1}} ∪ ⋯ ∪ C_{↾S_{k+1}} ⊆ C, |C| ≤ k. Hence, there exist i, j such that C_{↾S_{i}} ∩ C_{↾S_{j}} ≠ ϕ, i ≠ j.

Claim A.1 There exist type variables s_{i}, s_{j}, u such that s_{i} ∈ F T V (Γ_{i}), s_{j} ∈ F T V (Γ_{j}) and C ⊢ s_{i} ⪯ u, C ⊢ s_{j} ⪯ u.

Proof Since C_{↾S_{i}} ∩C_{↾S_{j}} ≠ ϕ, let s ⪯ t ∈ C_{↾S_{i}} ∩C_{↾S_{j}} . Then s or t is in S_{i} and s or t is in S_{j}.

• s ∈ S_{i}, t ∈ S_{j}. Take s_{i} = s, s_{j} = t, u = t.

• t ∈ S_{i}, s ∈ S_{j}. Take s_{i} = t, s_{j} = s, u = t.

• s ∈ S_{i}, s ∈ S_{j}. Take s_{i} = s_{j} = u = s.

• t ∈ S_{i}, t ∈ S_{j}. Take s_{i} = s_{j} = u = t.

Let ρ_{l} = α_{l}, ρ′_{l} = β_{l} → γ_{l} for l = i, j. For δ_{l} = α_{l}, β_{l}, or γ_{l}, define a term F (δ_{l}) as follows:

\begin{aligned}F (α_{l}) & = & EQ x_{l} y_{l} \\ F (β_{l}) & = & f_{l} y_{l} \\ F (γ_{l}) & = & EQ (f_{l} x_{l}) y_{l} \end{aligned}

⋮  ⋮  ⋮
C, Γ ▷ z: ρ_{z}  C, Γ ▷ f_{1}(f_{1} x_{1}): σ_{1}  ⋮  ⋮
C, Γ ▷ z (f_{1}(f_{1} x_{1})): ⋯  C, Γ ▷ f_{2}(f_{2} f_{2}): σ_{2}  ⋮
...  ⋮
...  ⋮

C, Γ ▷ f_{k+1}(f_{k+1} x_{k+1}): σ_{k+1}

C, Γ ▷ M: σ

Table 1: Derivation D of Theorem 5.10

The term EQ is defined as

EQ = λx. λy. λw. K w (λz. λw. w (z x) (z y))

which ensures that EQ M N is typable iff M and N can be given the same type. Then we can make the following observations:

(i) ⊢_{ST_{⪯}} C, Γ∪{y_{l}: δ_{l}}▷F (δ_{l}): τ for some type τ, i.e., F (δ_{l}) is typable under the assumptions C, Γ ∪ {y_{l}: δ_{l}}.

(ii) Suppose that ⊢_{ST_{⪯}} C′, Γ′′▷F (δ_{l}): τ and Γ′′ ⊃ Γ′. Then Γ′′(y_{l}) = p_{l}.

Case IIa: One of α_{i}, α_{j}, β_{i}, β_{j}, γ_{i}, γ_{j} is not a type variable. Then let δ_{l} be the one that is not. Consider the term

N = K M (λy_{l}. λw. w F (δ_{l}) (λz. (y_{l} z)))

From Observations (i) and (ii), we get that

⊢_{ST_{⪯}} C, Γ ▷ N: σ and ⊬_{ST_{⪯}} C′, Γ′ ▷ N: σ′

Case IIb: All of α_{l}, β_{l}, γ_{l} are type variables. By Claim A.1, we have variables s_{i}, s_{j}, u satisfying the required properties. We also know that s_{l} = α_{l}, β_{l} or γ_{l} for l = i or j and

⊢_{ST_{⪯}} C, Γ ∪ {y_{i}: s_{i}, y_{j}: s_{j}} ▷ EQ y_{i} y_{j}: τ

From Observations (i) and (ii), taking

N = K M (λy_{i}. λy_{j}. λw. w F (s_{i}) F (s_{j}) (EQ y_{i} y_{j}))

we have that

⊢_{ST_{⪯}} C, Γ ▷ N: σ but ⊬_{ST_{⪯}} C′, Γ′ ▷ N: σ′

Hence, in either case

C, Γ ▷ M: σ ⊁ C′, Γ′ ▷ M: σ′

Taking the term M_{k} = z f_{1}(f_{1} x_{1}) ⋯ f_{k+1}(f_{k+1} x_{k+1}), we see that |M_{k}| = O(k).