Decidable Higher Order Subtyping

Adriana Compagnoni

                                abc@dcs.ed.ac.uk

Department of Computer Science, University of Edinburgh The King’s Buildings, Edinburgh, EH9 3JZ, United Kingdom Tel: (+44) (131) 650-1000 Fax: (+44) (131) 667-7209

Abstract

This paper establishes the decidability of typechecking in F_{∧}^{ω}, a typed lambda calculus combining higher-order polymorphism, subtyping, and intersection types. It contains the first proof of decidability of subtyping for a higher-order system.

1 Introduction

The system F_{∧}^{ω} (F-omega-meet) was first introduced in [16], where it was shown to be rich enough to provide a typed model of object oriented programming with multiple inheritance. The system F_{∧}^{ω} is an extension of F^{ω} [22] with bounded quantification and intersection types, which can be seen as a natural generalization of the type disciplines present in the current literature, for example in [19, 26, 27, 11]. Systems including either subtyping or intersection types or both have been widely studied for many years. What follows is not intended to be an exhaustive description, but a framework for the present work.

First-order type disciplines with intersection types have been investigated by the group in Torino [18, 2] and elsewhere (see [10] for background and further references). A secondorder λ-calculus with intersection types was studied in [26]. Systems including subtyping were present in [9, 5]. Higher order generalizations of subtyping appear in [4, 17, 25, 3].

Lambda calculi syntax is often presented by several interdependent relations or judgements (such as context formation, kinding, and typing, for example), and we say that a given lambda calculus is decidable if its typing relation is, but because of the interdependence of judgements it actually means the decidability of all the interwoven relations.

The system F_{≤}, a second-order λ-calculus with bounded quantification, was studied in [21]. In [26] it was proved that typing in F_{≤} was undecidable and that undecidability was caused by the subtyping relation, the rule for bounded quantification being responsible for the failure.

An alternative rule for subtyping quantified types was presented in [11] in an attempt to find a decidable system, and the decidability of subtyping was proved for an extension of system F with bounded polymorphism, but different from F_{≤}. Unfortunately, the typing relation fails to satisfy the minimal type property. This failure, discovered by Ghelli, introduces serious problems in type checking and type inference. At the moment it is not clear how to solve them or, even more problematic, whether the typing relation is decidable. The solution we chose here to overcome this problem is to replace the subtyping rule between quantifiers by the corresponding rule of Cardelli and Wegner’s kernel Fun [9].

Because F_{∧}^{ω} has reduction on types we introduce a conversion rule that includes interconvertible types in the subtype relation. Therefore, our subtyping relation relates types of a more expressive type system than that presented in [11]. In fact, treating the interaction between interface refinement and encapsulation of objects, in object oriented programming, has required higher-order generalizations of subtyping: the F-bounded quantification of Canning, Cook, Hill, Olthoff and Mitchell [4] or system F_{≤}^{ω} [6, 8, 7, 25, 3].

In this paper we give a positive answer to the decidability of typing in the presence of β∧-convertible types and subtyping. We prove that subtyping in F_{∧}^{ω} is decidable, which a fortiori gives the decidability of subtyping for the F_{≤}^{ω} fragment because the former is a conservative extension of the latter – namely, each subtyping statement derivable in F_{∧}^{ω} containing no intersections other than the empty ones is also derivable in F_{≤}^{ω}. A major task in establishing the decidability result for our system is in proving that subtyping is decidable.

We use a definition of F_{∧}^{ω} from [15, 12] that differs from the one introduced in [16] in two ways. First, the ill-behaved Castagna and Pierce quantifier rule has been replaced by the Cardelli and Wegner rule. Secondly, we introduce a richer notion of reduction on types, and thereby the four distributivity rules become particular cases of the conversion rule. This alternative (and equivalent) presentation provides a different view of the system that is the key to proving the decidability of subtyping.

This new perspective suggests that to prove the decidability of subtyping it is enough to concentrate on types in normal form. Note that the solution cannot be as simple as to restrict the subtyping rules of F_{∧}^{ω} to handle only types in normal form and replace conversion by reflexivity. The following is a good example of the intricacies of the problem to be solved. Consider the context Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K, where every type is in normal form; observe that X and Z are subtypes of the identity on K. Then Γ ⊢ X(Z W) ≤ W, which is also in normal form, is not derivable without using conversion, i.e. without performing any β-reduction steps.

The subtyping rules of F_{∧}^{ω} are not syntax directed, in the sense that the form of a derivable subtyping statement does not uniquely determine the last rule of its derivation. A deterministic version of the subtyping relation, AlgF_{∧}^{ω}, is presented in [15, 12]. There it is proved to be equivalent to the original presentation on well-formed types. The system AlgF_{∧}^{ω} considers only types in normal form, and will be our starting point to prove the decidability of subtyping.

2 SYNTAX OF F_{∧}^{ω} 3

In this paper we establish the decidability of subtyping in F_{∧}^{ω} by proving that the algorithm described by AlgF_{∧}^{ω} terminates, which is equivalent to showing that the definition of the AlgF_{∧}^{ω} is well-founded. We discuss this further in section 5.3.

In the algorithm, checking whether Γ ⊢_{Alg} S T ≤ A is reduced to checking if Γ ⊢_{Alg} lub_{Γ}(S T)^{nf} ≤ A, where lub_{Γ}(S T) substitutes the leftmost innermost variable of S T by its bound in Γ. Such replacements may produce a term that is not in normal form, in which case we normalize it afterwards. (In an alternative notation used in [1], Γ ⊢_{Alg} XS_{1} ⋯ S_{n} ≤ A is reduced to checking if Γ ⊢_{Alg} (Γ(X)S_{1} ⋯ S_{n})^{nf} ≤ A.) The main problem here is that the size of the types to be examined in the recursive call may not decrease. This indicates that the proof of termination of the algorithm is not immediate. In particular, the proof of termination for the second order calculus presented in [11] cannot be modified to serve our purposes, because of the interaction between reduction and the substitution of type variables by their bounds in our system. See section 5.3 for more details.

Typing and subtyping are defined using context formation and kinding judgements, therefore in section 4 we show that the latter are decidable.

Finally we prove in section 8 that typing is decidable. To illustrate the problem of typing consider the following situation. Imagine trying to type f a in different contexts. We know we can type an application if we can find an arrow type for f whose domain types a. In the context Γ, X≤S→T:⋆, f:X, a:S, we need to use that the type X, with which f is declared, is a subtype of S→T. Note that X, the minimal type of f, does not have enough structural information to type an application. Therefore, one needs to “climb” the subtyping hierarchy until a type with enough information is found, in this case an arrow type.

If we want to type f a with respect to the context Γ′ ≡ Γ, Z≤ΛY:⋆.S→Y:⋆→⋆, W ≤Z:⋆ →⋆, f:W T , a:S, we have to use that W T is a subtype of S→T, which involves replacing W by Z, then Z by ΛY: ⋆ .S→Y in W T, and finishing with a step of β-reduction. Since we need to continue making replacements and reduction steps until we find an arrow type, this procedure is slightly more complicated than finding the lub_{Γ′}(W T), which is ZT. The situation is even more twisty because of the presence of intersection types, but we leave that for section 8. This suggests that proving the termination of typechecking is not immediate, and that we will need to use similar ideas to those needed to prove the termination of subtype checking.

This paper extends the decidability result of [13] for subtyping to the typing relation.

2 Syntax of F_{∧}^{ω}

We now present the rules for kinding, subtyping, and typing in F_{∧}^{ω}. They are organized as proof systems for four interdependent judgement forms:

Γ ⊢ ok  well-formed context
Γ ⊢ T : K well-kinded type
Γ ⊢ S ≤ T subtype
Γ ⊢ e : T well-typed term.

We sometimes use the metavariable Σ to range over statements (right-hand sides of judgements) of any of these four forms.

2.1 Syntactic Categories

The kinds of F_{∧}^{ω} are those of F^{ω}: the kind ⋆ of proper types and the kinds K_{1}→K_{2} of functions on types (sometimes called type operators).

𝕂 ::= ⋆ | 𝕂 →𝕂

The language of types of F_{∧}^{ω} is a straightforward higher-order extension of F_{≤}, Cardelli and Wegner’s second-order calculus of bounded quantification. Like F_{≤}, it includes type variables (written X), function types (T →T′), and polymorphic types (∀X≤T:K.T′), in which the bound type variable X ranges over all subtypes of the upper bound T. Moreover, like F^{ω}, we allow types to be abstracted on types (ΛX:K.T) and applied to argument types (T T′); in effect, these forms introduce a simply typed λ-calculus at the level of types. Finally, we allow arbitrary finite intersections (⋀^{K}[T_{1}..T_{n}]), where all the T_{i}’s are members of the same kind K.

𝕋 ::= | X | 𝕋→𝕋 | ∀X≤𝕋:𝕂 .𝕋 | ΛX:𝕂 .𝕋 | 𝕋 𝕋 | ⋀^{𝕂}[𝕋..𝕋]

We use the abbreviation ⊤^{K} for nullary intersections and sometimes X:K for X ≤ ⊤^{K}:K.

⊤^{K} ≡ ⋀^{K}[ ]  X:K ≡ X ≤ ⊤^{K}:K

We drop the maximal type Top of F_{≤}, since its role is played here by the empty intersection ⊤^{⋆}. For technical convenience, we provide kind annotations on bound variables and intersections so that every type has an “obvious kind,” which can be read off directly from its structure and the kind declarations in the context.

The language of terms includes the variables (x), applications (e e) , and functional abstractions (λx:T.e) of the simply typed λ-calculus, plus the type abstraction (λX≤T:K.e) and application (e T) of F^{ω}. As in F_{≤}, each type variable is given an upper bound at the point where it is introduced.

Intersection types are introduced by expressions of the form “for(X∈T_{1}..T_{n})e”, which can be read as instructions to the type-checker to analyze the expression e separately under the assumptions X ≡ T_{1}, X ≡ T_{2}, …, X ≡ T_{n} and conjoin the results. For example, if + : Int→Int→Int ∧ Real→Real→Real, then we can derive

for(X∈Int, Real)λx:X.x + x : Int→Int ∧ Real→Real.
e ::= x | λx:𝕋.e | e e | λX≤𝕋:𝕂 .e | e 𝕋 | for(X∈𝕋..𝕋)e

The operational semantics of F_{∧}^{ω} is given by the following reduction rules on types and terms.

Definition 2.1.1 (Reduction rules for types)

