TYPE INFERENCE AND PROGRAM EVALUATION

IN THE PRESENCE OF SUBTYPING

a dissertation

submitted to the department of computer science

and the committee on graduate studies

of stanford university

in partial fulfillment of the requirements

for the degree of doctor of philosophy

By My Khanh Hoang

July 1995

\begin{matrix}c \\ ◯ \end{matrix} Copyright 1995 by My Khanh Hoang All Rights Reserved

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

John C. Mitchell (Principal Adviser)

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Vaughan R. Pratt

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Patrick D. Lincoln

Approved for the University Committee on Graduate Studies:

Abstract

Many typed programming languages can be enhanced with subtyping, which is a relation between the types of the language. The distinguishing feature of subtyping is that if A is a subtype of B, then an expression of type A can be used anywhere that an expression of type B is required; the main advantage of subtyping is that it allows code reuse. This research focusses on two properties of programming languages with subtyping: type inference (that is, given any input term, find a most general typing) and symbolic evaluation. The formal framework for the investigation is lambda-calculus with subtyping.

Type inference is the problem of assigning types to expressions that do not contain complete type information. Our first main result is the characterization of the problem of determining whether a lambda term is typable in terms of a satisfiability problem over partial orders. We can then use this characterization to establish lower bounds on the time complexity of any type inference algorithm. Our second main result is a lower bound on the length of the output of any type inference algorithm. More specifically, most general typings grow at least linearly in the size of the input term.

The other aspect that we investigate is the design of reduction rules for evaluating lambda-terms in the presence of subtyping. A crucial property of any reduction system is confluence or the Church-Rosser property whose main consequence is that the final result of evaluating any term is determined uniquely independent of the choice of reductions made at each step. Without subtyping, lambda-terms can be evaluated using (β) and (η) reduction, which is well-known to be confluent. Surprisingly, (β) and (η) reduction fail to be confluent in the presence of subtyping. We construct an additional reduction rule (<: ), and prove the confluence of a reduction system consisting of (β), (η) and (<: ). Finally, we show that the rule (<: ) can be used to restore confluence in the presence of fixed-point reduction as well.

Contents

Abstract iv

1 Introduction 1

2 Preliminaries 4 2.1 Types and Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Satisfiability of Subtype Inequalities . . . . . . . . . . . . . . . . . . . 5 2.3 Simply-typed λ-calculus with subtyping:λ\overrightarrow{<:} . . . . . . . . . . . . . . 6 2.4 Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.5 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Typability 10 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Type Inference Reduced to Inequality Satisfaction . . . . . . . . . . . 12 3.3 Reducing Inequality Satisfaction to Typability . . . . . . . . . . . . . 14

3.3.1 SSI_{restr} reduced to TIS_{atom} . . . . . . . . . . . . . . . . . . . 14 3.3.2 SSI reduced to TIS . . . . . . . . . . . . . . . . . . . . . . . . 19

4 Most General Typings 22 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.2 Most General Typings . . . . . . . . . . . . . . . . . . . . . . . . . . 23

4.2.1 Instances . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2.2 A Theory of Most General Typings . . . . . . . . . . . . . . . 26 5 Confluence 36

5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.2 Failure of Confluence of β, η-reduction . . . . . . . . . . . . . . . . . 38 5.3 Reduction System for λ\overrightarrow{<:} . . . . . . . . . . . . . . . . . . . . . . . . 41

5.3.1 Intuitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.3.2 Formal Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

5.4 Confluence of Reduction System . . . . . . . . . . . . . . . . . . . . . 45

5.4.1 Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 5.5 Adding Recursion: λ_{<:}^{→,fix} . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.6 Reduction System for λ_{<:}^{→,fix} . . . . . . . . . . . . . . . . . . . . . . . 54 5.7 Labeled Fixed Points: λ_{<:}^{→,lab} . . . . . . . . . . . . . . . . . . . . . . . 55

5.7.1 Labeled Reduction System with Subtyping . . . . . . . . . . . 55 5.7.2 Fixed Points and Labeled Reduction: Going Back and Forth . 56

5.8 Confluence of Labeled Reduction . . . . . . . . . . . . . . . . . . . . 57 5.8.1 Type System for Untyped Terms . . . . . . . . . . . . . . . . 58 5.8.2 Type Erasure . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 5.8.3 Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

6 Conclusion 67

Bibliography 69

List of Tables

4.1 Derivation D of Theorem 4.2.10 . . . . . . . . . . . . . . . . . . . . 32

List of Figures

5.1 Proof of Theorem 5.4.10 . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.2 Proof of Theorem 5.8.7 . . . . . . . . . . . . . . . . . . . . . . . . . 66

Chapter 1

Introduction

A typed programming language is one in which a type is associated with every expression in the language by means of a set of type-checking rules that is called its type system. The basic property that the type system ensures is that programs that type-check never lead to run-time errors. Therefore, at least one advantage of a typed programming language is the early detection of errors at compile-time, thus making it easier to develop error-free programs. At the same time, it is important that the type system not place severe restrictions on the way one may program. A simple way of achieving flexible programming in a typed framework is through the notion of subtyping which is a relation between the types of the language. The defining characteristic of subtyping is that if A is a subtype of B, then expressions of type A can be used anywhere that an expression of type B is required. As an example, suppose f is a procedure of type real → int , i.e., it can be applied to arguments that are reals and returns integer results. Thus, f can be used on argument 3.6 since 3.6 is of type real . Since 3 is an integer, without subtyping f cannot be applied to 3. However, with subtyping, we can specify integers to be subtype of reals and we can use f on both 3.6 and 3. Thus, subtyping allows a procedure to be used on arguments of many different types, therefore supporting extensive code reuse. Subtyping is also an important and basic concept underlying typed object-oriented languages. This dissertation focuses on analyzing programming languages with subtyping. More precisely, it investigates issues related to type-checking and execution of programs , i.e., both static and dynamic aspects of the implementation of such languages. The formal framework for this investigation is the calculus λ\overrightarrow{<:} which is the extension of λ^{→} with subtyping. The calculus λ^{→} is the simply-typed lambda-calculus, an abstraction of a purely functional language with functional types.

A cumbersome aspect of typed programming languages is the necessity of annotating user programs with type declarations. This can be avoided if instead of just checking whether an input expression is type correct, the compiler can infer the necessary type declarations to make it so. This process of type-inference can be done efficiently in the absence of subtyping (e.g., for λ^{→}) and is practically available, for example, in the programming language ML. In Chapters 3 and 4, we investigate the implications of subtyping for the problem of type-inference.

In the presence of subtyping, there are several type inference problems depending on the form of the subtype partial order and whether the programmers can specify new subtype declarations in programs. In Chapter 3, we investigate the problem of checking whether an untyped λ-calculus expression admits any type declarations for its variables that would make it typable in λ\overrightarrow{<:}. Our fundamental result is that for any specific subtype partial order, this problem is algorithmically (polynomialtime) 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. From previous studies of this satisfiability problem, we can use the characterization to establish results on the algorithmic complexity of the typeinference problem. For example, since the satisfiability problem is pspace-hard over certain partial orders, this equivalence strengthens a previous lower bound of nphard to pspace-hard. On the other hand, since the satisfiability problem can be solved efficiently when the partial order is a lattice, we can get efficient algorithms for type-inference when the subtype partial order is restricted to be a lattice.

Typically, a practical type inference algorithm proceeds by producing the most general type of its input expression which characterizes all possible type declarations that would make the input expression type correct. Clearly, the length of the most general types of expressions places a lower bound on the complexity of any such type inference algorithm. In Chapter 4, we investigate the intrinsic length of most general typings when the subtype hierarchy may change as the result of additional subtype declarations within the program. More precisely, the property of a most general typing is that it has all other possible typings as instances. One of the novelties of our study is that instead of using a fixed notion of instance, we investigate most general typings even under arbitrarily powerful definitions of instance. With the programmers allowed to specify additional subtype declarations in programs, a typing for an expression consists of type declarations for the variable together with subtype declarations between types. We show that no sound definition of instance would allow the set of additional subtyping declarations in most general typings for a term to grow less than linearly in the size of the term. Since both the algorithmic complexity of typability of input expressions and the lack of succinct most general types from some forms of subtype orderings, this work suggests placing restrictions on subtypings in programs in practice.

Finally, in Chapter 5, we investigate some aspects of symbolic evaluation for languages with subtyping. One way to “interpret” programs is to design reduction rules that can be used to simplify subexpressions — the result of executing a program can then be found by repeatedly using these reduction rules on its subexpressions. An important property, called confluence, that such a reduction system needs to satisfy is that this strategy for executing a program is consistent, i.e., the result of executing a program is independent of the particular subexpression chosen to be simplified at each step. Surprisingly, the reduction system for λ^{→} consisting of (β), (η) reduction rules fails to be confluent in the presence of subtyping. We design a new reduction rule (<: ) for λ\overrightarrow{<:} and prove the confluence of the reduction system consisting of (<: ), (β), and (η). The proof of confluence relies on termination properties of all expressions of λ\overrightarrow{<:}. It is therefore not clear that the idea of adding the reduction rule (<: ) can be used to obtain confluence for languages that include non-terminating expressions. We therefore next investigate λ_{<:}^{→,fix} , a language with a mechanism for recursive definition of functions and subtyping and show that the addition of the rule (<: ) can be used to restore confluence for this language as well.

Preliminaries

We begin by defining the simply-typed λ-calculus with subtyping, λ\overrightarrow{<:}. This will help us define notation that will be used in subsequent chapters. We will also define the decision problems of typability and subtype inequality satisfiability, both of which are subjects of Chapter 3.

2.1 Types and Subtyping

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.

2.2 Satisfiability of Subtype Inequalities

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

2.3 Simply-typed λ-calculus with subtyping:λ\overrightarrow{<:}

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. Thus the typing judgement C, Γ ▷ M : σ denotes that M is a well-typed term with the declarations given by the context Γ and coercion set C. The following proof system is used to identify the set of valid typing judgements:

