Subtyping Dependent Types

David Aspinall

      <da@dcs.ed.ac.uk>

LFCS, Division of Informatics

University of Edinburgh King’s Buildings

Edinburgh EH9 3JZ, U. K.

Adriana Compagnoni^{∗}

                                <abc@cs.stevens-tech.edu>

Department of Computer Science Stevens Institute of Technology Castle Point on Hudson Hoboken, NJ 07030, U. S. A.

February 8, 2000

Abstract

The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system λP, which is an abstract version of the type system of the Edinburgh Logical Framework LF. By using an equivalent formulation, we establish some important properties of the new system λP_{≤}, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking.

This is an expanded version of the paper which appeared under the same title in Proc. 11th Annual Symposium on Logic in Computer Science, IEEE 1996. Keywords: type theory, dependent types, subtyping

Contents

1 Introduction 2 1.1 Summary of application areas … 3 1.2 Combining subtyping and depen-

dent types . . . . . . . . . . . . . . 4

2 The system λP_{≤} 6 2.1 Basic properties of λP_{≤} . . . . . . 9 2.2 Towards subject reduction . . . . . 14

3 A subtyping algorithm 15 3.1 Closure under β_{2}-reduction …. 17 3.2 Soundness . . . . . . . . . . . . . . 18 3.3 Reflexivity and transitivity …. 19 3.4 Completeness . . . . . . . . . . . . 23 3.5 Equivalence . . . . . . . . . . . . . 24 3.6 Decidability . . . . . . . . . . . . . 25

4 A type-checking algorithm 26 4.1 Basic properties of the algorithm . 27 4.2 Equivalence . . . . . . . . . . . . . 28 4.3 Decidability . . . . . . . . . . . . . 32

5 Conclusion 34

∗Most of this work was done while Adriana Compagnoni was at the LFCS, Division of Informatics, University of Edinburgh, King’s Buildings, Edinburgh EH9 3JZ, U. K., and at the University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, U. K.

1 Introduction

Subtyping captures concepts from diverse areas of computer science. If A and B are sets, then A ≤ B (‘A is a subtype of B’) means that elements of A are also elements of B. If A and B are specifications, then programs satisfying the specification A also satisfy B. In object-oriented programming, if A and B are object descriptions, then A ≤ B states that where an object with interface B is expected, it is safe to use an object with interface A. If A and B are theorems, then a proof of A is also a proof of B. Understanding the essence, subtleties, and general properties of subtyping illuminates a wide area.

Dependent types are types which depend on terms. A typical example is List(n), the type of lists of length n. Dependent types are more expressive than simple types: the functional map can be given the type πn:Nat. List(n) → List(n), expressing that it is parametric in the length of lists it is applied to. More generally, type dependency can express a relationship between the input of a function and its output, which can be used to specify its behaviour. Dependent types also facilitate the encoding of logics via the judgements-as-types paradigm of the Edinburgh Logical Framework LF [17]. Suppose p is a term which encodes a formula of some logic. Then the dependent type True(p) corresponds to a truth judgement and its elements encode proofs of p. The encoded proofs are constructed from constants that encode the axioms and rules of the logic.

There are several application areas where researchers have discovered a need to combine subtyping and dependent types. In the next section we shall give an overview of these applications; here we sketch a typical example of logic representation. (We assume some familiarity with LF; another example describing datatypes for a programming language is mentioned in Section 2.)

The example is a formal system for the call-by-value λ-calculus, taken from [4]. The syntax of the call-by-value λ-calculus is the same as that of the traditional λ-calculus, but it has a restricted rule of β-equality:

(λx. M) N = M[x := N] provided N is a value

where a value is a variable or an abstraction. The restriction is achieved in LF by massaging the syntax of the encoded λ-terms. Two syntactic categories are declared:

\begin{aligned}o & : ⋆ \\ v & : ⋆ \end{aligned}

(these are types in LF; ⋆ is the kind of types).

The intention is that o is the type of all expressions whilst v is a subset of o corresponding to the expressions which are values. The λ-constructor, lda, binds terms of type v and such terms can only be variables or other terms constructed with lda. An extra constructor “!” is needed, which can be thought of as an injection function from values to expressions:

\begin{aligned}! & : v → o \\ lda & : (v → o) → v \\ app & : o → o → o \end{aligned}

For the proof system, there is an equality judgement together with constants representing axioms and rules:

=  : o → o → ⋆
E_{refl} : ∏_{x:o} x = x
⋮
E_{β} : ∏_{m:v→o,n:v} app (!(lda m)) (!n) = mn

But the injection function “!” is a big nuisance. It pervades the encoding of terms yet it corresponds to nothing in the original syntax. Lambda expressions become more difficult to read and write; the example mechanisation in LEGO given in [4] is testimony to this. Clearly when we use the encoding we would rather not mention the injection at all.

With subtyping, we simply declare v as a subtype of o:

\begin{aligned}o & : ⋆ \\ v & ≤ o : ⋆ \end{aligned}

and then the injection function is not needed. In effect, it becomes implicit: we may imagine that it is inserted automatically wherever necessary. The β-rule now reads:

E_{β} : ∏_{m:v→o,n:v} app (lda m) n = mn

and we do not need any extra constructors.

1.1 Summary of application areas

Edinburgh Logical Framework The need for subtyping in a dependently typed lambda calculus was noticed during the Edinburgh LF project, around 1987. Mason pointed out that subtypes would be useful when representing Hoare’s logic: one would like to treat the type of quantifier-free boolean expressions (used in programs) as a subtype of the type of first-order formulae (used in assertions), because formulae contain quantifiers that cannot appear in programs [20]. Without subtypes extra machinery is necessary, either encoding explicit coercion functions or additional judgements to express syntactic properties. Either device complicates the encoding. As we have demonstrated above with the call-by-value λ-calculus example, other common examples of encodings in LF also benefit from subtyping.

Later, Pfenning gave more cases of cumbersome encodings of syntax, and proposed a solution by extending LF with refinement types, a restricted form of subtypes [21]. Moreover, he demonstrated that refinement types (or subtyping) can allow a limited form of proof reuse, so that one proof term proves several judgements. (This is connected with the interpretation of subtyping as intuitionistic implication explained by Longo et al. [18].) Pfenning proved that his system is decidable and is a conservative extension of LF; see Section 5 for comparison with our work.

Other Applied Type Theories Pfenning’s application was the proof assistant Elf which implements LF. A richer type theory is implemented by the LEGO system, in which researchers at Edinburgh and Erlangen recently tested Pierce and Turner’s subtyping model of object-orientation [24]. They extended the model to include proofs about objects and thus type-dependency. Because LEGO lacks subtyping, coercion functions are used, but it was found that inserting coercions quickly becomes tedious in practice.

Other applications in LEGO are easy to find. Subtyping is an important extension needed for proof assistants so that the formalization of mathematics can be brought closer to standard mathematical practice. Proof assistants such as Elf, LEGO, and their relatives NuPrl, Coq and Alf would all benefit from the addition of subtyping.

Type Systems for Programming Languages During the 1980’s, Cardelli proposed several rich type systems for programming languages combining subtyping and type-dependency. The system in [9] is illustrated with examples of dependent datatypes and subtypings between them. At a workshop in 1986, Cardelli described ideas about type-checking techniques for these systems but at the outset accepted that the techniques would only lead to a semi-decision procedure, because of (for example) the combination of recursive types and type dependency [8].

We believe that our system is the first fragment of Cardelli’s language, retaining subtyping and dependent types, to be shown to have a decidable type inference problem.

Type Systems for Specification Languages In algebraic specification, a language called ASL+ was proposed by Sannella, Sokołowski and Tarlecki [25] to model formal program development in-the-large. The types of ASL+ are algebraic specifications, terms are programs, and subtyping models specification refinement. Dependent types of the form πx:A. B model specifications of parameterised programs (similar to functors in Standard ML); an implementation of πx:A. B should map a program P satisfying A to a program satisfying B[x := P].

The investigations of Sannella et al. into this language were preliminary and the progress reported here has fed into the continuation of their work in [2].

1.2 Combining subtyping and dependent types

In separation, subtyping and type-dependency have been well-studied. Yet their combination leads to systems that are difficult to study. We tread close to the line of undecidability, as in Cardelli’s system or the second-order system F_{≤} [23]. Although it has been argued that semi-decision procedures may be acceptable in type-checkers for programming languages, decidability is essential for applied type theories where type-checking serves as proof-checking.

One thing that makes the study of these systems difficult is that with dependent types, the typing and subtyping relations become intimately tangled, which means that tested techniques of examining subtyping in isolation no longer apply.

Let us quickly show how typing and subtyping become tangled. The archetypal rule of subtyping is subsumption, which allows a term of a type A to be used where one of a supertype B is expected:

\begin{matrix}Γ ⊢ M : A & Γ ⊢ A ≤ B \\ Γ ⊢ M : B \end{matrix}

(as usual, Γ denotes a context of assumptions about the types of variables — see Section 2 below). So the typing judgement depends on the subtyping judgement. When a system has dependent types like List it must have a kinding rule to check that an application of a type-function to a term is well-formed:

Γ ⊢ List : Nat → ⋆  Γ ⊢ n : Nat
Γ ⊢ List(n) : ⋆

So the kinding judgement depends on the typing judgement. We expect the subtyping relationship to hold a priori only between well-formed types; for example, inferring reflexivity of subtyping between types:

{Γ ⊢ A : ⋆ \atop Γ ⊢ A ≤ A}

So subtyping depends on typing, via kinding. As a picture:

\xymatrix{ & Γ ⊢ A : K \ar[dl] \\ Γ ⊢ M : A \ar[rr] &  & Γ ⊢ A ≤ B \ar[ul]}

Of course there is nothing bad about such a mutually recursive definition per se. But it turns out to significantly complicate our meta-theoretic study, compared with other wellunderstood subtyping systems (e.g., [16, 22, 26, 13]) which lack this circularity.

In the remainder of this paper we study the addition of subtyping to the system λP, an abstract version of the type-system (sometimes called λΠ) which underlies LF [5, 17]. This is a pure system with type-valued functions dependent on terms. In Section 2 we define λP_{≤}, showing examples of using the rules, and we prove some basic meta-theoretic properties.

At a certain point in the development of the meta-theory, things become difficult to analyse directly because of the circularity described above. So we design an algorithmic version of the subtyping relation which breaks the cycle of dependencies. The new relation does not depend on kinding, and only relates normal forms. But still there is a circularity, since we want to know that normalization steps used by the subtyping algorithm preserve kinding. To solve this we make another separation: β-reduction is split into two levels, β_{1}-reduction on terms and β_{2}-reduction on types. Type normalization only depends on β_{2}-reduction; at the outset we can prove rather more about this than about β_{1}-reduction. This untangles things enough to prove equivalence of the two subtyping relations, and then properties about the original relation. The analysis of subtyping is described in Section 3.

In Section 4 we describe the type-checking algorithm. We break more dependencies between the judgements and then we prove our main result: the algorithm is correct and terminates on all inputs, so λP_{≤} is decidable. A corollary is the minimal type property: every typable term possesses a minimal type in the subtype relation.

We believe that this work (first reported in [3]) describes the first proof of decidability for subtyping dependent types, in a system uniformly extended with a subsumption rule and a subtyping relation. In Section 5 we summarise the achievement and the related work, and mention some directions for further research.

2 THE SYSTEM λP_{≤} 6

2 The system λP_{≤}

The system λP_{≤} (pronounced “lambda-pee-sub”) is formally defined by the rules which follow below, also summarized at the end of the paper. The rules define four judgement forms:

Γ ⊢ K  ‘K is a kind in context Γ’
Γ ⊢ A : K  ‘type A has kind K in context Γ’
Γ ⊢ M : A  ‘term M has type A in context Γ’
Γ ⊢ A ≤ B  ‘A is a subtype of B in context Γ’

In general, we use “type” to refer to both types (which have the kind ⋆) and type constructors (which have other kinds). We use the notation Γ ⊢ A, B : K to abbreviate the two judgements Γ ⊢ A : K and Γ ⊢ B : K.

For those familiar with the description of λP in [5], we differ by using a stratified presentation separating the syntactic categories of kinds, types, and terms, and replacing the start and weakening rules by the kind formation judgement. This is close to the presentation of λΠ in the appendix of [17].

The underlying grammar of pre-terms and pre-contexts is:

\begin{aligned}M & ::= & x | λx:A. M | MM \\ A & ::= & α | πx:A. A | Λx:A. A | AM \\ K & ::= & ⋆ | Πx:A.K \\ Γ & ::= & ⟨⟩ | Γ, x : A | Γ, α : K | Γ, α ≤ A : K \end{aligned}

We assume throughout that pre-contexts never contain repeated declarations of the same variable.

Sometimes the letters U, V, … will be used to range over pre-terms which may be terms, types or kinds. Substitution is defined in the usual way for term variables U[x := M] and type variables U[α := A]. As mentioned, we distinguish two kinds of β-reduction:

C[(λx:A. M)N] ⟶_{β_{1}} C[M[x := N]]
C[(Λx:A. B)M] ⟶_{β_{2}} C[B[x := M]]

(C[−] indicates a pre-term with a hole in it). The union of the two reductions is written ⟶_{β}. Generally, −↠_{R} is the reflexive and transitive closure of the reduction ⟶_{R}, and =_{R} is the symmetric closure of −↠_{R}. The term U^{R} is the R-normal form of U.

Formation, kinding and typing are as in λP (or λΠ), except that the type conversion rule is replaced by subsumption, and we allow bounded type-variables in the context.

Here are the rules for kind and context formation:

⟨⟩ ⊢ ⋆  (f-empty)

{Γ ⊢ A : ⋆ \atop Γ, x : A ⊢ ⋆}  (f-term)

{Γ ⊢ K \atop Γ, α : K ⊢ ⋆}  (f-type)