1. (ΛX:K.T_{1})T_{2} →_{β∧} T_{1}[X←T_{2}]

2. S → ⋀^{⋆}[T_{1}..T_{n}] →_{β∧} ⋀^{⋆}[S→T_{1} .. S→T_{n}]

3. ∀X≤S:K.⋀^{⋆}[T_{1}..T_{n}] →_{β∧} ⋀^{⋆}[∀X≤S:K.T_{1} .. ∀X≤S:K.T_{n}]

4. ΛX:K_{1}.⋀^{K_{2}}[T_{1}..T_{n}] →_{β∧} ⋀^{K_{1}→K_{2}}[ΛX:K_{1}.T_{1} .. ΛX:K_{1}.T_{n}]

5. (⋀^{K_{1}→K_{2}}[T_{1}..T_{n}]) U →_{β∧} ⋀^{K_{2}}[T_{1} U .. T_{n} U]

6. ⋀^{K}[T_{1} .. ⋀^{K}[S_{1}..S_{n}] .. T_{m}] →_{β∧} ⋀^{K}[T_{1} .. S_{1}..S_{n} .. T_{m}]

The first rule is the usual β-reduction rule for types. Rules 2 through 5 express the fact that intersections in positive positions distribute with respect to the other type constructors. Rule 6 states that intersection is an associative operator. The left-hand side of each reduction rule is a redex and the right-hand side its reduct. The relation →_{β∧} is extended so as to become a compatible relation with respect to type formation, ↠_{β∧} is the transitive and reflexive closure of →_{β∧}, and =_{β∧} is the least equivalence relation containing →_{β∧}. The capture-avoiding substitution of S for X in T is written T [X←S]. Substitution is written similarly for terms, and is extended point-wise to contexts. The β∧-normal form of a type S is written S^{nf}, and is extended point-wise to contexts.

Definition 2.1.2 (Reduction rules for terms)

1. (λx:T_{1}.e_{1})e_{2} →_{βfors} e_{1}[x←e_{2}]

2. (λX≤T_{1}:K_{1}.e)T →_{βfors} e[X←T]

3. (for(X∈T_{1}..T_{n})e_{1})e_{2} →_{βfors} for(X∈T_{1}..T_{n})(e_{1} e_{2})

4. for(X∈T_{1}..T_{n})e →_{βfors} e, if X ∉ FV(e)

Rules 1 and 2 are the β-reductions on terms. Rule 3 says that the for constructor can be pushed to the outermost level. We consider the reduction defined by rules 1 through 3 as →_{βfor} and the one defined by 4 as →_{s} (s comes from simplification). The left-hand side of each reduction rule is a redex and the right-hand side its reduct. The relation →_{βfors} is extended so as to become a compatible relation with respect to term formation, ↠_{βfors} is the transitive reflexive closure of →_{βfors}, and =_{βfors} is the least equivalence relation containing →_{βfors}.

2.2 Contexts

A context Γ is a finite sequence of typing and subtyping assumptions for a set of term and type variables.

The empty context is written ∅. Term variable bindings have the form x:T; type variable bindings have the form X≤T:K, where T is the upper bound of X and K is the kind of T.

Γ ::= ∅ | Γ, x:T | Γ, X≤T:K

When writing nonempty contexts, we omit the initial ∅. The domain of Γ is written dom(Γ). The functions FV(—) and FTV(—) give the sets of free term variables and free type variables of a term, type, or context. Since we are careful to ensure that no variable is bound more than once, we sometimes abuse notation and consider contexts as finite functions: Γ(X) yields the bound of X in Γ, where X is implicitly asserted to be in dom(Γ).

Types, terms, contexts, statements, and derivations that differ only in the names of bound variables are considered identical. The underlying idea is that variables are de Bruijn indexes [20].

Definition 2.2.1 (Closed)

1. A term e is closed with respect to a context Γ if FV(e) ∪ FTV(e) ⊆ dom(Γ).

2. A type T is closed with respect to a context Γ if FTV(T) ⊆ dom(Γ).

3. A typing statement Γ ⊢ e : T is closed if e and T are closed with respect to Γ.

4. A kinding statement Γ ⊢ T : K is closed if T is closed with respect to Γ.

5. A subtyping statement Γ ⊢ S ≤ T is closed if S and T are closed with respect to Γ.

We consider only closed typing statements. Observe that in the limit case of the rule T-Meet, when n = 0, not having the closure convention would allow nonsensical terms to be typed. On the other hand, the free variable lemma (lemma 3.2) guarantees that kinding statements are closed and the well-kindedness of subtyping (lemma 3.8) ensures that subtyping statements are closed as well.

2.3 Context Formation

The rules for well-formed contexts are the usual ones: a start rule for the empty context and rules allowing a given well-formed context to be extended with either a term variable binding or a type variable binding.

∅ ⊢ ok  (C-Empty)

\frac{Γ ⊢ T : ⋆  x ∉ dom(Γ)}{Γ, x:T ⊢ ok}  (C-Var)

\frac{Γ ⊢ T : K  X ∉ dom(Γ)}{Γ, X≤T:K ⊢ ok}  (C-TVar)

2.4 Type Formation

For each type constructor, we give a rule specifying how it can be used to build wellformed type expressions. The critical rules are K-OAbs and K-OApp, which form type abstractions and type applications (essentially as in a simply typed λ-calculus).

The well-formedness premise Γ ⊢ ok in K-Meet (and in T-Meet below) is required for the case where n = 0.

\frac{Γ_{1}, X≤T:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤T:K, Γ_{2} ⊢ X : K}  (K-TVar)

\frac{Γ ⊢ T_{1} : ⋆  Γ ⊢ T_{2} : ⋆}{Γ ⊢ T_{1}→T_{2} : ⋆}  (K-Arrow)
\frac{Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆}{Γ ⊢ ∀X≤T_{1}:K_{1}.T_{2} : ⋆}  (K-All)
\frac{Γ, X:K_{1} ⊢ T_{2} : K_{2}}{Γ ⊢ ΛX:K_{1}.T_{2} : K_{1}→K_{2}}  (K-OAbs)
\frac{Γ ⊢ S : K_{1}→K_{2}  Γ ⊢ T : K_{1}}{Γ ⊢ S T : K_{2}}  (K-OApp)
\frac{Γ ⊢ ok  for each i ∈ \{1..n\} , Γ ⊢ T_{i} : K}{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K}  (K-Meet)

2.5 Subtyping

The rules defining the subtype relation are a natural extension of familiar calculi of bounded quantification. Aside from some extra well-formedness conditions, the rules S-Trans, S-TVar, and S-Arrow are the same as in the usual, second-order case. Rules S-OAbs and S-OApp extend the subtype relation point-wise to kinds other than ⋆. The rule of type conversion in F^{ω}, that is, if Γ ⊢ e : T and T =_{β} T′ then Γ ⊢ e : T′, is captured here as the subtyping rule S-Conv, which also gives reflexivity as a special case. The rule S-All is the rule of Cardelli and Wegner’s Fun language [9] in which the bounds of the quantifiers are equal. Rules S-Meet-G and S-Meet-LB specify that an intersection of a set of types is the set’s order-theoretic greatest lower bound.

\frac{Γ ⊢ S : K  Γ ⊢ T : K  S =_{β∧} T}{Γ ⊢ S ≤ T}  (S-Conv)
\frac{Γ ⊢ S ≤ T  Γ ⊢ T ≤ U}{Γ ⊢ S ≤ U}  (S-Trans)
\frac{Γ_{1}, X≤T:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤T:K, Γ_{2} ⊢ X ≤ T}  (S-TVar)

\frac{Γ ⊢ T_{1} ≤ S_{1}  Γ ⊢ S_{2} ≤ T_{2}  Γ ⊢ S_{1}→S_{2} : ⋆}{Γ ⊢ S_{1}→S_{2} ≤ T_{1}→T_{2}}  (S-Arrow)

\frac{Γ, X≤U:K ⊢ S ≤ T  Γ ⊢ ∀X≤U:K.S : ⋆}{Γ ⊢ ∀X≤U:K.S ≤ ∀X≤U:K.T}  (S-All)

\frac{Γ, X:K ⊢ S ≤ T}{Γ ⊢ ΛX:K.S ≤ ΛX:K.T}  (S-OAbs)

\frac{Γ ⊢ S ≤ T  Γ ⊢ S U : K}{Γ ⊢ S U ≤ T U}  (S-OApp)

\frac{for each i ∈ \{1..n\} , Γ ⊢ S ≤ T_{i}  Γ ⊢ S : K}{Γ ⊢ S ≤ ⋀^{K}[T_{1}..T_{n}]}  (S-Meet-G)

\frac{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K}{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] ≤ T_{i}}  (S-Meet-LB)

2.6 Term Formation

Except for T-Meet and T-For, the term formation rules are precisely those of the secondorder calculus of bounded quantification. T-For provides for type checking under any of a set of alternate assumptions. For each S_{i}, the type derived for the instance of the body e when X is replaced by S_{i} is a valid type of the for expression itself. The T-Meet rule can then be used to collect these separate typings into a single intersection. Type-theoretically, T-Meet is the introduction rule for the ∧ constructor; the corresponding elimination rule need not be given explicitly, since it follows from T-Subsumption and S-Meet-LB.

\frac{Γ_{1}, x:T , Γ_{2} ⊢ ok}{Γ_{1}, x:T , Γ_{2} ⊢ x : T}  (T-Var)

\frac{Γ, x:T_{1} ⊢ e : T_{2}}{Γ ⊢ λx:T_{1}.e : T_{1}→T_{2}}  (T-Abs)

\frac{Γ ⊢ f : T_{1}→T_{2}  Γ ⊢ a : T_{1}}{Γ ⊢ f a : T_{2}}  (T-App)

\frac{Γ, X≤T_{1}:K_{1} ⊢ e : T_{2}}{Γ ⊢ λX≤T_{1}:K_{1}.e : ∀X≤T_{1}:K_{1}.T_{2}}  (T-TAbs)

\frac{Γ ⊢ f : ∀X≤T_{1}:K_{1}.T_{2}  Γ ⊢ S ≤ T_{1}}{Γ ⊢ f S : T_{2}[X←S]}  (T-TApp)

\frac{Γ ⊢ e[X←S]:T  S : \{S_{1}..S_{n}\}}{Γ ⊢ for(X∈S_{1}..S_{n})e : T}  (T-For)