(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: τ ∈ Γ,
= Γ ∪ {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 Σ. 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 : σ. Also, we use the notation Γ(x) to denote the unique σ such that x: σ ∈ Γ.

2.4 Type Inference

Given the proof system of Section 2.3, the problem of type checking can be formalized as follows. Given a set of user type declarations Γ and a set of subtype declarations C for a program M specified to be of type σ, type-checking this would correspond to asking for whether the typing judgement C, Γ ▷ M : σ is provable in the proof system. We can consider a more restricted version where the user is not allowed to supply subtype declarations, i.e., where C is the empty set.

As described in the Chapter 1, type-inference corresponds to the problem of inferring whether there exist any type-declarations that would make a program well-typed, i.e., whereby the user does not need to supply type-declarations. We formalize this problem as follows. Since the terms M described in the formal system λ\overrightarrow{<:} specify type-declarations for λ-bound variables, we take, as input for the type inference problem, untyped λ-terms in which there are no declarations for λ-bound variables. Recall that the set of untyped lambda-terms are generated by following grammar:

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

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

The untyped λ-terms for which there exist some type annotations for their λbound variables such that they are well-typed terms of λ\overrightarrow{<:} can now be easily identified. Formally, we can consider a proof system which is exactly the same as ST_{<:} except that we omit type-annotations for λ-bound variables in the (abs) rule. We call this resulting proof system ST_{<:} as well, relying on context, to understand whether the term in the judgement is an untyped term or one with typing annotations. To be complete, we detail this proof system:

(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 ⊢ σ <: τ

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 : σ. We now formally define 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 Σ.

2.5 Background

We recall some useful properties of the type system outlined in Section 2.4, which will be used in subsequent chapters. The proofs of these properties can either be found in or are similar to that of [Mit91b].

The first property is that the validity of a typing judgement for an expression M only depends on the type assumptions about its free variables.

Lemma 2.5.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 : σ.

The following lemmas are direct consequences of restricting the assertions in the coercion set of typing judgements to be atomic. Define the matching relation on types as follows:

(i) if σ is a type variable or base type, then σ matches τ iff τ is a type variable or base type.

(ii) if σ = σ_{1} → σ_{2}, then σ matches τ iff τ = τ_{1} → τ_{2} and σ_{i} matches τ_{i}, (i = 1, 2).

Intuitively, matching formalizes the idea of having the same shape; the following lemma states that if C ⊢ σ <: τ then σ and τ have the same shape.

Lemma 2.5.2 If C ⊢ σ <: τ, where C is an atomic coercion set, then σ matches τ.

The following lemma asserts that the rule (→) for subtyping is invertible.

Lemma 2.5.3 Let σ and τ be types with σ = σ_{1} → σ_{2} and τ = τ_{1} → τ_{2}. Then C ⊢ σ <: τ iff C ⊢ τ_{1} <: σ_{1} and C ⊢ σ_{2} <: τ_{2}.

Finally, the following lemma states that one may normalize proofs in ST_{<:} for untyped λ-terms so that the only uses of (subtp) rule occur immediately after (var) and (const).

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

Typability

3.1 Introduction

In this chapter, we study 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.

The main result of this chapter 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 satisfiability problems over partial orders of this form have 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 chapter, 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.

Our equivalence clearly implies that the only way to devise a practical, polynomialtime 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 can obtain polynomial-time algorithm for type-inference using our equivalence.

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. When there are no subtype assumptions on base types, type-checking for simply-typed λ-calculus with subtyping reduces to that of simply-typed λ-calculus. Thus, we obtain the well known equivalence between type inference for simply-typed λ-calculus and unification [Tys88, Mit91a, Wan87] as a consequence of our results.

3.2 Type Inference Reduced to Inequality Satis-

faction

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 analogous 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].

From now on, 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.2.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.5.4 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.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.

Proof Given a signature Σ, the poset P_{Σ} can easily be produced in polynomial time.

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

3.3 Reducing Inequality Satisfaction to Typabil-

ity

In Section 3.2, 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.2, this shows the equivalence of the two problems TIS and SSI.

3.3.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 3.3.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 3.3.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.5.4 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.5.4.

Lemma 3.3.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.5.4

\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 Σ_{P}^{atom} = ⟨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 Σ_{P}^{atom} assigns atomic types to all constants. We are now ready to establish the converse to Corollary 3.2.3.

Lemma 3.3.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 Σ_{P}^{atom} , i.e., P -SSI_{restr} ≤_{m} Σ_{P}^{atom} -TIS.

Proof 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 Σ_{P}^{atom} 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}.

Case i_{l} ≡ p ≤ t_{i}: Then [i_{l}] = (v_{i} c_{p}).

Since Γ_{uv} ▷ [i_{l}] : σ′_{l}, we must have occurring in D

Γ_{uv} ▷ v_{i}: δ → σ′_{l}  (3.1)
Γ_{uv} ▷ c_{p}: δ
Since Γ_{uv}(v_{i}) = σ_{i} → τ_{i} and c_{p}: p ∈ T, from (3.1) it follows that
σ_{i} → τ_{i} <:_{P} δ → σ′_{l} and p <:_{P} δ.
Thus, we have φ(p) <:_{P} δ <:_{P} σ_{i} <:_{P} φ(t_{i}) <:_{P} τ_{i}, i.e., φ(p) <:_{P} φ(t_{i}).

Case i_{l} ≡ t_{i} ≤ t_{j}: Then [i_{l}] = (v_{j} (v_{i} u_{i})).

Then we must have occurring in D

Γ_{uv} ▷ v_{j}: δ → σ′_{l}
Γ_{uv} ▷ v_{i} u_{i}: δ  (3.2)

By Lemma 3.3.2, and (3.2), we have τ_{i} <:_{P} δ and since Γ_{uv}(v_{j}) = σ_{j} → τ_{j}, we have that σ_{j} → τ_{j} <:_{P} δ → σ′_{l}. Therefore, φ(t_{i}) <:_{P} τ_{i} <:_{P} δ <:_{P} σ_{j} <:_{P} φ(t_{j}).

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}

Γ_{uv} ▷ ((v_{i} u_{i})(v_{j} u_{j})) : δ_{2}  (3.3)

from (3.3) we must have that

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

By Lemma 3.3.2, τ_{i} <:_{P} δ_{1} → δ_{2}, τ_{j} <:_{P} δ_{1}. Thus τ_{i} = s_{i} → w_{i}, δ_{1} <:_{P} s_{i}, and w_{i} <:_{P} δ_{2}. Since Γ_{uv}(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}  (3.4)
Γ_{uv}, x: σ_{x} ▷ v_{j} x: δ_{2}  (3.5)
Γ_{uv} ▷ N : σ_{x} → δ_{3}

where δ_{1} <:_{P} δ_{3}, since if ⊢_{ST_{<:}} Γ ▷ K: τ then τ = τ_{l} → τ′_{l} → τ_{r} with τ_{l} <:_{P} τ_{r}. By Lemma 3.3.2, from (3.5) we get that σ_{x} <:_{P} σ_{j} and from (3.4) 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})

Corollary 3.3.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} .

Proof The signature Σ_{P}^{atom} can be produced from the partial order P in polynomial time, and Σ_{P}^{atom} has atomic types for all constants.

Corollary 3.3.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 pspacehard.

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

3.3.2 SSI reduced to TIS

We now generalize the reduction described in Section 3.3.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 Σ_{P}^{atom} -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 3.3.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 3.3.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.2, 3.2.3, 3.3.4, and Lemma 3.3.6, we have the following theorem.

Theorem 3.3.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.

Most General Typings

4.1 Introduction

In this chapter we investigate a general theory of instances and most-general typing judgements for the type system ST_{<:}. While we considered the decision problem of typability in the previous chapter, typically, a practical type inference algorithm prints 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. Thus, an efficient satisfiability algorithm for special partial orders 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 4.2 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.

Finally, we note that while the typability problems we considered in Chapter 3 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.

4.2 Most General Typings

4.2.1 Instances

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 4.2.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 4.2.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 4.2.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  (4.1)

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

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

However, the typing (4.2) with empty coercion set cannot have the typing (4.1) as an instance, using Definition 4.2.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 4.2.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 (4.1) to be an instance of (4.2), and thus allows a most general typing of M from Example 4.2.2 with an empty coercion set.

Definition 4.2.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 (4.2) has (4.1) as an instance, by Definition 4.2.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 4.2.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 4.2.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 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 Section 4.2.2, we show that this is impossible. The main result 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.

4.2.2 A Theory of Most General Typings

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 4.2.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 4.2.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 4.2.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. Lemmas 4.2.7, 4.2.8, 4.2.9 are technical lemmas involving free type variables in coercion sets which will be useful in the proof of our main theorem.

Lemma 4.2.7 For any atomic coercion set C,

(i) Clos(C) is closed.

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

Proof

(i) Assume that Clos(C) ⊢ s <: t. We will prove by induction on the proof of Clos(C) ⊢ s <: t that C ⊢ s <: t. Consider the last step in Clos(C) ⊢ s <: t.

Case (asmp): This means s <: t ∈ Clos(C), by the definition of Clos(C), we

have C ⊢ s <: t. Case (ref ): By (ref ), we have C ⊢ s <: t. Case (trans): By induction hypothesis, we have C ⊢ s <: v, C ⊢ v <: t for

some v. By (trans), we have C ⊢ s <: t.

Now suppose that Clos(C) ⊢ s <: t, s ≠ t. Then C ⊢ s <: t and since s ≠ t, s <: t ∈ Clos(C).

(ii) Consider any s <: t ∈ Clos(C). Then C ⊢ s <: t. We will prove by induction on C ⊢ s <: t that s ∈ F T V (C), t ∈ F T V (C). Consider the last step in C ⊢ s <: t.

Case (asmp): This means s <: t ∈ C, trivially, s ∈ F T V (C), t ∈ F T V (C). Case (ref ): Impossible since s <: t ∈ Clos(C), i.e., s ≠ t.

Case (trans): If s = v or v = t then done by induction hypothesis. Otherwise, s ≠ t, v ≠ t and s <: v ∈ Clos(C), v <: t ∈ Clos(C). Hence, by induction hypothesis s ∈ F T V (C), t ∈ F T V (C).

Lemma 4.2.8 Let C be an atomic coercion set.

(i) If C ⊢ σ <: τ then Clos(C) ⊢ σ <: τ.

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

Proof

(i) By induction on σ

Case σ ≡ s: By Lemma 2.5.2, τ ≡ t for some variable t.

If s = t then Clos(C) ⊢ σ <: τ by (ref ). If s ≠ t then s <: t ∈ Clos(C) and Clos(C) ⊢ σ <: τ

Case σ ≡ σ_{1} → σ_{2}: By Lemmas 2.5.2 and 2.5.3, we have τ ≡ τ_{1} → τ_{2} and C ⊢ τ_{1} <: σ_{1}, C ⊢ σ_{2} <: τ_{2}. By induction hypothesis, Clos(C) ⊢ τ_{1} <: σ_{1}, Clos(C) ⊢ σ_{2} <: τ_{2}, hence by (→) Clos(C) ⊢ σ <: τ

(ii) By induction on the proof of C, Γ ▷ M : σ. Consider the last axiom or rule used, the case for (subtp) follows from (i), all other cases are trivially established.

Lemma 4.2.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 : σ.

Proof

(i) By induction on σ Case σ ≡ s: By Lemma 2.5.2, τ ≡ t for some variable t.

If s = t then C_{↾T} ⊢ σ <: τ by (ref ). Otherwise s ≠ t, since C is closed, we have s <: t ∈ C, and since either s ∈ T or t ∈ T, we have that s <: t ∈ C_{↾T} and therefore C_{↾T} ⊢ σ <: τ.