{Γ ⊢ A : K \atop Γ, α ≤ A : K ⊢ ⋆}  (f-subtype)

{Γ, x : A ⊢ K \atop Γ ⊢ Πx:A.K}  (f-Π)

The kind of types is ⋆, which is always well-formed. The statement Γ ⊢ ⋆ says that Γ is a well-formed context, avoiding the need for another judgement. The kind Πx:A.K classifies type families, which map a term of type A to a type of kind K.

We have two ways of adding type-variables α to a context: in (f-subtype) the declaration α ≤ A : K declares α to have the kind K and to be bounded by the type A. In (f-type) α is unbounded and only has a kind. This contrasts with other systems which have a “top” type ⊤^{K} for each kind K, and recover unbounded type variables by assuming α ≤ ⊤^{K} : K. Since we have no direct application for top types, we steer clear of their potentially bad behaviour: it is the top types that render the subtyping relation undecidable in F_{≤} when combined with the standard contravariant rule for bounded quantifiers [23]. (In the present system, we have no type abstraction or quantification, so using top types might not invalidate our results despite adopting a contravariant rule for π-types. But we haven’t investigated this).

Here are the rules for kinding:

Γ ⊢ ⋆  α ∈ Dom(Γ)
Γ ⊢ α : Kind_{Γ}(α)

(k-var)

{Γ, x : A ⊢ B : ⋆ \atop Γ ⊢ πx:A. B : ⋆}  (k-π)

{Γ, x : A ⊢ B : K \atop Γ ⊢ Λx:A. B : Πx:A.K}  (k-Λ)

\begin{matrix}Γ ⊢ A : Πx:B.K & Γ ⊢ M : B \\ Γ ⊢ A M : K[x := M] \end{matrix}  (k-app)

\begin{aligned}Γ ⊢ A : K & Γ ⊢ K′ & K =_{β} K′ \\ & Γ ⊢ A : K′ \end{aligned}  (k-conv)

The rule (k-var) assigns a type variable α the kind given to it in the context, written Kind_{Γ}(α). The set of variables declared in Γ is written Dom(Γ).

In (k-π) the type πx:A. B is the dependent function space. In (k-Λ) we can abstract over a type B by a term variable x to form the type family (dependent type) Λx:A. B. Such a type function can be instantiated in the rule (k-app). Finally the rule (k-conv) closes the judgement under well-formed conversion of kinds.

Here are the rules for typing:

\begin{matrix}Γ ⊢ ⋆ & x ∈ Dom(Γ) \\ Γ ⊢ x : Γ(x) \end{matrix}  (t-var)

{Γ, x : A ⊢ M : B \atop Γ ⊢ λx:A. M : πx:A. B}  (t-λ)

\begin{matrix}Γ ⊢ M : πx:A. B & Γ ⊢ N : A \\ Γ ⊢ MN : B[x := N] \end{matrix}  (t-app)

\begin{matrix}Γ ⊢ M : A & Γ ⊢ A ≤ B \\ Γ ⊢ M : B \end{matrix}  (t-sub)

These are completely standard. The subsumption rule (t-sub) replaces a rule of typeconversion.

Finally, here are the rules for subtyping:

\begin{aligned}Γ ⊢ A : K & Γ ⊢ B : K & A =_{β} B \\ & Γ ⊢ A ≤ B \end{aligned}  (s-conv)

\begin{matrix}Γ ⊢ A ≤ B & Γ ⊢ B ≤ C \\ Γ ⊢ A ≤ C \end{matrix}  (s-trans)
Γ ⊢ ⋆  α bounded in Γ

Γ ⊢ α ≤ Γ(α) (s-var)

\begin{aligned}Γ ⊢ A′ ≤ A & Γ, x : A′ ⊢ B ≤ B′ & Γ ⊢ πx:A. B : ⋆ \\ & Γ ⊢ πx:A. B ≤ πx:A′. B′ \end{aligned}  (s-π)

{Γ, x : A ⊢ B ≤ B′ \atop Γ ⊢ Λx:A. B ≤ Λx:A. B′}  (s-Λ)

\begin{matrix}Γ ⊢ A ≤ B & Γ ⊢ BM : K \\ Γ ⊢ A M ≤ B M \end{matrix}  (s-app)

Conversion is included in the subtyping relation by (s-conv), which also ensures reflexivity on types of the same kind. Transitivity is ensured by (s-trans).

The rule (s-var) allows us to use the bound of a bounded type-variable; Γ(α) stands for the bound of α.

The subtyping rule for π-types, (s-π), is contravariant in the domain and covariant in the codomain; the codomains are compared under the stronger restriction that x : A′. Because of this the final judgement is needed to ensure that πx:A. B is indeed a well-formed type.

Type families are included in the subtype relation by (s-Λ), which extends the relation pointwise. The corresponding rule for applications is (s-app). Only families with the same domain are comparable. (In principle it would be possible to generalise to a rule with the same form as (s-Λ), but this would break the invariant that only types of the same kind are comparable, so a relation of subkinding would be needed to compare kinds.)

Here is a brief example of using subtyping with type-dependency, to expresses basic relationships about datatypes for bags and lists. Assume that we begin with the context:

Γ_{Bag} ≡ Nat : ⋆,

Even ≤ Nat : ⋆, AllBags : ⋆, Bag ≤ Λn:Nat. AllBags : Πn:Nat.⋆, List ≤ Bag : Πn:Nat.⋆

The idea is that AllBags is the type of all bags, and the dependent types Bag(n) and List(n) represent bags and lists of size n. A list of length n is also a bag of size n.

The rule (s-π) lets us infer subtypings such as πn:Nat. List(n) ≤ πn:Even. Bag(n), so if we expect a function from an even number n to a bag of size n, we can use a function that maps any natural n to a list of length n.

If n : Nat, using (s-app), (s-conv), and (s-trans) we can show that List(n) ≤ AllBags. Using (s-Λ) we can show that Λn:Nat. List(n) ≤ Λn:Nat. Bag(n), for example.

2.1 Basic properties of λP_{≤}

Many basic properties of λP_{≤} can be established routinely, although the order of proofs is more critical than in systems without subtyping. This section contains the basic properties we need.

Proposition 2.1 (Commutativity of substitution). If x ≢ y and x ∉ FV (M) then, (A[y := M])[x := N[y := M]] = (A[x := N])[y := M].

Proposition 2.2 (Church-Rosser property). Let R be one of β_{1}, β_{2} or β. If U −↠_{R} U′ and U −↠_{R} U′′, then there exists a V such that U′ −↠_{R} V and U′′ −↠_{R} V. Proof Standard. □

Proposition 2.3 (Strong Normalization). Let R be one of β_{1}, β_{2} or β.

1. If Γ ⊢ K, then K is strongly R-normalizing.

2. If Γ ⊢ A : K, then A is strongly R-normalizing.

3. If Γ ⊢ M : A, then M is strongly R-normalizing. Proof To show strong normalization for λP_{≤}, we adapt the method given for LF in [17]. There, a reduction-preserving translation of pre-terms into Curry-typable terms of the simply-typed lambda-calculus λ^{→} is given, which establishes the strong normalization for LF since λ^{→} is known to be strongly normalizing.

To adapt this method to λP_{≤}, we have to make an adjustment to Definition A.9 of [17] so that the type-translation τ takes into account bounds of type variables. This reflects the fact that in LF, nothing is known about the structure of the types that a variable α ranges over, so it can be mapped to the base type ω. But in λP_{≤}, a variable α can be bounded, which, for example, could force it to range over Π-types. The details follow.

Definition 2.4 (Translations to λ^{→}). We define three translation functions on pre-terms. The function κ gives a λ^{→} type from a kind; it is the same as the function called τ in [17]. The function τ here gives a λ^{→} type from a λP_{≤} type; it is given with respect to a fixed context Γ.^{1} When we want to make this context explicit, we write τ_{Γ}(A).

\begin{aligned}κ(⋆) & = & ω \\ κ(Πx:A.K) & = & κ(A) → κ(K) \\ κ(α) & = & ω \\ κ(πx:A. B) & = & κ(A) → κ(B) \\ κ(Λx:A. B) & = & κ(B) \\ κ(A M) & = & κ(A) \end{aligned}