\frac{Γ ⊢ ok  for each i ∈ \{1..n\} , Γ ⊢ e : T_{i}}{Γ ⊢ e : ⋀^{⋆}[T_{1}..T_{n}]}  (T-Meet)

\frac{Γ ⊢ e : S  Γ ⊢ S ≤ T}{Γ ⊢ e : T}  (T-Subsumption)

Most of the rules include premises which have two rather different sorts: structural premises, which play an essential role in giving the rule its intended semantic force, and well-formation premises, which ensure that the entities named in the rule are of the expected sorts.

We sometimes omit well-formation premises that can be derived from others. For example, in the rule S-Arrow, we drop the premise Γ ⊢ T_{1}→T_{2} : ⋆, since it follows from Γ ⊢ S_{1}→S_{2} : ⋆ using structural properties.

3 Properties

In this section we list properties whose proofs can be found in [12].

Lemma 3.1 If Γ ⊢ Σ and Γ_{1} is a prefix of Γ, then Γ_{1} ⊢ ok as a subderivation. Moreover, except for the case Γ_{1} ≡ Γ and Σ ≡ ok, the subderivation is strictly shorter.

Lemma 3.2 (Free variables)

1. If Γ ⊢ T : K, then FTV(T) ⊆ dom(Γ).

2. If Γ ⊢ ok, then each variable or type variable in dom(Γ) is declared only once.

Lemma 3.3 (Generation for context judgements)

1. If Γ_{1}, X≤T:K, Γ_{2} ⊢ ok, then Γ_{1} ⊢ T : K by a proper subderivation.

2. If Γ_{1}, x:T , Γ_{2} ⊢ ok, then Γ_{1} ⊢ T : ⋆ by a proper subderivation.

Proposition 3.4 (Generation for kinding)

1. Γ ⊢ X : K implies Γ ≡ Γ_{1}, X≤T:K, Γ_{2} for some Γ_{1}, T, and Γ_{2}.

2. Γ ⊢ T_{1}→T_{2} : K implies K ≡ ⋆ and Γ ⊢ T_{1}, T_{2} : ⋆.

3. Γ ⊢ ∀X≤T_{1}:K_{1}.T_{2} : K implies K ≡ ⋆ and Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆.

4. Γ ⊢ Λ(X:K_{1})T_{2} : K implies K ≡ K_{1}→K_{2} and Γ, X≤⊤^{K_{1}}:K_{1} ⊢ T_{2} : K_{2}, for some K_{2}.

5. Γ ⊢ S T : K implies Γ ⊢ S : K′→K and Γ ⊢ T : K′, for some K′.

6. Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K′ implies K ≡ K′ and Γ ⊢ ok and Γ ⊢ T_{i} : K for each i.

If one tries to prove Weakening (Corollary 3.7) directly by induction on derivations the induction hypothesis is too weak in the cases for K-All and S-OAbs, for example. We adapt McKinna and Pollack’s idea of renaming [24] to overcome this problem.

Definition 3.5 (Parallel Substitution) A parallel substitution γ for Γ is an assignment of types to type variables in dom(Γ) and terms to term variables in dom(Γ). A renaming for Γ in Δ is a parallel substitution γ from variables to variables such that

• for every x:A in Γ, γ(x):A[γ] is in Δ, and

• for every X≤T:K in Γ, γ(X)≤A[γ]:K is in Δ.

We write Σ[γ] for the result of performing the substitution γ in the judgement Σ. The renaming γ{x ↦ y} maps x to y and behaves like γ elsewhere, similarly for type variables.

Lemma 3.6 (Renaming) If Δ ⊢ ok and γ is a renaming for Γ in Δ then Γ ⊢ Σ implies Δ ⊢ Σ[γ].

Corollary 3.7 (Weakening/Permutation) Let Γ and Γ′ be contexts such that Γ ⊆ Γ′ and Γ′ ⊢ ok. Then Γ ⊢ Σ implies Γ′ ⊢ Σ.

Proposition 3.8 (Well-kindedness of subtyping) If Γ ⊢ S ≤ T, then Γ ⊢ S : K and Γ ⊢ T : K for some K.

Proposition 3.9 (Well-kindedness of typing) If Γ ⊢ e : T, then Γ ⊢ T : ⋆.

4 Decidability of context formation and kinding

The decidability of kinding is used to prove the decidability of subtyping in section 5.3, and the decidability of ok judgements is used to prove the decidability of typechecking in section 8. We want to define a measure (size) on judgements to show that the complexity of the hypothesis in a kinding derivation rule is smaller than the complexity of the conclusion. Given that kinding rules may depend on ok judgements we need to define a measure for both kinding and well-formation judgements. Rules C-TVar and C-Var suggest that the size of ok should be bigger than 0 (let it be 1). The rule K-Meet in the empty case, suggests that the size of ⊤^{K} should be bigger than the size of ok, while K-TVar indicates that the size of a variable should be bigger than the size of ok. With all these ideas in mind we define the following measure.

Definition 4.1 (Size)

1. The size of a type expression T, size_{t}(T), is defined as follows.

(a) size_{t}(X) = 2,

(b) size_{t}(S→T) = size_{t}(∀X≤S:K.T) = size_{t}(S T) = size_{t}(S) + size_{t}(T) + 1,

(c) size_{t}(ΛX:K.T) = size_{t}(T) + 3,

(d) size_{t}(⋀^{K}[T_{1}..T_{n}]) = 2 + Σ_{1≤i≤n}size_{t}(T_{i}).

2. The homomorphic extension to contexts, size_{c}(Γ), is defined as follows.

(a) size_{c}(∅) = 0,

(b) size_{c}(Γ, X ≤ T:K) = size_{c}(Γ, x:T) = size_{c}(Γ) + size_{t}(T).

3. The size of a subtyping, kinding, or ok judgement J, size_{j}(J), is defined as follows.

(a) size_{j}(Γ ⊢ ok) = size_{c}(Γ) + 1,

(b) size_{j}(Γ ⊢ T : K) = size_{c}(Γ) + size_{t}(T).

(c) size_{j}(Γ ⊢ S ≤ T) = size_{c}(Γ) + size_{t}(S) + size_{t}(T).

Lemma 4.2 (Well-foundedness of context formation and kinding rules)

1. For every kinding or ok judgement J, size_{j}(∅ ⊢ ok) ≤ size_{j}(J).

2. If \frac{J_{1} .. J_{n}}{J} is a kinding rule or a context formation rule, then size_{j}(J_{i}) < size_{j}(J) for each i ∈ {1..n}.

Corollary 4.3 (Decidability of context formation and kinding)

1. For any context Γ it is decidable whether Γ ⊢ ok.

2. For any context Γ, type expression T, and kind K, it is decidable whether Γ ⊢ T : K.

Proof: Lemma 3.3 and proposition 3.4 imply that context formation rules and kinding rules determine an algorithm to check context judgements and kinding judgements, and lemma 4.2 implies that this algorithm terminates. □

5 Decidability of subtyping

In the solution for the second order lambda calculus presented in [26], the distributivity rules for intersection types are not considered as rewrite rules. For that reason, new syntactic categories have to be defined (composite and individual canonical types) and an auxiliary mapping (flattening) transforms a type into a canonical type. Our solution does not need either new syntactic categories or elaborate auxiliary mappings, since the role played there by canonical types is performed here by types in normal form.

After the work in [13] was completed, Steffen and Pierce proved a similar result for F_{≤}^{ω} [28]. There are several differences between our work and the proof of decidability of subtyping in [28]. Our result is for a stronger system which also includes intersection types, and implies the result for F_{≤}^{ω}. Moreover, our proof of termination has the novel idea of using a choice operator to model the behavior of type variables during subtype checking.

An important property of derivation systems is the information that a derivable judgement contains about its proofs. This information is essential to produce results which not only state properties about the subproofs, but also help identify ill formed judgements. Consider the following example.

Example 5.1 In F_{∧}^{ω} we can prove: W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K ⊢ X(Z W) ≤

W. Note that X and Z are subtypes of the identity on K, therefore it makes sense for X(Z W) to be a subtype of W. The derivation is as follows. Let Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K. For the sake of readability we omit kinding judgements.

Γ ⊢ ok
\overline{S-TVar}
Γ ⊢ X ≤ ΛY:K.Y
\overline{S-OApp}
Γ ⊢ X(Z W) ≤ (ΛY:K.Y)Z W

(ΛY:K.Y)Z W =_{β∧} Z W ; \overline{S-Conv} ; (ΛY:K.Y)Z W ≤ Z W

\overline{S-Trans}
Γ ⊢ X(Z W) ≤ Z W
Γ ⊢ ok ; \overline{S-TVar} ; Γ ⊢ Z ≤ X

Γ ⊢ ok

\overline{S-TVar}

Γ ⊢ X ≤ ΛY:K.Y

\overline{S-Trans}

Γ ⊢ Z ≤ (ΛY:K.Y)
\overline{S-OApp}
Γ ⊢ Z W ≤ (ΛY:K.Y)W

(ΛY:K.Y)W =_{β∧} W ; \overline{S-Conv} ; (ΛY:K.Y)W ≤ W

\overline{S-Trans}
Γ ⊢ Z W ≤ W
Γ ⊢ X(Z W) ≤ Z W Γ ⊢ Z W ≤ W
\overline{S-Trans}
Γ ⊢ X(Z W) ≤ W

This simple example already shows that S-Trans erases information obtained by S-Conv that is not present in the conclusion any longer.

5.1 A subtype checking algorithm, AlgF_{∧}^{ω}

Subtyping statements in AlgF_{∧}^{ω} are written Γ ⊢_{Alg} S ≤ T, and S, T, and all types appearing in Γ are in β∧-normal form. A, B, and C range over types whose outermost constructor is not an intersection.

Remark 5.1.1 It is an immediate consequence of the β∧-reduction rules that, if T is in β∧-normal form, then T is either X, S→A, ∀X≤S:K.A, ΛX:K.A, A S where A is not an abstraction, or ⋀^{K}[A_{1}..A_{n}]. We frequently use this notation as a reminder of the shape of types in normal form.

We now define lub_{Γ}(S). In [12], it is proved that, when defined, it is the smallest type beyond S with respect to Γ.

Definition 5.1.2 (Least strict Upper Bound)

lub_{Γ}(X) = Γ(X),
lub_{Γ}(T S) = lub_{Γ}(T) S.

Definition 5.1.3 (AlgF_{∧}^{ω} subtyping rules)