Case σ ≡ σ_{1} → σ_{2}: By Lemmas 2.5.2 and 2.5.3, we have τ ≡ τ_{1} → τ_{2}, and C ⊢ τ_{1} <: σ_{1}, C ⊢ σ_{2} <: τ_{2}. Since F T V (σ) ⊆ T or F T V (τ) ⊆ T, we have F T V (σ_{1}) ⊆ T and F T V (σ_{2}) ⊆ T or F T V (τ_{1}) ⊆ T and F T V (τ_{2}) ⊆ T. In either case, by induction hypothesis, C_{↾T} ⊢ τ_{1} <: σ_{1}, C_{↾T} ⊢ σ_{2} <: τ_{2}, thus C_{↾T} ⊢ σ <: τ.

(ii) Assume that ⊢_{ST_{<:}} C, Γ ▷ M : σ. Since C is atomic, by Lemma 2.5.4, there is a proof in which rule (subtp) is only used immediately after (var). We prove by induction on the length of this proof that ⊢_{<:} C_{↾F T V (Γ)}, Γ ▷ M : σ. Consider the last axiom or rule used in the proof.

Case (var), (app): trivially established using the induction hypothesis since

these rules do not depend on C. Case (subtp): In this case, by Lemma 2.5.4, M ≡ x, i.e., we have x: σ ∈ Γ

and C ⊢ σ <: τ. Now, F T V (σ) ⊆ F T V (Γ), hence by (i), C_{↾F T V (Γ)} ⊢ σ <: τ, thus ⊢_{<:} C_{↾F T V (Γ)}, Γ ▷ x: σ.

We are now ready to show that we cannot bound the size of the coercion set of most general typings. As in Lemma 4.2.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 4.2.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 4.2.7, 4.2.8, 4.2.9, in the proof of the following theorem.

Theorem 4.2.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.

Proof 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

⋮  ⋮  ⋮
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 4.1: Derivation D of Theorem 4.2.10

Since ⊢_{ST_{<:}} C, Γ ▷ M : σ and C is atomic, using Lemma 2.5.4 there is a proof D as in Table 4.1. Suppose that S_{j} = ϕ. From the proof D, we have that ⊢_{ST_{<:}} C, Γ ▷ f_{j}(f_{j} x_{j}) : σ_{j}. Using Lemma 2.5.1, we have that ⊢_{ST_{<:}} C, Γ_{j} ▷ f_{j}(f_{j} x_{j}) : σ_{j}. By Lemma 4.2.8(ii), ⊢_{ST_{<:}} Clos(C), Γ_{j} ▷ f_{j}(f_{j} x_{j}) : σ_{j}. By Lemma 4.2.7(i) and Lemma 4.2.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 4.2.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}  (4.3)

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 (4.3), 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 4.2.11 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}

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

Confluence

5.1 Introduction

In the previous chapter, we examined the implications of subtyping for type-inference. Type-inference is a static property of programs and is typically done at compile-time.

In this chapter, we begin to focus on the implications of subtyping on the dynamic or run-time aspect of programs. More precisely, formal evaluation rules are typically given via a reduction-system expressed in terms of rewrite rules. There are two flavors of reduction system — deterministic and non-deterministic. In deterministic reduction systems, for each term there is at most one term that it can reduce to. Evaluation of a program then proceeds by repeatedly reducing the program according to the deterministic strategy specified by the reduction system, until we reach a value that cannot be reduced further which is its result of evaluation. On the other hand, in non-deterministic reduction systems, there are potentially many terms to which a term can reduce to in one step. A non-deterministic reduction system is usually stated in a relatively simple form — one specifies that terms of a special form, called redexes, can be simplified to some other terms; reduction on a term then proceeds by simplifying arbitrary redexes that can occur as subterms. Redexes usually specify the basic computational steps and deterministic reduction systems can usually be seen as imposing a deterministic reduction strategy for a primitive non-deterministic reduction system. For example, for the λ-calculus, the basic computational steps can be expressed simply as β and η redexes and we can then obtain various deterministic evaluation mechanisms such as call-by-name and call-by-value by imposing a particular evaluation order on the redexes that can be simplified at each step. Another reason for the importance of the non-deterministic reduction system is that because it expresses computations without placing any restrictions on the evaluation order, it is a convenient framework from which other implementations such as parallel interpreters can be derived.

A technical problem with a reduction system being non-deterministic is that it is a priori not clear that the system specifies a unique answer for the result of evaluating any program. More specifically, because at each step in the evaluation of a program there are many possibilities for the term that one may reduce to in each step, it maybe that by following different reduction sequences, one can get different final answers as the result of evaluating a program. A crucial property of any reduction system is confluence or the Church-Rosser property which states that if a term M can be reduced to two different terms N and P, then there is a common term Q to which both N and P can be reduced. The main import of the confluence property is that the final result of evaluating any term is determined uniquely. It is therefore an important basic theorem of untyped λ-calculus [CR36, Bar84, Mit76] as well as various typed λ-calculi [HM90, How92] that β, η-reduction is confluent.

Since subtyping is a means of obtaining a more flexible typing system, (i.e., a purely “static” enhancement), at first glance it may seem that it would not have any impact on computations. However, in Section 5.2, we show the surprising phenomenon that β, η-reduction fails to be confluent in the presence of subtyping. We therefore investigate a reduction system for λ-calculus with subtyping that remains confluent. Our solution is to add a new reduction rule called (<: ) which performs a transformation on the type-tags of λ-bound variables. In particular, it does nothing interesting computationally if we look at the terms without their type-annotations. The second important idea in the solution is that the reduction rules depend on the type at which we are performing the reduction. This forces some care in the choice of the type at which we are performing reductions for subterms, since reduction proceeds by performing simplifications on subterms and the type of the subterms are not necessarily determined by the type of the whole term.

We prove confluence of the reduction system by using confluence of β, η-reduction for untyped terms. However, our proof of confluence hinges crucially on the fact that reductions on any term in the calculus cannot proceed indefinitely, i.e., that we cannot express any divergent terms in the simply-typed system with subtyping. However, we expect any interesting programming language to have the possibility of infinite loops and this typically occurs through the presence of recursion in the language. Given the importance of recursion and the crucial dependence of our proof of confluence on the strong normalization of the calculus, it becomes an important question to investigate whether we can have a confluent reduction system in the presence of subtyping if the language were to have some means of recursion.

We therefore next consider the extension of the language with fixed points and fixed-point reduction and investigate whether (β), (η), (<: ) and fixed-point reductions give us a confluent reduction system in the presence of subtyping. We show that this system is confluent by considering a related language with labeled fixed points which essentially bound the depth of recursion. The confluence of the labeled system can be easily shown to imply the confluence of the language with fixed points. We then prove the confluence of the labeled system in a similar way as for the confluence of the system without any additional rules besides β, η, by using confluence of β, ηreduction for untyped terms. The main twist is that we have an additional reduction rule now (labeled-fix reduction) which is not present in the untyped lambda-calculus. The technical details of how this is resolved are given in the proof of Section 5.8. This proof is also interesting in that it is the first proof (that we are aware of) of using confluence of untyped β, η-reduction to prove confluence of a system with fixed-point reduction.

5.2 Failure of Confluence of β, η-reduction

The basic operational semantics for untyped λ-calculus is given by β, η-redexes. Reduction on terms is defined as performing a β or η reduction on an arbitrary β or η redex that occurs as a subterm. For simply-typed λ-reduction, the same reduction relation then gives a confluent system.

More specifically, β and η redexes are defined for simply-typed λ-terms as follows:

(λx: σ . M) N →^{β} [N/x]M
λx: σ . M x →^{η} M, provided x not free in M

A term M is then said to reduce in one step to a term N, written M → N, if M ≡ (… P …), N ≡ (… Q …) and P →^{β} Q or P →^{η} Q. The reduction relation → → is then defined to be the reflexive transitive closure of →. A term N is said to be in normal form if there is no term P such that N → P; intuitively, normal forms correspond to the final results of execution that cannot be further evaluated. Since there could be a choice of more than one β or η redex that occurs as a subterm of M there is potentially more than one term that M can reduce to in one step. It is therefore conceivable that there is more than one normal form N such that M → → N. An crucial property of this reduction system is confluence which states that if M → → N_{1} and M → → N_{2} then there exists a term P such that N_{1} → → P and N_{2} → → P. This can be described pictorially as follows, where the top two arrows are universally quantified and the bottom two are existentially quantified.

M N_{1}  N_{2} P

A corollary of this confluence property that there is at most one normal form that any term reduces to.

Surprisingly, β, η reduction fails to be confluent in the presence of subtyping. The following example shows that a term could reduce to more than one normal form with β, η reduction for λ\overrightarrow{<:}.

Example 5.2.1 Let N be any closed normal-form term and let σ, τ be distinct types such that σ <: τ. Consider the term M ≡ λy: σ . (λx: τ . N) y. By β -reduction, M → λy: σ . N which is α-equivalent to λx: σ . N. Thus, we have

M → λx: σ . N  (5.1)

And, by η-reduction,

M → λx: τ . N  (5.2)
≡_{α} λy: σ.(λx: τ.N)y λx: τ.N  λy: σ.[y/x]N η  βλx: σ.N

Both λx: σ . N and λx: τ . N are distinct normal forms and the reductions (5.1) and (5.2) show that M reduces to two distinct normal form exhibiting the failure of confluence in the presence of subtyping.

The two distinct normal forms of the previous example differ only in the type annotations of the λ-bound variables. Both β and η reductions do not transform the type annotations of the λ-bound variables. One obvious solution may therefore be to add a reduction rule that allows us to change the type-tags of variables, as follows:

(subtype)  λx: τ . M → λx: σ . M  if σ <: τ

Using (subtype) on the previous example, we can now reduce λx: τ . N to λx: σ . N and therefore restore confluence for the particular example considered before.

However, this naive solution is not satisfactory either. The reduction system with (subtype) still fails to be confluent, as illustrated by the following example.

Example 5.2.2 Let N be a normal-form term and consider any types σ_{1}, σ_{2}, τ such that σ_{1} <: τ and σ_{2} <: τ and there is no type ρ such that ρ <: σ_{1}, ρ <: σ_{2}. Then, by (subtype) λx: τ . N can be reduced to both λx: σ_{1} . N and λx: σ_{2} . N but there is no common term to which the latter two terms can be reduced to.

λx: σ_{1}.N λx: τ.N λx: σ_{2}.N

5.3 Reduction System for λ\overrightarrow{<:}

5.3.1 Intuitions

To understand our formulation of a confluent reduction system in the presence of subtyping, it is useful to recall the connection between the equational theory of a calculus and its reduction system. For example, consider the simply-typed λ-calculus. Equations are written as Γ ▷ M = N : σ to denote that M and N are well-formed terms of type σ in the context Γ and M and N are equivalent terms. The essential difference between reduction and equality is that while reduction is directed, i.e., leads to simpler terms, equality is a symmetric notion. We therefore define the conversion relation ⟷ as the reflexive symmetric transitive closure of the reduction relation →. Equivalently, we say that M ⟷ N iff there exist terms M_{0}, …, M_{k}, k ≥ 0 such that M_{0} ≡ M, M_{k} ≡ N, and for every i < k, we have that M_{i} → M_{i+1} or M_{i+1} → M_{i}. It can then be shown that