τ(α) = \{ \begin{matrix}τ(A) & if α ≤ A : K ∈ Γ \\ ω & if α is not bounded in Γ \end{matrix}
τ(Λx:A. B) = τ(B)
τ(A M) = τ(A)
τ(πx:A. B) = τ(A) → τ(B)

We extend τ to contexts:

\begin{aligned}τ(⟨⟩) & = & ⟨⟩ \\ τ(Γ, x : A) & = & τ(Γ), x : τ_{Γ}(A) \\ τ(Γ, α : K) & = & τ(Γ), α : κ(K) \\ τ(Γ, α ≤ A : K) & = & τ(Γ), α : κ(K) \end{aligned}

The function | | maps types and terms of λP_{≤} into terms of λ^{→}:

\begin{aligned}|x| & = & x \\ |α| & = & α \\ |AM| & = & |A| |M| \\ |MN| & = & |M| |N| \\ |πx:A. B| & = & p_{τ(A)} |A| (λx. |B|) \\ |λx:A. M| & = & (λy. λx. |M|) |A|  (y ∉ FV (M)) \\ |Λx:A. B| & = & (λy. λx. |B|) |A|  (y ∉ FV (B)) \end{aligned}

The translation for π is defined using a family of simply-typed constants,

p_{τ} : ω → (τ → ω) → τ

We consider α and x to also be variables in λ^{→}.

Lemma 2.5 (Translation to λ^{→} preserves typing). 1. If Γ ⊢ A : K then τ(Γ) ⊢_{λ^{→}} |A| : κ(K).

1We only get away with a fixed context Γ because there is no abstraction or quantification over types, so the set of bounded type variables is fixed in a typing derivation. This fact is also important to our subtyping algorithm derived later.

2. If Γ ⊢ M : A then τ(Γ) ⊢_{λ^{→}} |M| : τ_{Γ}(A).

3. If Γ ⊢ A ≤ B then τ_{Γ}(A) ≡ τ_{Γ}(B). Proof By induction on derivations. The first two cases are similar to the proof in [17] for LF; for (t-sub) we use the third case. The third case is easily seen, using the simple Lemma A.10 in [17] (notice that this holds for β_{1}, β_{2} or full β conversion); the use of the bound for α in the definition of τ_{Γ}(α) is crucial for (s-var). □

Proof of Proposition 2.3 Follows from Lemma 2.5, by noticing that the | | translation preserves reductions. See [17]. □

The next proposition says that reduction commutes with substitution and that βequality can be factored into the β_{1}-equality of β_{2} normal forms. The facts mentioned are simply those which we need later on in the paper.

Proposition 2.6 (Reduction and conversion). 1. If U ⟶_{β_{1}} V, then U[x := M] ⟶_{β_{1}} V [x := M] and U[α := A] ⟶_{β_{1}} V [α := A].

2. If U =_{β_{1}} V, then U[x := M] =_{β_{1}} V [x := M] and U[α := A] =_{β_{1}} V [α := A].

3. If U ⟶_{β_{2}} V, then U[x := M] ⟶_{β_{2}} V [x := M] and U[α := A] ⟶_{β_{2}} V [α := A].

4. If U =_{β_{2}} V, then U[x := M] =_{β_{2}} V [x := M] and U[α := A] =_{β_{2}} V [α := A].

5. (U[x := M])^{β_{2}} ≡ U^{β_{2}}[x := M^{β_{2}}].

6. If A^{β_{2}} and B^{β_{2}} exist then A =_{β} B implies A^{β_{2}} =_{β_{1}} B^{β_{2}}. Proof Items 1, 3 and 5 follow by induction on the structure of U. Items 2 and 4, by induction on the definition of =_{β_{1}} and =_{β_{2}} respectively. Item 6 uses the Church-Rosser property, Proposition 2.2. □

The next proposition concerns the behaviour of well-formed contexts. A context Γ is a prefix of Γ′ if Γ′ extends Γ by zero or more declarations. A context Γ is included in a context Γ′, Γ ⊆ Γ′, if every declaration in Γ is also a declaration in Γ′. The size of a derivation of Γ ⊢ J is indicated by sizederiv(Γ ⊢ J), which we take to mean the number of rule applications used in the derivation tree; this is the measure we refer to when talking of a “shorter” derivation.

Proposition 2.7 (Context properties). 1. Variables. If Γ ⊢ J then each type or term variable is declared at most once in Γ, and FV (J) ⊆ Dom(Γ).

2. Generation.

(a) If Γ_{1}, x : A, Γ_{2} ⊢ J then Γ_{1} ⊢ A : ⋆

(b) If Γ_{1}, α : K, Γ_{2} ⊢ J then Γ_{1} ⊢ K (c) If Γ_{1}, α ≤ A : K, Γ_{2} ⊢ J then Γ_{1} ⊢ A : K

Moreover, there exists a derivation of the consequent which is shorter than the derivation of the antecendent.

3. Well-formedness.

Suppose Γ ⊢ J. Then for every prefix Γ′ of Γ, we have Γ′ ⊢ ⋆.

Moreover, if J ≢ ⋆ or Γ′ is a proper prefix of Γ, then sizederiv(Γ′ ⊢ ⋆) < sizederiv(Γ ⊢ J).

4. Renaming.

Suppose θ is a mapping from variables to variables. Then Γ ⊢ J implies θ(Γ) ⊢ θ(J), where θ(−) denotes the obvious extensions of the mapping.

5. Thinning.

Suppose Γ ⊆ Γ′, Γ ⊢ J and Γ′ ⊢ ⋆. Then Γ′ ⊢ J.

Substitution holds for each sort of variable assumption.

Proposition 2.8 (Substitution). 1. If Γ_{1}, x : A, Γ_{2} ⊢ J and Γ_{1} ⊢ M : A, then Γ_{1}, Γ_{2}[x := M] ⊢ J[x := M].

2. If Γ_{1}, α : K, Γ_{2} ⊢ J and Γ_{1} ⊢ A : K, then Γ_{1}, Γ_{2}[α := A] ⊢ J[α := A].

3. If Γ_{1}, α ≤ B : K, Γ_{2} ⊢ J and Γ_{1} ⊢ A ≤ B, then Γ_{1}, Γ_{2}[α := A] ⊢ J[α := A]. Proof Routine. Each part by simultaneous induction on derivations for the four judgement forms. □

One desirable property of a type system is type unicity: the type of a term is unique up to conversion. With subtyping this cannot hold, although we can hope for the property of minimal types. This property is useful because it allows us to factor the problem of type-checking into two parts: the inference of a minimal type for a term and deciding the subtyping relation. We will prove that λP_{≤} has minimal types in Section 4.

For the kinding fragment of our system, however, unicity does hold. The next proposition is that the kind of a type is unique up to conversion. We use the observation that conversion at the kind level is particularly simple since there is no application. If K =_{R} K′ (where R is one of β, β_{1}, β_{2}) then for some n ≥ 0, K ≡ Πx:A_{1}…. Πx:A_{n}.⋆ and K′ ≡ Πx:A′_{1}…. Πx:A′_{n}.⋆ with A_{i} =_{R} A′_{i} for each i.

Proposition 2.9 (Unicity of kinds). If Γ ⊢ A : K_{1} and Γ ⊢ A : K_{2}, then K_{1} =_{β} K_{2}. Proof By induction on the sum of the heights of the derivation of Γ ⊢ A : K_{1} and of Γ ⊢ A : K_{2}. If either derivation ends in (k-conv), the result follows immediately from the induction hypothesis and transitivity of =_{β}. Otherwise, we consider the last rule in each derivation, which must be the same. We show here the case for (k-app), when A ≡ A_{1}M. We have Γ ⊢ A_{1} : Πx:B_{1}.K_{1} and Γ ⊢ A_{1} : Πx:B_{2}.K_{2}. Using the induction hypothesis, K_{1} =_{β} K_{2}. Since conversion is preserved by substitution (Proposition 2.6(2,4)), K_{1}[x := M] =_{β} K_{2}[x := M] as required. □

Bound narrowing is the name given to the property that derivability of a judgement is preserved by replacing the bounding type in a type-variable declaration by a type which is smaller in the subtype relation. Informally, one can see this is true by adding an instance of subsumption or transitivity to each use of a variable rule. (And so the derivation of the judgement with a narrowed context may be longer than the original one).

We first prove a restricted form of this property.

Proposition 2.10 (Bound narrowing I). Suppose Γ ⊢ A′ ≤ A. Then

1. Γ, x : A, Γ′ ⊢ J and Γ ⊢ A′ : ⋆ implies Γ, x : A′, Γ′ ⊢ J

2. Γ, α ≤ A : K, Γ′ ⊢ J and Γ ⊢ A′ : K implies Γ, α ≤ A′ : K, Γ′ ⊢ J Proof

1. We prove the statement simultaneously for the four judgement forms, for all Γ_{1} and Γ_{2}, by induction on derivations. For (f-term), we use the assumption Γ ⊢ A′ : ⋆ and Proposition 2.7; for (t-var) when the variable being typed is x we also use (t-sub). The remaining cases are straightforward.

2. Similar to 1. For formation, we use the assumption and Proposition 2.7 to show Γ ⊢ A′ : K in (f-subtype). For subtyping derived with (s-var), we must show Γ′ ⊢ α ≤ A, which follows via (s-trans), using Proposition 2.7 and the assumption. Remaining cases are straightforward. □

The next property shows some anticipated agreements between the judgements, for example, that every type inhabited by a term indeed has kind ⋆.

Proposition 2.11 (Agreement of judgements). 1. If Γ ⊢ A : K then Γ ⊢ K.

2. If Γ ⊢ M : A then Γ ⊢ A : ⋆.

3. If Γ ⊢ A ≤ B then Γ ⊢ A, B : K, for some K. Proof By induction on derivations; parts 2 and 3 are proved together. We use Proposition 2.8 for (k-app), (t-app) and (s-app); Proposition 2.7 for (t-var) and (s-var), and Proposition 2.10 for (s-π) and (s-Λ). □

Agreement has important consequences. For example, we can see that the usual λP rule of conversion for typing is admissible:

\begin{aligned}Γ ⊢ M : A & Γ ⊢ A′ : ⋆ & A =_{β} A′ \\ & Γ ⊢ M : A′ \end{aligned}  (t-conv)

Using Proposition 2.11, Γ ⊢ A : ⋆ is implied by the first premise. So Γ ⊢ A ≤ A′ using the second and third premises with (s-conv). Then Γ ⊢ M : A′ follows using subsumption, (t-sub).

We can also use agreement to get a stronger version of Proposition 2.10. We write Γ ⊢ J to denote an arbitrary judgement.

Proposition 2.12 (Bound narrowing II). Suppose Γ ⊢ A′ ≤ A. Then

1. Γ, x : A, Γ′ ⊢ J implies Γ, x : A′, Γ′ ⊢ J

2. Γ, α ≤ A : K, Γ′ ⊢ J implies Γ, α ≤ A′ : K, Γ′ ⊢ J Proof From Proposition 2.10. Using context properties, Proposition 2.9 and Proposition 2.11 we get Γ_{1} ⊢ A′ : ⋆ in part 1 and Γ_{1} ⊢ A′ : K in part 2. □

2.2 Towards subject reduction

Another desirable property for type systems is subject reduction. This is the property that β-reduction preserves the type of a term. (Since a term may have several types in a subtyping system, and since an abstraction term λx:A. M may be applied to a term whose minimal type is smaller than A, in general we may have that reduction adds types.)

To prove subject reduction we need to reason about the way judgements are derived. This is the point where we hit a snag. In particular, to show that (λx:A. M) N and its reduct M[x := N] have the same type, we would like to assume that the application was typed using (t-λ) followed by (t-app). For this we need a generation principle.

Proposition 2.13 (Generation for typing). 1. If Γ ⊢ x : C then Γ ⊢ Γ(x) ≤ C.

2. If Γ ⊢ λx:A. M : C then for some B, (a) Γ, x : A ⊢ M : B and (b) Γ ⊢ πx:A. B ≤ C.

3. If Γ ⊢ MN : C then for some A, B,

(a) Γ ⊢ M : πx:A. B, (b) Γ ⊢ N : A, and (c) Γ ⊢ B[x := N] ≤ C. Proof By induction on typing derivations, using transitivity of subtyping. □

However, this is too weak to show type preservation; the possibility that subtyping was used in (t-sub) gets in the way. Suppose (λx:A. M)N : C. We want to show that Γ ⊢ M[x := N] : C as well. By generation for typing, for some A_{1} and B_{1}:

Γ ⊢ (λx:A. M) : πx:A_{1}. B_{1}, Γ ⊢ N : A_{1} and Γ ⊢ B_{1}[x := N] ≤ C.

Again, by generation for typing, for some B_{2}

Γ, x : A ⊢ M : B_{2} and Γ ⊢ πx:A. B_{2} ≤ πx:A_{1}. B_{1}.

If we could show that

Γ ⊢ A_{1} ≤ A and Γ, x : A_{1} ⊢ B_{2} ≤ B_{1}

then we could continue as follows. By narrowing,

Γ, x : A_{1} ⊢ M : B_{2}

then, by (t-sub),

Γ, x : A_{1} ⊢ M : B_{1},

and, by the substitution property, Proposition 2.8,

Γ ⊢ M[x := N] : B_{1}[x := N].

Finally, using (t-sub),

Γ ⊢ M[x := N] : C.

And that would be it. The judgements Γ ⊢ A_{1} ≤ A and Γ, x : A_{1} ⊢ B_{2} ≤ B_{1} are the problem; we would hope to prove them using a generation property for subtyping, applied to Γ ⊢ πx:A. B_{2} ≤ πx:A_{1}. B_{1}. Unfortunately, we cannot prove a suitable generation principle directly by induction on subtyping derivations because of the rules (s-conv) and (s-trans). The next section is a quest towards a generation principle for subtyping using a formulation without these troublesome rules.

3 A subtyping algorithm

To delve further into the meta-theory of λP_{≤} we must confront the subtyping system. We do this by analysing an equivalent system which is syntax directed (to derive any given statement, at most one rule applies), and so forms an algorithm when viewed in reverse. A generation principle for a syntax-directed system is immediate; the hard part is proving its equivalence with the original presentation.

Our algorithmic presentation is akin to that for F_{∧}^{ω} in [13], with two important differences. First, the rules here have no kinding premises, so the cycle of dependencies between subtyping and typing is destroyed. Second, we make a novel adjustment for dependent types: splitting β-reduction.

We shall explain the reason for splitting β-reduction shortly. Why remove kinding premises from the subtyping rules? This was a technique used in the study of F_{≤}^{ω} in [26], but we know from the F_{∧}^{ω} algorithm in [13] that removing kinding is not crucial to the study of that system. Things are more complex with λP_{≤} because of the circularity between typing and subtyping: keeping kinding premises, we could reduce deciding Γ ⊢_{A} A ≤ B to a finite number of typing constraints, but such constraints are in no obvious way “smaller” than the subtyping statement we began with. So it is hard to argue that an algorithm cannot loop by an infinite alternation of calls from one judgement to the other. Our first plan was to seek a cunning induction measure, but removing the circularity seems conceptually simpler and moreover closer to a practical subtyping algorithm.

The new rules derive statements Γ ⊢_{A} A ≤ B, with A and B in β_{2}-normal form. Normal forms allow us to grasp the fine structure of the subtyping relation, since occurrences of applications are restricted. Otherwise it is hard to tell whether an occurrence of A M was introduced by (s-app) or (s-conv), for example.

There are four rules definining the algorithmic subtyping relation.

\begin{matrix}Γ ⊢_{A} A′ ≤ A & Γ, x : A′ ⊢_{A} B ≤ B′ \\ Γ ⊢_{A} πx:A. B ≤ πx:A′. B′ \end{matrix}  (as-π)

\begin{matrix}A =_{β_{1}} A′ & Γ, x : A′ ⊢_{A} B ≤ B′ \\ Γ ⊢_{A} Λx:A. B ≤ Λx:A′. B′ \end{matrix}  (as-Λ)

{M_{1} =_{β_{1}} M′_{1} ⋯ M_{n} =_{β_{1}} M′_{n} \atop Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ α M′_{1} ⋯ M′_{n}}  (as-app-r)
α bounded in Γ, A ≠_{β_{1}} α M_{1} ⋯ M_{n}
Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤ A
Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ A

(as-app-t)

The first two rules correspond to (s-π) and (s-Λ), except that the kinding premises are removed and β_{1}-conversion of the type-label of Λ is allowed. The two rule schemes for application guarantee that the algorithmic subtyping relation is closed under reflexivity and transitivity (this claim is proved in Section 3.3). In the rule scheme (as-app-r), “R” stands for reflexivity and in (as-app-t), “T” stands for transitivity. To make the rules syntax-directed, we need the premise in (as-app-t) that A ≠_{β_{1}} α M_{1} ⋯ M_{n}, otherwise (as-app-r) would apply.

The motivation to use β_{2}-normal forms instead of full β-normal forms appears when designing (as-app-t). To make the new system deterministic, we must remove the transitivity rule. However, it cannot be eliminated completely so it is restricted: we only allow transitivity along the bound of a type-variable in head position of a normal form. To check whether Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ A, we check if Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n}) ≤ A. But this step introduces a possibly non-normal form, so the algorithm must normalize Γ(α) M_{1} ⋯ M_{n}. As a first attempt, we get the rule:

{Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β} ≤ A \atop Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ A}

Because the algorithmic rules do not check kinding, we must ensure that if we start with well-kinded types in the conclusion (the arguments, seen as an algorithm), we still have well-kinded types in the hypothesis (the arguments in any recursive call). Starting with Γ ⊢_{A} α M_{1} ⋯ M_{n} : K, we can prove (using Proposition 3.3 below) that replacing α by its bound preserves kinding, so Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n}) : K too. Now we need to prove that

Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β} : K

but this is proved using the subject reduction property for β, exactly the result that we could not prove without an algorithm for subtyping. So we are back where we started.

Fortunately, we can recover from this using β_{2}-normal forms instead of β-normal forms. To see the structure of types, β_{2}-normalization is enough, and subject reduction for β_{2}- reduction can be proved easily. This explains the use of β_{2}-reduction in (as-app-t).

The other rule that makes the original subtyping system non syntax-directed is (s-conv). Since we use types in β_{2}-normal form, the rule for reflexivity must incorporate β_{1}-conversion, and it suffices to use reflexivity on terms of the form α M_{1} ⋯ M_{n} for n ≥ 0. This explains (as-app-r).

The following subsections prove that the algorithmic subtyping relation is equivalent to the original system, and apply the algorithm to prove results about the original system. In Section 3.1 we prove that the original presentation is closed under β_{2}-reduction. In Section 3.2 we prove that the algorithmic rules are sound for the original presentation. In Section 3.3 we prove that reflexivity and transitivity are admissible in the algorithm, which is the core of the proof following in Section 3.4 that the algorithmic rules are complete. In Section 3.5 the equivalence result is stated, and used to prove the sought after generation principle for subtyping,

3.1 Closure under β_{2}-reduction

To prove subject reduction for β_{2}-reduction, we need generation only for kinding.

Proposition 3.1 (Generation for kinding). 1. If Γ ⊢ α : K then K =_{β} Kind_{Γ}(α).

2. If Γ ⊢ πx:A. B : K then K ≡ ⋆, and Γ, x : A ⊢ B : ⋆.

3. If Γ ⊢ Λx:A. B : K then there exists K’ such that K =_{β} Πx:A.K′, and Γ, x : A ⊢ B : K′.