\frac{Γ ⊢ X : K}{Γ ⊢_{Alg} X ≤ X}  (AlgS-TVarRefl)

\frac{Γ ⊢ T S : K}{Γ ⊢_{Alg} T S ≤ T S}  (AlgS-OAppRefl)

\frac{Γ ⊢_{Alg} Γ(X) ≤ A  X ≢ A}{Γ ⊢_{Alg} X ≤ A}  (AlgS-TVar)

\frac{Γ ⊢_{Alg} T ≤ S  Γ ⊢_{Alg} A ≤ B  Γ ⊢ S→A : ⋆}{Γ ⊢_{Alg} S→A ≤ T →B}  (AlgS-Arrow)

\frac{Γ, X≤S:K ⊢_{Alg} A ≤ B  Γ ⊢ ∀X≤S:K.A : ⋆}{Γ ⊢_{Alg} ∀X≤S:K.A ≤ ∀X≤S:K.B}  (AlgS-All)

\frac{Γ, X≤⊤^{K}:K ⊢_{Alg} A ≤ B}{Γ ⊢_{Alg} ΛX:K.A ≤ ΛX:K.B}  (AlgS-OAbs)

\frac{Γ ⊢_{Alg} (lub_{Γ}(T S))^{nf} ≤ A  Γ ⊢ T S : K  T S ≢ A}{Γ ⊢_{Alg} T S ≤ A}  (AlgS-OApp)

\frac{∀i ∈ \{1..m\} Γ ⊢_{Alg} A ≤ A_{i}  Γ ⊢ A : K}{Γ ⊢_{Alg} A ≤ ⋀^{K}[A_{1}..A_{m}]}  (AlgS-∀)

\frac{∃j ∈ \{1..n\} Γ ⊢_{Alg} A_{j} ≤ A  ∀k ∈ \{1..n\} Γ ⊢ A_{k} : K}{Γ ⊢_{Alg} ⋀^{K}[A_{1}..A_{n}] ≤ A}  (AlgS-∃)

\frac{∀i ∈ \{1..m\} ∃j ∈ \{1..n\} Γ ⊢_{Alg} A_{j} ≤ B_{i}  ∀k ∈ \{1..n\} Γ ⊢ A_{k} : K}{Γ ⊢_{Alg} ⋀^{K}[A_{1}..A_{n}] ≤ ⋀^{K}[B_{1}..B_{m}]}  (AlgS-∀∃)

In [15, 12] it was proved that this algorithm is equivalent to the original subtyping system.

Proposition 5.1.4 (Equivalence of ordinary and algorithmic subtyping)

Let Γ ⊢ S : K and Γ ⊢ T : K. Then Γ ⊢ S ≤ T if and only if Γ^{nf} ⊢_{Alg} S^{nf} ≤ T^{nf}.

Now first let’s go back to our example.

5.2 Example

In this section, we give the derivation in AlgF_{∧}^{ω} of the example 5.1 (also mentioned in the introduction). Let Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K. We present a proof in the normal system of Γ^{nf} ⊢_{n} X(Z W)^{nf} ≤ W^{nf}, which is the translation of Γ ⊢ X(Z W) ≤ W.

Observe that \begin{matrix}Γ^{nf} ≡ Γ, \\ (X(Z W))^{nf} ≡ X(Z W), and \\ W^{nf} ≡ W. \end{matrix}

For the sake of readability we omit kinding judgements. The derivation in normal form in AlgF_{∧}^{ω} is substantially shorter than the one in F_{∧}^{ω} shown in section 5.

Γ ⊢ W : K
\overline{AS-Refl}
Γ ⊢_{n} ((ΛY:K.Y)W)^{nf} ≤ W
\overline{AS-OApp}
Γ ⊢_{n} X W ≤ W
\overline{AS-OApp}
Γ ⊢_{n} ((ΛY:K.Y)(Z W))^{nf} ≤ W
\overline{AS-OApp}
Γ ⊢_{n} X(Z W) ≤ W

5.3 Termination of subtype checking

To establish the decidability of the subtyping relation of F_{∧}^{ω} we prove the termination or well-foundedness of the relation defined by the AlgF_{∧}^{ω} subtyping rules. We show this by reducing the well-foundedness of AlgF_{∧}^{ω} to the strong normalization property of the →_{β∧+} relation.

We begin by extending the language of types with the constructor + as follows.

𝕋^{+} ::= X  type variable
| 𝕋^{+}→𝕋^{+}  function type
| ∀(X≤𝕋^{+}:𝕂)𝕋^{+} polymorphic type
| Λ(X:𝕂)𝕋^{+}  operator abstraction
| 𝕋^{+} 𝕋^{+}  operator application
| ⋀^{𝕂}[𝕋^{+}..𝕋^{+} ] intersection at kind 𝕂
| 𝕋^{+} + 𝕋^{+}  choice

Since we have enriched the language of types with a new type constructor, we need to extend our kinding judgements (section 2.4) with the following kinding rule.

\frac{Γ ⊢_{+} S : K  Γ ⊢_{+} T : K}{Γ ⊢_{+} S + T : K}  (K-Plus)

The reduction →_{β∧+} is obtained from →_{β∧} by adding the reductions associated with the choice operator +, S + T →_{β∧+} S and S + T →_{β∧+} T. We also need the corresponding kinding rule saying that Γ ⊢ S + T : K whenever Γ ⊢ S, T : K. As far as we are aware, choice operators have not been used before to analyze subtyping.

Notation 5.3.1 We write + modulo commutativity and associativity.

We now define a new reduction →_{β∧+}.

Definition 5.3.2 (→_{β∧+}) The reduction on types →_{β∧+} is obtained from →_{β∧} (definition 2.1.1) by adding the following two rules:

1. S + T →_{β∧+} S, and

2. S + T →_{β∧+} T.

We also write →_{+} to refer to these two new reduction rules.

As usual, →_{β∧+} is extended to become a compatible relation with respect to type formation, ↠_{β∧+} is the reflexive, transitive closure of →_{β∧+}, and =_{β∧+} is the reflexive, symmetric, and transitive closure of →_{β∧+}.

Proposition 5.3.3 (Strong normalization for →_{β∧+})

If Γ ⊢_{+} T : K, then every β∧+-reduction sequence starting from T is finite.

Proof: The result follows using the strategy used to prove that the reduction →_{β∧} is strongly normalizing on well kinded types (see [15, 12]). We only need to modify the definition of saturated sets by adding the following closure condition: if T, U, R_{1}..R_{n} ∈ SN^{+}, then T R_{1}..R_{n} ∈ S and UR_{1}..R_{n} ∈ S imply (T + U)R_{1}..R_{n} ∈ S. □

Next, we define a measure for subtyping statements such that, given a subtyping rule, the measure of each hypothesis is smaller than that of the conclusion. Most measures for showing the well-foundedness of a relation defined by a set of inference rules involve a clever assignment of weights to judgements, often involving the number of symbols. We need a more sophisticated measure, since in AlgS-OApp it is not necessarily the case that the size of the hypothesis is smaller than the size of the conclusion.

We introduce a new mapping from types to types in the extended language in order to define a new measure on subtyping statements. To motivate the definition of this new measure, we analyze the behavior of type variables during subtype checking. Assume that we want to check if Γ ⊢_{Alg} S ≤ T, where S is a variable or a type application. It can be the case that the judgement is obtained with an application of AlgS-TVar or AlgS-OApp, in which case we have to consider a new statement Γ ⊢_{Alg} S′ ≤ T, where S′ is obtained from S by replacing a variable by its bound (and eventually normalizing). However, we do not replace every variable by its bound, as this would constitute an unsound operation with respect to subtyping. Consider the following example.

Example 5.3.4 Two unrelated variables may have the same bound.

\begin{matrix}X≤⊤^{⋆}:⋆, Y ≤⊤^{⋆}:⋆ ⊬ X ≤ Y, but \\ X≤⊤^{⋆}:⋆, Y ≤⊤^{⋆}:⋆ ⊢ ⊤^{⋆} ≤ ⊤^{⋆}. \end{matrix}

Our new mapping, plus, includes in each type expression this nondeterministic behavior of its type variables.

Definition 5.3.5 (plus)

The mapping plus_{Γ} : 𝕋→𝕋^{+} is defined as follows.

1. plus_{Γ_{1}, X≤T:K, Γ_{2}}(X) = X + plus_{Γ_{1}}(T),

2. plus_{Γ}(T →S) = plus_{Γ}(T)→plus_{Γ}(S),

3. plus_{Γ}(∀X≤T:K.S) = ∀X≤plus_{Γ}(T):K.plus_{Γ,X≤T:K}(S),

4. plus_{Γ}(ΛX:K.S) = ΛX:K.plus_{Γ,X:K}(S),

5. plus_{Γ}(S T) = plus_{Γ}(S) plus_{Γ}(T),

6. plus_{Γ}(⋀^{K}[S_{1}..S_{n}]) = ⋀^{K}[plus_{Γ}(S_{1})..plus_{Γ}(S_{n})].

Example 5.3.6 plus_{X≤⊤^{⋆}:⋆, Y ≤X:⋆, Z≤Y:⋆}(Z) = Z + Y + X + ⊤^{⋆}.

We need to show that plus is well defined on well kinded arguments.

Lemma 5.3.7 (Well-foundedness of plus) If Γ ⊢ T : K, then plus_{Γ}(T) is defined.

Proof: Observe that the size_{j} of the kinding judgements of the arguments strictly decreases in each recursive call. Consider

rank_{Γ}(S) = size_{j}(Γ ⊢ S : kind(Γ, S)),

where size_{j}(Γ ⊢ S : K) is the size of the derivation of the kinding judgement (see definition 4.1). The function kind can be defined straightforwardly using proposition 3.4, such that kind(Γ, S) = K if Γ ⊢ S : K, and gives a constant NoKind otherwise. Moreover, lemma 4.2 implies that the function kind is total. Given that Γ ⊢ S : K, by lemmas 3.3(1) and 3.4, the rank decreases in each recursive call and the least value is that of size_{j}(⊢ ⊤^{K} : K). □

Lemma 5.3.8 If Γ ⊢ T : K, then Γ ⊢_{+} plus_{Γ}(T) : K.