Γ ▷ M = N : σ iff M ⟷ N

In the presence of subtyping, there are are interesting subtleties in the way one needs to think about equality. In λ^{→} without subtyping, we include the context Γ and type σ in equations Γ ▷ M = N : σ simply to indicate the common typing of both terms and to facilitate writing “well-typed” inference rules for axiomatizing the true equations. Since the λ^{→} type σ is uniquely determined from Γ and M or N, the type does not have much to do with how M and N might be equal. With subtyping, however, terms M and N may have many different types (under the same assumptions about free variables) and so it is a priori possible for them to be equal at one type but different at another type. Informally, we can illustrate this by using the “floor” function ⌊·⌋, with ⌊x⌋ the greatest integer less than or equal to the real number x. Consider the terms M ≡ λx: real . ⌊x⌋ and N ≡ λx: real . x. Then, we have that

λx: real . ⌊x⌋x ≠ λx: real . x: real → real

i.e., M ≠ N: real → real since for example, M 3.6 is 3 while N 3.6 is 3.6. However, if M and N are only applied to integral arguments then they give identical results, i.e., they are the same as functions of integer arguments. Since real → real <: int → real , we thus have that the two terms are equal when considered at type int → real , i.e., M = N: int → real . Similarly, the equality of two terms depends on the typing assumptions of their free variables as given by the context. For example, assuming x: real , ⌊x⌋ ≠ x, but if x is assumed to be of type int , i.e., x: int , then ⌊x⌋ = x. Thus, in the presence of subtyping, the equality of two terms M and N is strongly dependent on the context and the type at which they are being considered. More formally, we can have contexts Γ, Γ′ and types σ, σ′ such that

Γ ▷ M = N : σ  (5.3)

but

Γ′ ▷ M ≠ N : σ′  (5.4)

The above dependence of equality on the context and type implies that reduction would also need to be dependent on the context and type if we there is to be the natural connection between equations and reduction. In more detail, suppose the reduction relation was independent of the type, then for two terms M and N we would either have that M ↔ N or not. In the former case, this would be inconsistent with the inequality (5.4) and in the latter case inconsistent with the equality (5.3). The independence of the reduction relation from the type can also be seen to be the cause of failure of confluence of the reduction rule (subtype) illustrated in Example 5.2.2.

We therefore express reduction for λ\overrightarrow{<:} in the form Γ ▷ M ⟶^{σ} N with the dependence of the reduction on the context Γ and the type σ at which M and N are being considered made explicitly. It would be possible in our reduction system that Γ ▷ M ⟶^{σ} N but that Γ ▷ M −̸⟶^{τ} N for a different type τ, i.e., redexes strongly depend on the type. Intuitively, we take as basic redexes β, η and the rule (subtype) with the restriction that Γ ▷ M ⟶^{σ} N only if both M and N have type σ in the context Γ. The individual reduction relations Γ ▷ · ⟶^{σ} · for each context Γ and type σ can then be shown to be confluent. Referring back to Example 5.2.2, if N has type δ we would have that

λx: τ . N ⟶^{σ_{1} → δ} λx: σ_{1} . N

and

λx: τ . N ⟶^{σ_{2} → δ} λx: σ_{2} . N

but not for example that λx: τ . N ⟶^{σ_{1} → δ} λx: σ_{2} . N, thus blocking the failure of confluence with the untyped version of (subtype).

However, defining the reduction rules to depend on the type σ leads to a problem in applying the reduction rules to subterms that are redexes, since it is not clear at what type to consider the redexes. In more detail, consider a term N ≡ (⋯ M ⋯) with a subterm M, and suppose that we wish to reduce N at type σ. The type σ of the whole term does not determine the type at which reductions on the subterm M can be performed and one therefore needs to specify which typed redexes can be simplified inside terms. Our solution is that we can consider M to be a redex of type τ, if the whole term (⋯ M ⋯) can be given type σ assuming that the subterm M is of type τ. Thus, the type at which we can apply the reductions for M are not all types of M but only those with which we can give the whole term type σ. These ideas are formalized in a proof system for Γ ▷ M ⟶^{σ} N defined in the next section.

5.3.2 Formal Rules

Following is a proof system for the relation Γ ▷ M ⟶^{σ} N where Γ is a context, σ a type.

(β)  \frac{Γ ▷ (λx: σ . M) N : τ}{Γ ▷ (λx: σ . M) N ⟶^{τ} [N/x] M}

(η)  \frac{Γ ▷ M : σ → τ  x ∉ F V (M)}{Γ ▷ (λx: σ . M x) ⟶^{σ → τ} M}

(<: )  \frac{Γ ▷ λx: τ . M : σ → δ σ <: τ, σ ≢ τ}{Γ ▷ (λx: τ . M) ⟶^{σ → δ} (λx: σ . M)}

(app1 )  \frac{Γ ▷ M ⟶^{σ → τ} N  Γ ▷ P : σ}{Γ ▷ M P ⟶^{τ} N P}

(app2 )  \frac{Γ ▷ M : σ → τ  Γ ▷ P_{1} ⟶^{σ} P_{2}}{Γ ▷ M P_{1} ⟶^{τ} M P_{2}}

(abs)  \frac{Γ, x: σ ▷ M ⟶^{τ} N  σ_{1} <: σ}{Γ ▷ λx: σ . M ⟶^{σ_{1} → τ} λx: σ . N}

The proof system has the effect that in reducing (… M …) at type σ, we can apply a reduction M ⟶^{τ} ⋯ to the subterm M if if the whole term can be given type τ using M of type σ. More formally,

\frac{Γ, x: τ ▷ (… x …) : σ Γ ▷ M ⟶^{τ} N}{Γ ▷ (… M …) ⟶^{σ} (… N …)}

5.4 Confluence of Reduction System

In this section, we prove the confluence of the reduction system defined in Section 5.3.2. Our proof proceeds by using the confluence of β, η-reduction for untyped λcalculus. In broad outline, we consider the untyped term resulting from erasing the type-annotations of λ-bound variables in λ\overrightarrow{<:} terms and use the common reduct given by confluence of untyped λ-calculus to extract the common reduct for the reduction in λ\overrightarrow{<:}.

Formally, we define the type erasure of a term M, written Erase(M), as follows.

Erase(x) = x
Erase(M N) = Erase(M) Erase(N)
Erase(λx: σ . M) = λx . Erase(M)

To be able to extract typed terms of λ\overrightarrow{<:} from untyped λ-terms, we need to know that the untyped term is of a special form. Specifically, it must be the erasure of some term of λ\overrightarrow{<:}. Formally, we can specify this property of an untyped λ-term via a type system which is obtained from that of λ\overrightarrow{<:} by omitting the type-annotations in the typing rule for λ-abstraction.

(var)  Γ ▷ x: σ  if x: σ ∈ Γ

(addvar)  \frac{Γ ▷ U : τ}{Γ, x: σ ▷ U : τ}  if x ∉ Dom(Γ)

(→ Intro)  \frac{Γ, x: σ ▷ U : τ}{Γ ▷ λx . U : σ → τ}

(→ Elim)  \frac{Γ ▷ U : σ → τ  Γ ▷ V : σ}{Γ ▷ U V : τ}

(subsump)  \frac{Γ ▷ U : σ Σ ⊢ σ <: τ}{Γ ▷ U : τ}

With these definitions, we can now state and prove the various lemmas needed to establish the confluence of the reduction system for λ\overrightarrow{<:}.

5.4.1 Proof

Our first lemma shows that the type-erasure of a term of λ\overrightarrow{<:} can be given the same type in the type system for untyped λ-terms.

Lemma 5.4.1 If Γ ▷ M : σ then Γ ▷ Erase(M) : σ.

Proof By induction on the proof of Γ ▷ M : σ.

The next lemma states that the typed reduction rules can be mimicked as β, ηreductions on the untyped terms resulting from their type-erasure.

Lemma 5.4.2 If Γ ▷ M ⟶^{σ} N then Erase(M) ⟶^{β,η} Erase(N)

Proof By induction on the proof of Γ ▷ M ⟶^{σ} N.

We next establish the converse, i.e., that β, η-reductions on untyped terms can be mimicked as typed reductions on the corresponding terms. To prove this, we need two technical propositions stating some obvious properties of substitutions.

Proposition 5.4.3 If Γ, x: σ ▷ M : τ and Γ ▷ N : σ then Γ ▷ [N/x]M : τ

Proof By induction on the proof of Γ, x: σ ▷ M : τ.

Proposition 5.4.4 Erase([N/x] M) ≡ [Erase(N)/x]Erase(M).

Proof By induction on the structure of M.

Lemma 5.4.5 If Γ ▷ M : σ and Erase(M) ⟶^{β,η} U then ∃ N such that Γ ▷ N : σ,

Γ ▷ M ⟶^{σ} N, and Erase(N) ≡ U.

Proof By induction on the structure of M.

Case M ≡ x: Vacuously true, since Erase(M) = x and x ⟶^{β,η} / U, for any term U.

Case M ≡ M_{1} M_{2}: Since Γ ▷ M : σ, we have that

Γ ▷ M_{1} : τ → ρ where ρ <: σ
Γ ▷ M_{2} : τ  (5.5)

Hence τ → ρ <: ρ → σ and by (subsump),

Γ ▷ M_{1} : τ → σ  (5.6)

Suppose that Erase(M) ⟶^{β,η} U. Since Erase(M) = Erase(M_{1}) Erase(M_{2}),

the reduction to U could be because Erase(M) itself is a β -redex, or we perform a β, η-reduction inside Erase(M_{1}) or Erase(M_{2}). We consider each of these cases separately.

Case I: Suppose that Erase(M_{1}) ≡ λx . V and U ≡ [Erase(M_{2})/x]V . Since Erase(M_{1}) ≡ λx . V , it follows that M_{1} is of the form λx: τ′ . M′_{1} with Erase(M′_{1}) = V . From (5.6), it follows that

Γ, x: τ′ ▷ M′_{1} : σ  (5.7)

with τ <: τ′. Using (5.5) with τ <: τ′, we get that

Γ ▷ M_{2} : τ′  (5.8)

Take N to be the term [M_{2}/x]M′_{1}. From judgements (5.7), (5.8), using Proposition 5.4.3, it follows that Γ ▷ N : σ. Since M ≡ (λx: τ′ . M′_{1}) M_{2}, we can use (β) to get that Γ ▷ M ⟶^{σ} N. Finally,

\begin{aligned}Erase(N) & ≡ & Erase([M_{2}/x]M′_{1}) \\ & ≡ & [Erase(M_{2})/x]Erase(M′_{1}) \end{aligned}