4. If Γ ⊢ A M : K then there exists B, K′ such that Γ ⊢ A : Πx:B.K′, Γ ⊢ M : B and

K′[x := M] =_{β} K. Moreover, the derivations of the consequents can be assumed to be shorter than the derivation of the antecedents. Proof By induction on derivations. In each case, the antecedent must either have been derived by a structural rule, when the result is immediate, or by (k-conv), when we use the induction hypothesis and transitivity of β-conversion. □

As well as β_{2} subject reduction for kinding, we also need closure of the subtyping relation under β_{2}-reduction. So we state a generalized form of the property, writing J ⟶_{β_{2}} J′ to indicate a β_{2}-reduction inside J.

Proposition 3.2 (Closure under β_{2}-reduction). If Γ ⊢ J and J −↠_{β_{2}} J′ then Γ ⊢ J′. Proof The one step case follows by induction on the derivation of Γ ⊢ J also proving simultaneously the statement for a reduction inside the context Γ. The only interesting case is for an outermost reduction in the kinding judgement. Suppose the premises are Γ ⊢ Λx:A. B : Πx:A′.K and Γ ⊢ M : A′, and the reduction is (Λx:A. B) M ⟶_{β_{2}} B[x := M]. By kinding generation, Proposition 3.1, we get Γ, x : A ⊢ B : K′ with K =_{β} K′ and A =_{β} A′. Using context properties, Γ ⊢ A : ⋆ and so by (t-conv), Γ ⊢ M : A. By substitution, Γ ⊢ B[x := M] : K′[x := M]. The result Γ ⊢ B[x := M] : K[x := M] follows by preservation of β-equality under substitution (Proposition 2.6(2,4)) and (k-conv) using agreement for the original conclusion.

The result for multiple reductions follows by induction on the definition of −↠_{β_{2}}. The one step case is what we have just proved, the reflexivity case is immediate and the transitivity case is by the induction hypothesis. □

3.2 Soundness

In the soundness proof, β_{2} subject reduction for kinding is crucial for the case of (as-app-t) to show that kindability is preserved from the conclusion to the premise.

The soundness lemma requires an auxiliary proposition.

Proposition 3.3 (Bounded type variables). 1. If Γ ⊢ α M_{1} ⋯ M_{n} : K, then Γ ⊢ Γ(α) M_{1} ⋯ M_{n} : K.

2. If Γ ⊢ α M_{1} ⋯ M_{n} : K, then Γ ⊢ α M_{1} ⋯ M_{n} ≤ Γ(α) M_{1} ⋯ M_{n}. Proof

1. By induction on the derivation of Γ ⊢ α M_{1} ⋯ M_{n} : K using structural properties.

2. By induction on n, using structural properties and (s-var) in the base case, part 1 and (s-app) in the inductive step. □

We can now prove soundness by a straightforward induction.

Lemma 3.4 (Soundness of algorithmic subtyping). Suppose we have two types of the same kind, Γ ⊢ A, B : K. Then Γ ⊢_{A} A ≤ B implies Γ ⊢ A ≤ B. Proof By induction on the derivation in the algorithmic system.

Case (as-Λ): Suppose the conclusion is Γ ⊢_{A} Λx:A_{1}. B_{1} ≤ Λx:A_{2}. B_{2}. We split the problem into two steps. We first prove that Γ ⊢ Λx:A_{2}. B_{1} ≤ Λx:A_{2}. B_{2} using the induction hypothesis; second we prove Γ ⊢ Λx:A_{1}. B_{1} ≤ Λx:A_{2}. B_{1} using (s-conv). The result then follows by transitivity.

First step. To use the induction hypothesis on Γ, x : A_{2} ⊢_{A} B_{1} ≤ B_{2} we need to show that Γ, x : A_{2} ⊢ B_{1}, B_{2} : K′ for some K′. By the assumption and Proposition 3.1, for some K_{1}, K_{2} we have Γ, x : A_{1} ⊢ B_{1} : K_{1} and Γ, x : A_{2} ⊢ B_{2} : K_{2} with K =_{β} Πx:A_{1}.K_{1} =_{β} Πx:A_{2}.K_{2}. So by the Church-Rosser property, K_{1} =_{β} K_{2}. By Proposition 2.7, Γ ⊢ A_{1}, A_{2} : ⋆, and, by (s-conv), Γ ⊢ A_{2} ≤ A_{1}. By narrowing, Proposition 2.12, Γ, x : A_{2} ⊢ B_{1} : K_{1}, and by agreement, Proposition 2.11, Γ, x : A_{2} ⊢ K_{2} and, by (k-conv), Γ, x : A_{2} ⊢ B_{1} : K_{2}. Take K′ to be K_{2}. We can now apply the induction hypothesis and infer Γ, x : A_{2} ⊢ B_{1} ≤ B_{2}, and, by (s-Λ), Γ ⊢ Λx:A_{2}. B_{1} ≤ Λx:A_{2}. B_{2}.

Second step. By (k-Λ), Γ ⊢ Λx:A_{1}. B_{1} : Πx:A_{1}.K_{1} and Γ ⊢ Λx:A_{2}. B_{1} : Πx:A_{2}.K_{1}. By agreement, Proposition 2.11, Γ ⊢ Πx:A_{1}.K_{1}. By (k-conv), Γ ⊢ Λx:A_{2}. B_{1} :

Πx:A_{1}.K_{1}. Finally, by (s-conv), Γ ⊢ Λx:A_{1}. B_{1} ≤ Λx:A_{2}. B_{1}.

Case (as-π): Suppose the conclusion is Γ ⊢_{A} πx:A_{1}. B_{1} ≤ πx:A_{2}. B_{2}. Then by the assumption and Proposition 3.1 we have Γ, x : A_{1} ⊢ B_{1} : ⋆ and Γ, x : A_{2} ⊢ B_{2} : ⋆. By Proposition 2.7, Γ ⊢ A_{1}, A_{2} : ⋆, and by the induction hypothesis, Γ ⊢ A_{2} ≤ A_{1}. By narrowing, Proposition 2.12, Γ, x : A_{2} ⊢ B_{1} : ⋆ and so by the induction hypothesis, Γ, x : A_{2} ⊢ B_{1} ≤ B_{2}. The result now follows via (s-π) using the second assumption.

Case (as-app-r): Immediately using (s-conv).

Case (as-app-t): where A ≡ α M_{1} … M_{n}, we use Proposition 3.3(1) and subject β_{2}- reduction to show that Γ ⊢ (Γ(α) M_{1} … M_{n})^{β_{2}} : K, hence by the induction hypothesis, Γ ⊢ (Γ(α) M_{1} … M_{n})^{β_{2}} ≤ A. Now by Proposition 3.3(2), Γ ⊢ α M_{1} … M_{n} ≤ Γ(α) M_{1} … M_{n}. The result follows using (s-conv) and (s-trans) twice. □

The proof above shows that each derivation in the algorithmic system induces a derivation in the original system; in effect, the algorithm suggests a strategy for using the rules of the original system. A derivation in the algorithm induces a derivation in the original system which uses transitivity only on variables, if at all, and which uses conversion only at the beginning and when subtyping applications.

3.3 Reflexivity and transitivity

For completeness we first show that reflexivity and transitivity are admissible in the new system. This is like the cut-elimination argument first used in a subtyping setting by Curien and Ghelli [16] for their study of F_{≤}. But instead of showing that reflexivity and transitivity can be removed, we show that they can be added without changing the derivable statements. This avoids consideration of special “cut-free” derivations.

Proposition 3.5 (Reflexivity of algorithmic subtyping). Let A and A′ be two types in β_{2}-normal form, with A =_{β_{1}} A′ and Γ ⊢ A, A′ : K. Then Γ ⊢_{A} A ≤ A′. Proof By induction on size(A) + size(A′), where size(U) is the number of symbols in U. Since A and A′ are in β_{2}-normal form, they may only differ at term components, so we consider four cases.

Case A ≡ A′ ≡ α: By (as-app-r).

Case A ≡ πx:B. C, A′ ≡ πx:B′. C′: Using the induction hypothesis and (as-π).

Case A ≡ Λx:B. C, A′ ≡ Λx:B′. C′: Using the induction hypothesis and (as-Λ).

Case A ≡ B M, A′ ≡ B′ M′: Since A and A′ are in β_{2}-normal form, we must have B ≡ αM_{1} … M_{n} and B′ ≡ αM′_{1} … M′_{n} for some n ≥ 0, with M_{i} =_{β_{1}} M′_{i}. The result follows immediately by (as-app-r). □

Showing admissibility of transitivity uses extra machinery. To define a measure for the main induction, we extend the language with a new type constructor and a new reduction. The crucial property of the measure is that it reduces from the conclusion to the premises of the algorithmic subtyping rules, notably (as-app-t). The same measure will be used to show termination of the subtyping algorithm.

The new type constructor is a binary “plus” operator, which has the kinding rule:

\begin{matrix}Γ ⊢ A : K & Γ ⊢ B : K \\ Γ ⊢ A + B : K \end{matrix}  (k-+)

The idea is this. Subtyping bounded type variables α typically, but not necessarily, can involve using transitivity along the bound: α ≤ Γ(α) ≤ D. A type thus contains many “choice” points where the bound of a variable may or may not be used during subtyping. We define an operation plus_{Γ}(C) which expands these points by recursively replacing bounded variables α in a type C with α + Γ(α).

We can recover a plus-free type from plus_{Γ}(C) by choosing either the left or right side of every plus expression. This is captured by +-reduction:

C[A + B] ⟶_{+} C[A]
C[A + B] ⟶_{+} C[B]

(where C[−] is a type or term in the extended language with a hole in it). The number of +- reductions possible from plus_{Γ}(C) affects the complexity of deciding a subtyping statement containing the type C.

Definition 3.6 (Plus-expansion of a type). Let Γ be a context and declare all the type variables of a type C. Then plus_{Γ}(C) is given by:

plus_{Γ_{1}, α≤A:K, Γ_{2}}(α) = α + plus_{Γ_{1}}(A)
plus_{Γ_{1}, α:K, Γ_{2}}(α) = α
plus_{Γ}(πx:A. B) = πx: plus_{Γ}(A). plus_{Γ}(B)
plus_{Γ}(Λx:A. B) = Λx: plus_{Γ}(A). plus_{Γ}(B)
plus_{Γ}(A M) = plus_{Γ}(A) M

When the condition on Γ is met, plus_{Γ}(C) is defined uniquely — this can be shown by appealing to properties of contexts and observing that the definition is well-founded on the lexicographic ordering of pairs ⟨length(Γ), size(C)⟩, where length(Γ) is the number of variables declared by Γ.

One important fact is that there is a +-reduction from the expansion of a type-variable to its bound in the context; this is used in the next proposition. We write −↠_{R}^{n} to indicate that a reduction is n steps long and −↠_{R}^{>n} for more than n steps. We extend β_{2}-reduction to A + B in the obvious (compatible) way.

Proposition 3.7 (Plus types and reduction). plus_{Γ}(α M_{1} ⋯ M_{n}) −↠_{β_{2}+}^{>0} plus_{Γ}((Γ(α) M_{1} ⋯ M_{n})^{β_{2}}). Proof We use several sub-lemmas to prove the statement:

1. For two contexts Γ and Γ′, if Γ ⊆ Γ′ then plus_{Γ}(A) = plus_{Γ′}(A).

2. plus_{Γ}(α M_{1} ⋯ M_{n}) −↠_{+}^{>0} plus_{Γ}(Γ(α) M_{1} ⋯ M_{n}).

3. If x ∉ Dom(Γ) and FV (A) ∈ Dom(Γ)−{x} then plus_{Γ}((A[x := M])) = (plus_{Γ}(A))[x := M];

4. If A ⟶_{β_{2}} B, then plus_{Γ}(A) −↠_{β_{2}} plus_{Γ}(B).

Parts 1 and 3 follow by induction on the structure of A. Part 2 follows by induction on n: in the base case, we have plus_{Γ}(α) −↠_{+}^{>0} plus_{Γ}(Γ(α)) by the definition of plus. Part 4 follows by induction on the structure of A using 3. The desired result then follows from 2 and 4. □

Now β_{2}+-reduction will help define the measure we seek. First, let maxred_{Γ}(A) be the maximal number of β_{2}+-reductions from the plus-expansion of a type:

maxred_{Γ}(A) =_{def} max { n plus_{Γ}(A) −↠_{β_{2}+}^{n} A′ for some A′ }

(Notice that maxred_{Γ}(A) only makes sense when plus_{Γ}(A) is β_{2}+-strongly normalizing.) Then we define the weight of two types A, B as the pair:

weight_{Γ}(A, B) =_{def} ⟨ maxred_{Γ}(A) + maxred_{Γ}(B), size(A) + size(B) ⟩

The number of bounded variables and the size of the types both contribute. Pairs weight_{Γ}(A, B) are well-ordered by the usual lexicographic ordering.

We now mention the extension of strong normalization to the system with the + constructor necessary to show that maxred_{Γ}(A) is defined whenever A is well-kinded with respect to Γ.

Proposition 3.8 (Normalization with +). 1. Strong normalization (Proposition 2.3) also holds for the +-enriched language with (k-+) and β+ reduction.

2. If Γ ⊢ A : K, then Γ ⊢ plus_{Γ}(A) : K in the + enriched language. Proof We can prove part 1 by an extension of the proof for Proposition 2.3, using a version of the simply-typed lambda-calculus extended with a +-reduction as in [13]. Part 2 is proved by induction on the derivation of Γ ⊢ A : K. □

The following lemmas are used in the proof of transitivity admissibility.

The first is a generalized version of a bound narrowing result for typing assumptions in algorithmic subtyping; intuitively the subtyping rules ignore their typing assumptions. If this lemma seems surprising, remember that the algorithmic subtyping rules make no check on the well-formedness of the context, so valid judgements may contain non well-kinded types.