Proof: By induction on the derivation of Γ ⊢ T : K, observing that Γ ⊢ T : K implies Γ ⊢_{+} T : K. It is straightforward to verify that ⊢_{+} satisfies weakening using renamings (see corollary 3.7). We consider here the case for K-TVar, the rest follows by straightforward induction. We are given, Γ_{1}, X ≤ T:K, Γ_{2} ⊢ ok. By lemma 3.3, there is a proper subderivation of Γ_{1} ⊢ T : K. Finally, the result follows by the induction hypothesis, weakening, and K-Plus. □

Lemma 5.3.9 (Strengthening for plus)

1. Let X ∉ FTV(Γ_{2}) ∪ FTV(S). Then Γ_{1}, X≤T_{X}:K_{X}, Γ_{2} ⊢ S : K implies plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}}(S) = plus_{Γ_{1}, Γ_{2}}(S).

2. Γ_{1}, x:T , Γ_{2} ⊢ S : K implies plus_{Γ_{1}, x:T , Γ_{2}}(S) = plus_{Γ_{1}, Γ_{2}}(S).

Proof:

1. By lemma 5.3.7, plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}}(S) is defined, therefore we can reason by induction on the number of unfolding steps of plus. We proceed by case analysis on the form of S.

S ≡ Y. We have to consider two cases.

(a) Γ_{1} ≡ Δ_{1}, Y ≤T_{1}:K_{1}, Δ_{2}. Then, by definition,

plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}}(Y) = Y + plus_{Δ_{1}}(T_{1}). On the other hand, also by the definition of plus,

plus_{Γ_{1}, Γ_{2}}(Y) = Y + plus_{Δ_{1}}(T_{1}).

(b) Γ_{2} ≡ Δ_{1}, Y ≤T_{1}:K_{1}, Δ_{2}. By the definition of plus,

plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}}(Y) = Y + plus_{Γ_{1}, X≤T_{X}:K_{X}, Δ_{1}}(T_{1}). By lemma 3.1,

Γ_{1}, X≤T_{X}:K_{X}, Γ_{2} ⊢ ok, and, by lemma 3.3(1),

Γ_{1}, X≤T_{X}:K_{X}, Δ_{1} ⊢ T_{1} : K_{1}. Moreover, since X ∉ FTV(Γ_{2}), it follows that X ∉ FTV(Δ_{1}) ∪ FTV(T_{1}). Then, applying the induction hypothesis we obtain

Y + plus_{Γ_{1}, X≤T_{X}:K_{X}, Δ_{1}}(T_{1}) = Y + plus_{Γ_{1}, Δ_{1}}(T_{1}), and the result follows by the definition of plus.

S ≡ ∀Y ≤T_{1}:K_{1}.T_{2}. By the definition of plus,

plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}}(∀Y ≤T_{1}:K_{1}.T_{2}) = ∀Y ≤plus_{Γ_{1}, ≤T_{X}:K_{X}, Γ_{2}}(T_{1}):K_{1}.plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}, Y ≤T_{1}:K_{1}}(T_{2}).

By generation for kinding (proposition 3.4),

Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}, Y ≤T_{1}:K_{1} ⊢ T_{2} : ⋆,

and, since X ∉ FTV(Γ_{2}, Y ≤T_{1}:K_{1}) ∪ FTV(T_{2}), by the induction hypothesis,

∀Y ≤plus_{Γ_{1}, ≤T_{X}:K_{X}, Γ_{2}}(T_{1}):K_{1}.plus_{Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}, Y ≤T_{1}:K_{1}}(T_{2}) = ∀Y ≤plus_{Γ_{1}, ≤T_{X}:K_{X}, Γ_{2}}(T_{1}):K_{1}.plus_{Γ_{1}, Γ_{2}, Y ≤T_{1}:K_{1}}(T_{2}).

By lemma 3.1,

Γ_{1}, X≤T_{X}:K_{X}, Γ_{2}, Y ≤T_{1}:K_{1} ⊢ ok,

by generation for context judgements (lemma 3.3(1)),

Γ_{1}, X≤T_{X}:K_{X}, Γ_{2} ⊢ T_{1} : K_{1}.

Since X ∉ FTV(Γ_{2}) ∪ FTV(T_{1}), by the induction hypothesis,

∀Y ≤plus_{Γ_{1}, ≤T_{X}:K_{X}, Γ_{2}}(T_{1}):K_{1}.plus_{Γ_{1}, Γ_{2}, Y ≤T_{1}:K_{1}}(T_{2}) = ∀Y ≤plus_{Γ_{1}, Γ_{2}}(T_{1}):K_{1}.plus_{Γ_{1}, Γ_{2}, Y ≤T_{1}:K_{1}}(T_{2}) = plus_{Γ_{1}, Γ_{2}}(∀Y ≤T_{1}:K_{1}.T_{2}).

For all the other cases, the result follows by straightforward application of the induction hypothesis, using generation for kinding (proposition 3.4).

2. The definition of plus does not depend on the assumptions of term variables. □

Lemma 5.3.10 (Weakening for plus) If Γ′ ⊢ ok, Γ ⊆ Γ′, and Γ ⊢ S : K, then plus_{Γ}(S) = plus_{Γ′}(S).

Proof: The assumptions ensure that plus_{Γ}(S) is defined, so we can proceed by induction on the number of unfolding steps of the definition of plus. We proceed by case analysis on the form of S.

S ≡ X. By generation for kinding (proposition 3.4) and the fact that Γ ⊆ Γ′,

Γ ≡ Γ_{1}, X≤T:K, Γ_{2} and Γ′ ≡ Γ′_{1}, X≤T:K, Γ′_{2}.

There are two cases to consider.

1. If Γ_{1} ≡ Γ′_{1}, then the result follows by the definition of plus.

2. If Γ_{1} ≢ Γ′_{1}, then Γ_{1} ⊆ Γ′_{1} ∪ Γ′_{2}. By the definition of plus,

plus_{Γ}(X) = X + plus_{Γ_{1}}(T).

By lemmas 3.1 and 3.3(1), it follows that Γ_{1} ⊢ T : K. Hence, by the induction hypothesis,

X + plus_{Γ_{1}}(T) = X + plus_{Γ′}(T).

Since Γ′ ⊢ ok, from lemma 3.3(1), it follows that Γ′_{1} ⊢ T : K. Consequently, ({X}∪FTV(Γ′_{2}))∩FTV(T) = ∅ by the free variables lemma (lemma 3.2). Hence, starting from the last declaration in Γ′_{2}, we can iterate the strengthening lemma for plus (lemma 5.3.9 items 1 and 2) to obtain

X + plus_{Γ′}(T) = X + plus_{Γ′_{1}}(T) = plus_{Γ′}(X).

S ≡ ∀X≤T_{1}:K_{1}.T_{2}. We have that Γ ⊢ ∀X≤T_{1}:K_{1}.T_{2} : ⋆, by generation for kinding (proposition 3.4).

Let Z be a new type variable, in particular Z ∉ dom(Γ′). Then, by α-conversion, S =_{α} ∀Z≤T_{1}:K_{1}.T_{2}[X←Z].

By the definition of plus,

plus_{Γ}(S) =_{α} plus_{Γ}(∀Z≤T_{1}:K_{1}.T_{2}[X←Z])
= ∀Z≤plus_{Γ}(T_{1}):K_{1}.plus_{Γ, Z≤T_{1}:K_{1}}(T_{2}[X←Z]).

By generation for kinding and lemmas 3.1 and 3.3(1), it follows that Γ ⊢ T_{1} : K_{1}. Then, by the induction hypothesis, ∀Z≤plus_{Γ}(T_{1}):K_{1}.plus_{Γ, Z≤T_{1}:K_{1}}(T_{2}[X←Z]) = ∀Z≤plus_{Γ′}(T_{1}):K_{1}.plus_{Γ, Z≤T_{1}:K_{1}}(T_{2}[X←Z]).

By generation for kinding, Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆ , and by renaming (lemma 3.6), we have that Γ, Z≤T_{1}:K_{1} ⊢ T_{2}[X←Z] : ⋆. (Taking the renaming that maps X to Z and is the identity elsewhere.)

Applying again the induction hypothesis, it follows that

∀Z≤plus_{Γ′}(T_{1}):K_{1}.plus_{Γ, Z≤T_{1}:K_{1}}(T_{2}[X←Z])
= ∀Z≤plus_{Γ′}(T_{1}):K_{1}.plus_{Γ′, Z≤T_{1}:K_{1}}(T_{2}[X←Z])
= plus_{Γ′}(∀Z≤T_{1}:K_{1}.T_{2}[X←Z])
=_{α} plus_{Γ′}(S).

The case for S ≡ ΛX:K.T is similar to the last case. In all other cases, the proof follows by straightforward application of the induction hypothesis. □

The operation plus does not have the usual properties under substitution; as following example shows, the equality

plus_{Γ_{1}, X≤S:K_{1}, Γ_{2}}(T_{2})[X←plus_{Γ_{1}}(T_{1})] = plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(T_{2}[X←T_{1}])

does not hold in general.

Example 5.3.11 Consider the case where Γ_{1} ≡ Y ≤⊤^{⋆}:⋆, Γ_{2} ≡ ∅, S ≡ Y, T_{1} ≡ Y, and T_{2} ≡ X. Then

plus_{Y ≤⊤^{⋆}:⋆, X≤Y:⋆}(X)[X←plus_{Y ≤⊤^{⋆}:⋆}(Y)] = (X + Y + ⊤^{⋆})[X←(Y + ⊤^{⋆})]
= Y + ⊤^{⋆} + Y + ⊤^{⋆}.

On the other hand,

plus_{Y ≤⊤^{⋆}:⋆}(X[X←Y]) = plus_{Y ≤⊤^{⋆}:⋆}(Y) = Y + ⊤^{⋆}.

We therefore need a lemma which says that the well-formed types are well-behaved under substitution with respect to the plus operation.

Lemma 5.3.12 (Substitution for plus) If Γ_{1}, X≤S:K_{1}, Γ_{2} ⊢ T_{2} : K_{2} and Γ_{1} ⊢ T_{1} : K_{1}, then

plus_{Γ_{1}, X≤S:K_{1}, Γ_{2}}(T_{2})[X←plus_{Γ_{1}}(T_{1})] ↠_{β∧+} plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(T_{2}[X←T_{1}]).

Proof: By induction on the size of the derivation of Γ_{1}, X≤S:K_{1}, Γ_{2} ⊢ T_{2} : K_{2}. We proceed by case analysis on the form of T_{2}.

T_{2} ≡ Y. By the free variables lemma (lemma 3.2), Y ∈ dom(Γ_{1}, X≤S:K_{1}, Γ_{2}). Then there are three cases to consider.