by Proposition 5.4.4, and we thus get that Erase(N) ≡ U. Case II: Suppose that Erase(M_{1}) ⟶^{β,η} V′_{1} and U ≡ V′_{1} Erase(M_{2}). By

(5.6), we can use induction hypothesis on M_{1} to get that there is a term

N′ such that Γ ▷ N′: τ → σ, Γ ▷ M_{1} ⟶^{τ → σ} N′ and Erase(N′) ≡ V′_{1}.

Take N ≡ N′ M_{2}. From (5.5), we get that Γ ▷ N : σ. Using (app1), we get that Γ ▷ M ⟶^{σ} N. Finally,

Erase(N) ≡ Erase(N′) Erase(M_{2})
≡ V′_{1} Erase(M_{2})
≡ U

Case III: The only possibility remaining is that Erase(M_{2}) ⟶^{β,η} V′_{2} and U ≡ Erase(M_{1}) V′_{2}. This case is dealt similarly as Case II.

Case M ≡ λx: σ_{1} . M_{1}: Since Γ ▷ M : σ, we have that σ ≡ σ_{2} → τ, and

Γ, x: σ_{1} ▷ M_{1} : τ′ where σ_{2} <: σ_{1} and τ′ <: τ,  (5.9)

By (subsump),

Γ, x: σ_{1} ▷ M_{1} : τ  (5.10)

Suppose that Erase(M) ⟶^{β,η} U. Since Erase(M) = λx . Erase(M_{1}), the reduction to U could be because Erase(M) itself is a η-redex, or we perform a β, η-reduction inside Erase(M_{1}). We consider each of these cases separately.

Case I: Suppose Erase(M_{1}) ≡ V x for some term V ,

then Erase(M) ≡ λx . V x and Erase(M) ⟶^{η} V , i.e., U ≡ V .

Since Erase(M_{1}) ≡ V x, we have that M_{1} ≡ M′_{1} x where Erase(M′_{1}) ≡ V . By judgement (5.10), Γ, x: σ_{1} ▷ M′_{1} x: τ, i.e., Γ ▷ M′_{1} : σ′_{1} → τ′ where σ_{1} <: σ′_{1} and τ′ <: τ. By (5.9), σ_{2} <: σ_{1}, hence Γ ▷ M′_{1} : σ_{2} → τ, i.e., Γ ▷ M′_{1} : σ.

Take N ≡ M′_{1}, we have that Γ ▷ N : σ. Since Γ ▷ M : σ where σ ≡ σ_{2} → τ and M ≡ λx: σ_{1} . M′_{1} x, we have the type judgement Γ ▷ λx: σ_{1} . M′_{1} x: σ_{2} → τ.

By (<: ), and (5.9), Γ ▷ λx: σ_{1} . M′_{1} x ⟶^{σ_{2} → τ} λx: σ_{2} . M′_{1} x.

Hence, by (η), Γ ▷ λx: σ_{2} . M′_{1} x ⟶^{σ_{2} → τ} M′_{1}, i.e., Γ ▷ M ⟶^{σ} N.

Finally,

Erase(N) ≡ Erase(M′_{1})
≡ V
≡ U

Case II: Suppose that Erase(M_{1}) ⟶^{β,η} V . We have U ≡ λx . V . By (5.10), we can use the induction hypothesis on M_{1} to get that there is a term N_{1}

such that Γ, x: σ_{1} ▷ N_{1} : τ, Γ, x: σ_{1} ▷ M_{1} ⟶^{τ} N_{1}, and Erase(N_{1}) ≡ V .

Take N ≡ λx: σ_{1} . N_{1}. Using (abs) on Γ, x: σ_{1} ▷ N_{1} : τ, we get Γ ▷ λx: σ_{1} . N_{1} : σ_{1} → τ. Since σ_{2} <: σ_{1}, by (<: ), we have that Γ ▷ λx: σ_{1} . N_{1} : σ_{2} → τ, i.e., Γ ▷ N : σ. Now, using (abs), we get that Γ ▷ λx: σ_{1} . M_{1} ⟶^{σ_{2} → τ} λx: σ_{1} . N_{1}, i.e.,

Γ ▷ M ⟶^{σ} N.

Finally,

Erase(N) ≡ λx . Erase(N_{1})
≡ λx . V
≡ U

Corollary 5.4.6 If Γ ▷ M : σ and Erase(M) ⟶^{β,η} U then ∃ N such that Γ ▷ N : σ,

Γ ▷ M ⟶^{σ} N, and Erase(N) ≡ U.

Proof By induction on the number of reduction step of Erase(M) ⟶^{β,η} U and Lemma 5.4.5.

Lemma 5.4.7 If U is a β, η−normal form then

U ≡ λx_{1} … λx_{n} . y V_{1} … V_{k}

where n ≥ 0, k ≥ 0, y is a variable, and V_{1}, …, V_{k} are β, η−normal forms.

Proof By induction on the structure of U.

Lemma 5.4.8 If U is a β, η−normal form and Γ ▷ U : σ, then there exists a term N such that Γ ▷ N : σ, Erase(N) ≡ U, and for any term P such that Γ ▷ P : σ and Erase(P) ≡ U, we have that Γ ▷ P ⟶^{σ} N.

Proof Let U be a β, η-normal form. By Lemma 5.4.7,

U ≡ λx_{1} … λx_{n} . y V_{1} … V_{k}, n ≥ 0, k ≥ 0

We proceed by induction on the length of U. Suppose Γ ▷ U : σ, then

σ ≡ σ_{1} → σ_{2} → ⋯ → σ_{n} → ρ  (5.11)
Γ′ ▷ y V_{1} … V_{k}: ρ where Γ′ ≡ Γ, x_{i}: σ_{i}, i = 1, …, n  (5.12)

By (5.12), we have

y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′  (5.13)
Γ′ ▷ V_{i}: ρ′_{i}, where ρ′_{i} <: ρ_{i}, i = 1, …, k (5.14)
ρ′ <: ρ  (5.15)

Hence, Γ′ ▷ V_{i}: ρ_{i}. By induction hypothesis applied to the shorter terms V_{i}, there exist terms Γ′ ▷ N_{i}: ρ_{i} with the stated property. Take N ≡ λx_{1} : σ_{1} … λx_{n}: σ_{n} . y N_{1} … N_{k}. Since Γ′ ▷ N_{i}: ρ_{i} and y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′, using ( → Elim) k times, we get that

Γ′ ▷ y N_{1} … N_{k}: ρ′,

by (5.15),

Γ′ ▷ y N_{1} … N_{k}: ρ.

Using ( → Intro) n times, we get

Γ ▷ λx_{1} : σ_{1} … λx_{n}: σ_{n} . y N_{1} … N_{k}: σ_{1} → σ_{2} → ⋯ → σ_{n} → ρ,

i.e.,

Γ ▷ N : σ.

Clearly, Erase(N) ≡ U. Now, suppose Γ ▷ P : σ and Erase(P) ≡ U. Then, P ≡ λx_{1} : σ′_{1} … λx_{n}: σ′_{n} . y P_{1} … P_{k} with Erase(P_{i}) ≡ V_{i}, i = 1, …, k. From Γ ▷ P : σ, we have Γ, x_{1} : σ′_{1}, …, x_{n}: σ′_{n} ▷ y P_{1} … P_{k}: τ′ and σ′_{1} → ⋯ → σ′_{n} → τ′ <: σ, i.e., σ_{i} <: σ′_{i} for i = 1, …, n and τ′ <: ρ. Hence, Γ, x_{1} : σ_{1}, …, x_{n}: σ_{n} ▷ y P_{1} … P_{k}: ρ. Since y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′, Γ′ ▷ P_{i}: ρ′′_{i} with ρ′′_{i} <: ρ_{i}, we have Γ′ ▷ P_{i}: ρ_{i}. By induction hypothesis, Γ′ ▷ P_{i} ⟶^{ρ_{i}} N_{i}. By repeated use of rule (app2) and the

fact that Γ′ ▷ y: ρ_{1} → ⋯ → ρ_{k} → ρ, we have Γ′ ▷ y P_{1} … P_{k} ⟶^{ρ} y N_{1} … N_{k}.

By repeated use of rule (abs), we get

Γ ▷ λx_{1} : σ_{1} … λx_{n}: σ_{n} . y P_{1} … P_{k}
⟶^{σ_{1} →··· → σ_{n} → ρ} λx_{1} : σ_{1} … λx_{n}: σ_{n} . y N_{1} … N_{k}  (5.16)

Now, since σ_{n} <: σ′_{n}, by (<: )

Γ, x_{1} : σ_{1}, …, x_{n−1} : σ_{n−1} ▷ λx_{n}: σ′_{n} . y P_{1} … P_{k}

⟶^{σ_{n} → ρ} λx_{n}: σ_{n} . y P_{1} … P_{k}

By repeating this argument, we get

Γ ▷ λx_{1} : σ′_{1} … λx_{n}: σ′_{n} . y P_{1} … P_{k}
⟶^{σ_{1} →··· → σ_{n} → ρ} λx_{1} : σ_{1} … λx_{n}: σ_{n} . y P_{1} … P_{k}  (5.17)

Using the reduction (5.17) followed by (5.16), we get that

Γ ▷ P ⟶^{σ} N

Lemma 5.4.9 Let U be any untyped term such that Γ ▷ U : σ for some context Γ and type σ. Then, U is strongly-normalizing under β, η-reduction.

Proof By Corollary 22 of [Mit91b], it follows that U is the erasure of a simply-typed λ-term. Since simply-typed λ-calculus is strongly normalizing under β, η-reduction, the result follows.

Theorem 5.4.10 Suppose that Γ ▷ M : σ and Γ ▷ M ⟶^{σ} N_{1}, Γ ▷ M ⟶^{σ} N_{2}, then there is a term Γ ▷ P : σ such that Γ ▷ N_{1} ⟶^{σ} P and Γ ▷ N_{2} ⟶^{σ} P.

Proof Suppose Γ ▷ M ⟶^{σ} N_{1}, Γ ▷ M ⟶^{σ} N_{2}. By Lemmas 5.4.2 and 5.4.1, we have Γ ▷ Erase(M) ⟶^{β,η} Erase(N_{1}),

Γ ▷ Erase(M) ⟶^{β,η} Erase(N_{2}), and Γ ▷ Erase(N_{1}) : σ, Γ ▷ Erase(N_{2}) : σ.

By confluence of β, η-reduction for untyped λ−calculus, there exists a term U′ such

that Erase(N_{1}) ⟶^{β,η} U′, Erase(N_{2}) ⟶^{β,η} U′.

By Corollary 5.4.6, there exist P′_{1}, P′_{2} such that Γ ▷ P′_{1} : σ, Γ ▷ P′_{2} : σ, Γ ▷ N_{1} ⟶^{σ} P′_{1},