Lemma 3.9 (Bound change). If Γ, x : A, Γ′ ⊢_{A} B ≤ B′ then Γ, x : A′, Γ′ ⊢_{A} B ≤ B′ Proof By induction on the derivation of Γ, x : A, Γ′ ⊢_{A} B ≤ B′ □

{Lemma 3.10. \atop 1.} If Γ ⊢ α M_{1} ⋯ M_{n} : K, then Γ ⊢ α M_{1} ⋯ M_{n} ≤ (Γ(α) M_{1} ⋯ M_{n})^{β_{2}}.

2. If Γ ⊢ α M_{1} ⋯ M_{n} : K, then Γ ⊢ (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} : K. Proof Item 1 follows from Proposition 3.3 and Proposition 3.2. Item 2 follows from 1 using agreement, Proposition 2.11, and unicity of kinds, Proposition 2.9. □

Proposition 3.11 (Transitivity of algorithmic subtyping). Let Γ ⊢ A, B, C : K. Then Γ ⊢_{A} A ≤ B and Γ ⊢_{A} B ≤ C implies Γ ⊢_{A} A ≤ C. Proof For all Γ using induction on weight_{Γ}(A, C). Since A, B, and C are well-kinded in Γ, we have that plus_{Γ}(A), plus_{Γ}(B), plus_{Γ}(C) and the plus-expansion of the bound of every type variable in Γ are all defined and β_{2}+-strongly normalizing. Therefore the inductive measure is always well-defined. Then using case analysis on the last rule used to derive Γ ⊢_{A} A ≤ B we can break down the transitivity into smaller instances, using Proposition 3.7.

Case (as-Π): From:

\begin{matrix}Γ ⊢_{A} A_{2} ≤ A_{1} & Γ, x : A_{2} ⊢_{A} B_{1} ≤ B_{2} \\ Γ ⊢_{A} πx:A_{1}. B_{1} ≤ πx:A_{2}. B_{2} \end{matrix}

and:

\begin{matrix}Γ ⊢_{A} A_{3} ≤ A_{2} & Γ, x : A_{3} ⊢_{A} B_{2} ≤ B_{3} \\ Γ ⊢_{A} πx:A_{2}. B_{2} ≤ πx:A_{3}. B_{3} \end{matrix}

Since there is no kinding information in the algorithm, the kindedness of the subexpressions of the types we started from has to be obtained by structural properties of the original system, using the kinding assumptions of the present proposition. By generation (Proposition 3.1), it follows that

K ≡ ⋆, Γ, x : A_{1} ⊢ B_{1} : ⋆,
Γ, x : A_{2} ⊢ B_{2} : ⋆, and
Γ, x : A_{3} ⊢ B_{3} : ⋆,

and, by agreement (Proposition 2.11), Γ ⊢ A_{1}, A_{2}, A_{3} : ⋆.

We can now apply the induction hypothesis to get:

\begin{matrix}Γ ⊢_{A} A_{3} ≤ A_{2} & Γ ⊢_{A} A_{2} ≤ A_{1} \\ Γ ⊢_{A} A_{3} ≤ A_{1} \end{matrix}

By narrowing (Proposition 2.12)

Γ, x : A_{3} ⊢ B_{1} : ⋆ and Γ, x : A_{3} ⊢ B_{2} : ⋆

and we use the bound change lemma (Lemma 3.9) to obtain Γ, x : A_{3} ⊢_{A} B_{1} ≤ B_{2}. Then we can apply the induction hypothesis again to get:

\begin{matrix}Γ, x : A_{3} ⊢_{A} B_{1} ≤ B_{2} & Γ, x : A_{3} ⊢_{A} B_{2} ≤ B_{3} \\ Γ, x : A_{3} ⊢_{A} B_{1} ≤ B_{3} \end{matrix}

So the result Γ ⊢ πx:A_{1}. B_{1} ≤ πx:A_{3}. B_{3} follows using (as-Π). The uses of the induction hypothesis are justified because in each, the maximal β_{2}+-reduction can be no longer than before, and the sum of the sizes of the terms is strictly smaller.

Case (as-Λ): Similar to the π case.

Case (as-app-r): Consider the last rule in the derivation of Γ ⊢_{A} B ≤ C. If it is (as-app-r), then we get the result by transitivity of β_{1}-conversion using (as-app-r) again. Otherwise, the last rule must be (as-app-t). Lemma 3.10(2) and subject β_{2}-reduction (Proposition 3.2) imply:

Γ ⊢ (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} : K and Γ ⊢ (Γ(α) M′_{1} ⋯ M′_{n})^{β_{2}} : K.

Then we can apply the induction hypothesis and (as-app-t) to get this derivation:

\begin{matrix}Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤ (Γ(α) M′_{1} ⋯ M′_{n})^{β_{2}} \\ Γ ⊢_{A} (Γ(α) M′_{1} ⋯ M′_{n})^{β_{2}} ≤ C \end{matrix} ; Γ ⊢_{A} Γ(α) M_{1} ⋯ M_{n} ≤ C

Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ C

The first premise is an instance of reflexivity, since by Proposition 2.6(6), the two sides are β_{1} convertible and we can use Proposition 3.5. Proposition 3.7 assures us that the new instance of transitivity has a strictly smaller measure because the sum of the lengths of the maximal β_{2}+-reductions in the new transitivity instance is strictly smaller.

Case (as-app-t): Lemma 3.10(2) and subject β_{2}-reduction (Proposition 3.2) imply:

Γ ⊢ (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} : K.

We apply the induction hypothesis and (as-app-t) again to deduce:

\begin{matrix}Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤ B & Γ ⊢_{A} B ≤ C \\ Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤ C \end{matrix} ; Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ C

By Proposition 3.7 the new instance of transitivity has a strictly smaller measure. □

3.4 Completeness

Now we can establish completeness, using some properties of the new system.

Parts 2 and 3 of the next proposition hold for all M such that the normal forms mentioned exist (a weaker condition than kindability).

Proposition 3.12 (Properties of algorithmic subtyping). 1. If Γ ⊢_{A} A ≤ B and Γ =_{β_{2}} Γ′, then Γ′ ⊢_{A} A ≤ B.

2. If Γ_{1}, x : A, Γ_{2} ⊢_{A} B ≤ C, then Γ_{1}, Γ_{2}[x := M] ⊢_{A} (B[x := M])^{β_{2}} ≤ (C[x := M])^{β_{2}}.

3. If Γ ⊢_{A} A ≤ B and B is not a π-type, then Γ ⊢_{A} (AM)^{β_{2}} ≤ (BM)^{β_{2}}. (Provided the normal forms in parts 2 and 3 exist). Proof Parts 1 and 2 are proved by induction on derivations. Part 3 then follows by another induction on derivations, using parts 1 and 2. □

Part 3 of the proposition above is crucial in the completeness proof, where the induction hypothesis alone is too weak to show the admissibility of (s-app).

Lemma 3.13 (Completeness of algorithmic subtyping). If Γ ⊢ A ≤ B then Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}}. Proof Using induction on the derivation of Γ ⊢ A ≤ B, considering the last rule:

Case (s-conv): Using β_{2}-subject reduction for kinding, Proposition 3.2, Γ ⊢ A^{β_{2}}, B^{β_{2}} : K. By Proposition 2.6(6) A^{β_{2}} =_{β_{1}} B^{β_{2}} so we can use the admissibility of reflexivity, Proposition 3.5, to get the result.

Case (s-trans): By Proposition 3.11, since by Proposition 2.11 A, B, and C are kindable in the context.

Case (s-var): By Proposition 2.11, for some K, Γ ⊢ α : K and Γ ⊢ Γ(α) : K. By subject reduction for kinding, Γ ⊢ Γ(α)^{β_{2}} : K too. Then Γ ⊢_{A} α ≤ Γ(α)^{β_{2}} via (as-app-t).

Case (s-π): Let the conclusion of the rule be Γ ⊢ πx:C. D ≤ πx:C′. D′. By the induction hypothesis and the premises, we get Γ ⊢_{A} C′^{β_{2}} ≤ C^{β_{2}} and Γ, x : C′ ⊢_{A} D^{β_{2}} ≤ D′^{β_{2}}. By Proposition 3.12(1), Γ, x : C′^{β_{2}} ⊢_{A} D^{β_{2}} ≤ D′^{β_{2}} too. The result Γ ⊢_{A}

(πx:C. D)^{β_{2}} ≤ (πx:C′. D′)^{β_{2}} follows using (as-π).

Case (s-Λ): Similar to the previous case.

Case (s-app): By the induction hypothesis and Proposition 3.12(3); the assumption that B is not a π-type follows from the premise Γ ⊢ BM : K and kinding generation. □

3.5 Equivalence

Combining the soundness and completeness lemmas, we get the following theorem.

Theorem 3.14 (Equivalence of algorithmic subtyping). Γ ⊢ A ≤ B iff for some K, Γ ⊢ A, B : K and Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}}. Proof By Lemma 3.13 with Proposition 2.11, and Lemma 3.4 using (conv) and (trans).

□

The equivalence of the two systems gives a powerful tool for analysing the subtyping relation. We can prove the generation principle we wanted.

Proposition 3.15 (Generation for subtyping). 1. If Γ ⊢ α ≤ C and α is bounded in Γ, then either C =_{β} α, or Γ ⊢ Γ(α) ≤ C.

2. If Γ ⊢ πx:A. B ≤ C then for some A′, B′, (a) C =_{β} πx:A′. B′, (b) Γ ⊢ A′ ≤ A, and (c) Γ, x : A′ ⊢ B ≤ B′.

3. If Γ ⊢ Λx:A. B ≤ C then for some B′, (a) C =_{β} Λx:A. B′, and (b) Γ, x : A ⊢ B ≤

B′. Proof Using Lemma 3.13, by considering the last rule of a derivation in the algorithmic system and then converting back to the original system using Lemma 3.4. □

There is no case for applications in this proposition. When Γ ⊢ A M ≤ C, we can only make deductions about the form of C based on (A M)^{β_{2}}; this reduces to one of the last two cases above, or a generalisation of the first (with C =_{β_{1}} α M_{1} ⋯ M_{n}). To prove subject β_{1}-reduction, we only need part 2.

Proposition 3.16 (Closure under β_{1}-reduction). 1. If Γ ⊢ J and Γ −↠_{β_{1}} Γ′ then Γ′ ⊢ J.

2. If Γ ⊢ J and J −↠_{β_{1}} J′ then Γ ⊢ J′. Proof By simultaneous induction on derivations. The proof is similar to that of Proposition 3.2, except the case of an outermost reduction is in the rule (t-app), where we use generation for both typing and subtyping. The one-step case of course relies on substitution, Proposition 2.8. □

3.6 Decidability

The “algorithmic” subtyping rules are syntax-directed, so they form an algorithm when viewed in reverse. Using the same measure used to prove the admissibility of transitivity, we can show that the algorithm for subtyping terminates on well-kinded types. Thus the subtyping relation is decidable for well-kinded types.

Lemma 3.17 (Decidability of subtyping for well-kinded types). Let Γ ⊢ A : K_{a} and Γ ⊢ B : K_{b}. Then by applying the algorithmic subtyping rules, we can decide whether Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}}. Moreover, this extends to a decision procedure for deciding Γ ⊢ A ≤ B. Proof For any algorithmic subtyping rule, weight_{Γ}(A_{i}, B_{i}) for each premise is strictly smaller than weight_{Γ}(A, B) for the conclusion. So every derivation ending in well-kinded types must be of finite height. The procedure of applying the rules backwards will either finish successfully (checking β_{1} equalities in the leaves (as-app-r), which can be done by normalization), or else lead to a case where no rule is applicable. By Theorem 3.14 and the strong normalization property Proposition 2.3, this decides Γ ⊢ A ≤ B. □

Of course, we don’t yet have an algorithm for determining the kinding relation so this lemma may not be useful — especially because to find whether types are well-kinded we have to do subtyping! In Section 4 we give an algorithm for kinding which only calls the subtyping algorithm on types which we already know to be well-kinded.

4 A type-checking algorithm

The next step towards proving decidability of λP_{≤} is to design algorithmic versions of the remaining judgements. In the same way that we removed kinding premises from subtyping, we remove formation premises from kinding and typing. Again this gives us something nearer a feasible algorithm, and helps prove termination.

Figures 2, 4 and 6 at the end of the paper show the new rules against the old ones, below we just give highlights. The new rules are syntax-directed, and with the convention that premises are evaluated in order (from left to right, “stacked” premises from top to bottom), they form a deterministic algorithm when viewed in reverse. Moreover, the rules for kinding and typing can be seen as functions, which given an input context and type (or term), yield a uniquely inferred kind (or type).

For formation, the rule for introducing a bounded type-variable becomes:

\begin{aligned}Γ ⊢_{A} K & Γ ⊢_{A} A : K′ & K =_{β} K′ \\ & Γ, α ≤ A : K ⊢_{A} ⋆ \end{aligned}  (af-subtype)

The first premise checks the well-formedness of the new kind K and the context. The second premise is used to find a kind K′ for the bound A. Because the rules are syntax-directed, if K′ exists, it is determined uniquely by A, so we can think of this as an inference procedure. Moreover, by the soundness property for the algorithmic system (Lemma 4.4), K′ will be well-formed. This means that it is safe to check whether K =_{β} K′ by normalizing. Conversion is needed at this point because the conversion rule has been removed to make the system syntax-directed.

The algorithmic rule for kinding applications is:

\begin{matrix}Γ ⊢_{A} A : Πx:B.K & Γ ⊢_{A} M : B′ & Γ ⊢_{A} B′^{β_{2}} ≤ B^{β_{2}} \\ Γ ⊢_{A} A M : K[x := M] \end{matrix}  (ak-app)