Y ∈ dom(Γ_{1}). Let Γ_{1} ≡ Δ_{1}, Y ≤U:K, Δ_{2}. Then

plus_{Γ_{1}, X≤S:K_{1}, Γ_{2}}(Y)[X←plus_{Γ_{1}}(T_{1})],

by the definitions of plus and substitution, = Y + (plus_{Δ_{1}}(U)[X←plus_{Γ_{1}}(T_{1})])

since X ∉ FTV(U) ∪ FTV(Δ_{1}), X ∉ FTV(plus_{Δ_{1}}(U)). = Y + plus_{Δ_{1}}(U), = plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(Y [X←T_{1}]).

Y ≡ X. Then

plus_{Γ_{1}, X≤S:K_{1}, Γ_{2}}(X)[X←plus_{Γ_{1}}(T_{1})],

by the definitions of plus and substitution, = plus_{Γ_{1}}(T_{1}) + (plus_{Δ_{1}}(U)[X←plus_{Γ_{1}}(T_{1})]), →_{+} plus_{Γ_{1}}(T_{1}). On the other hand, plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(X[X←T_{1}]) = plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(T_{1}),

since FTV(T_{1}) ∪ dom(Γ_{1}), by strengthening for plus(5.3.9), = plus_{Γ_{1}}(T_{1}).

Y ∈ dom(Γ_{2}). Let Γ_{2} ≡ Δ_{1}, Y ≤U:K, Δ_{2}. Then

plus_{Γ_{1}, X≤S:K_{1}, Γ_{2}}(Y)[X←plus_{Γ_{1}}(T_{1})],

by the definitions of plus and substitution, = Y + (plus_{Γ_{1}, X≤S:K_{1}, Δ_{1}}(U)[X←plus_{Γ_{1}}(T_{1})]),

by generation (3.4) and the induction hypothesis, →_{β∧+} Y + plus_{Γ_{1}, Δ_{1}[X←T_{1}]}(U[X←T_{1}]), = plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(Y [X←T_{1}]).

T_{2} ≡ ∀Y ≤S_{1}:K.S_{2}. Let Γ ≡ Γ_{1}, X≤S:K_{1}, Γ_{2}. Then

plus_{Γ}(∀Y ≤S_{1}:K.S_{2})[X←plus_{Γ_{1}}(T_{1})],

by the definitions of plus and substitution, = ∀Y ≤plus_{Γ}(S_{1})[X←plus_{Γ_{1}}(T_{1})]:K.plus_{Γ, Y ≤S_{1}:K}(S_{2})[X←plus_{Γ_{1}}(T_{1})],

by generation (proposition 3.4) and the induction hypothesis, →_{β∧+} ∀Y ≤plus_{Γ_{1}, Γ_{2}[X←T_{1}]}(S_{1}[X←T_{1}]):K.

plus_{Γ_{1}, Γ_{2}[X←T_{1}], Y ≤S_{1}[X←T_{1}]:K}(S_{2}[X←T_{1}])

by the definitions of plus and substitution, = plus_{Γ_{1}, Γ_{2}[X←T_{1}]}((∀Y ≤S_{1}:K.S_{2})[X←T_{1}]).

Other cases. All the other cases are similar to the case T_{2} ≡ ∀Y ≤S_{1}:K.S_{2}. □

Lemma 5.3.13 (Monotonicity of plus with respect to →_{β∧}) If Γ ⊢ T : K, then

1. Γ →_{β∧} Γ′ implies plus_{Γ}(T) ↠_{β∧+} plus_{Γ′}(T).

2. T →_{β∧} T′ implies plus_{Γ}(T) ↠_{β∧+}^{>0} plus_{Γ}(T′).

Proof: By simultaneous induction on the size of the derivation of Γ ⊢ T : K. We proceed by case analysis on the form of T.

1. Γ →_{β∧} Γ′.

T ≡ X. Let Γ ≡ Γ_{1}, X≤S:K_{1}, Γ_{2}. Then we have to consider three cases.

(a) Γ_{1} →_{β∧} Γ′_{1}. Then

plus_{Γ}(X) = X + plus_{Γ_{1}}(S)

by lemma 3.3 and part (1) of the induction hypothesis, ↠_{β∧} X + plus_{Γ′_{1}}(S) = plus_{Γ′_{1}}(X).

(b) S →_{β∧} S′. By lemma 3.3 and part (2) of the induction hypothesis.

(c) Γ_{2} →_{β∧} Γ′_{2}. By the definition of plus.

T ≡ ∀X≤T_{1}:K_{1}.T_{2}. By generation for kinds (proposition 3.4), there are proper subderivations of Γ ⊢ T_{1} : K_{1} and Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆. Then, by part (1) of the induction hypothesis, it follows that

plus_{Γ}(T_{1}) ↠_{β∧} plus_{Γ′}(T_{1}), and
plus_{Γ, X≤T_{1}:K_{1}}(T_{2}) ↠_{β∧} plus_{Γ′, X≤T_{1}:K_{1}}(T_{2}).

The result follows by the definitions of plus and ↠_{β∧}.

Other cases. The rest of the cases are similar to the case T ≡ ∀X≤T_{1}:K_{1}.T_{2}, using generation for kinding (proposition 3.4) and part 1 of the induction hypothesis.

2. T →_{β∧} T′.

T ≡ ∀X≤T_{1}:K_{1}.T_{2}. We have to consider three cases.

(a) T_{1} →_{β∧} T′_{1}. By generation for kinding (proposition 3.4), there are proper subderivations of Γ ⊢ T_{1} : K_{1} and Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆. Then, by parts (2) and (1) of the induction hypothesis respectively, it follows that

plus_{Γ}(T_{1}) ↠_{β∧}^{>0} plus_{Γ}(T′_{1}), and
plus_{Γ, X≤T_{1}:K_{1}}(T_{2}) ↠_{β∧} plus_{Γ, X≤T_{1}′:K_{1}}(T_{2}).

The result follows by the definitions of plus and ↠_{β∧}.

(b) T_{2} →_{β∧} T′_{2}. By part (2) of the induction hypothesis.

(c) ∀X≤T_{1}:K_{1}.⋀^{⋆}[S_{1}..S_{n}] →_{β∧} ⋀^{⋆}[∀X≤T_{1}:K_{1}.S_{1}..∀X≤T_{1}:K_{1}.S_{n}].

plus_{Γ}(∀X≤T_{1}:K_{1}.⋀^{⋆}[S_{1}..S_{n}])
= ∀X≤plus_{Γ}(T_{1}):K.⋀^{⋆}[plus_{Γ, X≤T_{1}:K_{1}}(S_{1})..plus_{Γ, X≤T_{1}:K_{1}}(S_{n})]
→_{β∧+} ^{⋀⋆}[∀X≤plus_{Γ}(T_{1}):K.plus_{Γ, X≤T_{1}:K_{1}}(S_{1})..
..∀X≤plus_{Γ}(T_{1}):K.plus_{Γ, X≤T_{1}:K_{1}}(S_{n})]
= plus_{Γ}(⋀^{⋆}[∀X≤T_{1}:K_{1}.S_{1}..∀X≤T_{1}:K_{1}.S_{n}])

T ≡ T_{1} T_{2}. We have to consider four cases.

(a) T_{1} →_{β∧} T′_{1},

(b) T_{2} →_{β∧} T′_{2},

(c) T ≡ ⋀^{⋆}[S_{1}..S_{n}] and ⋀^{⋆}[S_{1}..S_{n}]T_{2} →_{β∧} ⋀^{⋆}[S_{1} T_{2}..S_{n} T_{2}].

(d) T ≡ ΛX:K.S_{1} and (ΛX:K.S_{1}) T_{2} →_{β∧} S_{1}[X←T_{2}]

Cases 2a, 2b, and 2c follow using similar arguments to those used for the case T ≡ ∀X≤T_{1}:K_{1}.T_{2}. Consider case 2d. plus_{Γ}((ΛX:K.S_{1}) T_{2}) = (ΛX:K.plus_{Γ, X≤⊤^{K}:K}(S_{1}))plus_{Γ}(T_{2})

→_{β∧} plus_{Γ, X≤⊤^{K}:K}(S_{1})[X←plus_{Γ}(T_{2})],

by lemma 5.3.12, ↠_{β∧+} plus_{Γ}(S_{1}[X←T_{2}]).

Other cases. The rest of the cases follows using a similar argument to the one used in the case T ≡ ∀X≤T_{1}:K_{1}.T_{2}. □

Lemma 5.3.14 Let lub_{Γ}(S) be defined and Γ ⊢ S : K. Then plus_{Γ}(S) ↠_{+}^{>0} plus_{Γ}(lub_{Γ}(S)).

Proof: By induction on the structure of S. Since lub_{Γ}(S) is defined, it is enough to consider the following two cases.

S ≡ X. Let Γ ≡ Γ_{1}, X ≤ T:K, Γ_{2}.

plus_{Γ}(X) = X + plus_{Γ_{1}}(T)
= X + plus_{Γ}(T)  by weakening (lemma 5.3.10),
→_{+} plus_{Γ}(T)
= plus_{Γ}(lub_{Γ}(X))

S ≡ A T. By the induction hypothesis. □

Our measure to show the well-foundedness of AlgF_{∧}^{ω} considers the β∧+-reduction paths of the plus versions of the types in the subtyping judgements. As we mentioned before, in AlgS-TVar and AlgS-OApp the types appearing in the hypothesis may be larger than those in their conclusions. Therefore, the well foundedness of the AlgF_{∧}^{ω} relation is not immediate. The next corollary gathers the previous results to serve our purposes.

6 OUR DECIDABILITY PROOF AND FULL F_{≤} 23

Corollary 5.3.15

1. If Γ ⊢ X : K, then plus_{Γ}(X) ↠_{β∧+}^{>0} plus_{Γ}(Γ(X)).

2. If Γ ⊢ A T : K then plus_{Γ}(A T) ↠_{β∧+}^{>0} plus_{Γ}(lub_{Γ}(A T)^{nf}).

Proof: Item 1 is a particular case of the previous lemma (lemma 5.3.14), and item 2 is a consequence of lemma 5.3.14 and the monotonicity of plus with respect to →_{β∧+} (5.3.13(2)). □

Finally, we can define our measure.

Definition 5.3.16 (Weight)