Γ ▷ N_{2} ⟶^{σ} P′_{2}, and Erase(N_{1}) ≡ U′, Erase(N_{2}) ≡ U′.

Thus, by Lemma 5.4.1 Γ ▷ U′: σ. By Lemma 5.4.9, there exists a term U of β, η−normal form such that Γ ▷ U : σ, U′ ⟶^{β,η} U. By Corollary 5.4.6, there exists P_{1}, P_{2} such that Γ ▷ P_{1} : σ, Γ ▷ P_{2} : σ, Γ ▷ P′_{1} ⟶^{σ} P_{1},

Γ ▷ P′_{2} ⟶^{σ} P_{2}, and Erase(P_{1}) ≡ U, Erase(P_{2}) ≡ U.

Now, by Lemma 5.4.8 there exists a term P such that Γ ▷ P : σ, and Γ ▷ P_{1} ⟶^{σ} P, Γ ▷ P_{2} ⟶^{σ} P, i.e., there exists P such that Γ ▷ N_{1} ⟶^{σ} P, Γ ▷ N_{2} ⟶^{σ} P. This can be illustrated as in Figure 5.1.

M  _{N_{2}}_{N_{1}}_{σ}  _{P′_{2}}_{P′_{1}}  _{Erase(M)} Untyped_{Erase(N_{1})}  _{Erase(N_{2})}_{σ}  _{σ} _{σ}  _{β, η}_{β, η}  _{β, η}_{β, η}_{β, η}_{P}_{P_{1}}  _{P_{2}}  _{U} _{β, η − normal form}_{U′}_{σ} _{σ}_{σ} _{σ}  λ\overrightarrow{<:}

Figure 5.1: Proof of Theorem 5.4.10

5.5 Adding Recursion: λ_{<:}^{→,fix}

We next focus our attention on enhancing λ\overrightarrow{<:} with a mechanism for recursion and recursive definitions of terms, and consider the problem of obtaining a confluent reduction system in the presence of recursion. There are two reasons for our interest in this problem. First, recursion is an important and expressive computational mechanism found in any useful and expressive programming language. Without recursion, the system λ\overrightarrow{<:} is strongly normalizing and hence by standard results from computability theory we would not be able to express all computable functions. Secondly, we note that our confluence proof for λ\overrightarrow{<:} relied strongly on the strong-normalization property for all terms, i.e., no term has an infinite reduction sequence. This property would clearly fail in the presence of recursion, and it is therefore not obvious that the confluence results for λ\overrightarrow{<:} could be easily lifted through for a language with subtyping that has divergent computations due to the inclusion of recursion.

We obtain recursion by adding fixed-point operators at all types. Formally, we take as our set of constants,

Const = {fix_{σ}: (σ → σ) → σ | σ a type }

i.e., we include a constant fix_{σ} that can be applied to any term M of type σ → σ with the resulting value of type σ. We call the resulting calculus λ_{<:}^{→,fix} , simply-typed λ-calculus with subtyping and fixed points.

5.6 Reduction System for λ_{<:}^{→,fix}

The value fix_{σ} M is intended to be the fixed point of M. Recall that a is a fixed point of a function f if f(a) = a. We can thus obtain this desired fixed point behavior by the reduction rule

fix_{σ} → λf : σ → σ . f(fix_{σ} f)

Intuitively, the above reduction rule corresponds to a single unwinding of a recursive definition.

As in Section 5.3, our reduction system for λ_{<:}^{→,fix} will be defined by making the type at which we are considering a reduction explicit. We thus recast the above reduction rule for fix in our framework as follows:

(fix)  Γ ▷ fix_{σ} ⟶^{τ} λf : σ → σ . f (fix_{σ} f)  if Γ ▷ fix_{σ}: τ

Essentially, the reduction rule (fix) is obtained by our condition that Γ ▷ M ⟶^{τ} N only if Γ ▷ M : τ and Γ ▷ N : τ are valid typings. This condition simplifies in the case of the fixed-point reduction because the fact that Γ ▷ fix_{σ}: τ automatically guarantees that Γ ▷ λf : σ → σ . f(fix_{σ} f) : τ. The reduction system for λ_{<:}^{→,fix} is given by the proof system consisting of all the axioms and inference rules given in Section 5.3 together with the axiom (fix).

5.7 Labeled Fixed Points: λ_{<:}^{→,lab}

We prove confluence of the reduction system for λ_{<:}^{→,fix} by using a calculus with labeled fixed points. Essentially, labeled fixed points allow only a bounded number of recursive unwindings with the bound given by their label. The distinction between the calculus with fixed points and the one with labeled fixed points is that unlike the former which has divergent computations, the latter is strongly normalizing. Similar labeling techniques for untyped lambda calculus were developed by Hyland, Lévy and Wadsworth [Bar84, Hyl76, Lév75, Wad76] and a similar system for typed lambda calculus without subtyping can be found in [HM90, How92].

Formally, we define the calculus λ_{<:}^{→,lab} by including the following term constants.

Const = {fix_{σ}^{n}: (σ → σ) → σ | σ a type , n ≥ 0}

5.7.1 Labeled Reduction System with Subtyping

The proof system for the relation Γ ▷ M ⟶^{σ}_{lab} N is essentially the same as the one for the relation Γ ▷ M ⟶^{σ} N with one additional rule (fix_{lab}).

(β_{lab})  \frac{Γ ▷ (λx: σ . M) N : τ}{Γ ▷ (λx: σ . M) N ⟶^{τ}_{lab} [N/x] M}

(η_{lab})  \frac{Γ ▷ M : σ → τ  x ∉ F V (M)}{Γ ▷ (λx: σ . M x) ⟶^{σ → τ}_{lab} M}

(<:_{lab} )  \frac{Γ ▷ λx: τ . M : σ → δ σ <: τ, σ ≢ τ}{Γ ▷ (λx: τ . M) ⟶^{σ → δ}_{lab} (λx: σ . M)}

(app1_{lab})  \frac{Γ ▷ M ⟶^{σ → τ}_{lab} N  Γ ▷ P : σ}{Γ ▷ M P ⟶^{τ}_{lab} N P}

(app2_{lab})  \frac{Γ ▷ M : σ → τ  Γ ▷ P_{1} ⟶^{σ}_{lab} P_{2}}{Γ ▷ M P_{1} ⟶^{τ}_{lab} M P_{2}}

(abs_{lab})  \frac{Γ, x: σ ▷ M ⟶^{τ}_{lab} N  σ_{1} <: σ}{Γ ▷ λx: σ . M ⟶^{σ_{1} → τ}_{lab} λx: σ . N}

(fix_{lab})  Γ ▷ fix_{σ}^{n+1} ⟶^{τ}_{lab} λf : σ → σ . f (fix_{σ}^{n} f)  if Γ ▷ fix_{σ}^{n+1} : τ

We say that Γ ▷ M ⟶^{σ}_{lab} N if provable in the above system.

5.7.2 Fixed Points and Labeled Reduction: Going Back and Forth

In this section we express the connection between reductions in λ_{<:}^{→,fix} and λ_{<:}^{→,lab} . We show that reductions in either calculus can be suitably mimicked in the other. The import of this correspondence is Corollary 5.7.3 which states that confluence of the reduction system for λ_{<:}^{→,lab} implies the confluence of the reduction system for λ_{<:}^{→,fix} .

The correspondence between the terms of the two calculi is expressed via a relation lab. Informally, if M is a term in λ_{<:}^{→,lab} and N is a term in λ_{<:}^{→,fix} , we say that M ∈ lab(N) if M can be obtained from N by replacing each fix_{σ} occurring in N with fix_{σ}^{k} for some k, i.e., by specifying a bound for each fixed point of N. Formally, M ∈ lab(N) is defined inductively as:

fix_{σ}^{n} ∈ lab(fix_{σ})  for every n ≥ 0
x ∈ lab(x)
λx: σ . N ∈ lab(λx: σ . M)  if N ∈ lab(M)
N_{1} N_{2} ∈ lab(M_{1} M_{2})  if N_{1} ∈ lab(M_{1}), N_{2} ∈ lab(M_{2})

Lemma 5.7.1 Suppose that Γ ▷ M ⟶^{σ} N. Then there exists a natural number k such that if M^{∗} ∈ lab(M) with each label in M at least k then Γ ▷ M^{∗} ⟶^{σ}_{lab} N^{∗}.

Proof If Γ ▷ M ⟶^{σ} N then there exist terms M_{1}, …, M_{k}, k ≥ 0 such that M ≡ M_{0}, Γ ▷ M_{i} ⟶^{σ} M_{i+1}, M_{k} ≡ N. Proof by induction on k.

Lemma 5.7.2 If Γ ▷ M^{∗} ⟶^{σ}_{lab} N^{∗} then Γ ▷ M ⟶^{σ} N where M^{∗} ∈ lab(M), N^{∗} ∈ lab(N).

Proof By induction on the proof of Γ ▷ M^{∗} ⟶^{σ}_{lab} N^{∗}.

Corollary 5.7.3 Confluence of ⟶^{σ}_{lab} implies confluence of ⟶^{σ} .

5.8 Confluence of Labeled Reduction

As shown in the previous section, confluence of the reduction system for λ_{<:}^{→,fix} follows from the confluence of labeled reduction. In this section we establish the confluence of the reduction system for λ^{→,lab} thereby proving confluence for λ-calculus with subtyping and fixed points.

Just as in Section 5.4, we prove the confluence of labeled reduction by considering untyped λ-terms and using confluence properties of β, η-reduction on them. However, there is one main step in extending the ideas from the proof for λ\overrightarrow{<:} to that for λ_{<:}^{→,lab} . In λ\overrightarrow{<:} the only additional basic reduction rule besides β and η was (<: ) which could be easily mimicked in the untyped λ-calculus (as a 0-step reduction!). However, in λ_{<:}^{→,lab} , we have an additional set of reduction rules, namely those of labeled fixed points that need to be suitably mimicked as reduction on untyped terms. One possibility is to introduce labeled fixed point constants in the target untyped calculus and include their reduction rules in the untyped calculus. Unfortunately, this would not be very fruitful since confluence of the untyped system with labeled fixed-point reduction is unknown. Our solution is to take the target untyped λ-calculus to only include β, η-reductions (whose confluence is known) and to mimic labeled fixed-point reductions through the definition of the erasure function which maps typed terms to their corresponding terms in the untyped calculus. More specifically, we translate labeled fixed points by performing their bounded number of unwindings completely and erasing the type-annotations of the λ-bound variables from the resulting term. This reduces all labeled fixed points to terms involving fix_{σ}^{0} which we include as constants in the untyped λ-calculus. The inclusion of these constants does not interfere with the confluence of the system since there are no associated reduction rules with these constants, and thus the reduction system is still only β, η on untyped terms.

5.8.1 Type System for Untyped Terms

We consider untyped terms which may include constants of the form fix_{σ}^{0} . Thus, the typing rules for untyped terms are those given in Section 5.4 together with the following additional axiom.