The first premise infers a unique kind for A, which must be a Π-kind if A M is a valid application. As with the kinding rules, the algorithmic typing rules are syntax-directed, so the second premise infers a unique type B′ for the argument M, if possible. Finally we must check that the inferred type B′ is a subtype of the domain type B. Because the subtyping algorithm works on β_{2}-normal forms, we must normalize the two types before checking the subtyping relation. The normalization will be terminating because the kind and type inference procedure only infer valid types and kinds.

The third premise for (ak-app) is necessary because subsumption is removed from the new typing relation. Similarly, we must allow subtyping when typing term applications:

Γ ⊢_{A} M : A  FLUB_{Γ}(A) ≡ πx:B. C  Γ ⊢_{A} N : B′  Γ ⊢_{A} B′^{β_{2}} ≤ B

Γ ⊢_{A} MN : C[x := N] (at-app)

Once again, a subtyping check appears in the final premise. The inferred type of a function term need not have the form of a π-type; so in the second premise of the rule we invoke a function FLUB (“functional least upper bound”) to search for a π-type for M. It climbs the context, following the subtyping order, until it finds a π-type or can go no farther. This is achieved by repeatedly β_{2}-normalizing and replacing head variables by their bounds.

FLUB_{Γ}(A) = \{ \begin{matrix}FLUB_{Γ|_{α}}(Γ(α) M_{1} ⋯ M_{n}) & A^{β_{2}} ≡ α M_{1} ⋯ M_{n} \\ A^{β_{2}} & otherwise \end{matrix}

(where the first case only applies if α is declared with a bound in Γ, and then Γ|_{α} is the initial prefix of Γ up to the declaration of α).

Now we must show that the algorithmic system is equivalent to the original one. First we prove some useful properties for the algorithm.

4.1 Basic properties of the algorithm

Proposition 4.1 (Context properties). 1. Renaming.

Suppose θ is a mapping from variables to variables. Then Γ ⊢_{A} J implies θ(Γ) ⊢_{A} θ(J), where θ(−) denotes the obvious extensions of the mapping.

2. Thinning.

Suppose Γ ⊆ Γ′, Γ ⊢_{A} J and Γ′ ⊢_{A} ⋆. Then Γ′ ⊢_{A} J.

Proposition 4.2 (Substitution in the algorithm). 1. For subtyping. If Γ_{1}, x : A, Γ_{2} ⊢_{A} C ≤ D, Γ_{1} ⊢_{A} M : B, and Γ_{1} ⊢ B ≤ A then Γ_{1}, (Γ_{2}[x := M])^{β_{2}} ⊢_{A} (C[x := M])^{β_{2}} ≤ (D[x := M])^{β_{2}}.

2. For the other judgements. If Γ_{1}, x : A, Γ_{2} ⊢_{A} J, Γ_{1} ⊢_{A} M : B, and Γ_{1} ⊢ B ≤ A

then Γ_{1}, Γ_{2}[x := M] ⊢_{A} J[x := M]. Proof By simultaneous induction on derivations, using Proposition 2.6 and Proposition 2.1. □

To prove equivalence, we also make use of some simple properties of FLUB, including the fact that FLUB_{Γ}(A) is an upper bound of A.

Proposition 4.3 (Properties of FLUB). 1. If Γ ⊢ A : K, then FLUB_{Γ}(A) is well-defined.

2. If FLUB_{Γ}(A) is defined and Γ is a prefix of the context Γ′, then FLUB_{Γ′}(A) ≡ FLUB_{Γ}(A).

3. If Γ ⊢ A : K, then Γ ⊢ A ≤ FLUB_{Γ}(A). Proof

1. By assumption, A is normalizing and by Proposition 3.3(1), so too is Γ(α) M_{1} ⋯ M_{n} in the first case of the definition; the argument Γ|_{α} is shorter than Γ, which guarantees well-foundedness.

2. In the first case of the definition, FLUB_{Γ}(A) = FLUB_{Γ|_{α}}(Γ(α) M_{1} ⋯ M_{n}) whilst FLUB_{Γ′}(A) = FLUB_{Γ′|_{α}}(Γ′(α) M_{1} ⋯ M_{n}) but we must have α ∈ Dom(Γ), hence Γ′(α) = Γ(α) and Γ′|_{α} = Γ|_{α}. The result is immediate for the second case.

3. By induction on the number of unfolding steps of FLUB_{Γ}( ), a good measure since FLUB_{Γ}(A) is well-defined by part 1. In the base case, the second clause of the definition, FLUB_{Γ}(A) = A^{β_{2}} and the result follows by Proposition 3.2 and (s-conv). In the step case, we know from Proposition 3.3(1) that Γ ⊢ Γ(α) M_{1} ⋯ M_{n} : K and so we can use the induction hypothesis to obtain Γ ⊢ Γ(α) M_{1} ⋯ M_{n} ≤ FLUB_{Γ}(Γ(α) M_{1} ⋯ M_{n}). By part 2, FLUB_{Γ}(Γ(α) M_{1} ⋯ M_{n}) ≡ FLUB_{Γ}(α M_{1} ⋯ M_{n}). The result follows using Proposition 3.3(2) and (s-trans). □

4.2 Equivalence

We prove that the algorithm is sound and complete for the original system defining λP_{≤}. This is easier than it was for subtyping: the proofs proceed by induction on derivations in either system.

Lemma 4.4 (Soundness of algorithmic system). 1. Γ ⊢_{A} K implies Γ ⊢ K.

2. If Γ ⊢ ⋆ then Γ ⊢_{A} A : K implies Γ ⊢ A : K.

3. If Γ ⊢ ⋆ then Γ ⊢_{A} M : A implies Γ ⊢ M : A. Proof Simultaneously by induction on the derivation in the algorithmic system. Most cases follow immediately applying the corresponding rule of the original system, perhaps using the induction hypothesis. The case for (af-subtype) uses Proposition 2.7(3). Here are the only two non-immediate cases:

Case (at-app): We have Γ ⊢_{A} M : A, Γ ⊢_{A} N : B′, Γ ⊢_{A} B′^{β_{2}} ≤ B and FLUB_{Γ}(A) ≡ πx:B. C. By the induction hypothesis for 3, Γ ⊢ M : A and by agreement Γ ⊢ A : ⋆. By Proposition 4.3, Γ ⊢ A ≤ FLUB_{Γ}(A) and so by (t-sub) Γ ⊢ M : πx:B. C. Using the induction hypothesis for 3, Γ ⊢ N : B′. Using Lemma 3.4 together with agreement, kinding generation and (s-conv), we get Γ ⊢ B′ ≤ B. Finally by (t-sub), Γ ⊢ N : B and by (t-app), Γ ⊢ MN : C[x := N].

Case (ak-app): We have Γ ⊢_{A} A : πx:B. K, Γ ⊢_{A} N : B′ and Γ ⊢_{A} B′^{β_{2}} ≤ B^{β_{2}}. By the induction hypothesis for part 2, Γ ⊢ A : πx:B. K and by agreement, generation for kinding and context properties, Γ ⊢ B : ⋆. By the induction hypothesis for part 3, Γ ⊢ M : B′ and by agreement Γ ⊢ B′ : ⋆. Using Lemma 3.4, Γ ⊢ B′^{β_{2}} ≤ B^{β_{2}} and by (s-conv) and (s-trans), Γ ⊢ B′ ≤ B. So using (t-sub), Γ ⊢ M : B and by (k-app), Γ ⊢ AM : K[x := M]. □

For completeness we use the crucial characteristic of FLUB, which justifies its name: if a type A is a subtype of some π-type, then FLUB_{Γ}(A) is the least π-type greater than or equal to A in the subtype ordering. So an application typed with (at-app) is given a minimal type.

Proposition 4.5 (π-types and FLUB). 1. If Γ ⊢ A ≤ πx:C. D then FLUB_{Γ}(A) ≡ πx:C′. D′ for some C′, D′.

2. If Γ ⊢ A ≤ πx:C. D then Γ ⊢ FLUB_{Γ}(A) ≤ πx:C. D. Proof Each part via a corresponding result using induction in the algorithmic system.

1. We show by induction on the derivation that Γ ⊢_{A} A ≤ πx:C. D implies FLUB_{Γ}(A) ≡ πx:C′. D′.

Case (as-π): We are given that A ≡ πx:C_{1}. D_{1} so the result follows by the definition

of FLUB. Case (as-app-t): We are given that A ≡ α M_{1} ⋯ M_{n} and Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤

πx:C_{1}. D_{1} By the induction hypothesis, FLUB_{Γ}((Γ(α) M_{1} ⋯ M_{n})^{β_{2}}) ≡ πx:C′_{1}. D′_{1} for some C′_{1}, D′_{1} and by the definition of FLUB and Proposition 4.3, it follows that FLUB_{Γ}(α M_{1} ⋯ M_{n}) = FLUB_{Γ}((Γ(α) M_{1} ⋯ M_{n})^{β_{2}}).

Rules (as-Λ) and (as-app-r) do not apply. The result for the original system follows from Lemma 3.13 and the properties of normal forms.

2. We show by induction on the derivation that Γ ⊢_{A} A ≤ πx:C. D implies Γ ⊢_{A} FLUB_{Γ}(A) ≤ πx:C. D.

Case (as-π): Then A ≡ FLUB_{Γ}(A) ≡ πx:C′. D′, so the result is by assumption; Case (as-app-t): Then A ≡ α M_{1} ⋯ M_{n}.

By the induction hypothesis, Γ ⊢_{A} FLUB_{Γ}((Γ(α) M_{1} ⋯ M_{n})^{β_{2}}) ≤ πx:C′. D′.

But by Proposition 4.3 and the definition of FLUB, it follows that FLUB_{Γ}(α M_{1} ⋯ M_{n}) ≡ FLUB_{Γ}((Γ(α) M_{1} ⋯ M_{n})^{β_{2}}) so we are done.

Rules (as-Λ) and (as-app-r) do not apply. The result for the original system follows using soundness and completeness of algorithmic subtyping, and a use of conversion and transitivity.

□

Lemma 4.6 (Completeness of algorithmic system). 1. If Γ ⊢ K, then Γ ⊢_{A} K.

2. If Γ ⊢ A : K, then there is a K_{a} such that Γ ⊢_{A} A : K_{a}, K_{a} =_{β} K, Γ ⊢_{A} K_{a}, and Γ ⊢_{A} K.

3. If Γ ⊢ M : A, then there is an A_{a} such that Γ ⊢_{A} M : A_{a} and Γ ⊢ A_{a} ≤ A. Proof Simultaneously by induction on derivations in the original system, using the corresponding algorithmic rules.

1. Case (f-empty): By (af-empty).

Case (f-term): Let the conclusion be Γ_{1}, x : A ⊢ ⋆, and the premise be Γ_{1} ⊢ A : ⋆. By the induction hypothesis, there exists K_{a}, such that Γ_{1} ⊢_{A} A : K_{a}, Γ_{1} ⊢_{A} K_{a}, Γ_{1} ⊢_{A} ⋆, and K_{a} =_{β} ⋆. Since ⋆ can only be β-equal to itself, K_{a} ≡ ⋆. Then we get Γ_{1}, x : A ⊢_{A} ⋆, by (af-term).

Case (f-type): By the induction hypothesis and (af-type). Case (f-subtype): Let the premise be Γ_{1} ⊢ A : K′. By the induction hypothesis

Γ_{1} ⊢_{A} A : K′_{a}, Γ_{1} ⊢_{A} K′ and K′_{a} =_{β} K′. We can now apply (af-subtype). Case (f-π): By induction hypothesis and (af-π). □

2. Case (k-var): By (ak-var), K_{a} ≡ Kind_{Γ}(α). Let Γ ≡ Γ_{1}, α : Kind_{Γ}(α), Γ_{2}. By generation of contexts (Proposition 2.7(2)) Γ_{1} ⊢ Kind_{Γ}(α) with a shorter derivation. Then by the induction hypothesis, Γ_{1} ⊢_{A} Kind_{Γ}(α). From Γ ⊢ ⋆, by the induction hypothesis it follows that Γ ⊢_{A} ⋆, and by Thinning (Proposition 4.1), Γ ⊢_{A} Kind_{Γ}(α).

Case (k-π): Let the premise be Γ, x : C ⊢ B : ⋆. By the induction hypothesis Γ, x : C ⊢_{A} B : K_{b} and K_{b} =_{β} ⋆. Since the only kind β-equal to ⋆ is itself, K_{b} ≡ ⋆. By generation of contexts (Proposition 2.7(2)), Γ ⊢ C : ⋆ with a shorter derivation. Hence by the induction hypothesis, Γ ⊢_{A} C : ⋆, and by (ak-π), Γ ⊢_{A} πx:C. B : ⋆. By well-formedness of contexts (Proposition 2.7(3)), from Γ, x : C ⊢ B : ⋆ it follows that Γ ⊢ ⋆ with a shorter derivation, hence by the induction hypothesis, Γ ⊢_{A} ⋆.

Case (k-Λ): Let the premise be Γ, x : C ⊢ B : K. By the induction hypothesis, there exists K_{b} such that Γ, x : C ⊢_{A} B : K_{b}, K_{b} =_{β} K, Γ, x : C ⊢_{A} K_{b}, and Γ, x : C ⊢_{A} K. By (af-π), Γ ⊢_{A} Πx:C.K and Γ ⊢_{A} Πx:C.K_{b}, and by the definition of β-equality Πx:C.K_{b} =_{β} Πx:C.K. From the premise, by generation of contexts (Proposition 2.7(2)), Γ ⊢ C : ⋆ with a shorter derivation, and by the induction hypothesis, Γ ⊢_{A} C : ⋆. We can now apply (ak-Λ) to obtain Γ ⊢_{A} Λx:C. B : Πx:C.K_{b}. Take K_{a} ≡ Πx:C.K_{b}.

Case (k-app): Let the premises be Γ ⊢ C : Πx:B.K and Γ ⊢ M : B. By the induction hypothesis on the second premise there exists B_{b} such that Γ ⊢_{A} M : B_{b} and Γ ⊢ B_{b} ≤ B. By the induction hypothesis on the first premise, there exists K_{c} such that Γ ⊢_{A} C : K_{c}, Γ ⊢_{A} K_{c}, Γ ⊢_{A} Πx:B.K, and K_{c} =_{β} Πx:B.K. By Church Rosser, K_{c} ≡ Πx:B.′K′ with B′ =_{β} B and K′ =_{β} K. By inversion of (af-π), Γ ⊢_{A} Πx:B.′K′ implies Γ, x : B′ ⊢_{A} K′. By soundness, Γ, x : B′ ⊢ K′ and by generation of contexts (Proposition 2.7), Γ ⊢ B′ : ⋆. By agreement (Proposition 2.11), Γ ⊢ C : Πx:B.K implies Γ ⊢ Πx:B.K, and from Γ ⊢ M : B it follows that Γ ⊢ B : ⋆. From, B′ =_{β} B, Γ ⊢ B : ⋆ and Γ ⊢ B′ : ⋆, by (s-conv), Γ ⊢ B ≤ B′. By (s-trans), Γ ⊢ B_{b} ≤ B′, and by equivalence (Theorem 3.14), Γ ⊢_{A} B_{b}^{β_{2}} ≤ B′^{β_{2}}. Hence, by (ak-app), Γ ⊢_{A} CM : K′[x := M].

From Γ, x : B′ ⊢_{A} K′, Γ ⊢_{A} M : B_{b} and Γ ⊢ B_{b} ≤ B′, by substitution in the algorithm (Proposition 4.2), Γ ⊢_{A} K′[x := M]. By inversion of (af-π), Γ ⊢_{A} Πx:B.K implies Γ, x : B ⊢_{A} K, and since Γ ⊢ B_{b} ≤ B, again by substitution (Proposition 4.2), Γ ⊢_{A} K[x := M]. Finally, by Proposition 2.6(4), K′[x := M] =_{β} K[x := M]. Take K_{a} ≡ K′[x := M].

Case (k-conv): By induction hypothesis and transitivity of =_{β}.

3. Case (t-var): By (at-var). We get Γ ⊢ Γ(x) ≤ Γ(x) by (s-conv) and agreement (Proposition 2.11).

Case (t-λ): Let the premise be Γ, x : C ⊢ M : B. By the induction hypothesis, there exists B_{b} such that, Γ, x : C ⊢_{A} M : B_{b} and Γ, x : C ⊢ B_{b} ≤ B. By generation of contexts, there is a shorter derivation of Γ ⊢ C : ⋆ and by the induction hypothesis Γ ⊢_{A} C : ⋆, since there exists K_{c} with K_{c} =_{β} ⋆, and hence K_{c} ≡ ⋆. Then by (at-λ) Γ ⊢_{A} λx:C. M : πx:C. B_{b}. From Γ ⊢ C : ⋆, by (s-conv), Γ ⊢ C ≤ C. From Γ, x : C ⊢ B_{b} ≤ B, by agreement, uniqueness of kinds, and (k-π), Γ ⊢ πx:C. B : ⋆. Finally, by (s-π), Γ ⊢ πx:C. B_{b} ≤ πx:C. B. Take A_{a} ≡ πx:C. B_{b}.

Case (t-app): Suppose the premises are Γ ⊢ N : πx:B. C and Γ ⊢ N′ : B. By induction hypothesis, Γ ⊢_{A} N : D_{a} with Γ ⊢ D_{a} ≤ πx:B. C and Γ ⊢_{A} N′ : B_{a} with Γ ⊢ B_{a} ≤ B. Hence by Proposition 4.5, FLUB_{Γ}(D_{a}) ≡ πx:B′. C′ and Γ ⊢ πx:B′. C′ ≤ πx:B. C. By subtyping generation, Γ ⊢ B ≤ B′ and by (s-trans) Γ ⊢ B_{a} ≤ B′. By the completeness of algorithmic subtyping, Γ ⊢_{A} B_{a}^{β_{2}} ≤ B′^{β_{2}}. Observe that since FLUB_{Γ}(D_{a}) is in β_{2}-normal form, B′^{β_{2}} ≡ B′. So we can apply (at-app) to get Γ ⊢_{A} N N′ : A_{a} where A_{a} ≡ C′[x := N′]. Finally, Γ ⊢ A_{a} ≤ C[x := N′] follows from subtyping generation and substitution for the subtyping judgement.

Case (t-sub): By induction hypothesis and (s-trans).

We now have an equivalence between the two systems.

Theorem 4.7 (Equivalence). 1. Γ ⊢ A ≤ B iff for some K, Γ ⊢ A, B : K and Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}}.