1. weight(Γ ⊢_{Alg} S ≤ T) = <max-red(plus_{Γ}(S)) + max-red(plus_{Γ}(T)), size_{j}(Γ ⊢ S ≤ T)>,

2. weight(Γ ⊢ T : K) = <0, 0>,

where max-red(S) is the length of a maximal β∧+-reduction path starting from S, and size_{j} is defined in definition 4.1.

Pairs are ordered lexicographically. Note that <0, 0> is the least weight.

Proposition 5.3.17 (Well-foundedness of AlgF_{∧}^{ω})

If \begin{aligned}J_{1} & .. & J_{n} \\ & J \end{aligned} is an AlgF_{∧}^{ω} rule, then weight(J_{i}) < weight(J), for each i ∈ \{1..n\}.

Proof: By inspection of the rules of AlgF_{∧}^{ω}. □ Finally, we can state the main result of this section.

Theorem 5.3.18 (Decidability of subtyping in F_{∧}^{ω})

For any context Γ and for any two types S and T, it is decidable whether Γ ⊢ S ≤ T.

6 Our decidability proof and full F_{≤}

In the introduction we mentioned that subtyping in F_{≤}, a second-order λ-calculus with bounded quantification defined by Curien and Ghelli in 1989, is undecidable. A question that comes to mind is: if we try to apply our proof of the decidability of subtyping in F_{∧}^{ω} to F_{≤}, where will it fail?

If we consider the algorithm for the subtyping relation in [21], the place where our proof does not go through is when we try to prove that the algorithm terminates by calculating the maximal length of the plus versions of the types in the rule for subtyping quantified types. Remember that the subtyping rule for quantified types in full F_{≤} is:

\frac{Γ ⊢ T_{1} ≤ S_{1} Γ, X≤T_{1} ⊢ S_{2} ≤ T_{2}}{Γ ⊢ ∀X≤S_{1}. S_{2} ≤ ∀X≤T_{1}. T_{2}}  (F_{≤}- S-All)

Consider now the following case.

\begin{aligned}Γ & ≡ & Y_{4}≤⊤^{⋆}, Y_{3}≤Y_{4}, Y_{2}≤Y_{3}, Y_{1}≤Y_{2}, \\ T_{1} & ≡ & Y_{1}, \\ S_{1} & ≡ & ⊤^{⋆}, \\ T_{2} & ≡ & X→X, and \\ S_{2} & ≡ & X→X. \end{aligned}

The plus versions of the types in the subtyping statements of this example are as follows.

plus_{Γ, X≤Y_{1}}(S_{2}) ≡ (X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆})→(X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆}) plus_{Γ, X≤Y_{1}}(T_{2}) ≡ (X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆})→(X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆}) plus_{Γ}(∀X≤S_{1}. S_{2}) ≡ ∀X≤⊤^{⋆}. (X + ⊤^{⋆})→(X + ⊤^{⋆}) plus_{Γ}(∀X≤T_{1}. T_{2}) ≡ ∀X≤Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆}.

(X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆})→(X + Y_{1} + Y_{2} + Y_{3} + Y_{4} + ⊤^{⋆})

The length of a maximal +-reduction in each case is:

max-red(plus_{Γ, X≤Y_{1}}(S_{2}))  = 10
max-red(plus_{Γ, X≤Y_{1}}(T_{2}))  = 10
max-red(plus_{Γ}(∀X≤S_{1}. S_{2})) = 2
max-red(plus_{Γ}(∀X≤T_{1}. T_{2})) = 14.

The weight of the conclusion Γ ⊢ ∀X≤S_{1}. S_{2} ≤ ∀X≤T_{1}. T_{2}, as defined in definition 5.3.16, is smaller than the weight of the hypothesis Γ, X≤T_{1} ⊢ S_{2} ≤ T_{2}, because the maximal length of a +-reduction starting from the plus version of the conclusion is shorter than the maximal length of a +-reduction starting from the plus version of that hypothesis. To be more precise,

max-red(plus_{Γ}(∀X≤S_{1}. S_{2})) + max-red(plus_{Γ}(∀X≤T_{1}. T_{2}))
<
max-red(plus_{Γ, X≤Y_{1}}(S_{2})) + max-red(plus_{Γ, X≤Y_{1}}(T_{2})).

7 Type checking and type inference

Motivating examples of the following definitions can be found in [15, 12].

The function lub (definition 5.1.2) is a partial function which is only defined for type variables and type applications. Here, we extend the definition of lub to intersection types in such a way that it is defined if the least upper bound is defined for at least one of the types in the intersection.

Definition 7.1 (Homomorphic extension of lub to intersections, lub^{∗})

lub_{Γ}^{∗}(X) = Γ(X),
lub_{Γ}^{∗}(S T) = lub_{Γ}^{∗}(S) T,
lub_{Γ}^{∗}(⋀^{K}[T_{1}..T_{n}]) = ⋀^{K}[T′_{1}..T′_{n}], if ∃i ∈ {1..n} such that lub_{Γ}^{∗}(T_{i})↓,

where T′_{i} is lub_{Γ}^{∗}(T_{i}), if lub_{Γ}^{∗}(T_{i})↓, and T_{i} otherwise.

We define the mapping flub which given a type T (and a context Γ) finds the smallest type larger than T (with respect to the subtype relation) having structural information to perform an application.

Definition 7.2 (Functional Least Upper Bound) The functional least upper bound of a type T, in a context Γ, flub_{Γ}(T) is defined as follows.

flub_{Γ}(T) = \{ \begin{matrix}flub_{Γ}(lub_{Γ}^{∗}(T^{nf})), & if lub_{Γ}^{∗}(T^{nf})↓; \\ T^{nf}, & otherwise.^{1} \end{matrix}

The intuition behind the definition of the function flub is to find S→T starting form W T as in the last example mentioned in the introduction. In other words, flub_{Γ′}(W T) = S→T. For simplicity we assume S→T in normal form. Step by step,

flub_{Γ′}(W T) = flub_{Γ′}(lub_{Γ′}^{∗}(W T))
= flub_{Γ′}(Z T)
= flub_{Γ′}(lub_{Γ′}^{∗}(Z T))
= flub_{Γ′}((ΛY: ⋆ .S→Y) T)
= S→T .

More generally, flub climbs the subtyping hierarchy until it finds an arrow, a quantifier, or an intersection of these two.

Definition 7.3 (arrows and alls )

1. arrows (T_{1}→T_{2})  = {T_{1}→T_{2}},

arrows (⋀^{⋆}[T_{1}..T_{n}]) = ∪_{i∈{1..n}} arrows (T_{i}),
arrows (T)  = ∅, if T ≢ T_{1}→T_{2} and T ≢ ⋀^{⋆}[T_{1}..T_{n}].

2. alls (∀X≤T_{1}:K.T_{2}) = {∀X≤T_{1}:K.T_{2}},

alls (⋀^{⋆}[T_{1}..T_{n}])  = ∪_{i∈{1..n}} alls (T_{i}),
alls (T)  = ∅, if T ≢ ∀X≤T_{1}:K.T_{2} and T ≢ ⋀^{⋆}[T_{1}..T_{n}].

1This step can be optimised in an implementation of the type checking algorithm, allowing us to avoid the normalization of T when T is either an arrow type or a quantified type.

The situation here is significantly more complex than in [26] for F_{∧}, an extension of the second order λ-calculus. There it is enough to recursively search for arrows or polymorphic types in the context, because in F_{∧} there is no reduction on types. The information to be searched for is explicit in the context, so the job done here by flub is simply an extra case in the definition of arrows and alls . Namely,

arrows (X) = arrows (Γ(X)) and
alls (X) = alls (Γ(X)).

Moreover, to prove that flub is well-founded is similar for us in complexity to proving termination of subtype checking. The similarity comes from the fact that computing flub involves replacing variables by their bounds in a given context and normalizing with respect to →_{β∧}, as in lemma 7.8. In contrast, in [26] it is enough to observe that well-formed contexts cannot contain cycles of variable references.

Notation 7.4 We introduce a new notation for intersection types. We write ⋀^{K}[T | ϕ(T)], meaning the intersection of all types T such that ϕ(T) holds. Note that this is an alternative notation to ⋀^{K}[T_{1}..T_{n}] such that ϕ(T_{i}) holds if and only if i ∈ {1..n}.

We can now define a type inference algorithm for F_{∧}^{ω}.

Definition 7.5 (A type inference algorithm, inf)

\frac{Γ_{1}, x:T , Γ_{2} ⊢ ok}{Γ_{1}, x:T , Γ_{2} ⊢_{inf} x : T}  (AT-Var)

\frac{Γ, x:T_{1} ⊢_{inf} e : T_{2}}{Γ ⊢_{inf} λx:T_{1}.e : T_{1}→T_{2}}  (AT-Abs)

\frac{Γ ⊢_{inf} f : T  Γ ⊢_{inf} a : S}{Γ ⊢_{inf} f a : ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}]}  (AT-App)

\frac{Γ, X≤T_{1}:K_{1} ⊢_{inf} e : T_{2}}{Γ ⊢_{inf} λX≤T_{1}:K_{1}.e : ∀X≤T_{1}:K_{1}.T_{2}}  (AT-TAbs)

\frac{Γ ⊢_{inf} f : T}{Γ ⊢_{inf} f S : ⋀^{⋆}[T_{i}[X←S] | ∀X≤S_{i}:K.T_{i} ∈ alls (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}]} (AT-TApp)

\frac{for all i ∈ \{1..n\} Γ ⊢_{inf} e[X←S_{i}] ∈ T_{i}}{Γ ⊢_{inf} for(X∈S_{1}..S_{n})e : ⋀^{⋆}[T_{1}..T_{n}]}  (AT-For)

The algorithmic information of rule AT-App is that in order to find a type for f a in Γ, we need to infer a type S for a and a type T for f, and to take the intersection of all the T′_{i}s such that T_{i}→S_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}.

To show that flub is well-defined we use a similar argument to that used in section 5.3 to show that the relation defined by AlgF_{∧}^{ω} is well-founded. We show in lemma 7.8 that a maximal β∧+-reduction path of the plus version of the argument of flub is strictly longer than a maximal β∧+-reduction path of the plus version of the argument of its recursive call. But first we need to show the following auxiliary result.

Lemma 7.6 If lub_{Γ}^{∗}(T) is defined, then Γ ⊢ T ≤ lub_{Γ}^{∗}(T).