(fix)  ϕ ▷ fix_{σ}^{0} : (σ → σ) → σ

5.8.2 Type Erasure

The type erasure of a term M, written Erase(M), is defined as follows.

Erase(x) = x
Erase(fix_{σ}^{0}) = fix_{σ}^{0}
Erase(fix_{σ}^{n+1}) = λf . f ((Erase(fix_{σ}^{n})) f)
Erase(M N) = Erase(M) Erase(N)
Erase(λx: σ . M) = λx . Erase(M)

5.8.3 Proof

Lemma 5.8.1 If Γ ▷ M : σ then Γ ▷ Erase(M) : σ.

Proof By induction on the proof of Γ ▷ M : σ.

Lemma 5.8.2 If Γ ▷ M ⟶^{σ}_{lab} N then Erase(M) ⟶^{β,η} Erase(N)

Proof By induction on the proof of Γ ▷ M ⟶^{σ}_{lab} N.

Lemma 5.8.3 If Γ ▷ M : σ and Erase(M) ⟶^{β,η} U then ∃ N such that Γ ▷ N : σ,

Γ ▷ M ⟶^{σ}_{lab} N, and Erase(N) ≡ U.

Proof By induction on the structure of M. We need to prove for the case where M ≡ fix_{τ}^{n}, for the other cases the proof is the same as that of Lemma 5.4.5.

Case M ≡ fix_{τ}^{n}: We have that Γ ▷ fix_{τ}^{n}: σ where (τ → τ) → τ <: σ.

Proof by induction on n.

n = 0: Vacuously true, since M ≡ fix_{τ}^{0} and fix_{τ}^{0} ⟶^{β,η} / U for any term U.

n = k + 1: Suppose Γ ▷ fix_{τ}^{k+1} : σ and Erase(fix_{τ}^{k+1}) ⟶^{β,η} U.

By definition of Erase, we have λf . f ((Erase(fix_{τ}^{k})) f) ⟶^{β,η} U. We proceed by examining possible reductions.

Case I: U ≡ λf . f (V f) and Erase(fix_{τ}^{k}) ⟶^{β,η} V .

By induction hypothesis, ∃ N_{k} such that

Γ ▷ N_{k}: (τ → τ) → τ, since Γ ▷ fix_{τ}^{k}: (τ → τ) → τ,
Γ ▷ fix_{τ}^{k} ⟶^{(τ → τ) → τ}_{lab} N_{k},  (5.18)
Erase(N_{k}) = V .  (5.19)

Take

N_{k+1} = λf : τ → τ . f (N_{k} f)

Since Γ ▷ N_{k+1} : (τ → τ) → τ and (τ → τ) → τ <: σ, we have Γ ▷ N_{k+1} : σ We also have, since (τ → τ) → τ <: σ,

σ ≡ (σ_{1} → σ_{2}) → σ_{3}, where σ_{2} <: τ, τ <: σ_{1}, and τ <: σ_{3}

By (fix_{lab}), Γ ▷ fix_{τ}^{k+1} ⟶^{σ}_{lab} λf : τ → τ . f (fix_{τ}^{k} f), i.e., we need to

prove that

Γ ▷ λf : τ → τ . f (fix_{τ}^{k} f) ⟶^{σ}_{lab} λf : τ → τ . f (N_{k} f)

CHAPTER 5. CONFLUENCE 60

From (5.18), we can get that

Γ, f : τ → τ ▷ fix_{τ}^{k} ⟶^{(τ → τ) → τ}_{lab} N_{k},  (5.20)

Using (app1_{lab}) on (5.20) and Γ, f : τ → τ ▷ f : τ → τ, we get

Γ, f : τ → τ ▷ (fix_{τ}^{k} f) ⟶^{τ}_{lab} N_{k} f,  (5.21)

Since τ <: σ_{3}, we have Γ, f : τ → τ ▷ f : τ → σ_{3}, applying (app2_{lab}) on this judgement and (5.21), we have

Γ, f : τ → τ ▷ f (fix_{τ}^{k} f) ⟶^{σ_{3}}_{lab} f (N_{k} f),  (5.22)

Now, since σ_{1} → σ_{2} <: τ → τ, using (abs_{lab}) on (5.22), we get

Γ ▷ λf : τ → τ . f (fix_{τ}^{k} f) ⟶^{(σ_{1} → σ_{2}) → σ_{3}}_{lab} λf : τ → τ . f (N_{k} f),

Thus,

Γ ▷ λf : τ → τ . f (fix_{τ}^{k} f) ⟶^{σ}_{lab} λf : τ → τ . f (N_{k} f), i.e.,

Γ ▷ fix_{τ}^{k+1} ⟶^{σ}_{lab} N_{k+1}

From (5.19), we have

Erase(N_{k+1}) = λf . f ((Erase(M_{k})) f)
= U

Case II: If k ≥ 1, then by the definition of Erase, we have

λf . f ((λg . g ((Erase(fix_{τ}^{k−1})) g)) f) ⟶^{β,η} U

Thus, U ≡ λf . f (f ((Erase(fix_{τ}^{k−1})) f)).

Take

N_{k+1} = λf : τ → τ . f (f (fix_{τ}^{k−1} f))

Then, Γ ▷ N_{k+1} : (τ → τ) → τ, since (τ → τ) → τ <: σ, we have that Γ ▷ N_{k+1} : σ. Now, since Γ ▷ fix_{τ}^{k+1} : σ we have that

Γ ▷ fix_{τ}^{k+1} ⟶^{σ}_{lab} λf : τ → τ . f (fix_{τ}^{k} f)
⟶^{σ}_{lab} λf : τ → τ . f ((λg: τ → τ . g (fix_{τ}^{k−1}g)) f)
⟶^{σ}_{lab} λf : τ → τ . f (f (fix_{τ}^{k−1}f)) = N_{k+1}

Thus, Γ ▷ fix_{τ}^{k+1} ⟶^{σ}_{lab} N_{k+1}.

We also have that, from (5.19),

Erase(N_{k+1}) = λf . f ((Erase(M_{k})) f)
= U

Corollary 5.8.4 If Γ ▷ M : σ and Erase(M) ⟶^{β,η} U then ∃ N such that Γ ▷ N : σ,

Γ ▷ M ⟶^{σ}_{lab} N, and Erase(N) ≡ U.

Proof By induction on the number of reduction step of Erase(M) ⟶^{β,η} U and Lemma 5.8.3.

Lemma 5.8.5 If U is a β, η−normal form then

U ≡ λx_{1} … λx_{n} . h V_{1} … V_{k}

where n ≥ 0, k ≥ 0, h is a variable or fix_{σ}^{0} , and V_{1}, …, V_{k} are β, η−normal forms.

Proof By induction on the structure of U.

Lemma 5.8.6 If U is a β, η−normal form and Γ ▷ U : σ, then there exists a term N such that Γ ▷ N : σ, Erase(N) ≡ U, and for any term P such that Γ ▷ P : σ and Erase(P) ≡ U, we have that Γ ▷ P ⟶^{σ}_{lab} N.

Proof Let U be a β, η-normal form. By Lemma 5.8.5,

U ≡ λx_{1} … λx_{n} . h V_{1} … V_{k}, n ≥ 0, k ≥ 0, and h a variable, or fix_{σ}^{0}

We proceed by induction on the length of U. Suppose Γ ▷ U : σ, then

σ ≡ σ_{1} → σ_{2} → ⋯ → σ_{n} → ρ  (5.23)
Γ′ ▷ h V_{1} … V_{k}: ρ where Γ′ ≡ Γ, x_{i}: σ_{i}, i = 1, …, n  (5.24)

By (5.24), we have

y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′  if h ≡ y, or  (5.25)
ρ_{1} → ⋯ → ρ_{k} → ρ′ ≡ (τ → τ) → τ  if h ≡ fix_{τ}^{0}  (5.26)
Γ′ ▷ V_{i}: ρ′_{i},  where ρ′_{i} <: ρ_{i}, i = 1, …, k  (5.27)
ρ′ <: ρ  (5.28)

Hence, Γ′ ▷ V_{i}: ρ_{i}. By induction hypothesis applied to the shorter terms V_{i}, there exist terms Γ′ ▷ N_{i}: ρ_{i} with the stated property. Take N ≡ λx_{1} : σ_{1} … λx_{n}: σ_{n} . h N_{1} … N_{k}. We need to prove that Γ ▷ N : σ, there are two cases to consider.

Case I: h ≡ y Since Γ′ ▷ N_{i}: ρ_{i} and y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′, using ( → Elim) k times, we get that

Γ′ ▷ y N_{1} … N_{k}: ρ′,

by (5.28),

Γ′ ▷ y N_{1} … N_{k}: ρ.

Using ( → Intro) n times, we get

Γ ▷ λx_{1} : σ_{1} … λx_{n}: σ_{n} . y N_{1} … N_{k}: σ_{1} → σ_{2} → ⋯ → σ_{n} → ρ,

i.e.,

Γ ▷ N : σ.

Case II: h ≡ fix_{τ}^{0} Since Γ′ ▷ fix_{τ}^{0} : (τ → τ) → τ, by (5.26), we have Γ′ ▷ fix_{τ}^{0} : ρ_{1} → ⋯ → ρ_{k} → ρ′. Since Γ′ ▷ N_{i}: ρ_{i}, using ( → Elim) k times, we get that

Γ′ ▷ fix_{τ}^{0} N_{1} … N_{k}: ρ′,

by (5.28),

Γ′ ▷ fix_{τ}^{0} N_{1} … N_{k}: ρ.

Using ( → Intro) n times, we get

Γ ▷ λx_{1} : σ_{1} … λx_{n}: σ_{n} . fix_{τ}^{0} N_{1} … N_{k}: σ_{1} → σ_{2} → ⋯ → σ_{n} → ρ,

i.e.,

Γ ▷ N : σ.

Clearly, Erase(N) ≡ U. Now, suppose Γ ▷ P : σ and Erase(P) ≡ U. There are two cases to consider.

Case I: P ≡ λx_{1} : σ′_{1} … λx_{n}: σ′_{n} . h P_{1} … P_{k} with Erase(P_{i}) ≡ V_{i}, i = 1, …, k. From Γ ▷ P : σ, we have Γ, x_{1} : σ′_{1}, …, x_{n}: σ′_{n} ▷ h P_{1} … P_{k}: τ′ and σ′_{1} → ⋯ → σ′_{n} → τ′ <: σ, i.e., σ_{i} <: σ′_{i} for i = 1, …, n and τ′ <: ρ. Hence, Γ, x_{1} : σ_{1}, …, x_{n}: σ_{n} ▷ h P_{1} … P_{k}: ρ.