2. Γ ⊢ A : K iff for some K_{a}, Γ ⊢_{A} A : K_{a}, K_{a} =_{β} K and Γ ⊢_{A} K.

3. Γ ⊢ M : A iff for some A_{a}, Γ ⊢_{A} M : A_{a} and Γ ⊢ A_{a} ≤ A.

4. Γ ⊢ K iff Γ ⊢_{A} K. Proof For part 1, the equivalence for subtyping was proved in Theorem 3.14. The right-to-left direction of parts 2–4 follow by soundness, Lemma 4.4, using (t-sub) for part 2 and Proposition 2.7(3) and (k-conv) for part 3. The left-to-right directions follow by completeness, Lemma 4.6. □

This theorem also proves that the algorithmic typing rules assign a minimal type to a typable term. The minimal typing property for the original system follows, by soundness.

Corollary 4.8 (Minimal typing property for λP_{≤}). Suppose M is typable in Γ. Then there is an A_{a} such that

1. Γ ⊢ M : A_{a} and

2. whenever Γ ⊢ M : A, then Γ ⊢ A_{a} ≤ A. Proof By Lemma 4.6, there is an A_{a} such that Γ ⊢_{A} M : A_{a}. By Lemma 4.4, Γ ⊢ M : A_{a} too, showing part 1. Because the algorithmic system is deterministic, A_{a} only depends on Γ and M; it is necessarily unique. So for any A such that Γ ⊢ M : A, we have Γ ⊢ A_{a} ≤ A by Lemma 4.6, showing part 2. □

4.3 Decidability

Our final theorem establishes the decidability of the algorithmic judgements, which guarantees the termination of subtype checking, kind inference, minimal type inference and formation checking.

Theorem 4.9 (Decidability of algorithmic judgements). 1. If Γ ⊢ A : K_{a} and Γ ⊢ B : K_{b}, then it is decidable whether Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}}.

2. If Γ ⊢ ⋆, it is decidable whether there exists a K_{a} such that Γ ⊢_{A} A : K_{a}.

3. If Γ ⊢ ⋆, it is decidable whether there exists an A_{a} such that Γ ⊢_{A} M : A_{a}.

4. It is decidable whether Γ ⊢_{A} K. Proof Each case follows by induction on a measure that decreases from conclusion to premises in each rule. Part 1 was proved in Lemma 3.17. Parts 2 and 3 using part 1 by simultaneous induction on the size of the subject (the term to the left of “:”), and part 4 by induction on the size of the judgement, using parts 1–3.

2. The size of the subject decreases from conclusion to kinding and typing premises. It remains to prove that checking the subtyping premise in (ak-app) terminates. For that it is enough to show that Γ ⊢ B′^{β_{2}} : ⋆ and Γ ⊢ B^{β_{2}} : ⋆, because, by part 1, the call to the subtyping algorithm Γ ⊢_{A} B′^{β_{2}} ≤ B^{β_{2}} terminates.

By soundness (Lemma 4.4), Γ ⊢ M : B′, and by agreement (Proposition 2.11) Γ ⊢ B′ : ⋆. By strong normalization (Proposition 2.3), B′^{β_{2}} exists, and by β_{2}-subject reduction (Proposition 3.2), Γ ⊢ B′^{β_{2}} : ⋆.

By soundness and agreement, Γ ⊢ Πx:B.K, and because of the determinacy of the formation rules Γ, x : B ⊢ K. By generation of contexts (Proposition 2.7(2)), Γ ⊢ B : ⋆, then by strong normalization and β_{2}-subject reduction, Γ ⊢ B^{β_{2}} : ⋆.

3. The rule (at-λ) is the only rule that has a kinding premise, and is why we need to consider kinding and typing together. The size of the subject of each typing or kinding premise is strictly smaller than the size of the subject of the conclusion, so there can be no infinite paths in the typing or kinding rules. The interesting case is (at-app). By soundness we know that Γ ⊢ M : A after the first premise; by agreement this guarantees Γ ⊢ A : ⋆, so by Proposition 4.3(1) and its proof, FLUB_{Γ}(A) is defined and the process of calculating it terminates. If we can establish that Γ ⊢ B′^{β_{2}} : ⋆ and Γ ⊢ B : ⋆ then, by part 1, the call to the subtyping algorithm Γ ⊢_{A} B′^{β_{2}} ≤ B terminates. (Notice by the definition of FLUB that B is already in β_{2}-normal form.)

By soundness and agreement, Γ ⊢ B′ : ⋆ and by strong normalization and β_{2}-subject reduction Γ ⊢ B′^{β_{2}} : ⋆.

By Proposition 4.3(3), agreement and uniqueness of kinds (Proposition 2.9), Γ ⊢ πx:B. C : ⋆, by generation for kinding, Γ, x : B ⊢ C : ⋆, and by generation for contexts Γ ⊢ B : ⋆.

4. In each formation premise the total number of symbols in the judgement is strictly smaller than in the conclusion, so there can be no infinite path of formation rules. In (af-term) and (af-subtype), by Lemma 4.4 and the first premise, we have Γ ⊢ ⋆ and so by part 2 the algorithm for checking or inferring kinds will terminate. □

Theorem 4.9, together with the equivalence proved in Theorem 4.7, shows that we have a correct and terminating algorithm for deciding any judgement of the original presentation. Here is the argument.

The formation judgement is primary; Γ ⊢ K holds iff Γ ⊢_{A} K, and Γ ⊢_{A} K is decidable. For the other judgements, we must be careful to invoke the algorithmic judgements only when we know the context and pre-terms to be well-formed.

Recall that the rules for kind and type checking allow no conversion or subsumption for an arbitrary kind or type, so viewed in reverse they form deterministic functions, for kind and type inference. So given a type, we can compute a kind of it, provided one exists. Given a term, we can compute a type of it. Again, this is subject to checking well-formedness of the context first.

Consider the subtyping judgement. To check if Γ ⊢ A ≤ B, we use the following four steps:

\begin{matrix}1. Γ ⊢_{A} ⋆ \\ 2. Γ ⊢_{A} A : K_{a} \\ 3. Γ ⊢_{A} B : K_{b} \\ 4. Γ ⊢_{A} A^{β_{2}} ≤ B^{β_{2}} \end{matrix} ; Γ ⊢ A ≤ B  (subtype-check)

The first step checks whether Γ is a well-formed context, which is decidable, and by soundness Γ ⊢ ⋆. Knowing this, we see whether A and B have kinds, say K_{a} and K_{b}. These are synthesized by the algorithmic rules for kind-checking. Furthermore, kind-checking in a well-formed context is decidable. If kinds can be found for A and B, by soundness we know that Γ ⊢ A : K_{a} and Γ ⊢ B : K_{b}, which implies that step 4 is decidable. Finally, by equivalence, if any step fails, then Γ ⊢ A ≤ B does not hold.

The typing and kinding judgements yield similar procedures.

Consider now the kinding judgement. To check if Γ ⊢ A : K, we use the following four steps:

\begin{matrix}1. Γ ⊢_{A} K \\ 2. Γ ⊢_{A} A : K_{a} \\ 3. Γ ⊢_{A} K_{a} \\ 4. K_{a} =_{β} K \end{matrix} ; Γ ⊢ A : K  (kind-check)

Step 1 checks that the given kind K is well-formed in the context Γ, and it is decidable. By soundness, we have that Γ ⊢ K, and by well-formedness of contexts Proposition 2.7(3), Γ ⊢ ⋆. Hence it is decidable whether there exists K_{a} such that Γ ⊢_{A} A : K_{a}, which is step 2. If there is such a K_{a}, we check in step 3 if Γ ⊢_{A} K_{a}, which is also decidable. If so, by soundness, Γ ⊢ K_{a}, and by strong normalization (Proposition 2.3) step 4 is decidable, because we can check if K_{a} =_{β} K by reducing both K and K_{a} to normal form and compare them. Finally, by equivalence, if any step fails, then Γ ⊢ A : K does not hold.

Finally, let us consider the typing judgement. To check whether Γ ⊢ M : A, we use the following five steps:

\begin{matrix}1. Γ ⊢_{A} ⋆ \\ 2. Γ ⊢_{A} M : A_{a} \\ 3. Γ ⊢_{A} A_{a} : K_{a} \\ 4. Γ ⊢_{A} A : K \\ 5. Γ ⊢_{A} A_{a}^{β_{2}} ≤ A^{β_{2}} \end{matrix} ; Γ ⊢ M : A  (type-check)

Step 1 is decidable, and by soundness, Γ ⊢ ⋆. The second step infers a type A_{a} for M in Γ, which is decidable because Γ ⊢ ⋆. In steps 3 and 4, kinds K_{a} for A_{a} and K for A are inferred. We know that the last two steps are decidable, because Γ ⊢ ⋆. If such kinds exist, it finally ckecks wether Γ ⊢_{A} A_{a}^{β_{2}} ≤ A^{β_{2}}, which is decidable for well-kinded types A_{a} and A. Finally, by equivalence, if any step fails, then Γ ⊢ M : A does not hold.

As stated, these procedures are of theoretical interest only; we expect that practical implementations would make use of β_{2}-weak-head normal forms instead of full β_{2}-normal forms, amongst other efficiency improvements.

Finally we can state our main result.