Lemma 7.7 Let lub_{Γ}^{∗}(T) be defined and Γ ⊢ T : K. Then plus_{Γ}(T) ↠_{β∧+}^{>0} plus_{Γ}(lub_{Γ}^{∗}(T)).

Proof: The proof follows by induction on the structure of T. If T ≡ X or T ≡ S T, then the argument is the same as in lemma 5.3.14. The case remaining to be checked is when T ≡ ⋀^{K}[T_{1}..T_{n}]. Then

plus_{Γ}(⋀^{K}[T_{1}..T_{n}]) = ⋀^{K}[plus_{Γ}(T_{1})..plus_{Γ}(T_{n})]
plus_{Γ}(lub_{Γ}^{∗}(⋀^{K}[T_{1}..T_{n}])) = ⋀^{K}[plus_{Γ}(T′_{1})..plus_{Γ}(T′_{n})],

where T′_{1} ≡ T_{i} or T′_{i} = lub_{Γ}^{∗}(T_{i}). Since lub_{Γ}^{∗}(T) is defined, there exists j ∈ {1..n} such that lub_{Γ}^{∗}(T_{j}) is defined. Now, for every k such that lub_{Γ}^{∗}(T_{k}) is defined, by the induction hypothesis, we have that

plus_{Γ}(T_{k}) ↠_{β∧+}^{>0} plus_{Γ}(lub_{Γ}^{∗}(T_{k})).

Hence,

plus_{Γ}(⋀^{K}[T_{1}..T_{n}]) ↠_{β∧+}^{>0} plus_{Γ}(lub_{Γ}^{∗}(⋀^{K}[T_{1}..T_{n}])).  □

Lemma 7.8 (Well-foundedness of flub)

If Γ ⊢ T : K, then flub_{Γ}(T) is defined.

Proof: If lub_{Γ}^{∗}(T^{nf}) is undefined, flub terminates because →_{β∧} is strongly normalizing on well kinded types. Otherwise, define

weight(flub_{Γ}(T)) = max-red(plus_{Γ}(T)), where max-red(S) is the length of a maximal β∧+-reduction path starting from S. Lemma 5.3.8 and the strong normalization property of →_{β∧+} imply that weight is well defined and always positive on well kinded types. Since lub_{Γ}^{∗}(T^{nf}) is defined,

plus_{Γ}(T) ↠_{β∧+} plus_{Γ}(T^{nf}),  by lemma 5.3.13(2),
↠_{β∧+}^{>0} plus_{Γ}(lub_{Γ}^{∗}(T^{nf})), by lemma 7.7.

Then the weight of the arguments of flub reduces in each recursive call, which proves that flub is well-founded. □

Lemma 7.9 Let Γ ⊢ S, T : ⋆ and S =_{β∧} T. Then flub_{Γ}(S) ≡ flub_{Γ}(T).

8 Decidability of type checking and type inference

We know from [15, 12], that the algorithm inf is sound and computes minimal types for the F_{∧}^{ω} typing system.

Proposition 8.1 (Soundness of inf) If Γ ⊢_{inf} e : T, then Γ ⊢ e : T.

Proposition 8.2 (inf computes minimal types)

If Γ ⊢ e : T and Γ ⊢_{inf} e : T′, then Γ ⊢ T′ ≤ T.

The next step is to prove that the algorithm inf always terminates. This result completes the proof of decidability of type checking and type inference in F_{∧}^{ω}.

We first define a measure for terms such that the type information inside the terms is considered to have constant value. The intuition behind the definition is to find a measure on terms which is invariant under type substitution (see lemma 8.4).

Definition 8.3 (size ∥−∥)

\begin{aligned}∥x∥ & = & 1, \\ ∥λx:T.e∥ & = & 1 + ∥e∥, \\ ∥e_{1} e_{2}∥ & = & ∥e_{1}∥ + ∥e_{2}∥, \\ ∥λX≤T:K.e∥ & = & 1 + ∥e∥, \\ ∥e T ∥ & = & 1 + ∥e∥, \\ ∥for(X∈T_{1}..T_{n})e∥ & = & 1 + ∥e∥. \end{aligned}

Lemma 8.4 ∥e∥ = ∥e[X←T]∥.

Proposition 8.5 (Well-foundedness of inf)

The inference rules for inf define a terminating algorithm.

Proof: In the case of AT-Var, the termination follows from the decidability of ok judgements (see corollary 4.3(1)). Furthermore, for each rule R of inf, if Γ ⊢ e : T is a hypothesis and Γ ⊢ e′ : T′ is the conclusion of R, then ∥e∥ < ∥e′∥. Moreover, in the cases for AT-App and AT-TApp, Γ ⊢ f : T by the soundness of inf (proposition 8.1), Γ ⊢ T : ⋆ by well-kindedness of typing (proposition 3.9). Hence flub_{Γ}(T) is defined by lemma 7.8. Furthermore, arrows and alls define finite sets, and, as we proved in section 5.3, subtyping is decidable. Hence, the algorithm inf always terminates. □

We can now state and prove that type checking in F_{∧}^{ω} is decidable.

Theorem 8.6 (Decidability of type checking in F_{∧}^{ω})

For any context Γ, and for any term e and type T closed in Γ, it is decidable whether Γ ⊢ e : T.

Proof: Infer a minimal type T′ for e in Γ using inf, which is decidable by proposition 8.5, and check whether Γ ⊢ T′ ≤ T, which is also decidable by theorem 5.3.18. □

Every term e closed in a context Γ has type ⊤^{⋆}. We are interested in finding types other than ⊤^{⋆}, namely non-trivial types. Since inf computes minimal types and ⊤^{⋆} is the largest type (modulo =_{β∧}) , if a term has a non trivial type in a given context, then the algorithm inf finds it.

Theorem 8.7 (Decidability of type inference in F_{∧}^{ω})

For any context Γ and for any term e closed in Γ, it is decidable whether there exists a type T such that Γ ⊢ e : T and T ≠_{β∧} ⊤^{⋆}.

Proof: Infer a minimal type T for e in Γ using inf, which is decidable by proposition 8.5, and reduce T to normal form which is decidable because →_{β∧} is strongly normalising. Finally, check whether T^{nf} ≡ ⊤^{⋆}. □

9 Conclusions

In this paper we proved that typing in F_{∧}^{ω} is decidable. A major part of the problem is proving that the subtyping relation is decidable. A novel aspect of our proof is the use of a choice operator to model the behaviour of variables during subtype checking.

This paper contains the first proof of decidability of subtyping for a higher order lambda calculus. (The proof presented in [28] was developed afterwards and with knowledge of our proof.) The decidability of subtyping is reduced to proving the strong normalization of the language of types enriched with a choice reduction. In section 6 we show where our proof of decidability breaks if applied to the undecidable second order system F_{≤}. Because the decidability of subtyping is established for well-formed types, we also show that wellformation of types and contexts are decidable judgements. Finally, the proof of termination of typechecking uses the technology developed for the decidability of subtyping.

The work presented here has been extracted from the Ph.D thesis of the author [15]. A short version of the decidability of subtyping result has been published in CSL’94 [14], and the decidability of subtyping result was first published in [13]. The techniques developed here have been applied to study the combination of dependent types and subtyping in [1].

10 Acknowledgements

I want to express my gratitude to Mariangiola Dezani-Ciancaglini for her scientific and moral support which made the present work possible. I am also grateful for discussions with Henk Barendregt and Benjamin Pierce, and for Healfdene Goguen’s comments on previous versions.

This research was supported by the Dutch organization for scientific research, NWO-SION project Typed lambda calculus, and by a European Community TMR grant.

REFERENCES 30

References

[1] D. Aspinall and A. Compagnoni. Subtyping dependent types. In Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA., July 27-30 1996. Preliminary version July 1995.

[2] H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

[3] K. B. Bruce and J. Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992.

[4] P. Canning, W. Cook, W. Hill, W. Olthoff, and J. Mitchell. F-bounded quantification for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273–280, September 1989.

[5] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. Preliminary version in Semantics of Data Types, Kahn, MacQueen, and Plotkin, eds., Springer-Verlag LNCS 173, 1984.

[6] L. Cardelli. Types for data-oriented languages. In First Conference on Extending Database Technology, volume 303 of Lecture Notes in Computer Science. Springer-Verlag, May 1988.

[7] L. Cardelli. Notes about F_{<:}^{ω}. Unpublished manuscript, October 1990.

[8] L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC Systems Research Center Research Report #45, February 1989.

[9] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985.

[10] F. Cardone and M. Coppo. Two extensions of Curry’s type inference system. In P. Odifreddi, editor, Logic and Computer Science, number 31 in APIC Studies in Data Processing, pages 19–76. Academic Press, 1990.

[11] G. Castagna and B. Pierce. Decidable bounded quantification. In Proceedings of Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, OR. ACM, January 1994.

[12] A. Compagnoni. Subject reduction and minimal types for higher order subtyping. Technical Report ECS-LFCS-97-363, University of Edinburgh, LFCS, August 1997.

[13] A. B. Compagnoni. Subtyping in F_{∧}^{ω} is decidable. Technical Report ECS-LFCS-94-281, LFCS, University of Edinburgh, January 1994.

[14] A. B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL’94, Kazimierz, Poland, number 933 in Lecture Notes in Computer Science. Springer-Verlag, June 1995. Preliminary version available as University of Edinburgh technical report ECS-LFCS-94-281, under the title “Subtyping in F_{∧}^{ω} is decidable”, January 1994.

[15] A. B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, The Netherlands, January 1995. ISBN 90-9007860-6.

[16] A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6:469–501, 1996. Preliminary version available under the title Multiple Inheritance via Intersection Types as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer science technical report 93-18, Aug. 1993.

[17] W. R. Cook, W. L. Hill, and P. S. Canning. Inheritance is not subtyping. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 125–135, San Francisco, CA, January 1990. Also in [23].

[18] M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19:139–156, 1978.

[19] P.-L. Curien and G. Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[20] N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381– 392, 1972.

[21] G. Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Università di Pisa, March 1990. Technical report TD–6/90, Dipartimento di Informatica, Università di Pisa.

[22] J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[23] C. A. Gunter and J. C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1994.

[24] J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer–Verlag, LNCS 664, Mar. 1993.

[25] J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, January 1990. Also in [23].

[26] B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science technical report CMU-CS-91-205.

[27] B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, Apr. 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92-225, under the title “Object-Oriented Programming Without Recursive Types”.

[28] M. Steffen and B. Pierce. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994. An earlier version appeared as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, February 1994.