Case I–a: If h ≡ y then Since y: ρ_{1} → ⋯ → ρ_{k} → ρ′ ∈ Γ′, Γ′ ▷ P_{i}: ρ′′_{i} with ρ′′_{i} <: ρ_{i}, we have Γ′ ▷ P_{i}: ρ_{i}. By induction hypothesis, Γ′ ▷ P_{i} ⟶^{ρ_{i}}_{lab} N_{i}. By repeated use of rule (app2_{lab}) and the fact that Γ′ ▷ y: ρ_{1} → ⋯ → ρ_{k} → ρ, we have

Γ′ ▷ y P_{1} … P_{k} ⟶^{ρ}_{lab} y N_{1} … N_{k}.

By repeated use of rule (abs_{lab}), we get

Γ ▷ λx_{1} : σ_{1} … λx_{n}: σ_{n} . y P_{1} … P_{k}

⟶^{σ_{1} →··· → σ_{n} → ρ}_{lab} λx_{1} : σ_{1} … λx_{n}: σ_{n} . y N_{1} … N_{k}  (5.29)

Now, since σ_{n} <: σ′_{n}, by ( <:_{lab})

Γ, x_{1} : σ_{1}, …, x_{n−1} : σ_{n−1} ▷ λx_{n}: σ′_{n} . y P_{1} … P_{k}

⟶^{σ_{n} → ρ}_{lab} λx_{n}: σ_{n} . y P_{1} … P_{k}

By repeating this argument, we get

Γ ▷ λx_{1} : σ′_{1} … λx_{n}: σ′_{n} . y P_{1} … P_{k}

⟶^{σ_{1} →··· → σ_{n} → ρ}_{lab} λx_{1} : σ_{1} … λx_{n}: σ_{n} . y P_{1} … P_{k}  (5.30)

Using the reduction (5.30) followed by (5.29), we get that

Γ ▷ P ⟶^{σ}_{lab} N

Case I–b: If h ≡ fix_{τ}^{0} then By (5.26), Γ′ ▷ f_{τ}^{0} : ρ_{1} → ⋯ → ρ_{k} → ρ′, then this case is dealt similarly to Case I–a above.

Case II: P ≡ λx_{1} : σ′_{1} … λx_{n−1} : σ′_{n−1} . fix_{γ}^{1} .

CHAPTER 5. CONFLUENCE 65

Since Erase(P) ≡ U, by definition of Erase, we have that

U ≡ λx_{1} : σ′_{1} … λx_{n−1} : σ′_{n−1} λf . f (fix_{γ}^{0} f)

Let

P′ ≡ λx_{1} : σ′_{1} … λx_{n−1} : σ′_{n−1} λf : (γ → γ) . f (fix_{γ}^{0} f)

P′ falls into previous case, Case I, so by previous argument

Γ ▷ P′ ⟶^{σ}_{lab} N

If Γ ▷ P ⟶^{σ}_{lab} P′ then done. Now from Γ ▷ P : σ we have,

Γ, x_{1} : σ′_{1}, …, x_{n−1} : σ′_{n−1} ▷ fix_{γ}^{1} : ρ where σ′_{1} → ⋯ → σ′_{n−1} → ρ <: σ. By (fix_{lab}),

Γ, x_{1} : σ′_{1}, …, x_{n−1} : σ′_{n−1} ▷ fix_{γ}^{1}

⟶^{ρ}_{lab} λf : γ → γ . f (fix_{γ}^{0} f) where (γ → γ) → γ <: ρ

Applying (abs_{lab}) n − 1 times on the above term, we get

Γ ▷ λx_{1} : σ′_{1} … λx_{n−1} : σ′_{n−1} . fix_{γ}^{1}

⟶^{σ′_{1} →··· → σ′_{n−1} → ρ}_{lab} λx_{1} : σ′_{1} … λx_{n−1} : σ′_{n−1} λf : γ → γ . f (fix_{γ}^{0} f)

i.e., Γ ▷ P ⟶^{σ}_{lab} P′

Theorem 5.8.7 Suppose that Γ ▷ M : σ and Γ ▷ M ⟶^{σ}_{lab} N_{1}, Γ ▷ M ⟶^{σ}_{lab} N_{2}, then there is a term Γ ▷ P : σ such that Γ ▷ N_{1} ⟶^{σ}_{lab} P and Γ ▷ N_{2} ⟶^{σ}_{lab} P.

M  _{N_{2}}_{N_{1}}_{σ}  _{P′_{2}}_{P′_{1}}  _{Erase(M)} Untyped_{Erase(N_{1})}  _{Erase(N_{2})}_{σ}  _{σ} _{σ}  _{β, η}_{β, η} λ_{<:}^{→,lab}  _{β, η}_{β, η}_{β, η}_{P}_{P_{1}}  _{P_{2}}  _{U} _{β, η − normal form}_{U′}_{σ} _{σ}_{σ} _{σ}

Figure 5.2: Proof of Theorem 5.8.7

Proof Suppose Γ ▷ M ⟶^{σ}_{lab} N_{1}, Γ ▷ M ⟶^{σ}_{lab} N_{2}.

By Lemmas 5.8.2 and 5.8.1, we have Γ ▷ Erase(M) ⟶^{β,η} Erase(N_{1}),

Γ ▷ Erase(M) ⟶^{β,η} Erase(N_{2}), and Γ ▷ Erase(N_{1}) : σ, Γ ▷ Erase(N_{2}) : σ.

By confluence of β, η-reduction for untyped λ−calculus, there exists a term U′ such

that Erase(N_{1}) ⟶^{β,η} U′, Erase(N_{2}) ⟶^{β,η} U′.

By Corollary 5.8.4, there exist P′_{1}, P′_{2} such that Γ ▷ P′_{1} : σ, Γ ▷ P′_{2} : σ, Γ ▷ N_{1} ⟶^{σ}_{lab} P′_{1},

Γ ▷ N_{2} ⟶^{σ}_{lab} P′_{2}, and Erase(N_{1}) ≡ U′, Erase(N_{2}) ≡ U′.

Thus, by Lemma 5.8.1 Γ ▷ U′: σ. By Lemma 5.4.9, there exists a term U of β, η−normal form such that Γ ▷ U : σ, U′ ⟶^{β,η} U. By Corollary 5.8.4, there exists P_{1}, P_{2} such that Γ ▷ P_{1} : σ, Γ ▷ P_{2} : σ, Γ ▷ P′_{1} ⟶^{σ}_{lab} P_{1},

Γ ▷ P′_{2} ⟶^{σ}_{lab} P_{2}, and Erase(P_{1}) ≡ U, Erase(P_{2}) ≡ U.

Now, by Lemma 5.8.6 there exists a term P such that Γ ▷ P : σ, and Γ ▷ P_{1} ⟶^{σ}_{lab} P,

Γ ▷ P_{2} ⟶^{σ}_{lab} P, i.e., there exists P such that Γ ▷ N_{1} ⟶^{σ}_{lab} P, Γ ▷ N_{2} ⟶^{σ}_{lab} P.

The above proof is illustrated in Figure 5.2.

Conclusion

We conclude with a summary of the work described in this dissertation and some comments on directions for future work.

We have investigated the implications of subtyping in a functional language from two points of view. The first point of view relates to static type checking. We considered the problem of type inference and obtained two important results. One set of results characterizes the problem of typability of a term in the presence of a fixed subtype ordering as equivalent to the problem of satisfiability of subtype inequalities over a fixed partial order. A natural subproblem of the general problem of typability is one in which all program constants only have atomic types. This subproblem can be characterized as the satisfiability of a certain restricted form of subtype inequalities. Since this latter problem has been shown previously to be pspace-hard, this allows us to give a lower bound on the algorithmic problem of typability. The second set of results deals with most general typings which is the typical output of a type-inference algorithm. Instead of focusing on a particular notion of instance, we have developed a general theory independent of the notion of instance one may chose to use (as long as it is sound) which shows that we cannot have succinct characterization of all typings of terms.

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. Useful results would be a knowledge of the complexity-theoretic relation between the problem of solving arbitrary subtype inequalities and inequalities of the restricted form. Another useful theoretical result would be the structural complexities of the two problems and getting tight upper bounds and lower bounds that would match. Another interesting line of investigation is the further study of most general types under arbitrary notions of instance; in particular, more exact characterizations of their intrinsic lengths.

The lower bounds established here 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 arise due to some special partial order cases of the subtype ordering. A characterization of some particular class of subtype orderings of interest for which one can have succinct most general typings and for which the typability problem is tractable would suggest placing similar restrictions on programs in practice.

The second point of view relates to the dynamic notion of program evaluation. We began by observing that β, η-reduction fails to be confluent in the presence of subtyping. The main result obtained is a confluent reduction system. Our solution was to parameterize the reduction system by the type at which we are considering the terms and to introduce a new rule (<: ) which would transform the type annotations of variables. Our proof of confluence makes use of the known confluence of β, η-reduction on untyped λ-terms. We then showed how the same combination of type-dependent reductions together with the new rule (<: ) yields a confluent system, for a language with subtyping, in the presence of recursion as well. However, the proof of confluence in the presence of recursion required some significant modifications to that for the case without recursion. These were to consider a related language with labeled bounds on depths of recursion and the simulation of the reduction rule for fixed points with β, η-reduction of untyped λ-terms. One line of future investigation is the extension of these results along the lines of [Mit76, HM90, How92] for languages which include reduction rules for term constants. In particular, it would be interesting to compare the properties that one requires of the reduction rules for the term constants, to obtain confluence in the presence of subtyping with that without subtyping.

Bibliography

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

[Bar84] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984. Second edition.

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

[CR36] A. Church and J.B. Rosser. Some properties of conversion. Trans. Amer. Math. Soc., 39:472–482, 1936.

[FM89] Y. Fuh and P. Mishra. Polymorphic subtype inference: closing the theorypractice 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.

[HM90] B.T. Howard and J.C. Mitchell. Operational and axiomatic semantics of PCF. In ACM Conference on LISP and Functional Programming, pages 298–306, 1990.

[HM95] My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes. In Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages, pages 176–185. ACM, 1995.

[How92] B.T. Howard. Fixed points and extensionality in typed functional programming languages. PhD thesis, Stanford University, 1992.

[Hyl76] J.M.E. Hyland. A syntactic characterization of the equality in some models of the lambda calculus. J. London Math. Society, 2(12):361–370, 1976.

[Lév75] J.-J. Lévy. An algebraic interpretation of the λ-β -k-calculus and a labeled λ-calculus. In C. Böhm, editor, Proc. Lambda calculus and computer science theory, pages 147–165. Springer LNCS 37, 1975.

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

[Mit76] G Mitschke. λ-Kalukül, δ-Konversion und axiomatische Rekursionstheorie. Fachbereit Mathematik Preprint Number 274, Technische Hochschule, Darmstadt, 1976.

[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 typability. 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 pspace-hard. 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, pages 1–16, Berlin, 1985. Springer LNCS 201.

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

[Wad76] C. Wadsworth. The relation between computational and denotational properties for Scott’s D^{∞} models. Siam J. Comput., 5(3):488–521, 1976.

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