Corollary 4.10 (Decidability). Each judgement of λP_{≤} is decidable.

5 Conclusion

Our system λP_{≤} adds subtyping to λP. The system λP is the simplest corner of Barendregt’s λ-cube with type dependency, yet it is the core of many applied type theories for which subtyping is desirable. Subtyping posed a challenge for meta-theoretical study; we met the challenge by proving properties in a carefully chosen order and formulating an algorithmic version of the system. The main result is the decidability of the typing and subtyping relations, achieved using non-trivial extensions of work that dates back to Cardelli’s early ideas [8], Curien and Ghelli’s analysis of F_{≤} [16] and subsequent studies of non-dependent subtyping systems [22, 13, 26].

Of the related work when we began, Pfenning’s study of refinement types [21] is closest. There, a sort is declared as a refinement of a type, and there is a subsorting relation. Whilst subsorting is a richer relation than our subtyping (for example, intersections of sorts are permitted), there is a strict separation between types and sorts to ensure a straightforward proof of decidability of the system. Sorts cannot appear in labels of λ-abstractions, so it is impossible to write functions with domains limited via subsorting, a disadvantage Pfenning mentions. No such restriction applies to our calculus, where subtyping applies uniformly.

Other early related work includes that of Cardelli [8, 9], who gave basic definitions and ideas about semi-decision procedures; Aspinall [1], who describes a system that has subtyping and dependent types but no type variables; Coquand [14] who considers subtyping inductive data types in a dependent type theory, and Betarte and Tasistro who investigated adding dependent records to Martin-Löf’s type theory [6].

There are several ways to continue the work begun here. One goal is to find a semantics for λP_{≤}. The ideal would be to translate λP_{≤} into λP by removing subtyping, along the lines of [7]. We hinted at this understanding in Section 1 when we suggested that the injection function “!” is implicit in the presence of subtyping, as if inserted automatically. To generalise, we must assume families of coercions for each bounded type variable in a λP_{≤} context, and show that there is a canonical way of inserting coercions to translate pre-terms at each level to λP. Then any model of λP will serve as a model of λP_{≤} and the class of logics that can be encoded will be the same as for LF.

For the application of logic encoding, it is well known that including η-conversion in the framework is important. Studying examples, the need for intersection types which Pfenning recognised also seems important, allowing constants to be overloaded. If the techniques of [13] can be adapted, we could reproduce Pfenning’s examples in [21].

In another direction, we need to examine richer type systems, adding the polymorphism and bounded quantification of F_{≤}, and approaching the type theories underlying the proof assistants mentioned in the introduction. We suspect that a careful combination of these features would also give a good type system for a programming language, although investigation of programming with type-dependency alone is in its infancy. And to integrate our work into real proof assistants, we must consider more than type-checking, since systems like Elf and LEGO do more than check proofs. Searching for a proof or applying a tactic involves unification and matching procedures which would need modification to take subtyping into account.

Finally, it would be nice to lift the results to a more general setting, pursuing the idea of adding subtyping to the Calculus of Constructions [15] or to Pure Type Systems [5]. It is easy to formulate such extensions, maybe using Cardelli’s power types [9], but it seems much harder to prove things about them. We believe that variations of the techniques used here may help. Indeed, since publication of [3], this has been achieved. Extending the Calculus of Construction with subtyping has been undertaken by Chen, starting from a system similar to our algorithm [10], and Zwanenburg has extended Pure Type Systems [27]. Both avoid circularity problems by defining subtyping on pre-terms in the first place; but then one is obliged to show that the resulting relation is the intended one on well-formed types, which amounts to proving equivalence results broadly similar to ours. Compagnoni and Goguen have used another technique, Typed Operational Semantics, to study a higher order calculus with bounded operator abstraction and subtyping, containing similar circularities to the ones here [12, 11]. In other related work, Luo has developed a system of coercive subtyping intended for dependent type theories of proof assistants, where a subtyping relation is induced by coercion functions [19].

Acknowledgements. Our sincere thanks are due to R. Constable, M. Dezani, H. Goguen, M. Hofmann, Z. Luo, R. Pollack and D. Sannella for their comments on drafts. The TCS referees gave us useful suggestions for clarifications.

We gratefully acknowledge the support provided by the LFCS, a UK EPSRC studentship and EPSRC grant GR/H73103 (DA), and EPSRC grants GR/K38403, GR/G55792, and CONFER and EuroFOCS (AC).

⟨⟩ ⊢ ⋆  (f-empty)
{Γ ⊢ A : ⋆ \atop Γ, x : A ⊢ ⋆}  (f-term)
{Γ ⊢ K \atop Γ, α : K ⊢ ⋆}  (f-type)
{Γ ⊢ A : K \atop Γ, α ≤ A : K ⊢ ⋆} (f-subtype)
{Γ, x : A ⊢ K \atop Γ ⊢ Πx:A.K}  (f-Π)

Figure 1: Formation of contexts and kinds

⟨⟩ ⊢_{A} ⋆  (af-empty)
\begin{matrix}Γ ⊢_{A} ⋆ & Γ ⊢_{A} A : ⋆ \\ Γ, x : A ⊢_{A} ⋆ \end{matrix}  (af-term)
{Γ ⊢_{A} K \atop Γ, α : K ⊢_{A} ⋆}  (af-type)
\begin{matrix}\begin{matrix}Γ ⊢_{A} K \\ Γ ⊢_{A} A : K′ \end{matrix} & K =_{β} K′ \\ Γ, α ≤ A : K ⊢_{A} ⋆ \end{matrix} (af-subtype)
{Γ, x : A ⊢_{A} K \atop Γ ⊢_{A} Πx:A.K}  (af-Π)

Figure 2: Algorithmic Formation

Γ ⊢ ⋆  α ∈ Dom(Γ)

Γ ⊢ α : Kind_{Γ}(α)

(k-var)

{Γ, x : A ⊢ B : ⋆ \atop Γ ⊢ πx:A. B : ⋆}  (k-π)
{Γ, x : A ⊢ B : K \atop Γ ⊢ Λx:A. B : Πx:A.K}  (k-Λ)
\begin{matrix}Γ ⊢ A : Πx:B.K & Γ ⊢ M : B \\ Γ ⊢ A M : K[x := M] \end{matrix}  (k-app)
\begin{aligned}Γ ⊢ A : K & Γ ⊢ K′ & K =_{β} K′ \\ & Γ ⊢ A : K′ \end{aligned} (k-conv)

Figure 3: Kinding

α ∈ Dom(Γ)
Γ ⊢_{A} α : Kind_{Γ}(α)

(ak-var)

\begin{matrix}Γ ⊢_{A} A : ⋆ & Γ, x : A ⊢_{A} B : ⋆ \\ Γ ⊢_{A} πx:A. B : ⋆ \end{matrix}  (ak-π)
\begin{matrix}Γ ⊢_{A} A : ⋆ & Γ, x : A ⊢_{A} B : K \\ Γ ⊢_{A} Λx:A. B : Πx:A.K \end{matrix}  (ak-Λ)
\begin{matrix}Γ ⊢_{A} A : Πx:B.K & \begin{matrix}Γ ⊢_{A} M : B′ \\ Γ ⊢_{A} B′^{β_{2}} ≤ B^{β_{2}} \end{matrix} \\ Γ ⊢_{A} A M : K[x := M] \end{matrix}  (ak-app)

Figure 4: Algorithmic Kinding

\begin{matrix}Γ ⊢ ⋆ & x ∈ Dom(Γ) \\ Γ ⊢ x : Γ(x) \end{matrix}  (t-var)
{Γ, x : A ⊢ M : B \atop Γ ⊢ λx:A. M : πx:A. B}  (t-λ)
\begin{matrix}Γ ⊢ M : πx:A. B & Γ ⊢ N : A \\ Γ ⊢ MN : B[x := N] \end{matrix} (t-app)
\begin{matrix}Γ ⊢ M : A & Γ ⊢ A ≤ B \\ Γ ⊢ M : B \end{matrix}  (t-sub)

Figure 5: Typing

{x ∈ Dom(Γ) \atop Γ ⊢_{A} x : Γ(x)}  (at-var)
\begin{matrix}Γ ⊢_{A} A : ⋆ & Γ, x : A ⊢_{A} M : B \\ Γ ⊢_{A} λx:A. M : πx:A. B \end{matrix}  (at-λ)
\begin{matrix}Γ ⊢_{A} M : A \\ FLUB_{Γ}(A) ≡ πx:B. C \end{matrix}  \begin{matrix}Γ ⊢_{A} N : B′ \\ Γ ⊢_{A} B′^{β_{2}} ≤ B \end{matrix}

Γ ⊢_{A} MN : C[x := N] (at-app)

Figure 6: Algorithmic Typing

\begin{aligned}Γ ⊢ A : K & Γ ⊢ B : K & A =_{β} B \\ & Γ ⊢ A ≤ B \end{aligned}  (s-conv)
\begin{matrix}Γ ⊢ A ≤ B & Γ ⊢ B ≤ C \\ Γ ⊢ A ≤ C \end{matrix}  (s-trans)
Γ ⊢ ⋆  α bounded in Γ

Γ ⊢ α ≤ Γ(α) (s-var)

\begin{matrix}\begin{matrix}Γ ⊢ A′ ≤ A \\ Γ, x : A′ ⊢ B ≤ B′ \end{matrix} & Γ ⊢ πx:A. B : ⋆ \\ Γ ⊢ πx:A. B ≤ πx:A′. B′ \end{matrix}  (s-π)
{Γ, x : A ⊢ B ≤ B′ \atop Γ ⊢ Λx:A. B ≤ Λx:A. B′}  (s-Λ)
\begin{matrix}Γ ⊢ A ≤ B & Γ ⊢ BM : K \\ Γ ⊢ A M ≤ B M \end{matrix}  (s-app)

Figure 7: Subtyping

\begin{matrix}Γ ⊢_{A} A′ ≤ A & Γ, x : A′ ⊢_{A} B ≤ B′ \\ Γ ⊢_{A} πx:A. B ≤ πx:A′. B′ \end{matrix}  (as-π)
\begin{matrix}A =_{β_{1}} A′ & Γ, x : A′ ⊢_{A} B ≤ B′ \\ Γ ⊢_{A} Λx:A. B ≤ Λx:A′. B′ \end{matrix}  (as-Λ)
{M_{1} =_{β_{1}} M′_{1} ⋯ M_{n} =_{β_{1}} M′_{n} \atop Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ α M′_{1} ⋯ M′_{n}}  (as-app-r)

α bounded in Γ, A ≢ α M_{1} ⋯ M_{n} Γ ⊢_{A} (Γ(α) M_{1} ⋯ M_{n})^{β_{2}} ≤ A

Γ ⊢_{A} α M_{1} ⋯ M_{n} ≤ A (as-app-t)

Figure 8: Algorithmic Subtyping

References

[1] David Aspinall. Subtyping with singleton types. In Proc. Computer Science Logic, CSL’94, Kazimierz, Poland, Lecture Notes in Computer Science 933. Springer-Verlag, 1995.

[2] David Aspinall. Type Systems for Modular Programs and Specification. PhD thesis, Department of Computer Science, University of Edinburgh, 1997.

[3] David Aspinall and Adriana Compagnoni. Subtyping dependent types. In E. Clarke, editor, Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 86–97, New Brunswick, New Jersey, 1996. IEEE Computer Society Press.

[4] Arnon Avron, Furio Honsell, Ian A. Mason, and Robert Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309–354, 1992.

[5] Henk Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science. Oxford University Press, 1992.

[6] Gustavo Betarte and Alvaro Tasistro. Extension of Martin-Löf’s type theory with record types and subtyping. In Proceedings of 25 Years of Constructive Type Theory. Oxford University Press, 1997.

[7] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

[8] Luca Cardelli. Typechecking dependent types and subtypes. In M. Boscarol, L. Carluccia Aiello, and G. Levi, editors, Proc. of the Workshop on Foundations of Logic and Functional Programming, Lecture Notes in Computer Science 306. Springer-Verlag, 1987.

[9] Luca Cardelli. Structural subtyping and the notion of power type. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 70–79, San Diego, California, January 13–15, 1988. ACM SIGACT-SIGPLAN, ACM Press.

[10] Gang Chen. Subtyping calculus of constructions. In Proceedings of 22nd International Symposium, MFCS ’97, volume Lecture Notes in Computer Science 1295, pages 189–198. Springer-Verlag, 1997.

[11] Adriana Compagnoni and Healfdene Goguen. Decidability of higher-order subtyping via logical relations, December 1997.

[12] Adriana Compagnoni and Healfdene Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. To appear in Information and Computation.

[13] Adriana Beatriz Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, Nijmegen Catholic University, 1995.

[14] Thierry Coquand. Pattern matching with dependent types. In Proceedings on Types for Proofs and Programs, pages 71–83, Båstad, Sweden, 1992.

[15] Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, February/March 1988.

[16] Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and typechecking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[17] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. JACM, 40(1):143–184, 1993.

[18] Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. A logic of subtyping (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 292–299, San Diego, California, 26–29 June 1995. IEEE Computer Society Press.

[19] Zhaohui Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, 1999.

[20] Ian A Mason. Hoare’s Logic in the LF. Technical Report ECS-LFCS-87-32, LFCS, Department of Computer Science, University of Edinburgh, June 1987.

[21] Frank Pfenning. Refinement types for logical frameworks. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pages 315–328, May 1993.

[22] Benjamin 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.

[23] Benjamin C. Pierce. Bounded quantification is undecidable. In Proceedings, Nineteenth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 305–315, Albuquerque, New Mexico, January 19–22, 1992. ACM Press.

[24] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994.

[25] Donald Sannella, Stefan Sokołowski, and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica, 29:689– 736, 1992.

[26] Martin Steffen and Benjamin Pierce. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994.

[27] Jan Zwanenburg. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. PhD thesis, Eindhoven University of Technology, 1999. PhD Thesis.