A tutorial on type-based termination

Gilles Barthe^{1} Benjamin Grégoire^{2} Colin Riba^{2}

1 IMDEA Software, Madrid, Spain 2 INRIA Sophia-Antipolis, France

Abstract. This is a tutorial on type-based termination.

1 Introduction

Functional programming languages advocate the use of mathematically intuitive constructions to develop programs. In particular, functional programming languages feature mechanisms to introduce and manipulate finite datatypes such as lists and trees, and infinite datatypes such as streams and infinite trees. There are two basic ingredients to manipulate elements of a datatype: case analysis, that enables to reason by analysis on the top constructor, and fixpoints, that enable to define functions by recursion and co-recursion. Traditionally, functional programming languages allow for unrestricted fixpoints, which are subsumed by the construction

\frac{Γ,f : τ ⊢ e : τ}{Γ ⊢ (letrec_{τ} f = e) : τ}

whose computational behavior is given by the reduction rule

(letrec_{τ} f = e) → e[f := (letrec_{τ} f = e)]

Unrestricted use of fixpoints leads to typable expressions that diverge, i.e. that have an infinite reduction sequence. While non-termination is acceptable in functional programming languages, logical systems based on type theory must be terminating in order to guarantee coherence and decidability of equivalence between terms. Thus, logical systems based on type theory seek to restrict the usage of recursive definitions to enforce termination.

A standard means to enforce termination is to abandon the syntax of functional programming languages and to rely instead on combinators, known as recursors. Such recursors allow to define functions of type d → σ, where d is an inductive datatype such as natural numbers of lists; more generally, the notion of inductive datatype captures in a type-theoretical setting the notion of least fixpoint of a monotone operator. To guarantee termination, recursors combine case analysis and structural recursion, and their reduction rules ensure that recursive calls are applied to smaller arguments. Unfortunately, recursors are not intuitive to use. Therefore, proof assistants based on type theory, such as Coq and Agda, tend to rely on an alternative approach, that maintains the syntax of functional programming languages, but imposes instead syntactic conditions that ensure termination. Restrictions concern both the typing rule and the reduction rule. Restrictions for the typing rule impose conditions, both on the type τ and on the expression e, under which recursive definitions are well-formed. Essentially, the type τ must be of the form d → σ, where d is an inductive datatype, as for recursors. Then, the expression e must be of the form λx: d. b where b can only make recursive calls to f on arguments that are structurally smaller than x. Finally, reductions must be restricted to the case where e is applied to an expression of the form c t⃗ for some constructor c. While the first and third restrictions are easily enforced, it is difficult to find appropriate criteria that enforce the second restriction. A common means to ensure that recursive calls are performed on smaller arguments is to define a syntactic check on the body b of recursive calls. However, such a syntactic approach is problematic, as shall be explained in the course of this chapter.

Type-based termination is an alternative approach to guarantee strong normalization of typable expressions through the use of a non-standard typing system in which inhabitants of inductive datatypes are given a size, which in turn is used to guarantee termination of recursive definitions. Type-based termination draws its inspiration from the set-theoretic and domain-theoretic semantics of inductive definitions, in which inductive sets are viewed as the upper limit of their approximation. In effect, type-based termination embeds these semantical intuitions into the syntax of the type theory, by letting inductive datatypes carry size annotations, and by restricting the rule for fixpoints

\frac{Γ,f : d^{ı}→ σ ⊢ e : dî→ σ}{Γ ⊢ (letrec_{d^{∞} →σ} f = e) : d^{∞} → σ}

where d is an inductive datatype, ı is an arbitrary (i.e. implicitly quantified universally) size, d^{ı} denotes the ı-approximation of d, and dî denotes the next approximation of d, and d^{∞} denotes the inductive datatype itself. As should appear from the typing rule, termination is enforced naturally by requiring that recursive calls, that correspond to occurrences of f in e, can only be made to smaller elements, as f only takes as arguments elements of type d^{ı}.

Type-based termination benefits from essential characteristics that make it an attractive means to ensure termination of recursive definitions in a typed λ-calculus, both from the point of view of the users and of the designers of the type system. First and foremost, it is intuitive and easy to grasp, since the type system simply captures the idea that a recursive definition terminates whenever the size of arguments decreases in recursive calls. As a consequence, the type system is also predictable (i.e. it is possible to have a priori an intuition as to whether a definition is correct) and transparent (i.e. it is possible a posteriori to understand why a definition is incorrect) for users, which we view as essential properties of a formal system. Second, type-based termination is expressive: even for the simplest instance of type-based termination, in which the arithmetic of stages only builds on zero, successor and infinity, type-based termination is sufficiently powerful to encode many typed λ-calculi using syntactic termination criteria, and to provide precise typings for some functions that do not increase the size of their arguments (i.e. for unary functions the size of the result is smaller or equal than the size of the argument). Third, type-based termination is based on a solid theoretical foundation, namely that of approximation, which substantially simplifies in the development of realizability models. As shall be illustrated in Section 3.4, there is a good match between the syntax of the type system and its semantics, which facilitates the interpretation of recursive definitions in the realizability model. Fourth, type-based termination isolates in the design of the type system itself the components that are relevant for termination, i.e. constructors, case analysis, and fixpoint definitions, from the remaining components, whose syntax and typing rules are unaffected. Such a separation makes type-based termination robust to language extensions, and compatible with modular verification and separate compilation.

In summary, type-based termination appears as a suitable approach to guarantee strong normalization of typable terms, which in the near future may well supplant syntactic methods that are currently in use in logical systems based on type theory. On this account, the main objective of this tutorial is to provide a gentle introduction to typebased termination. For pedagogical purposes, we start with a review of mechanisms to introduce recursive definitions in typed λ-calculi, and proceed to define a type system that uses type-based termination. Then, we provide high-level proofs of the essential properties of the type system, in particular of strong normalization and of decidability of type inference; we explain the latter in great length, because of the complexity of the algorithm. We conclude with a brief examination of some possible extensions to our system, and a brief account of related work. For simplicity, we focus on a polymorphically typed λ-calculus, although all of the results that we present in this chapter scale up to dependent types.

2 Computations in polymorphic type systems

This section presents the basic framework of this tutorial and the main problem we want to address: having a convenient way for computing in type systems issued from the Curry-Howard isomorphism, while preserving crucial logical properties such as subject reduction, strong normalization and coherence.

We start in Sect. 2.1 from Girard’s System F, with terms à la Church, as presented in [8]. This system enjoys strong normalization and coherence. It has interesting computing capabilities, since it can encode every inductive datatype and every function provably total in second order Peano’s arithmetic [8]. However, it has a quite unsatisfactory algorithmic behavior, since basic functions such as the predecessor function on Church’s numerals is not implementable in constant time [11], and it is more generally the case of primitive recursion over all inductive datatypes, at least when the computing relation is β-reduction [12].

Hence, from the computational point of view, it is convenient to add datatypes and recursion to System F, leading to System F^{rec} presented in Sect. 2.2. However, F^{rec} lacks both strong normalization and coherence, because of general recursion and of the ability to define non well-founded datatypes.

We address the problem of datatypes in Sect. 2.3, where we present the notion of inductive datatypes. Concerning the problem of general recursion, we recall in Sect. 2.5 a syntactic termination criteria, which allows to retrieve strong normalization and coherence. The limitations of such criteria motivate the use of type-based termination, to be presented in Sect. 3.

2.1 System F

We begin by a short review of System F [8].

Types. We assume given a set 𝒱_{𝒯} of type variables. The set 𝒯 of types is given by the abstract syntax:

𝒯 ::= 𝒱_{𝒯} | 𝒯 → 𝒯 | Π𝒱_{𝒯} . 𝒯

Types are denoted by lower-case Greek letters σ,τ,θ,.... Free and bound variables are defined as usual. The capture-avoiding substitution of τ⃗for X⃗ in σ is written σ[X⃗:= τ⃗]. We let FV_{𝒯} (e) be the set of type variable occurring free in τ. A type τ is closed if FV_{𝒯} (τ) = ∅.

Example 2.1.

(i) The type of the polymorphic identity is

ΠX. X → X

(ii) It is well-known that inductive datatypes can be coded into System F, see e.g. [8]. For instance, Peano’s natural numbers can be encoded as Church’s numerals, whose type is

N_{Ch} := ΠX. X → (X → X) → X

From this type, we can read that Church numerals represent the free structure built from one nullary constructor (which stands for 0), and one unary constructor (which stands for the successor).

(iii) The ”false” proposition is

⊥ := ΠX. X
⊓ ⊔

Terms and reductions. We assume given a set 𝒱_{ℰ} = {x,y,z,...} of (object) variables. The set ℰ of terms is given by the abstract syntax:

ℰ ::= 𝒱_{ℰ} | λ𝒱_{ℰ} : 𝒯. ℰ | Λ𝒱_{𝒯} . ℰ | ℰ ℰ | ℰ 𝒯

Free and bound variables, substitution, etc. are defined as usual. The capture-avoiding substitution of e′for x in e is written e[x := e′]. We let FV_{ℰ} (e) be the set of free term variables occurring in e. We say that e is closed when FV_{ℰ} (e) = ∅.

The reduction calculus is given by β-reduction for function application and type instantiation. Formally, β-reduction →_{β} is defined as the compatible closure of

(λx: τ. e) e′ ≻_{β} e[x:= e′] and (ΛX. e) τ ≻_{β} e[X := τ]

The rewrite system β is orthogonal; it follows that the relation →_{β} is confluent.

Notation 2.2. We write e →_{β}^{n} e′if there is k ≤ n such that

e \underbrace{→_{β} ... →_{β}}_{k times} e′

Example 2.3.

(i) The polymorphic identity is ΛX. λx: X. x. (ii) The Church’s numerals are terms of the form

c_{n} := ΛX. λx: X. λf : X → X. f^{n}x

The numeral c_{n} encodes the natural number n by computing iterations. Indeed, the expression c_{n}pf performs n iterations of f on p:

c_{n} p f →_{β}^{∗} \underbrace{f ··· (f}_{n times} p) = f^{n} p

The constructors of Church’s numerals are the terms Z and S defined as:

\begin{matrix}Z := & ΛX. λx: X. λf : X → X. x \\ S := & λn: N_{Ch}. ΛX. λx: X. λf : X → X. f (nX xf) \end{matrix}

where N_{Ch} is the type of Church’s numerals defined in Ex. 2.1.(ii). Given τ ∈ 𝒯, we can code iteration at type τ with the term

Iter_{τ} u v n := n τ u v

For all n,u,v ∈ ℰ we have

Iter_{τ} u v Z  →_{β}^{2} (λx: τ. λf : τ → τ. x) u v  →_{β}^{2} u
Iter_{τ} u v (S n) →_{β}^{2} (λx: τ. λf : τ → τ. f (n τ x f)) u v →_{β}^{2} v (n τ u v)

Hence, Iter_{τ}uv(Sn) β-reduces in four steps to v(Iter_{τ}uvn). Using this iteration scheme, every function provably total in second order Peano’s arithmetic can be coded in System F [8]. ⊓ ⊔

Typing. A context is a map Γ : 𝒱_{ℰ} → 𝒯 of finite domain. Given x ∉ dom(Γ), we let Γ,x: τ be the context

(Γ,x: τ)(y) =_{def} \{ \begin{matrix}τ & if y = x \\ Γ(y) & otherwise \end{matrix}

The notation Γ,x: τ always implicitly assumes that x ∉ dom(Γ). The typing relation of System F is the smallest relation Γ ⊢ e : τ closed under the rules of Fig. 1.

Example 2.4.

(i) As expected, the polymorphic identity of Ex. 2.3.(i)can be given the type of Ex. 2.1.(i):

⊢ ΛX. λx: X. x : ΠX. X → X

(ii) As expected also, Church’s numerals can be given the type N_{Ch}:

⊢ ΛX. λx: X. λf : X → X. f^{n}x : ΠX. X → (X → X) → X

Moreover, we have Z : N_{Ch} and S : N_{Ch} → N_{Ch}. Iteration can be typed as follows:

n: N_{Ch},u: τ,v: τ → τ ⊢ Iter_{τ} n u v : τ

⊓ ⊔

(var) \overline{Γ,x : σ ⊢ x : σ}

(abs) \frac{Γ,x : τ ⊢ e : σ}{Γ ⊢ λx: τ. e : τ → σ}  (app) \frac{Γ ⊢ e : τ → σ  Γ ⊢ e′ : τ}{Γ ⊢ e e′ : σ}

(T-abs) \frac{Γ ⊢ e : σ}{Γ ⊢ ΛX. e : ΠX. σ} if X ∉ Γ  (T-app) \frac{Γ ⊢ e : ΠX. σ}{Γ ⊢ e τ : σ[X := τ]}

Fig. 1. Typing rules of System F

Some important properties. We have seen that System F has some computing capabilities. As a programming language, one of the most important property of the type system is subject reduction.

Theorem 2.5 (Subject reduction). If Γ ⊢ e : τ and e →_{β} e′, then Γ ⊢ e′ : τ.

Terms typable in System F enjoy a very strong computational property: they are strongly normalizing. A term is strongly normalizing if every reduction sequence starting from it is finite. We can thus define the set SN_{β} of strongly β-normalizing terms as being the smallest set such that

∀e. (∀e′. e →_{β} e′ ⟹ e′∈ SN_{β}) ⟹ e ∈ SN_{β}

Strong normalization is also useful for the implementation of the language, because it ensures that every reduction strategy (i.e. every way of reducing a term) is terminating. Strong normalization can be proved using the reducibility technique [8], which is sketched in Sect. 3.4.

Theorem 2.6 (Strong normalization). If Γ ⊢ e : τ then e ∈ SN_{β}.

We now discuss some logical properties of System F. It is easy to see that Γ ⊢ e : ⊥ implies Γ ⊢ eτ : τ for all type τ. According to the Curry-Howard propositions-as-types isomorphism, this means that the type ⊥ is the false proposition: every proposition τ can be deduced from it. Therefore, having Γ ⊢ e : ⊥ means that everything can be deduced from Γ. From a logical perspective, it is crucial to ensure that there is no term of type ⊥ in the empty context. This property is fortunately satisfied by System F. It can be proved by syntactical reasoning, using subject reduction and strong normalization, but a direct reducibility argument is also possible, see Sect. 3.4.

Theorem 2.7 (Coherence). In System F, there is no term e such that ⊢ e : ⊥.

2.2 A polymorphic calculus with datatypes and general recursion

It is well-known that System F has limited computational power, e.g. it is not possible to encode in System F a predecessor function that computes in constant time. Therefore, programming languages and proof assistants rely on languages that extend the λ-calculus with new constants and rewrite rules. In this section, we discuss one such extension of System F à la Church, as presented in Sect. 2.1. This system, called F^{rec}, consists in adding datatypes and general recursion to System F. Before giving the formal definitions, we informally present the system with some examples of datatypes. We then recall some well-known examples showing that System F^{rec} lacks two of the most important properties of System F, namely termination and coherence.

Basic features. In System F^{rec}, we represent the type natural numbers using a special type constant Nat. Furthermore, the language of λ-terms is extended by two constants o : Nat and s : Nat → Nat representing the two constructors of Nat. All this information is gathered in the datatype definition:

Datatype Nat := o : Nat | s : Nat → Nat

This defines Nat as the least type build from the nullary constructor o and the unary constructor s.

Example 2.8. We can now represent the number n by the term s^{n}o. ⊓ ⊔

System F^{rec} provides two ways of computing on datatypes. The first one performs the destruction of constructor-headed terms, and allows to reason by case-analysis, similarly as in functional programming languages. For instance, we can define the predecessor function as follows:

pred := λx: Nat. case_{Nat} x of {o ⇒ o
| s ⇒ λy: Nat. y }

This function is evaluated as follows:

predo → case_{Nat} o of {o ⇒ o | s ⇒ λy: Nat. y} → o
pred(sn) → case_{Nat} (sn) of {o ⇒ o | s ⇒ λy: Nat. y} → (λy: Nat. y)n → n

and is typed using the rule

\frac{x: Nat ⊢ x : Nat  x: Nat ⊢ o : Nat  x: Nat ⊢ λy: Nat. y : Nat → Nat}{x: Nat ⊢ case_{Nat} x of \{o ⇒ o | s ⇒ λy: Nat. y\} : Nat}

Performing a case analysis over an expression e of type Nat means building an object of a given type, say σ, by reasoning by cases on the constructors of Nat. We therefore must provide a branch e_{o} for the case of o and a branch e_{s} for the case of s. If e evaluates to o, then the case-analysis evaluates to e_{o}, and if e evaluates to sn, then the we get e_{s} n:

case_{σ} o of {o ⇒ e_{o} | s ⇒ e_{s}}  → e_{o}
case_{σ} (s n) of {o ⇒ e_{o} | s ⇒ e_{s}}  → e_{s} n

Since this case-analysis must evaluate to a term of type σ, we must have e_{o} : σ and e_{s} : Nat → σ. We therefore arrive at the general rule for case-analysis over natural numbers:

(case) \frac{Γ ⊢ e : Nat  Γ ⊢ e_{o} : σ  Γ ⊢ e_{s} : Nat → σ}{Γ ⊢ case_{σ} e of \{o ⇒ e_{o} | s ⇒ e_{s}\} : σ}

The second computing mechanism of System F^{rec} is general recursion. The system is equipped by a general fixpoint operator (letrec_{τ} f = e), which is typed by the rule

(rec) \frac{Γ,f : τ ⊢ e : τ}{Γ ⊢ (letrec_{τ} f = e) : τ}

and which reduces as follows:

(letrec_{τ} f = e) → e[f := (letrec_{τ} f = e)]

This allows to encode efficiently primitive recursion over natural numbers.

Example 2.9 (Gödel’s System T). In F^{rec}, we can encode primitive recursion on natural numbers as follows:

rec := ΛX. (letrec_{Nat→X} rec = λx: Nat. λu: X. λv: Nat → X → X.
case_{X} x of {o ⇒ u
| s ⇒ λy: Nat. v y (rec y u v) }
) : ΠX. Nat → (Nat → X → X) → X → X

Therefore, writing rec_{τ} for the head β-reduct of rec τ, we have the following reductions, which are performed in a constant number of steps:

rec_{τ} o u v →^{6} u and rec_{τ} (s n) u v →^{6} v n (rec_{τ} n u v)

⊓ ⊔

Functions defined by primitive recursion can also be directly coded in F^{rec}. Take for instance the addition and subtraction on Nat.

Example 2.10 (Addition of two natural numbers).

plus := (letrec_{Nat→Nat→Nat} plus = λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ y
| s ⇒ λx′: Nat. s (plus x′y) }

) : Nat → Nat → Nat

⊓ ⊔

Example 2.11 (Subtraction of natural numbers).

minus := (letrec_{Nat→Nat→Nat} ms= λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ x
| s ⇒ λx′: Nat. case_{Nat} y of {o ⇒ x
| s ⇒ λy′: Nat. msx′y′}
}

) : Nat → Nat → Nat

⊓ ⊔

Since general fixpoints are allowed, we can also give definitions where recursive calls are not performed on structurally smaller terms. This is the case of the Euclidean division on natural numbers. We will see in Sect. 3 that this function terminates.

Example 2.12 (Euclidean division). This program for the Euclidean division depends on the function minus. It is not typable in systems with a syntactic guard predicate, as, syntactically, (minusx′y) is not properly structurally smaller than x in the program below.

div := (letrec_{Nat→Nat→Nat} div= λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ o
| s ⇒ λx′: Nat. s (div(minus x′y) y) }

) : Nat → Nat → Nat

⊓ ⊔

Polymorphic datatypes. System F^{rec} features polymorphic datatypes, such as polymorphic lists and polymorphic trees.

Polymorphic lists have two constructors, nil and cons, typed as follows:

nil : ΠX. List X cons : ΠX. X → List X → List X

Hence, lists of type Listτ are lists parametrized by the type τ. This is materialized by the definition:

Datatype List X := nil : List X | cons : X → List X→ List X

List are eliminated using case-analysis, along a pattern similar to that of natural numbers. The case-analysis of polymorphic lists is performed on one particular instantiation of the datatype:

(case) \frac{Γ ⊢ e : List τ  Γ ⊢ e_{nil} : σ  Γ ⊢ e_{cons} : τ → List τ → σ}{Γ ⊢ case_{σ} e of \{nil ⇒ e_{nil} | cons ⇒ e_{cons}\} : σ}

This means that nilτ can be the subject of case-analysis, while nil can not. Accordingly, the branches of the case-analysis must be typable with the corresponding instantiation of the polymorphic type: e_{cons} takes an argument of type Listτ, but not of type ΠX. ListX. The reduction rules are similar to that of natural numbers:

case_{σ} (nil τ) of {nil ⇒ e_{nil} | cons ⇒ e_{cons}}  → e_{nil}
case_{σ} (cons τ x xs) of {nil ⇒ e_{nil} | cons ⇒ e_{cons}} → e_{cons} x xs

Here are two basic functions on lists, namely the concatenation of two lists and the map function.

Example 2.13 (The concatenation of two lists).

app := ΛX. (letrec_{ListX→ListX→ListX} app = λx: List X. λy: List X.
case_{ListX} x of {nil ⇒ y
| cons ⇒ λz: X. λx′: List X. cons X z (app x′y)
}
) : ΠX. List X→ List X→ List X
⊓ ⊔

Example 2.14 (The map function on a list).

map := ΛX. ΛY. λf : X → Y. (letrec_{ListX→ListY} map = λx: ListX.
case_{ListY} x of {nil ⇒ nil
| cons ⇒ λz: X. λx′: ListX. cons Y (f z) (map f x′)
}
) : ΠX. ΠY. (X → Y) → List X→ List Y
⊓ ⊔

We can also define the concatenation of a list of lists. In F^{rec} the polymorphic type of lists of lists is ΠX. List (List X). The concatenation of a list of lists is therefore of type ΠX. List (List X) → List X.

Example 2.15 (The concatenation of a list of lists).

conc := ΛX. (letrec_{List(ListX)→ListX} conc = λx: List(ListX).
case_{ListX} x of {nil ⇒ nil
| cons ⇒ λz: ListX. λx′: List(ListX). app X z (conc x′)
}

) : ΠX. List (List X) → List X

⊓ ⊔

An other interesting polymorphic type is that of polymorphic finitely branching trees. These trees are composed of leaves, with one token of information, and of inner nodes, with one token of information and a list of successor subtrees. These two kinds of nodes are represented by the same constructor:

node : ΠX. X → List (Tree X) → Tree X

For instance, the types of trees of natural numbers is Tree Nat, and a leave with token n is represented by node Nat n (nil (Tree Nat)). The important point with this type is that the recursive argument of nodeτ, which is a list of trees of τ, is not directly of type Treeτ but of type List(Treeτ). This allows to encode trees where each node can have a different, but finite, arity.

Like natural numbers and lists, trees are eliminated by case-analysis. Since this type has only one constructor, the scheme of elimination essentially performs the projection of that constructor:

(case)

Γ ⊢ e : List τ Γ ⊢ e_{node} : τ → List (Tree τ) → σ
Γ ⊢ case_{σ} e of {node ⇒ e_{node}} : σ

The reduction rule is as follows:

case_{σ} (nodeτxl) of {node ⇒ e_{node}} → e_{node} xl

For instance, the first projection is typed as

\frac{Γ ⊢ e : List τ Γ ⊢ λx: τ. λl : List (Tree τ). x : τ → List (Tree τ) → τ}{Γ ⊢ case_{τ} e of \{node ⇒ λx: τ. λl : List (Tree τ). x\} : τ}

and we have case_{τ} (node τ x l) of {node ⇒ λx: τ. λl : List (Tree τ). x} →^{3} x. The following example treats the flattening of finitely branching trees.

Example 2.16 (Flattening of finitely branching trees). This program depends on map, defined in Ex. 2.14 and on conc, defined in Ex. 2.15. Similarly to div, it is not typable in systems with a syntactic guard predicate.

flatten := ΛX. (letrec_{TreeX→ListX} flat= λt : TreeX. case_{List X} t of {

node ⇒ λx: X. λl : List (Tree X). cons x (conc (map flat l)) } ) : ΠX. Tree X → List X

For readability, we have left the instantiation of polymorphic types implicit at the term level, but note that map flatl should have been written map (Tree X) (List X) flatl with

map (Tree X) (List X) : (Tree X → List X) → List (Tree X) → List (List X)

and that conc (map flat l) should have been written

conc X (map (Tree X) (List X) flat l) with conc X : List (List X) → List X

⊓ ⊔

Higher-order datatypes. Up to now, we only have presented first order datatypes, i.e. datatypes whose inhabitants represent particular forms of finitely branching trees.

There can in fact be much more powerful datatypes, representing infinitely branching trees, that we call higher-order datatypes. One of them is the type Ord of Brouwer’s ordinals. It is defined as follows:

Datatype Ord := o : Ord | s : Ord → Ord | lim : (Nat → Ord) → Ord

Thanks to the constructors o : Ord and s : Ord → Ord, Brouwer’s ordinals contain natural numbers. This is represented by the canonical injection inj : Nat → Ord defined as follows:

inj := (letrec_{Nat→Ord} inj = λx: Nat.
case_{Nat} x of {o ⇒ o
| s ⇒ λx′: Nat. s (inj x′)}
) : Nat → Ord

For all p ∈ ℕ, we have inj (s^{p}o) → s^{p}o. Moreover, ordinals also feature the higherorder constructor lim : (Nat → Ord) → Ord. The expression lim f represents the supremum of the countable list of ordinals represented by f : Nat → Ord. For instance, lim inj is a term-level representation of the set of natural numbers.

Addition of ordinals can easily be defined in F^{rec}.

Example 2.17 (The addition of two ordinals).

add := (letrec_{Ord→Ord→Ord} add = λx: Ord. λy: Ord.
case_{Ord} x of {o ⇒ y
| s ⇒ λx′: Ord. s (add x′y)
| lim ⇒ λf : Nat → Ord. lim (λz: Nat. add (f z) y)
}

) : Ord → Ord → Ord

The addition of lim f and o is the limit for n: Nat of the addition of each f n and o. For instance, add (lim inj) o →^{∗} lim (λx: Nat. add (inj x) o). ⊓ ⊔ Formal definition. Now that we have presented the main features of F^{rec}, we can give its formal definition.

At the type level, F^{rec} extends System F with datatypes, which have names taken in a set 𝒟 of datatypes identifiers. Moreover, each datatype has a fixed number of parameters. Hence we assume that each datatype identifier d ∈ 𝒟 comes equipped with an arity ar(d).

Example 2.18. We have ar(Nat) = 0 and ar(List) = ar(Tree) = 1. ⊓ ⊔

Formally, the types of F^{rec} extend that of System F as follows:

𝒯 ::= ... | 𝒟 𝒯⃗

where in 𝒟 𝒯⃗, it is assumed that the length of the vector 𝒯⃗ is exactly the arity of the datatype.

We now turn to datatype declarations. Each datatype d ∈ 𝒟 has a fixed set of constructors 𝒞(d), and each constructor c ∈ 𝒞(d) is assigned a closed type of the form

ΠX⃗. θ_{1} → ... → θ_{p} → d X⃗

Note that the arity condition on d imposes that X⃗ has the same length for all c ∈ 𝒞(d). We let 𝒞 =_{def} ⋃ {𝒞(d) | d ∈ 𝒟}. The declaration of a datatype, which gathers its parameters, its constructors and their types, is performed in a datatype definition of the form:

Datatype d X⃗ := c_{1} : σ_{1} | ... | c_{n}: σ_{n}

where 𝒞(d) = {c_{1}, ... ,c_{n}} and each σ_{k} is of the form θ⃗_{k} → d X⃗. Given k ∈ {1,...,k}, we write c_{k}: ΠX⃗. θ⃗_{k} → d X⃗.

Example 2.19. We recapitulate here the datatypes that we have already seen. All these datatypes represent a form of well-founded trees. We call them inductive, and come back on this notion in Sect. 2.3. Moreover, we give an example of a non-well founded datatype, noted D.

(i) The inductive datatype of natural number is defined as

Datatype Nat := o : Nat | s : Nat → Nat

(ii) The inductive datatype of polymorphic lists is defined as

Datatype List X := nil : List X | cons : X → List X→ List X

(iii) The inductive datatype of polymorphic finitely branching trees is

Datatype Tree X := node : X → List (Tree X) → Tree X

(iv) The inductive datatype of Brouwer’s ordinals is defined as

Datatype Ord := o : Ord | s : Ord → Ord | lim : (Nat → Ord) → Ord (v) The following datatype is not well-founded. We will see in Ex. 2.22 that it allows

to build a non-terminating term of type ⊥.

Datatype D := c : (D → ⊥) → D

⊓ ⊔

The terms of System F^{rec} extend those of the Church’s style System F with constructors, case-expressions and recursive definitions:

ℰ ::= ... | 𝒞 | case_{𝒯} ℰ of {𝒞⃗ ⇒ ℰ⃗} | (letrec_{𝒯} 𝒱_{ℰ} = ℰ)

The reduction calculus extends β-reduction with ι-reduction for case analysis and μ-reduction for unfolding recursive definitions. Formally,

– ι-reduction →_{ι}is defined as the compatible closure of

case_{σ} (c_{i} τ⃗ a⃗) of {c_{1} ⇒ e_{1} | ... | c_{n} ⇒ e_{n}} ≻_{ι} e_{i} a⃗

– μ-reduction →_{μ} is defined as the compatible closure of

(letrec_{τ} f = e) ≻_{μ} e[f := (letrec_{τ} f = e)]

Then, βιμ-reduction, written →_{βιμ}, is →_{β} ∪ →_{ι}∪ →_{μ}. The relation →_{βιμ} is confluent.

(cons) \overline{Γ ⊢ c_{k} : ΠX⃗. θ⃗_{k} → d X⃗} if c_{k} ∈ 𝒞(d) for some d (rec) \frac{Γ,f : τ ⊢ e : τ}{Γ ⊢ (letrec_{τ} f = e) : τ}

(case) \frac{\begin{aligned}& c_{k}: ΠX⃗. θ⃗_{k} → d X⃗ \\ Γ ⊢ e : dτ⃗ & Γ ⊢ e_{k} : θ⃗_{k}[X⃗:= τ⃗] → σ & (1 ≤ k ≤ n) \end{aligned}}{Γ ⊢ case_{σ} e of \{c_{1} ⇒ e_{1} | ···| c_{n} ⇒ e_{n}\} : σ} if 𝒞(d) = \{c_{1},...,c_{n}\}

Fig. 2. Typing rules for F^{rec}

The type system is standard. The typing relation Γ ⊢ e : τ extends that of System F with the rules given in Fig. 2. System F^{rec} enjoys subject reduction.

Theorem 2.20 (Subject reduction). If Γ ⊢ e : τ and e →_{βιμ}e′, then Γ ⊢ e′ : τ.

Non-termination and incoherence. In this paragraph, we show that although convenient for computing, System F^{rec} lacks two of the most important properties of System F, namely termination and coherence. These problems are due to the presence of general recursion and non well-founded datatypes. We recall two independent examples, one involving unrestricted recursion and the other involving the non well-founded datatype D of Ex. 2.19.(v). Both examples provide a non-terminating incoherent term, that is, a non-terminating closed term of type ⊥.

Example 2.21 (Recursion). The typing rule (rec) for fixpoints can be instantiated as:

\frac{f : ⊥ ⊢ f : ⊥}{⊢ (letrec_{⊥} f = f) : ⊥}

The closed term (letrec_{⊥} f = f) of type ⊥ is non-terminating:

(letrec_{⊥} f = f) →_{μ} (letrec_{⊥} f = f) →_{μ} ...
⊓ ⊔

The second well-known example shows how to write a non-normalizing term using case-analysis on the non well-founded datatype D of Ex. 2.19.(v). Note that it involves no recursion.

Example 2.22 (Non well-founded datatypes [10]). Consider the non well-founded datatype D of Ex. 2.19.(v). Recall that c : (D → ⊥) → D and let

p := λx: D. case_{D→⊥} x of {c ⇒ λy: D → ⊥. y}

We can derive

x: D ⊢ x : D x: D ⊢ λy: D → ⊥. y : (D → ⊥) → (D → ⊥)
x: D ⊢ case_{D→⊥} x of {c ⇒ λy: D → ⊥. y} : D → ⊥
⊢ λx: D. case_{D→⊥} x of {c ⇒ λy: D → ⊥. y} : D → (D → ⊥)

That is p: D → (D → ⊥). Furthermore, let ω_{D} := λx: D. p x x: D → ⊥. We then have c ω_{D} : D, hence p (c ω_{D}) (c ω_{D}) : ⊥. This incoherent term is non-terminating:

p (c ω_{D}) (c ω_{D}) →_{βι}^{∗} (λx: D. p x x) (c ω_{D}) →_{βι} p (c ω_{D}) (c ω_{D}) →_{βι} ...

⊓ ⊔

These two examples show that to achieve termination and coherence, we must restrict the formation of both recursive definitions and datatypes.

2.3 Inductive datatypes

We begin by discussing datatypes. In order to ensure the safety of case-analysis over datatypes, we ensure that datatypes can be constructed by induction. This leads to inductive datatypes, to be defined in Def. 2.25. The key ingredient of inductive datatypes is their positivity.

Definition 2.23 (Positivity). Let σ nocc τ if σ does not occur in τ. The predicate σ pos τ (resp. σ neg τ), stating that all occurrences of σ in τ are positive (resp. negative), is inductively defined in Fig. 3.

\overline{σ pos σ}

\frac{σ nocc τ}{σ pos τ}

\frac{σ neg τ_{2} σ pos τ_{1}}{σ pos τ_{2} → τ_{1}}

\frac{σ pos τ}{σ pos ΠX. τ}

\frac{σ pos τ_{i} (1 ≤ i ≤ ar(d))}{σ pos dτ⃗}

\frac{σ nocc τ}{σ neg τ}

\frac{σ pos τ_{2} σ neg τ_{1}}{σ neg τ_{2} → τ_{1}}

\frac{σ neg τ}{σ neg ΠX. τ}

\frac{σ neg τ_{i} (1 ≤ i ≤ ar(d))}{σ neg dτ⃗}

Fig. 3. Positivity and negativity of a type occurrence

Example 2.24. In the following types, the occurrences of τ are positives and the occurrences of σ are negative:

τ  σ → τ  (τ → σ) → τ

In particular, Nat pos Nat, Tree Xpos List (Tree X)and Ord pos (Nat → Ord), but not D pos (D → ⊥). ⊓ ⊔

Inductive datatypes are datatypes d ∈ 𝒟 in which d and its parameters occur only positively in the type of their constructors.

Definition 2.25 (Inductive datatypes).

(i) An inductive datatype definition is a datatype declaration

Datatype d X⃗ := c_{1} : σ_{1} | ... | c_{n}: σ_{n}

where for all k ∈ {1,...,n}, σ_{k}is of the formθ⃗_{k}→ d X⃗with X⃗pos θ⃗_{k} and d X⃗pos θ⃗_{k}. Inductive datatypes definitions are written

Inductive d X⃗ := c_{1} : σ_{1} | ... | c_{n}: σ_{n}

(ii) An environment is a sequence of datatype definitions I_{1} ...I_{n} in which constructors of the datatype definition I_{k} only use datatypes introduced by I_{1}...I_{k}.

In the remainder of this tutorial, we implicitly assume given an environment in which every d ∈ 𝒟 is an inductive datatype.

Example 2.26. The datatypes Nat, List, Tree and Ord are inductive, but D is not. ⊓ ⊔ 2.4 Guarded reduction for strong normalization

The μ-reduction is inherently non strongly normalizing. Since

(letrec_{τ} f = e) →_{μ} e[f := (letrec_{τ} f = e)]

there are infinite μ-reductions starting from every expression (letrec f = e) such that f occurs free in e. Hence, devising termination criteria for fixpoints (letrec f = e) is not sufficient to ensure strong-normalization. We need in addition a syntactical way to control the unfolding of fixpoints.

On the other hand, it is possible to restrict fixpoints to functions whose domain is a datatype. This will allow us to formulate a requirement for termination stating that fixpoints must be functions defined by induction on an inductive datatype. Therefore, instead of the rule (rec) of Fig. 2, we will restrict to the following typing rule:

\frac{Γ,f : dτ⃗→ θ ⊢ e : dτ⃗→ θ}{Γ ⊢ (letrec_{dτ⃗→θ} f = e) : dτ⃗→ θ}  (1)

If fixpoints are typed by the rule (1) instead if (rec), then we can replace μ-reduction with a notion of guarded γ-reduction →_{γ} defined as the compatible closure of:

(letrec_{dτ⃗→θ} f = e) (c τ⃗ a⃗) ≻_{γ} e[f := (letrec_{dτ⃗→θ} f = e)] (c τ⃗ a⃗)

Definition 2.27 (Guarded reduction). The relation → is defined as

→ =_{def} →_{β} ∪ →_{ι} ∪ →_{γ}

The relation → is confluent since the rewrite system βιγ is orthogonal.

Note that all examples on natural numbers, lists, trees and ordinals presented in Sect. 2.2 can by typed with the rule (1). However, it does not rule out non-terminating and incoherent expressions.

Example 2.28 (Non-termination and incoherence). We can derive

\frac{f : Nat → ⊥ ⊢ f : Nat → ⊥}{⊢ (letrec_{Nat→⊥} f = f) : Nat → ⊥}

and we have (letrec_{Nat→⊥} f = f) o : ⊥ with

(letrec_{Nat→⊥} f = f) o → (letrec_{Nat→⊥} f = f) o → ...
⊓ ⊔

2.5 Syntactic termination criteria

Termination of recursive definitions can be enforced by adopting the guarded reduction rule of Definition 2.27 and by restricting the rule for recursive definitions:

\frac{Γ,f : dτ⃗→ σ ⊢ λx: dτ⃗. a : dτ⃗→ σ 𝒢_{f}^{x}(∅,a)}{Γ ⊢ (letrec f = λx: dτ⃗. a) : dτ⃗→ σ}

where the guard predicate 𝒢 is defined to ensure that the calls to f are performed over expressions that are structurally smaller than x. Informally, a recursive definition is guarded by destructors, i.e. satisfies 𝒢, if all occurrences of f in e are protected by a case analysis on x and are applied to a subcomponent of x. The notion of subcomponent is defined as the smallest transitive relation such that the variables that are introduced in the branches of a case analysis are subcomponents of the expression being matched. On this account, the addition on natural numbers, which we recall from Sect. 2.2:

plus := (letrec_{Nat→Nat→Nat} plus = λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ y
| s ⇒ λx′: Nat. s (plus x′y) }

) : Nat → Nat → Nat

is guarded, since the only application of plus is protected by a case analysis on x, the formal argument of plus. The argument of this application is the pattern variable n, which is a component of x.

It is important to consider not only direct components of the formal argument of recursive definitions, but also inner components (i.e. components derived by transitivity), as illustrated by the following predicate function that checks whether a natural number is even:

(letrec even = λx: Nat. case x of { o ⇒ true
| s ⇒ λy: Nat. case y of {o ⇒ false
| s ⇒ λz: Nat. even z}}
) : Nat → Bool

In this example the application of even is guarded by a case analysis on the argument x. The argument of this application is the pattern variable z, an inner component of x which becomes available in the case analysis on the pattern variable y, a direct component of x.

The formal definition of the guard predicate 𝒢_{f}^{x}(V,a) involves, in addition to the identifier f of the recursive function and x of its formal parameter and the body a of the definition, a set V of variables that is used to collect the pattern variables in a representing the components of x. The definition of 𝒢_{f}^{x}(V,a) proceeds by induction on the structure of expressions. Barthe et al [3] provide a formal definition of the guard predicate for a simply typed λ-calculus and show that the resulting type system can be embedded in the simply typed fragment of System F that we introduce in the next section.

While syntactic criteria are widely used, they suffer from several weaknesses. A first weakness is that the syntactic criterion must consider all constructs of the language, and can only be applied if the body of the recursive definition is completely known. Thus, the approach is not compatible with separate compilation.

A second weakness of the approach is that the guard predicate is very sensitive to syntax; for example, the function

(letrec always zero = λx: Nat.case x of {o ⇒ o
| s ⇒ λn: Nat.((λf : Nat → Nat.f) always zero) n }
) :  Nat → Nat

is not accepted by the guard predicate of [3], because f is passed as an argument to the identity function. Unfortunately, the phenomenon is not unusual and therefore existing implementations of the guard condition also add a rule of the form

𝒢_{f}^{x}(V,a′) a ↠_{0} a′
𝒢_{f}^{x}(V,a)

where ↠_{0} is a subset of the reduction relation. Thus, checking termination of recursive definitions in large developments may become prohibitive, because of the necessity to reduce the body of recursive definitions for checking the guard condition. Worse, an inappropriate choice of ↠_{0} may lead to allow non-terminating expressions in the type system. For example, allowing ↠_{0} to include reductions of the form (λx: A.a) a′→ a when x does not appear in a leads to non-terminating expressions, because it fails to impose any condition on a′ which may then contain recursive calls that are not wellfounded, e.g. with such a rule the term

(letrec always zero = λx: Nat.case x of {o ⇒ o

| s ⇒ λn: Nat.(λz: Nat.always zero n) (always zero x) }

) :  Nat → Nat

would be typable if the term

(letrec always zero = λx: Nat.case x of {o ⇒ o
| s ⇒ λn: Nat.always zero n
}
) :  Nat → Nat

is, whereas the first term is non-terminating and should be rejected, and the second term should clearly be accepted by the type system. In summary, syntactic guard conditions lead to type systems that are difficult to predict, that are not transparent, and that are not robust to language extensions.

3 The system F of type-based termination

This section presents the system F of type-based termination. This system has been published in [4], and is an extension of the system λ of [3].

3.1 Semantical ideas for a type-based termination criterion

In this section, we present some intuitions underlying type-based termination. To keep things as simple as possible, we focus on weak termination. Recall that an expression e is weakly terminating if and only if it has a normal form.

Consider the definition of a recursive function over natural numbers:

\frac{f : Nat → θ ⊢ e : Nat → θ}{⊢ (letrec f = e) : Nat → θ}

This function will be computed using the evaluation rules:

(letrec f = e) o →_{γ} e[f := (letrec f = e)] o
(letrec f = e) (sn) →_{γ} e[f := (letrec f = e)] (sn)

In order to make sure that the evaluation terminates, we have to ensure that something decreases during the computation. Think of F =_{def} (letrec f = e) as being a function defined using successive approximations F_{0},...,F_{p},.... Now, assume that we want to evaluate F (sn). If there is some p such that the result of that evaluation can be computed using only F_{0},...,F_{p+1} , with

F_{k+1}(sn) →_{γ} e[f := F_{k}] (sn) for all k ≤ p ,

then the evaluation of F (sn) terminates.

To express a notion of function approximation, we rely on a notion of approximation of inductive datatypes. Consider, for instance, the datatype Nat of natural numbers, as defined in system F^{rec} (Sect. 2.2). Its construction can be expressed by the two typing rules:

\overline{⊢ o : Nat}  \frac{⊢ n : Nat}{⊢ sn : Nat}

Hence, roughly speaking, the type Nat of natural numbers can be drawn as

⟦Nat⟧ = {o,so,...,s^{p}o,...}

Let ⟦Nat⟧(0) =_{def} {o} and ⟦Nat⟧(p + 1) =_{def} ⟦Nat⟧(p) ∪ {se | e ∈ ⟦Nat⟧(p)} for all p ∈ ℕ. Now, the set ⟦Nat⟧ is the limit of its approximations

⟦Nat⟧(0) ⊆ ⟦Nat⟧(1) ⊆ ... ⊆ ⟦Nat⟧(p) ⊆ ...

These approximations of the type of natural numbers can be used to define functions as the limit of their approximants. More precisely, a total function F : ⟦Nat⟧ → θ can be seen as the limit of its finite approximants F_{p} : ⟦Nat⟧(p) → θ for p ∈ ℕ. Indeed, if sn is the representation of a natural number p+1, then F (sn) can by computed by evaluating F_{p+1} (sn). Conversely, in order to ensure that F is the limit of its approximants (F_{p})_{p∈ℕ}, we can proceed by induction on p ∈ ℕ, and force F_{p+1} to be defined only in terms of F_{p}, as follows:

\frac{∀p ∈ ℕ  F_{p} : ⟦Nat⟧(p) → θ ⊢ F_{p+1} : ⟦Nat⟧(p + 1) → θ}{⊢ F : ⟦Nat⟧ → θ} if F = ⋃ _{p∈ℕ} F_{p} (2)

The basic idea of type-based termination is to use a type system to convey these notions of approximations. Each ⟦Nat⟧(p) can be represented in the type system by an annotated type Nat^{p}. In such a system, the typing rules of o and s would become

\overline{⊢ o : Nat^{0}}  \frac{⊢ n : Nat^{p}}{⊢ sn : Nat^{p+1}}

Then, ⟦Nat⟧ can be represented by Nat^{∞}, as it is the limit, for p ∈ ℕ, of the sets ⟦Nat⟧(p) represented by Nat^{p}. By the way, the datatype Nat of system F^{rec} corresponds to Nat^{∞}.

Moreover, the inclusions ⟦Nat⟧(p) ⊆ ⟦Nat⟧(p+1) ⊆ ⟦Nat⟧ for p ∈ ℕ can be expressed by the subsumption rules:

\frac{⊢ n : Nat^{p}}{⊢ n : Nat^{p+1}}  \frac{⊢ n : Nat^{p}}{⊢ n : Nat^{∞}}

Now, the requirement expressed by (2) can be represented by the typing rule

\frac{∀p ∈ ℕ  f : Nat^{p} → θ ⊢ e : Nat^{p+1} → θ}{⊢ (letrec f = e) : Nat^{∞} → θ}  (3)

However, the system is unfortunately unsound, both for termination and for coherence. Indeed, Ex. 2.28 can be easily adapted.

Example 3.1. Assume that o : Nat^{0}. Then by subsumption we have o : Nat^{p} for all p ∈ ℕ, and thus, using (3),

∀p ∈ ℕ f : Nat^{p} → ⊥ ⊢ λx: Nat. f o : Nat^{p+1} → ⊥
⊢ (letrec f = λx: Nat. f o) : Nat^{∞} → ⊥

Since ⊢ o : Nat^{∞}, we have a closed term (letrec f = λx: Nat. f o)o of type ⊥, which is moreover non-terminating:

(letrec f = λx: Nat. f o) o → (λx: Nat. (letrec f = λx: Nat. f o) o) o → ...

⊓ ⊔

A solution is to assume that o belongs to all ⟦Nat⟧(p + 1) with p ∈ ℕ, but not to ⟦Nat⟧(0). This leads to the interpretation of inductive datatypes detailed in Sect. 3.4. The typing rules for the constructors of Nat now become:

\overline{⊢ o : Nat^{p+1}}  \frac{⊢ n : Nat^{p}}{⊢ sn : Nat^{p+1}}

Hence, the expression s^{p}o has size p + 1.

3.2 Formal definition

Stages. Generalizing the discussion of the previous section, every datatype d is replaced by a family of approximations indexed over a set of stages, which are used to record a bound on the “depth” of values. Stages expression are build from a set 𝒱_{𝒮} = {ı,ȷ,κ,...} of stage variables. They use the successor operationˆ·and the constant ∞ denoting the greatest stage.

Definition 3.2 (Stages). The set 𝒮 = {s,r,...} of stage expressions is given by the abstract syntax:

𝒮 ::= 𝒱_{𝒮} | ∞ | 𝒮̂

The substitution s[ı:= r] of the stage variable ı for r in s is defined in the obvious way.

The inclusions ⟦Nat⟧(0) ⊆ ... ⊆ ⟦Nat⟧(p) ⊆ Nat(p + 1) ⊆ ... ⊆ ⟦Nat⟧(∞) will hold for each datatype d ∈ 𝒟. This is reflected by a subtyping relation, which is derived from a substage relation s ≤ r.

Definition 3.3 (Substage relation). The substage relation is the smallest reflexive and transitive relation s ≤ r, where s,r ∈ 𝒮, such that s ≤ ŝand s ≤ ∞.

Note that s ≤ ∞ implies ˆ∞ ≤ ∞. Hence, ŝcan be thought of as s + 1 provided ∞ ≰ s.

Types. The approximations (d^{s})_{s∈𝒮} of datatypes are directly represented in the syntax of types. Therefore, the types of F are the types of F^{rec} where datatype identifiers d ∈ 𝒟 are annotated by size expressions s ∈ 𝒮.

Definition 3.4 (Sized types). The set \overline{𝒯} of sized types is given by the following abstract syntax:

\overline{𝒯} ::= 𝒱_{𝒯} | \overline{𝒯} → \overline{𝒯} | Π𝒱_{𝒯} . \overline{𝒯} | 𝒟^{𝒮} \overline{𝒯}

where in the clause for datatypes, it is assumed that the length of the vector \overline{𝒯} is exactly the arity of the datatype.

Sized types are denoted by lower-case over lined Greek letters \overline{τ},\overline{θ},\overline{σ},....

The subtyping relation \overline{τ} ⊑ \overline{σ} is directly inherited from the substage relation. The subtyping rule for datatypes

(data) \frac{s ≤ r \overline{τ}⊑ \overline{σ}}{d^{s}\overline{τ} ⊑ d^{r}\overline{σ}}

expresses two things. First, it specifies that datatypes are covariant w.r.t. their parameters. For instance we have List^{∞} Nat^{s} ⊑ List^{∞} Natŝ. Second, it reflects inclusions of datatypes approximations:

\frac{e: d^{s} \overline{τ} s ≤ r}{e: d^{r} \overline{τ}}

The substage relation imposes that ∞ is the greatest stage of the system. Hence, we have Nat^{s} ⊑ Nat^{∞} for all stage s. This means that the type Nat^{∞} has no information on the size of its inhabitants. Therefore, it corresponds to the type Nat of system F^{rec}.

Notation 3.5. Given a datatype identifier d, we write d \overline{τ}to mean d^{∞} \overline{τ}.

Definition 3.6 (Subtyping). The subtyping relation is the smallest relation \overline{τ}⊑ \overline{σ}, where \overline{τ},\overline{σ} ∈ \overline{𝒯}, such that

(var) \overline{X ⊑ X}  (func) \frac{\overline{τ′}⊑ \overline{τ} \overline{σ} ⊑ \overline{σ′}}{\overline{τ}→ \overline{σ} ⊑ \overline{τ′}→ \overline{σ′}}  (prod) \frac{\overline{τ}⊑ \overline{σ}}{ΠX. \overline{τ}⊑ ΠX. \overline{σ}}  (data) \frac{s ≤ r \overline{τ}⊑ \overline{σ}}{d^{s}\overline{τ} ⊑ d^{r}\overline{σ}}

We denote by |.| : \overline{𝒯} → 𝒯 the erasure function from sized types to types, which forgets the size information represented in a type of F . It is inductively defined as:

|X| = X  |\overline{τ}→ \overline{θ}| = |\overline{τ}| → |\overline{θ}|  |ΠX. \overline{τ}| = ΠX. |\overline{τ}|  |d^{s} \overline{τ}| = d |\overline{τ}|

Sized inductive datatypes. We now turn to datatype definitions. In Def. 2.25, we have defined inductive datatypes definitions for F^{rec} as declarations of the form

Inductive d X⃗ := c_{1} : σ_{1} | ... | c_{n}: σ_{n}

where for all k ∈ {1,...,n}, σ_{k} is of the form θ⃗_{k} → d X⃗ with X⃗ pos θ⃗_{k} and d X⃗ pos θ⃗_{k}.

The inductive datatypes of F are annotated versions of the inductive datatypes of F^{rec}. Each occurrence of d′≠ d in \overline{θ}_{k} is annotated with ∞, and each occurrence of d in θ⃗_{k} is annotated with the stage variable ı. Then, the annotated type of c_{k} is ΠX⃗. \overline{θ}_{k} → dîX⃗. Definitions of sized inductive datatypes are like definitions of inductive datatypes in F^{rec}, excepted that constructors are now given their sized type. For instance, sized natural numbers are declared as follows:

Inductive Nat := o : Natî | s : Nat^{ı}→ Natî

In words, the constructor o always build an expression with at least one constructor, hence of size ˆ0. Since stages record upper-bound on sizes, we have o of stage p̂ for all stage p. On the other hand, s turns an expression of stage p into one of stage p̂.

We now turn to the formal definition.

Definition 3.7 (Sized inductive datatypes).

(i) A sized inductive datatype definition is a declaration

Inductive d X⃗ := c_{1} : \overline{σ}_{1} | ... | c_{n}: \overline{σ}_{n}

such that

– its erased form Inductive d X⃗ := c_{1} : |\overline{σ}_{1}| | ... | c_{n}: |\overline{σ}_{n}| is an inductive datatype definition in F^{rec}, and

– for all k ∈ \{1,...,n\}, the sized type \overline{σ}_{k} is of the form \overline{θ}_{k} → dîX⃗ where each occurrence of d′≠ d in \overline{θ}_{k} is annotated with ∞, and each occurrence of d in θ⃗_{k} is annotated with the stage variable ı. For all k ∈ \{1,...,n\}, we write c_{k}: ΠX⃗. \overline{θ}_{k} → dî X⃗.

(ii) A sized environment is a sequence of sized inductive datatype definitions I_{1} ...I_{n} in which constructors of the sized inductive datatype definition I_{k} only use datatypes introduced by I_{1}...I_{k}.

Note that our definition of inductive datatypes types rules out heterogeneous and mutually inductive datatypes. This is only a matter of simplicity.

Besides, the positivity requirement for d^{ı}X⃗is necessary to guarantee strong normalization. Also, the positivity requirement for X⃗ is added to guarantee the soundness of the subtyping rule (data) for datatypes, and to avoid considering polarity, as in e.g. [13].

Example 3.8 (Sized datatypes definitions).

(i) The sized inductive datatype of polymorphic lists is defined as

Inductive List X := nil : ListîX | cons : X → List^{ı}X→ ListîX

The minimal stage of a list is its length, with the nil list being of stage at least î. For instance, leaving implicit the type argument of constructors, we have cons n nil : ListˆîNat and cons n_{1}(...(cons n_{p} nil)...) : Listî^{p+1} Nat.

(ii) The sized inductive datatype of polymorphic finitely branching trees is

Inductive Tree X := node : X → List (Tree^{ı}X) → TreeîX

The minimal stage of a tree is its depth. The least tree contains just one leave nodennil and is of stage at least î. Consider p trees t_{1},...,t_{p} of respective types Tree^{s_{1}} Nat,...,Tree^{s_{p}} Nat, and let l := cons t_{1}(...(cons t_{p} nil)...). For all stage s greater than each s_{k}, we have l : Listî^{p+1} (Tree^{s}Nat), hence nodenl : TreeŝNat. Therefore, the least stage of nodenl is the strict supremum of the stages of the trees in l. Moreover, the stage of l as a list has been forgotten in the stage of nodenl.

(iii) The sized inductive datatype of Brower’s ordinals is defined as

Inductive Ord := o : Ordî | s : Ord^{ı}→ Ordî | lim : (Nat → Ord^{ı}) → Ordî

As with finitely branching trees, the least stage of limf is the strict supremum of the stages of f n for n ∈ Nat. Moreover, we will see in Ex. 3.15 that if inj : Nat → Ord is the canonical injection of natural numbers into ordinals, then ∞ is the best size approximation that can be given to liminj. ⊓ ⊔

In the remaining of this tutorial, we implicitly assume given a sized environment in which every d ∈ 𝒟 is a sized inductive datatype.

Terms and reductions. The terms of F are those of F^{rec}, defined in Sect. 2.2. The reduction relation of F is the rewrite relation → defined in Def. 2.27.

Remark 3.9 (Stages in terms). Note that the types appearing in terms are those of F^{rec}: they do not carry stage expressions. As shown in [4], subject reduction would have failed if terms conveyed stage expressions. However, it is often useful to write these annotations in examples. For instance, we may write λx : Nat^{ı}. x to denote the term λx: Nat. x.

Typing rules. The typing system is that of [4]. Its rules are given in Fig. 5, page 29.

All rules but (cons), (case), (rec) and (sub) do not mention stages. They are therefore the same as in F^{rec}. The rule (cons) for constructors simply says that a constructor can be given any possible stage instance of its type specified in a datatype definition.

In order to understand the rule (case), we look at it for natural numbers:

\frac{\overline{Γ} ⊢ e : Natŝ  \overline{Γ} ⊢ e_{o} : \overline{σ}  \overline{Γ} ⊢ e_{s} : Nat^{s} → \overline{σ}}{\overline{Γ} ⊢ case_{|\overline{σ}|} e of \{0 ⇒ e_{o} | s ⇒ e_{s}\} : \overline{σ}}

The important point, which makes the difference with the rule of F^{rec}, is that the type of the expression e subject to case analysis must have a stage of the form ŝ. Note that this is always possible thanks to subtyping. Now, assume that e is of the form sn. The rule (case) says that the term e_{s} sees n as an expression of stage s. Indeed, we have

case_{|\overline{σ}|} (sn) of \{0 ⇒ e_{o} | s ⇒ e_{s}\} →_{ι} e_{s} n with \overline{Γ} ⊢ e_{s} : Nat^{s} → \overline{σ}

We now discuss the typing rule (rec) for fixpoints. In the simple case where ı does not occur in \overline{θ}, it can be written as follows:

(rec) \frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}}{\overline{Γ} ⊢ (letrec_{d|\overline{τ}|→|\overline{θ}|} f = e) : d^{s}\overline{τ}→ \overline{θ}} if ı ∉ \overline{Γ},\overline{τ},\overline{θ}

In the case of fixpoints on natural numbers, we get

(rec) \frac{\overline{Γ},f : Nat^{ı}→ \overline{θ} ⊢ e : Natî→ \overline{θ}}{\overline{Γ} ⊢ (letrec_{Nat→|\overline{θ}|} f = e) : Nat^{s} → \overline{θ}} if ı ∉ \overline{Γ},\overline{τ}

As explained in Sect. 3.1, this means that to obtain a fixpoint fix := (letrec_{Nat→|\overline{θ}|} f = e) of type Nat^{∞} → \overline{θ}, we must show that the body e turns an approximation of fix of type Nat^{ı}→ \overline{θ} into its next approximation, which is of type Natî→ \overline{θ}. As discussed in Sect 3.4, such recursive functions are terminating and, despite its simplicity, this mechanism is powerful enough to capture course-of-value recursion.

Notation 3.10. When writing examples of typings of fixpoints, it is convenient to write at the term level the stage annotations corresponding to fixpoint variables. For instance, given a derivation of the form

(rec) \frac{f : Nat^{ı}→ \overline{θ} ⊢ e : Natî→ \overline{θ}}{⊢ (letrec_{Nat→|\overline{θ}|} f = e) : Nat^{s} → \overline{θ}}

where ı ∉ \overline{θ}, it is convenient to write (letrec f : Nat^{ı}→ \overline{θ} = e) : Nat^{s} → \overline{θ} to mean that using f : Nat^{ı}→ \overline{θ}, we must have e: Natî→ \overline{θ}. We use a similar notation when ı ∈ \overline{θ}.

In the general case, where ı may appear in \overline{θ}, we must ensure that all its occurrences in \overline{θ} are positive. This is expressed by a predicate ı pos \overline{σ}, which is defined similarly as the predicate τ pos σ of Sect. 2.3.

Definition 3.11 (Positivity). Given two stage expressions s and r, let s occ r (resp. s nocc r) if and only if s occurs in r (resp. does not occurs in r). Moreover, let s nocc \overline{τ} if the stage expression s does not occur in the sized type \overline{τ}.

The predicate s pos \overline{τ} (resp. s neg \overline{τ}), stating that all occurrences of s in \overline{τ} are positive (resp. negative), is inductively defined in Fig. 4.

The following example, taken from [2], shows that strong normalization may fail if the positivity condition is not met. However, there are finer conditions on the occurrences of ı in \overline{θ} than positivity that nevertheless preserve strong normalization. An interesting proposal is made in [2]. We will not detail it in this tutorial.

Example 3.12 (Counter-example for the positivity condition [2]). Consider the terms

shift := λf : Nat → Natˆî. λx: Nat. case_{Nat} \overbrace{f (sx)}^{Natˆî} of \{ o ⇒ o
| s ⇒ λy: Natî. y }
plus 2 := λx: Nat. s(sx)

of type respectively Nat → Natˆî and Nat → Natî. Note that shiftplus 2 →^{∗} plus 2. Consider now the following fixpoint:

loop := (letrec loop : Nat^{ı}→ (Nat → Natî) → Nat = λx: Natî. λf : Nat → Natˆî.
case_{Nat} (f x) of {o ⇒ o
| s ⇒ λx′: Natî. case x′of {
| o ⇒ o
| s ⇒ λy′: Nat^{ı}. loop y′(shift f)
}
}
) : Nat^{s} → (Nat → Natŝ) → Nat

The stage variable ı occurs negatively in the type (Nat → Natî) → Nat. Therefore, the expression loop would have been typable in F if we had dropped the condition ı pos \overline{θ} in the rule (rec). But then the term loop o plus 2 would have been typable, while we have loop o plus 2 →^{∗} loop o (shift plus 2) →^{∗} loop o plus 2 → .... ⊓ ⊔

\frac{s nocc \overline{τ}}{s pos \overline{τ}}  \frac{s pos \overline{τ}_{i} (1 ≤ i ≤ ar(d))}{s pos d^{r} \overline{τ}}

\frac{s neg \overline{τ}_{2} s pos \overline{τ}_{1}}{s pos \overline{τ}_{2} → \overline{τ}_{1}}

\frac{s pos \overline{τ}}{s pos ΠX. \overline{τ}}

\frac{s pos \overline{τ}_{i} (1 ≤ i ≤ ar(d))}{s pos d^{r} \overline{τ}}

\frac{s nocc \overline{τ}}{s neg \overline{τ}}  \frac{s neg \overline{τ}_{i}  (1 ≤ i ≤ ar(d))}{s neg d^{r} \overline{τ}}

\frac{s pos \overline{τ}_{2} s neg \overline{τ}_{1}}{s neg \overline{τ}_{2} → \overline{τ}_{1}}

\frac{s neg \overline{τ}}{s neg ΠX. \overline{τ}}

\frac{s neg \overline{τ}_{i} (1 ≤ i ≤ ar(d))}{s neg d^{r} \overline{τ}}

Fig. 4. Positivity and negativity of a stage occurrence

Definition 3.13 (Typing). A sized context is a map \overline{Γ} : 𝒱_{ℰ} → \overline{𝒯} of finite domain. The typing relation is the smallest relation \overline{Γ} ⊢ e : \overline{τ} which is closed under the rules of Fig. 5, page 29.

Examples. We now review some examples of functions presented in Sect. 2.2. We begin with the minus and div functions on natural numbers.

Example 3.14 (minus and div). In F^{rec}, minus and div are defined as follows:

minus := (letrec_{Nat→Nat→Nat} ms= λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ x
| s ⇒ λx′: Nat. case y of {o ⇒ x
| s ⇒ λy′: Nat. msx′y′}
}

) : Nat → Nat → Nat

div := (letrec_{Nat→Nat→Nat} div= λx: Nat. λy: Nat.
case_{Nat} x of {o ⇒ o
| s ⇒ λx′: Nat. s (div(minus x′y) y) }

) : Nat → Nat → Nat

For minus, in \overline{Γ′} =_{def} ms: Nat^{ı}→ Nat → Nat^{ı},x: Natî,y: Nat,x′: Nat^{ı}we have

\frac{\overline{Γ′} ⊢ y : Natˆ∞  \overline{Γ′} ⊢ x : Natî  \overline{Γ′} ⊢ λy′: Nat. msx′y′ : Nat^{∞} → Natî}{\overline{Γ′} ⊢ case_{Nat} y of \{o ⇒ x | s ⇒ λy′: Nat. msx′y′\} : Natî}

We deduce that

\frac{\overline{Γ} ⊢ x : Natî  \overline{Γ} ⊢ x : Natî  \overline{Γ} ⊢ λx′: Nat. e_{s} : Natî→ Natî}{\overline{Γ} ⊢ case_{Nat} x of \{o ⇒ x | s ⇒ λx′: Nat. e_{s}\} : Natî}

where e_{s} := case_{Nat} y of \{o ⇒ x | s ⇒ λy′: Nat. msx′y′\} and \overline{Γ} is the typing context ms: Nat^{ı}→ Nat → Nat^{ı},x: Natî,y: Nat. Using (rec), for all stage s we get

\frac{ms: Nat^{ı}→ Nat → Nat^{ı}⊢ λx: Nat. λy: Nat. e_{minus} : Natî→ Nat → Natî}{⊢ (letrec ms= λx: Nat. λy: Nat. e_{minus}) : Nat^{s} → Nat → Nat^{s}}

where e_{minus} := case_{Nat} x of {o ⇒ x | s ⇒ λx′: Nat. e_{s}}. Hence, system F is powerful enough to express that the size of (minus n m) is at most the size of n. This information is essential for the typing of div, which is not defined by structural recursion, in contrast with minus. In the computation of (div(sn)m), the recursive call to div is performed on the argument (minus n m) which is not a subterm of (sn). It can even be syntactically arbitrary bigger! However, with stages we have the information that if (sn), as a natural number, is of size at most p̂, then (minus n m) is of size at most p. The termination argument relies on this decreasing from p̂ to p.

Formally, using (rec), for all stage s we obtain div : Nat^{s} → Nat → Nat^{s} from the judgment

div: Nat^{ı}→ Nat → Nat^{ı}⊢
λx: Nat. λy: Nat. case_{Nat} x of {o ⇒ o
| s ⇒ λx′: Nat. s \underbrace{(div \underbrace{(minus x′y)}_{Nat^{ı}}y)}_{Nat^{ı}}

} : Natî→ Nat → Natî
⊓ ⊔

Example 3.15 (Ordinals). In F^{rec}, the addition on ordinals is defined as

add := (letrec_{Ord→Ord→Ord} add = λx: Ord. λy: Ord.

case_{Ord} x of {o ⇒ y

| s ⇒ λx′: Ord. s (add x′y)
| lim ⇒ λf : Nat → Ord. lim (λz: Nat. add (f z) y)}

) : Ord → Ord → Ord

Therefore, we have add (lim f) e →^{∗} lim (λz: Nat. add (f z) e). The difficulty here is that f z is not a subterm of limf. However, this example is handled by the syntactic termination criterion described in Sect. 2.5. In F , add is typed as follows:

add := (letrec add : Ord^{ı}→ Ord → Ord = λx: Ordî. λy: Ord.
case_{Ord} x of {o ⇒ y
| s ⇒ λx′: Ord^{ı}. s (add x′y)
| lim ⇒ λf : Nat → Ord^{ı}. lim (λz: Nat. add \underbrace{(f z)}_{Ord^{ı}} y)\}
) : Ord^{s} → Ord → Ord

We now come back to the discussion of Ex. 3.8.(iii), about the stage of liminj, where inj : Nat → Ord is the canonical injection of natural numbers into ordinals. In F , it is defined as follows:

inj := (letrec inj : Nat^{ı}→ Ord^{ı}= λx: Natî.
case_{Nat} x of {o ⇒ o
| s ⇒ λx′: Nat^{ı}. s (inj x′)}
) : Nat^{s} → Ord^{s}

Note that this definition uses the same stage variable ı to annotate both Nat and Ord. Moreover, for all p ∈ ℕ we have inj(s^{p}o) →^{∗} (s^{p}o). The only way to apply inj to lim is to instantiate their sized types as Nat^{∞} → Ord^{∞} and (Nat^{∞} → Ord^{∞}) → Ord^{ˆ∞≤∞} respectively. We thus get liminj : Ord^{∞}, and ∞ is the best possible approximation expressible in the system. ⊓ ⊔

Example 3.16 (Concatenations of lists). The function app concatenates two lists. Therefore, if l_{1} and l_{2} are of respective size s_{1} and s_{2}, then app l_{1}l_{2} is of size s_{1} + s_{2}. But system F does not feature stage addition. Hence the precise size of app l_{1}l_{2} is not expressible in the system, and we have app l_{1}l_{2} : List^{∞} X. Since recursion is performed only on the first argument of app, the size of the second one is not relevant, and for all stage s we have app : ΠX. List^{s}X → List X → List X. The function app is defined as follows.

app := ΛX. (letrec app : List^{ı}X → ListX → ListX = λx: ListîX. λy: List X.
case_{ListX} x of {nil ⇒ y
| cons ⇒ λz: X. λx′: List^{ı}X. cons z (app x′y)
}
) : ΠX. List^{s}X→ List X→ List X

The function conc concatenates a list of lists. As for app, we can not express its precise typing in F , and for all stage s we have conc : ΠX. List^{s}(List X) → List X. The function conc is defined as follows, note that it uses the function app:

conc := ΛX. (letrec conc : List^{ı}(ListX) → ListX = λx: Listî(ListX).
case_{List(ListX)}x of {nil ⇒ nil

| cons ⇒ λz: ListX. λx′: List^{ı}(ListX). app z (conc x′)

}
) : ΠX. List^{s}(List X) → List X
⊓ ⊔

Example 3.17 (The map function on a list). The function mapf l applies the function f to each element of the list l and produces the corresponding list. Hence mapf l evaluates to a list of the same size as l. This is expressible in F by map : ΠX. ΠY. (X → Y) → List^{s}X→ List^{s}Y. The function map is defined as follows.

map := ΛX. ΛY. λf : X → Y. (letrec map : List^{ı}X → List^{ı}Y = λx: ListîX.
case_{ListX} x of {nil ⇒ nil

| cons ⇒ λz: X. λx′: List^{ı}X. \underbrace{cons (f z) \underbrace{(map f x′)}_{List^{ı}Y}}_{ListîY}

}

) : ΠX. ΠY. (X → Y) → List^{s}X→ List^{s}Y
⊓ ⊔

Example 3.18 (Flattening of finitely branching trees). As for app and conc, the system F can not express the precise typing of the flattening of finitely branching trees flatten. The function flatten is defined by induction on the depth of its argument. We thus have

flatten := ΛX. (letrec flat: Tree^{ı}X → ListX = λt : TreeîX. case_{Tree X} t of {
node ⇒ λx: X. λxs: List (Tree^{ı}X). cons x (\underbrace{conc (\underbrace{map flat xs}_{List(ListX)})}_{ListX})

}
) : ΠX. Tree^{s}X → List X
⊓ ⊔

3.3 Some important properties

We now state some important properties of system F . They are the properties underlined in Sect. 2.1 for system F, namely subject reduction, strong normalizability of typable terms, and coherence of the type system. Recall that both strong normalization and coherence fail for system F^{rec} (see Sect. 2.2).

(var) \overline{\overline{Γ},x : \overline{σ} ⊢ x : \overline{σ}}  (sub) \frac{\overline{Γ} ⊢ e : \overline{σ}  \overline{σ} ⊑ \overline{τ}}{\overline{Γ} ⊢ e : \overline{τ}}

(abs) \frac{\overline{Γ},x : \overline{τ}⊢ e : \overline{σ}}{\overline{Γ} ⊢ λx: |\overline{τ}|. e : \overline{τ}→ \overline{σ}}  (app) \frac{\overline{Γ} ⊢ e : \overline{τ}→ \overline{σ}  \overline{Γ} ⊢ e′ : \overline{τ}}{\overline{Γ} ⊢ e e′ : \overline{σ}}

(T-abs) \frac{\overline{Γ} ⊢ e : \overline{σ}}{\overline{Γ} ⊢ ΛX. e : ΠX. \overline{σ}} if X ∉ \overline{Γ}  (T-app) \frac{\overline{Γ} ⊢ e : ΠX. \overline{σ}}{\overline{Γ} ⊢ e |\overline{τ}| : \overline{σ}[X := \overline{τ}]}

(cons) \overline{\overline{Γ} ⊢ c_{k} : ΠX⃗. \overline{θ}_{k} → dîX⃗} if c_{k} ∈ 𝒞(d) for some d

(case) \frac{\begin{aligned}& c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗ \\ \overline{Γ} ⊢ e : dŝ \overline{τ} & \overline{Γ} ⊢ e_{k} : \overline{θ}_{k}[X⃗:= \overline{τ},ı:= s] → \overline{σ} & (1 ≤ k ≤ n) \end{aligned}}{\overline{Γ} ⊢ case_{|\overline{σ}|} e of \{c_{1} ⇒ e_{1} | ···| c_{n} ⇒ e_{n}\} : \overline{σ}} if 𝒞(d) = \{c_{1},...,c_{n}\}

(rec) \frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}[ı:= î] ı pos \overline{θ}}{\overline{Γ} ⊢ (letrec_{d|\overline{τ}|→|\overline{θ}|} f = e) : d^{s}\overline{τ}→ \overline{θ}[ı:= s]} if ı ∉ \overline{Γ},\overline{τ}

Fig. 5. Typing rules for F

Subject reduction. The proof of this property is easily adapted from the proof for λ presented in [3].

Theorem 3.19 (Subject reduction). If \overline{Γ} ⊢ e : \overline{τ}and e → e′, then \overline{Γ} ⊢ e′ : \overline{τ}.

With respect to stage annotations, subject reduction says that the size approximations represented by stages are preserved by reduction, and moreover that they can be retrieved by the type system after a reduction step.

Strong normalization and coherence. System F enjoys the two crucial properties that failed with F^{rec}, namely strong normalizability of typable terms and coherence. Proofs are sketched in the next section, respectively in Cor. 3.31 and in Cor. 3.32. They both rely on a reducibility interpretation of F by saturated sets [7,14]. Let SN be the set of strongly normalizing terms. Hence SN is the least set of terms such that

∀e. (∀e′. e →_{βιγ}e′ ⟹ e′∈ SN) ⟹ e ∈ SN

Theorem 3.20 (Strong normalization). If \overline{Γ} ⊢ e : \overline{τ}then e ∈ SN.

Theorem 3.21 (Coherence). In F , there is no term e such that ⊢ e : ⊥.

3.4 A reducibility interpretation

In this section, we sketch the correctness proof of a reducibility semantics for F . Our semantics is based on a variant of reducibility [8] called Tait’s saturated sets [14], and will be used to prove both the strong normalization of typable terms and the coherence of the type system. We begin by the interpretation of stages, and turn to the model construction. We then state its correctness, from which we deduce strong normalization and coherence.

In the whole section, if f is a map from A to B, a ∈ A and b ∈ B, then f(a:= b) : A → B maps a to b and is equal to f everywhere else.

The stage model. Stages are interpreted by the ordinals used to build the interpretation of inductive types. While first-order inductive types can be interpreted by induction on ℕ, higher-order inductive types may require an induction on countable ordinals.

Definition 3.22 (Countable ordinals). We denote by (Ω,≤_{Ω}) the well-ordered set of countable ordinals and by +_{Ω} the usual ordinal addition on Ω.

Definition 3.23 (Stage model). Let Ω̂ =_{def} Ω ∪ {Ω}. For all α ∈ Ω and all β ∈ Ω̂, let α < β iff (β = Ω or α <_{Ω} β).

Definition 3.24 (Interpretation of stages). A stage valuation is a map π from 𝒱_{𝒮} to Ω̂, and is extended to a stage interpretation ⦇.⦈_{π} : 𝒮 → Ω̂ as follows:

⦇ι⦈_{π} = π(ι)  ⦇0⦈_{π} = 0  ⦇∞⦈_{π} = Ω  ⦇ŝ⦈_{π} = \{ \begin{matrix}⦇s⦈_{π} + 1 & if⦇s⦈_{π} < Ω \\ Ω & if⦇s⦈_{π} = Ω \end{matrix}

Type interpretation. In this section, we define the type interpretation and prove its correctness. Our proof follows the pattern of [1]. We interpret types by saturated sets. It is convenient to define them by means of elimination contexts:

E[ ] ::= [ ] | E[ ] e | E[ ] |τ|| case_{|τ|} E[ ] of {c⃗ ⇒ e⃗}

Note that the hole [ ] of E[ ] never occurs under a binder. Thus E[ ] can be seen as a term with one occurrence of a special variable [ ]. Therefore, we can define E[e] as E[ ][[ ] := e]. The relation of weak head βιγ-reduction is defined as E[e] →_{wh} E[e′] if and only if e ≻_{βιγ}e′.

Definition 3.25 (Saturated sets). A set S ⊆ SN is saturated (S ∈ SAT) if

(SAT1) E[x] ∈ S for all E[ ] ∈ SN and all x ∈ 𝒱_{ℰ}, (SAT2) if e ∈ SN and e →_{wh} e′for some e′∈ S then e ∈ S.

One can easily show that SN ∈ SAT and that ⋂ 𝒴,⋃ 𝒴 ∈ SAT for all non-empty 𝒴 ⊆ SAT. Hence, for each X ⊆ SN there is a smallest saturated set containing X, written \overline{X}. It follows that the smallest element of SAT is ⊥ =_{def} \overline{∅}. The following properties precisely characterizes the membership of an expression to a saturated set.

Lemma 3.26.

(i) ⊥ = {e ∈ SN | ∃E[ ],x. e →_{wh}^{∗} E[x]}. (ii) If X ⊆ SN then \overline{X} = ⊥ ∪ \{e ∈ SN | e →_{wh}^{∗} X\}.

As usual, the function space on SAT is

X → Y =_{def} {e | ∀e′. e′∈ X ⟹ ee′∈ Y } for all X,Y ⊆ SAT .

The interpretation of types is defined in two steps. We first define the interpretation scheme of types, given an interpretation of datatypes. We then define the interpretation of datatypes.

Definition 3.27. An interpretation of datatypes is a family of functions (I_{d})_{d∈𝒟} where I_{d}: SAT^{ar(d)}×Ω̂ → SAT for each d ∈ 𝒟. Given an interpretation of datatypes I, a stage valuation π and a type valuation ξ: 𝒱_{𝒯} → SAT, the type interpretation ⟦.⟧_{π,ξ}^{I} : \underline{𝒯} → SAT is defined by induction on types as follows

⟦X⟧_{π,ξ}^{I} = ξ(X)
⟦τ → σ ⟧_{π,ξ}^{I} = ⟦τ⟧_{π,ξ}^{I} → ⟦σ⟧_{π,ξ}^{I}
⟦ΠX. τ⟧_{π,ξ}^{I} = {e | ∀|σ| ∈ |𝒯|, ∀S ∈ SAT, e |σ| ∈ ⟦τ⟧_{π,ξ(X:=S)}^{I}}
⟦d^{s}τ⃗⟧_{π,ξ}^{I} = I_{d}(⟦τ⃗⟧_{π,ξ}^{I},⦇s⦈_{π})

We now define the interpretation of inductive datatypes. Recall that they are defined in an ordered list I_{1},...,I_{n} of declarations (see Def. 2.25). Let us say that k is the rank of d if d is defined in I_{k}. The interpretation (I_{d})_{d∈𝒟} is defined by induction on the rank, and for each d ∈ 𝒟, the map I_{d} : SAT^{ar(d)}× Ω̂ → SAT is defined by induction on Ω̂.

Definition 3.28. For all d ∈ 𝒟, all S⃗∈ SAT^{ar(d)} and all α ∈ Ω̂, we define I_{d}(S⃗,α), by induction (k,α), where k is the rank of d, ordered by (<,<)_{lex}, as follows:

I_{d}(S⃗,0) = ⊥
I_{d}(S⃗,α + 1) = ⋃ \{c⟦\overline{θ}⟧_{ι:=α,X⃗:=S⃗}^{I} | c ∈ 𝒞(d) ∧ Type(c) = ΠX⃗. \overline{θ} → dι̂X⃗\}
I_{d}(S⃗,λ) = ⋃ {I_{d}(S⃗,α) | α < λ}  if λ is a limit ordinal

where cS⃗ =_{def} \overline{\{c|τ⃗|a⃗ | a⃗ ∈ S⃗ ∧ |τ⃗| ∈ |𝒯|\}} for all S⃗∈ SAT.

Note that I_{d}(S⃗,α+1) only uses c⟦\overline{θ}⟧_{ι:=α,X⃗:=S⃗}^{I} with c ∈ 𝒞(d), which in turn only uses

I_{d}(U⃗,β) with (p,β)(<,<)_{lex}(k,α + 1), where k (resp. p) is the rank of d (resp. d′).

Now that we have an interpretation of inductive datatypes (I_{d})_{d∈𝒟} , we can interpret types as in Def. 3.27 using this interpretation of datatypes. It is convenient to denote ⟦.⟧_{π,ξ}^{I} by ⟦.⟧_{π,ξ}.

We gather in Fig. 6 some properties of ⦇.⦈_{π} and ⟦.⟧_{π,ξ}. The following Proposition states that each inductive datatype can be interpreted by a countable ordinal. This is crucial in order to deal with the rule (cons) in the proof of Thm. 3.30. The key-point is that for every countable S ⊆ Ω, there is β ∈ Ω such that α < β for all α ∈ S [6].

Substitution  ⦇p[ι:= s]⦈_{π} = ⦇p⦈_{π(ι:=⦇s⦈_{π})}
⟦\overline{τ}[ι:= s]⟧_{π,ξ} = ⟦\overline{τ}⟧_{π(ι:=⦇s⦈_{π}),ξ}
⟦\overline{τ}[X := \overline{σ}]⟧_{π,ξ} = ⟦\overline{τ}⟧_{π,ξ(X:=⟦\overline{σ}⟧_{π,ξ})}
Stage monotony  α ≤ β ⇒ I_{d}(S⃗,α) ⊆ I_{d}(S⃗,β)
α ≤ β ∧ ι pos θ ⇒ ⟦θ⟧_{π(ι:=α),ξ} ⊆ ⟦θ⟧_{π(ι:=β),ξ}
α ≤ β ∧ ι neg θ ⇒ ⟦θ⟧_{π(ι:=β),ξ} ⊆ ⟦θ⟧_{π(ι:=α),ξ}
Substage soundness  s ≤ p ⇒ ⦇s⦈_{π} ≤ ⦇p⦈_{π}
Subtyping soundness  \overline{τ}⊑ \overline{σ} ⇒ ⟦\overline{τ}⟧_{π,ξ} ⊆ ⟦\overline{σ}⟧_{π,ξ}

Fig. 6. Properties of the type interpretation

Proposition 3.29. For all d ∈ 𝒟 and all S⃗∈ SAT^{ar(d)}, there is an ordinal α < Ω such that I_{d}(S⃗,α) = I_{d}(S⃗,β) for all β such that α ≤ β ≤ Ω.

Correctness of the interpretation. As usual, soundness is shown by induction on typing derivations. Given π: 𝒱_{𝒮} → Ω̂, ξ: 𝒱_{𝒯} → SAT and ρ: (𝒱_{ℰ} → ℰ) ⊎ (𝒱_{𝒯} → |𝒯|), we let (π,ξ,ρ) ⊧ \overline{Γ} if and only if ρ(x) ∈ ⟦\overline{Γ}(x)⟧_{π,ξ} for all x ∈ dom(\overline{Γ}).

Theorem 3.30 (Typing soundness). If \overline{Γ} ⊢ e : \overline{τ}, then eρ ∈ ⟦\overline{τ}⟧_{π,ξ} for all π,ξ,ρ such that (π,ξ,ρ) ⊧ \overline{Γ}.

We deduce the strong normalization of typable terms and the coherence of the system.

Corollary 3.31 (Strong normalization). If \overline{Γ} ⊢ e : \overline{τ}then e ∈ SN.

Proof. Apply Thm. 3.30 with any π and ξ, and with the identity substitution for ρ. We thus have (π,ξ,ρ) ⊧ \overline{Γ}, hence e = eρ ∈ ⟦\overline{τ}⟧_{π,ξ} ⊆ SN. ⊓ ⊔

Corollary 3.32 (Coherence). There is no term e such that ⊢ e : ΠX. X.

Proof. Assume that ⊢ e : ΠX. X. Note that e must be a closed term, i.e. FV_{ℰ} (e) = ∅. By Thm. 3.30, we have e ∈ ⟦ΠX. X⟧. Therefore, for all τ ∈ 𝒯, we have eτ ∈ ⊥. By Lem. 3.26.(i), eτ reduces to a term of the form E[x] for some x ∈ 𝒱_{ℰ}. But E[x] is an open term, which contradicts the fact that eτ is closed. ⊓ ⊔

4 Type inference

The purpose of this section is to present a sound and complete algorithm that infers size annotations for F . One particularity of our algorithm is to return concise results, in the form of constrained types (C,τ) where τ is a sized type and C is a set of stage inequalities. Restricting such constrained types is beneficial for two reasons: first of all, sets of stage inequalities are always satisfiable (by mapping all stage variables to ∞), hence a term e is typable whenever the inference algorithm does not return an error. Second of all, the algorithm avoids the use of disjunction, which makes satisfiability of constraints complex. Disjunctive typings are avoided by requiring recursive definitions to carry tags that identify which positions are meant to carry a size annotation related to the size of the recursive argument. Consider the following expression:

(letrec_{Nat→Nat} f = λx: Nat. o)

It may be given the types Nat^{ı}→ Nat^{ı}and Nat^{ı}→ Natĵ. If we restrict to conjunctive constrained types discussed above, it is impossible to obtain a more general type that subsumes both types. In order to achieve more general types without using disjunctive constrained types, we tag positions whose size must use the same base size variable as the recursive argument with a special symbol ⋆. These tags will be used by the inference algorithm to separate between stage variables that must pertain to the same hierarchy as the stage variable of the recursive arguments, and those that must not. In effect, the inference algorithm will produce the following results:

(letrec_{Nat^{⋆}→Nat^{⋆}} f = λx: Nat. o) : Nat^{ı}→ Nat^{ı}
(letrec_{Nat^{⋆}→Nat} f = λx: Nat. o) : Nat^{ı}→ Natĵ

For clarity, the inference algorithm is defined together with a checking algorithm, that takes as additional argument a candidate type and verifies that it is a correct instance of the computed type. Since we start from terms that do not carry size annotations, both algorithms must generate size variables that are used to build the size annotations that decorate the inferred or checked types. In order to guarantee that they only introduce fresh size variables, the algorithms take an auxiliary parameter V, that represents the set of size variables that have been used elsewhere, and return an extended set V′that includes V and the new stage variables that were used for the expression under evaluation. Therefore,

– the type inference algorithm Infer(V,\overline{Γ},e) takes as input a context \overline{Γ}, an expression e and a set of size variables V s.t. FV(\overline{Γ}) ⊆ V, and returns a tuple (V′,C,\overline{τ}) where \overline{τ} is an annotated type, C is a constraint, and V′is a set of size variables s.t. FV(C,\overline{τ})∪ V ⊆ V′;

– the type checking algorithm takes as additional input a candidate type \overline{τ}; then Check(V,\overline{Γ},e,\overline{τ}) returns a pair (V′,C) s.t. FV(C,\overline{τ}) ∪ V ⊆ V′ and ensuring that e has type ρ\overline{τ}in environment \overline{Γ} provided that ρ is a solution for C.

The algorithm is sound and complete.

Proposition 4.1 (Soundness and completeness of Check and Infer).

– Soundness:

(i) If Check(V,\overline{Γ},e,\overline{τ}) = (V′,C) then for all ρ s.t. ρ ⊧ C, we have ρ(\overline{Γ}) ⊢ e : ρ(\overline{τ}). (ii) If Infer(V,\overline{Γ},e) = (V′,C,\overline{τ}) then for all ρ s.t. ρ ⊧ C, we have ρ(\overline{Γ}) ⊢ e : ρ(\overline{τ}).

– Completeness:

(i) If ρ(\overline{Γ}) ⊢ e : ρ\overline{τ}and FV_{ℐ}(\overline{Γ},\overline{τ}) ⊆ V then there exist V′,C,ρ′such that Check(V,\overline{Γ},e,\overline{τ}) = (V′,C) and ρ′⊧ C ∧ ρ =_{V} ρ′.

(ii) If ρ(\overline{Γ}) ⊢ e : \overline{θ} and FV_{ℐ}(\overline{Γ}) ⊆ V there exist V′,C,\overline{τ},ρ′such that Infer(V,\overline{Γ},e) =

(V′,C,\overline{τ}) and ρ′⊧ C and ρ′(\overline{τ}) ⊑ \overline{θ} and ρ′=_{V} ρ where ρ =_{V} ρ′means that ρ(α) = ρ′(α) for all α ∈ V.

Since every constraint has a solution, it is always possible to find ρ such that ρ ⊧ C whenever the inference algorithm is successful on input (\overline{Γ},e), i.e. Infer(\overline{Γ},e) = (C,τ), and by soundness ρ\overline{Γ} ⊢ e : ρτ.

The crux of the algorithm is the rule for recursive definitions, which must check the existence of solutions for more elaborate constraint, in which one can also declare that a stage variable ı can only be interpreted as itself (in effect it amounts to restrict ourselves to substitutions ρ such that ρ(ı) = ı), and that a stage s cannot be in the same hierarchy as a fixed stage variable ı. For such systems, the existence of a solution is not always guaranteed, and we shall therefore device a dedicated algorithm to verify whether a solution exists.

Outline. Type inference is presented step by step. We begin by recalling the straightforward type inference algorithm of system F in Sect. 4.1. Then, in Sect. 4.2, we discuss the effect of adding sized inductive datatypes, with subtyping and case analysis but without recursion. We concentrate on the subtyping relation and the necessity to infer stage annotations for λ-abstractions, type applications and case analysis. At this level, we do not need to be precise about freshness conditions. Its is sufficient to work with

– the judgment C ; \overline{Γ} ⊢ e ↑ \overline{τ}, which stands for Infer(\overline{Γ},e) = (C,\overline{τ}), and

– the judgment C ; \overline{Γ} ⊢ e ↓ \overline{τ}, which stands for Check(\overline{Γ},e,\overline{τ}) = C.

In Sect. 4.3, we informally discuss the way we handle recursive definitions. The main point is an auxiliary algorithm called RecCheck, which is informally presented and justified. Finally, in Sect. 4.4 we discuss the full type inference algorithm of F , as presented in [4] and using the functions Infer(V,\overline{Γ},e) and Check(V,\overline{Γ},e,\overline{τ}).

4.1 Preliminaries: Type inference in system F

In the Church style system F, as presented in Sect. 2.1, type inference is trivial, because the typing derivation of a term is uniquely determined by the shape of a term. Hence, the type inference algorithm is directly given by the typing rules read bottom-up:

– The type of x in the context Γ is Γ(x) if and only if x ∈ dom(Γ).

– The type of λx: τ. e in Γ if and only if τ → σ is the type of e in Γ,x : τ is σ;

– The type of ee′in Γ is σ if and only if there is a (necessarily unique) type τ such that the type of e (resp. e′) in Γ is τ → σ (resp. τ).

– The type of Λx. e in Γ is ΠX. τ if and only if the type of e in Γ is τ and X ∉ Γ.

– The type of eτ in Γ is σ[X := τ] if and only if the type of e in Γ is ΠX. σ.

4.2 Adding sized inductive datatypes

In this section, we present type inference in system F enriched with the sized typing rules for constructors, case analysis, and subtyping. Recall that sized types, defined in Def. 3.4, are given by the abstract syntax:

\overline{𝒯} ::= 𝒱_{𝒯} | \overline{𝒯} → \overline{𝒯} | Π𝒱_{𝒯} . \overline{𝒯} | 𝒟^{𝒮} \overline{𝒯}

and that the typing rule (cons), (case) and (sub) are the following:

(cons) \overline{\overline{Γ} ⊢ c_{k} : ΠX⃗. \overline{θ}_{k} → dîX⃗} if c_{k} ∈ 𝒞(d) for some d  (sub) \frac{\overline{Γ} ⊢ e : \overline{σ}  \overline{σ} ⊑ \overline{τ}}{\overline{Γ} ⊢ e : \overline{τ}}

(case) \frac{\begin{aligned}& c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗ \\ \overline{Γ} ⊢ e : dŝ \overline{τ} & \overline{Γ} ⊢ e_{k} : \overline{θ}_{k}[X⃗:= \overline{τ},ı:= s] → \overline{σ} & (1 ≤ k ≤ n) \end{aligned}}{\overline{Γ} ⊢ case_{|\overline{σ}|} e of \{c_{1} ⇒ e_{1} | ···| c_{n} ⇒ e_{n}\} : \overline{σ}} if 𝒞(d) = \{c_{1},...,c_{n}\}

In this section, it is not mandatory for the informal discussion to be very precise on freshness conditions. Moreover, we work step by step, and progressively introduce the features of the type inference algorithm. Therefore, instead of using Infer(\overline{Γ},e) and Check(\overline{Γ},e,\overline{τ}), we start with two simple unconstrained judgments \overline{Γ} ⊢ e ↑ \overline{τ}for type inference and \overline{Γ} ⊢ e ↓ \overline{τ} for type-checking. we will then introduce constraints, which lead us to

– the judgment C ; \overline{Γ} ⊢ e ↑ \overline{τ}, which stands for Infer(\overline{Γ},e) = (C,\overline{τ}), and

– the judgment C ; \overline{Γ} ⊢ e ↓ \overline{τ}, which stands for Check(\overline{Γ},e,\overline{τ}) = C.

Inference of size annotations. We now discuss the case of λ-abstractions. The natural inference rule would be

\frac{\overline{Γ},x : \overline{τ}⊢ e ↑ \overline{σ}}{\overline{Γ} ⊢ λx: |\overline{τ}|. e ↑ \overline{τ}→ \overline{σ}}  (4)

That is, we infer the type \overline{τ}→ \overline{σ} for λx: |\overline{τ}|. e if we can infer the type \overline{σ} for e in a context where the variable x is given the type \overline{τ}. In other words, we have to infer the type \overline{τ}from its erasure |\overline{τ}|. The difficulty is that the type \overline{τ}may depend on e. For instance, with

\overline{Γ} =_{def} f : Nat^{ı}→ Nat^{ı},g: Nat^{ȷ}→ Nat^{ȷ}

we have

\frac{\overline{Γ},x : Nat^{ı}⊢ f x : Nat^{ı}}{\overline{Γ} ⊢ λx: Nat. f x : Nat^{ı}→ Nat^{ı}}  and  \frac{\overline{Γ},x : Nat^{ȷ}⊢ gx : Nat^{ı}}{\overline{Γ} ⊢ λx: Nat. gx : Nat^{ȷ}→ Nat^{ı}}

where the typing of λx: Nat. f x and λx: Nat. gx require two different annotations of Nat. A solution is to proceed similarly as in Hindley-Milner type inference for MLlike languages. We perform type inference in a system whose stage expressions feature inference stage variables 𝒱_{ℐ} = {α,β,...}.

Definition 4.2 (Inference stages). The set 𝒮_{ℐ} = {s,r,...} of inference stage expressions is given by the abstract syntax:

𝒮_{ℐ} ::= 𝒱_{𝒮} | 𝒱_{ℐ} | 𝒮̂_{ℐ} | ∞

The substitution s[α := r] of the inference stage variable α for r in s is defined in the obvious way.

Then, each type σ ∈ 𝒯 can be systematically annotated with inference variables. This is performed by a function Annot satisfying the following specification. If V is a set of inference stage variables and σ ∈ 𝒯 is a type, then Annot(σ,V) returns a pair (\overline{σ},V′) such that

– |\overline{σ}| = σ,

– each occurrence of an inductive datatype in \overline{σ} is annotated with a distinct inference stage variable α ∉ V (so that α occurs at most once in \overline{σ}),

– V′= V ∪ FV_{ℐ}(\overline{σ}).

For instance, Annot(Nat → Nat,{α_{1},α_{2}}) = (Nat^{α_{3}} → Nat^{α_{4}},{α_{1},α_{2},α_{3},α_{4}}). For the moment, we do not use the set of variables V′produced by Annot. If we add these systematic annotations to the rule (4), we obtain

(abs) \frac{\overline{Γ},x : \overline{τ}⊢ e ↑ \overline{σ}  (\overline{τ},V) = Annot(τ,FV_{ℐ}(\overline{Γ}))}{\overline{Γ} ⊢ λx: τ. e ↑ \overline{τ}→ \overline{σ}}

In such system, the intended semantics of type inference and type checking can be phrased by the property that for all substitution ρ: 𝒱_{ℐ} → 𝒮_{ℐ} we have

Γ ⊢ e ↑ \overline{τ} ⟹ Γρ ⊢ e : \overline{τ}ρ
Γ ⊢ e ↓ \overline{τ} ⟹ Γρ ⊢ e : \overline{τ}ρ

Checking subtyping derivations. Type inference with a rule like the above does not work directly: we have to take subtyping into account more seriously. Let us look at the type inference derivation of λx: Nat. f x in the context f : Nat^{ı}→ Nat^{∞}. We would have a derivation of the form

\frac{f : Nat^{ı}→ Nat^{∞} ,x: Nat^{α} ⊢ f x ↑?  (Nat^{α},V) = Annot(Nat,∅)}{f : Nat^{ı}→ Nat^{∞} ⊢ λx: Nat. f x ↑?}  (5)

but we get stuck because this would require Nat^{α} ⊑ Nat^{ı}, which does not hold.

In other words, once we generate sized types featuring stage inference variables, we have to adapt our way of handling subtyping. In Sect. 3.2, we have seen that the substage relation s ≤ r (defined in Def. 3.3) leads to the subtyping relation \overline{τ} ⊑ \overline{σ} (defined in Def. 3.6). For type checking, we go the other way: starting from a subtyping assertion \overline{τ}⊑ \overline{σ}, we generate a conjunction of substage assertions s_{1} ≤ r_{1},...,s_{n}≤ r_{n}, which holds if and only if \overline{τ}⊑ \overline{σ} is derivable.

Definition 4.3 (Constraints).

(i) A constraint is either the false constraint ⊥ or a set of inference stage expressions inequalities {s_{1} ≤ r_{1},...,s_{n} ≤ r_{n}}.

(ii) A substitution ρ : 𝒱_{ℐ} → 𝒮_{ℐ} satisfies a constraint C, notation ρ ⊧ C, if and only if C ≠ ⊥ and sρ ≤ rρ is derivable using the rules of Def. 3.3 for all s ≤ r ∈ C.

(iii) A subtyping assertion \overline{τ}⊑ \overline{σ} generates a constraint ⦇\overline{τ}⊑ \overline{σ}⦈ defined as follows

⦇X ⊑ X⦈ =_{def} ∅
⦇\overline{τ}_{2} → \overline{τ}_{1} ⊑ \overline{σ}_{2} → \overline{σ}_{1} ⦈ =_{def} ⦇\overline{σ}_{2} ⊑ \overline{τ}_{2}⦈ ∪_{⊥} ⦇\overline{τ}_{1} ⊑ \overline{σ}_{1}⦈
⦇ΠX. \overline{τ} ⊑ ΠX. \overline{σ} ⦈ =_{def} ⦇\overline{τ}⊑ \overline{σ}⦈
⦇d^{s} \overline{τ}⊑ d^{r} \overline{σ}⦈ =_{def} \{s ≤ r\} ∪_{⊥} ⦇\overline{τ}⊑ \overline{σ}⦈
⦇\overline{τ}⊑ \overline{σ}⦈ =_{def} ⊥  in all other cases

where

C_{1}∪_{⊥} C_{2} =_{def} \{ \begin{matrix}⊥ & if C_{1} = ⊥ or C_{2} = ⊥ \\ C_{1}∪ C_{2} & otherwise \end{matrix}

We write s_{1} ≤ r_{1},...,s_{n} ≤ r_{n} instead of {s_{1} ≤ r_{1},...,s_{n} ≤ r_{n}}. Note that we have ρ ⊧ ∅ for all ρ: 𝒱_{ℐ} → 𝒮_{ℐ}, and that the empty substitution does not satisfies the false constraint ⊥. The satisfaction of constraints generated by subtyping assertions corresponds exactly to the derivability of subtyping judgments.

Proposition 4.4. ρ ⊧ ⦇\overline{τ}⊑ \overline{σ}⦈ if and only if \overline{τ}ρ ⊑ \overline{σ}ρ.

Example 4.5.

(i) The assertion Nat^{∞} ⊑ Bool^{∞} generates the constraint ⊥. It follows that Nat^{∞} ⊑ Bool^{∞} is not derivable.

(ii) The assertion Nat^{ı}⊑ Nat^{∞} generates the constraint {ı ≤ ∞}. The inequality ı ≤ ∞

is derivable, hence Nat^{ı}⊑ Nat^{∞} is also derivable. (iii) The assertion Nat^{ı}⊑ Nat^{ȷ}generates the constraint {ı ≤ ȷ}. The inequality ı ≤ ȷ is

not derivable, hence Nat^{ı}⊑ Nat^{ȷ}is not derivable. ⊓ ⊔

Inference rules. We have to adapt type inference to take into account the constraints generated by subtyping. We now consider judgments of the form

C ; \overline{Γ} ⊢ e ↑ \overline{τ} and C ; \overline{Γ} ⊢ e ↓ \overline{τ}

where C is a constraint. The constraints are generated by subtyping

(sub) \frac{C ; \overline{Γ} ⊢ e ↑ \overline{τ}}{C ∪_{⊥} ⦇\overline{τ}⊑ \overline{σ}⦈ ; \overline{Γ} ⊢ e ↓ \overline{σ}}

and transmitted by the other rules. In all rules, constraints have to be read top-bottom. The system is presented in Fig. 7, and its correctness is stated the following Proposition. The rule (cons) and (case) are commented in the next paragraph.

Proposition 4.6 (Correctness).

(i) If C ; \overline{Γ} ⊢ e ↑ \overline{τ}and ρ ⊧ C then \overline{Γ}ρ ⊢ e : \overline{τ}ρ (ii) If C ; \overline{Γ} ⊢ e ↓ \overline{τ}and ρ ⊧ C then \overline{Γ}ρ ⊢ e : \overline{τ}ρ Let us now look at the derivation (5). We have

\frac{∅ ; f : Nat^{ı}→ Nat^{∞} ,x: Nat^{α} ⊢ x ↑ Nat^{α}}{α ≤ ı ; f : Nat^{ı}→ Nat^{∞} ,x: Nat^{α} ⊢ x ↓ Nat^{ı}}

and it follows that

\frac{α ≤ ı ; f : Nat^{ı}→ Nat^{∞} ,x: Nat^{α} ⊢ f x ↑ Nat^{∞} (Nat^{α},V) = Annot(Nat,∅)}{α ≤ ı ; f : Nat^{ı}→ Nat^{∞} ⊢ λx: Nat. f x ↑ Nat^{α} → Nat^{∞}}

By Prop. 4.6.(i), since ı ≤ ı we get f : Nat^{ı}→ Nat^{∞} ⊢ λx: Nat. f x : Nat^{ı}→ Nat^{∞}.

Inductive datatypes. We have not yet discussed the type inference rules (cons) and (case), that correspond respectively to the introduction and to the elimination of inductive datatypes. The only particular feature of the type inference rule for constructors is that it introduces a fresh inference stage variable:

(cons) \frac{c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗}{∅ ; \overline{Γ} ⊢ c_{k} ↑ ΠX⃗. \overline{θ}_{k}[ı:= α] → dα̂ X⃗} if α ∉ 𝒱_{ℐ}(\overline{Γ}) and c_{k} ∈ 𝒞(d) for some d

Consider now the type inference rule (case) for case-analysis:

\frac{\begin{matrix}C ; \overline{Γ} ⊢ e ↑ d^{s} \overline{τ}  α ∉ 𝒱_{ℐ}(\overline{Γ})  (\overline{σ},V) = Annot(σ,𝒱_{ℐ}(\overline{Γ}) ∪ \{α\}) \\ c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗ C_{k} ; \overline{Γ} ⊢ e_{k} ↓ \overline{θ}_{k}[X⃗:= \overline{τ},ı:= α] → \overline{σ} (1 ≤ k ≤ n) \end{matrix}}{\{s ≤ α̂\} ∪_{⊥} C ∪_{⊥} (⋃ _{⊥} C_{k}) ; \overline{Γ} ⊢ case_{σ} e of \{c_{1} ⇒ e_{1} | ···| c_{n} ⇒ e_{n}\} ↑ \overline{σ}}
where 𝒞(d) = {c_{1},...,c_{n}}

In order to explain it, we consider a simple case where the output type σ does not contain any datatype (hence \overline{σ} = σ) and where the datatype d subject of the case-analysis is the type of natural numbers. Assume that we want to infer the type of case_{σ} e of {0 ⇒ e_{o} | s ⇒ e_{s}\} in the context \overline{Γ}. First, we infer the type of the subject e of the case-analysis, and we get a constraint C such that C ; \overline{Γ} ⊢ e ↑ Nat^{s}. Now, recall the typing rule case imposes that the subject can be typed with a stage of the form r̂, and that in our case, the branch e_{s} corresponding to the constructor s has type Nat^{r} → σ:

\frac{\overline{Γ} ⊢ e : Natr̂  \overline{Γ} ⊢ e_{o} : σ  \overline{Γ} ⊢ e_{s} : Nat^{r} → σ}{\overline{Γ} ⊢ case_{σ} e of \{0 ⇒ e_{o} | s ⇒ e_{s}\} : σ}

We express this by using a fresh stage variable α together with a constraint s ≤ α̂, and we typecheck the branch e_{s} against the type Nat^{α} → σ. This gives:

\frac{C ; \overline{Γ} ⊢ e ↑ Nat^{s}  C_{o} ; \overline{Γ} ⊢ e_{o} ↓ σ  C_{s} ; \overline{Γ} ⊢ e_{s} ↓ Nat^{α} → σ}{\{s ≤ α̂\} ∪_{⊥} C ∪_{⊥} C_{o} ∪_{⊥} C_{s} ; \overline{Γ} ⊢ case_{σ} e of \{0 ⇒ e_{o} | s ⇒ e_{s}\} ↑ σ} where α ∉ 𝒱_{ℐ}(\overline{Γ})

Example 4.7. Let us look at the following example, where V ∈ 𝒱_{𝒯}:

? ; v: V, f : Nat^{α} → V, y: Nat^{β} ⊢ case_{V} y of {0 ⇒ v | s ⇒ λz: Nat. f z} ↑?

Since γ ≤ α ; v: V, f : Nat^{α} → V, y: Nat^{β}, z: Nat^{γ} ⊢ f z ↑ V, we deduce

γ ≤ α, α ≤ γ ; v: V, f : Nat^{α} → V, y: Nat^{β} ⊢ λz: Nat. f z ↓ Nat^{α} → V

It follows that

γ ≤ α, α ≤ γ, β ≤ α̂ ;
v: V, f : Nat^{α} → V, y: Nat^{β} ⊢ case_{V} y of {0 ⇒ v | s ⇒ λz: Nat. f z} ↑ V

There are two things to note about the constraint γ ≤ α,α ≤ γ,β ≤ α̂. First, it contains a variable γ that appears nowhere else in the sequent. It is in fact the inference stage variable that correspond to the bound variable z. Hence, if the types recorded under abstractions were annotated by stages, we would have:

γ ≤ α, α ≤ γ, β ≤ α̂ ;
v: V, f : Nat^{α} → V, y: Nat^{β} ⊢ case_{V} y of {0 ⇒ v | s ⇒ λz: Nat^{γ}. f z} ↑ V

Second, this constraint implies α = γ, hence the type inference judgment above can be simplified to

β ≤ α̂ ; v: V, f : Nat^{α} → V, y: Nat^{β} ⊢ case_{V} y of {0 ⇒ v | s ⇒ λz: Nat^{α}. f z} ↑ V

This kind of notations is very convenient to write type inference judgments. ⊓ ⊔

4.3 Checking the correctness of recursive definitions

We now discuss the typing rule of fixpoints:

(rec) \frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}[ı:= î] ı pos \overline{θ}}{\overline{Γ} ⊢ (letrec_{d|\overline{τ}|→|\overline{θ}|} f = e) : d^{s}\overline{τ}→ \overline{θ}[ı:= s]} if ı ∉ \overline{Γ},\overline{τ}

For the sake of simplicity, we assume for the moment that d is a monomorphic inductive datatype (hence \overline{τ}= ∅) and that ı ∉ \overline{θ}. In this case, the typing rule of fixpoints becomes

(rec) \frac{\overline{Γ},f : d^{ı}→ \overline{θ} ⊢ e : dî→ \overline{θ}}{\overline{Γ} ⊢ (letrec_{d→|\overline{θ}|} f = e) : d^{s} → \overline{θ}} if ı ∉ \overline{Γ},\overline{θ}

Consider now that rule from the point of view type inference. If we start from

? ; \overline{Γ} ⊢ (letrec_{d→θ} f = e) ↑?

then we have to compute a constraint C^{Rec} and a type d^{α} → \overline{θ} such that |\overline{θ}| = θ and

C^{Rec} ; \overline{Γ} ⊢ (letrec_{d→θ} f = e) ↑ d^{α} → \overline{θ}

(var)  \overline{∅ ; \overline{Γ},x : \overline{σ} ⊢ x ↑ \overline{σ}}

(abs) \frac{C ; \overline{Γ},x : \overline{τ}⊢ e ↑ \overline{σ}  (\overline{τ},V) = Annot(τ,𝒱_{ℐ}(\overline{Γ}))}{C ; \overline{Γ} ⊢ λx: τ. e ↑ \overline{τ}→ \overline{σ}}

(app)  \frac{C_{1} ; \overline{Γ} ⊢ e ↑ \overline{τ}→ \overline{σ}  C_{2} ; \overline{Γ} ⊢ e′↓ \overline{τ}}{C_{1}∪_{⊥} C_{2} ; \overline{Γ} ⊢ e e′↑ \overline{σ}}

(T-abs)  \frac{C ; \overline{Γ} ⊢ e ↑ \overline{σ}}{C ; \overline{Γ} ⊢ ΛX. e ↑ ΠX. \overline{σ}}  if X ∉ \overline{Γ}

(T-app) \frac{C ; \overline{Γ} ⊢ e ↑ ΠX. \overline{σ}  (\overline{τ},V) = Annot(τ,𝒱_{ℐ}(\overline{Γ}))}{C ; \overline{Γ} ⊢ e τ ↑ \overline{σ}[X := \overline{τ}]}

(cons) \frac{c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗}{∅ ; \overline{Γ} ⊢ c_{k} ↑ ΠX⃗. \overline{θ}_{k}[ı:= α] → dα̂ X⃗} if α ∉ 𝒱_{ℐ}(\overline{Γ})
where 𝒞(d) = {c_{1},...,c_{n}} for some d

(case) \frac{\begin{matrix}C ; \overline{Γ} ⊢ e ↑ d^{s} \overline{τ}  α ∉ 𝒱_{ℐ}(\overline{Γ})  (\overline{σ},V) = Annot(σ,𝒱_{ℐ}(\overline{Γ}) ∪ \{α\}) \\ c_{k}: ΠX⃗. \overline{θ}_{k} → dîX⃗ C_{k} ; \overline{Γ} ⊢ e_{k} ↓ \overline{θ}_{k}[X⃗:= \overline{τ},ı:= α] → \overline{σ} (1 ≤ k ≤ n) \end{matrix}}{\{s ≤ α̂\} ∪_{⊥} C ∪_{⊥} (⋃ _{⊥} C_{k}) ; \overline{Γ} ⊢ case_{σ} e of \{c_{1} ⇒ e_{1} | ···| c_{n} ⇒ e_{n}\} ↑ \overline{σ}}

where 𝒞(d) = {c_{1},...,c_{n}}

(sub)  \frac{C ; \overline{Γ} ⊢ e ↑ \overline{τ}}{C ∪_{⊥} ⦇\overline{τ}⊑ \overline{σ}⦈ ; \overline{Γ} ⊢ e ↓ \overline{σ}}

Fig. 7. Type inference with constraints The constraint C^{Rec} must be computed from the constraint C generated by typechecking the body e of the recursive definition. Keeping an eye on the rule (rec), this can be written

\frac{C ; \overline{Γ},f : d^{α} → \overline{θ} ⊢ e ↓ dα̂ → \overline{θ}}{C^{Rec} ; \overline{Γ} ⊢ (letrec_{d→θ} f = e) ↑ d^{α} → \overline{θ}}

We want to stick to the semantics of type inference provided by Prop. 4.6. Hence, if ρ ⊧ C^{Rec} we must have

\overline{Γ}ρ ⊢ (letrec_{d→θ} f = e) : d^{ρ(α)} → \overline{θ}ρ

Therefore, we must be able to check the premises of the rule (rec). This means that there must exist a substitution ρ′such that \overline{Γ}ρ′= \overline{Γ}ρ′, ρ′⊧ C, ρ′(α) = ı and

\overline{Γ}ρ′,f : d^{ı}→ \overline{θ}ρ′⊢ e : dî→ \overline{θ}ρ′ with ı ∉ \overline{Γ}ρ′

We will try to explain how to do this by considering two examples of fixpoints definitions:

fix_{1} := (letrec_{Nat→Nat} f = λx: Nat. o)
fix_{2} := (letrec_{Nat→Nat} f = λx: Nat. (f o))

Note that fix_{1}o terminates while fix_{2}o does not. Hence, fix_{1} must be typable while fix_{2} must be rejected by the type inference algorithm. Let us now inspect the typechecking derivations of the bodies of these two functions.

– For the body of fix_{1}, we have

\frac{∅ ; f : Nat^{α} → Nat^{β},x: Nat^{γ} ⊢ o ↑ Natδ̂}{∅ ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. o ↑ Nat^{γ} → Natδ̂}

Since ⦇Nat^{γ} → Natδ̂ ⊑ Natα̂ → Nat^{β} ⦈ = α̂ ≤ γ, δ̂ ≤ β, it follows that

α̂ ≤ γ, δ̂ ≤ β ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. o ↓ Natα̂ → Nat^{β}

– For the body of fix_{2}, we have

\frac{∅ ; f : Nat^{α} → Nat^{β},x: Nat^{γ} ⊢ o ↑ Natδ̂}{δ̂ ≤ α ; f : Nat^{α} → Nat^{β},x: Nat^{γ} ⊢ o ↓ Nat^{α}}

Hence

\frac{δ̂ ≤ α ; f : Nat^{α} → Nat^{β},x: Nat^{γ} ⊢ f o ↑ Nat^{β}}{δ̂ ≤ α ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. (f o) ↑ Nat^{γ} → Nat^{β}}

It follows that

δ̂ ≤ α, α̂ ≤ γ ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. (f o) ↓ Natα̂ → Nat^{β}

We arrive at these two derivations

\frac{α̂ ≤ γ, δ̂ ≤ β ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. o ↓ Natα̂ → Nat^{β}}{C_{1}^{Rec} ; ⊢ (letrec_{Nat→Nat} f = λx: Nat. o) ↑ Natα̂ → Nat^{β}}  (fix_{1})

δ̂ ≤ α, α̂ ≤ γ ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. (f o) ↓ Natα̂ → Nat^{β}
C_{2}^{Rec} ; ⊢ (letrec_{Nat→Nat} f = λx: Nat. (f o)) ↑ Natα̂ → Nat^{β}

(fix_{2})

where

C_{1}^{Rec}  is computed from  C_{1} =_{def} α̂ ≤ γ, δ̂ ≤ β
C_{2}^{Rec}  is computed from  C_{2} =_{def} δ̂ ≤ α, α̂ ≤ γ

The constraints C_{1}^{Rec} and C_{2}^{Rec} must satisfy different properties:

– We want fix_{1} to be typable. Hence, C_{1}^{Rec} must be satisfiable, and moreover, for all substitution ρ such that ρ ⊧ C_{1}^{Rec}, there must be a substitution ρ′ and a stage variable ı such that ı ∉ codom(ρ), ρ′(α) = ı, ρ′(β) = ρ(β) and ρ′⊧ α̂ ≤ γ, δ̂ ≤ β.

– C_{2}^{Rec} must be unsatisfiable because fix_{2} is not typable since it does not terminate. C_{2}^{Rec} will actually be the false constraint ⊥.

These properties are provided by an algorithm called RecCheck. We present it on the simplified version of the rule (rec):

(rec) \frac{\overline{Γ},f : d^{ı}→ \overline{θ} ⊢ e : dî→ \overline{θ}}{\overline{Γ} ⊢ (letrec_{d→|\overline{θ}|} f = e) : d^{s} → \overline{θ}} if ı ∉ \overline{Γ},\overline{θ}

Recall that stage expressions s ∈ 𝒮 are either of the form î^{n}with ı ∈ 𝒱_{𝒮} or of the form ∞^{n}. Hence, any stage expression s has at most one occurrence of a unique stage variable ı ∈ 𝒱_{𝒮}. We call this stage variable the base stage of s, and write it ⌊s⌋.

Now, consider a fixpoint (letrec_{d→θ} f = e) such that

C ; \overline{Γ},f : d^{α} → \overline{θ} ⊢ e ↓ dα̂ → \overline{θ}  with α ∉ \overline{Γ},\overline{θ}  (6)

We say that α is the fixpoint inference stage variable of (letrec_{d→θ} f = e).

Example 4.8. The fixpoint stage variable of both fix_{1} and fix_{2} is α. ⊓ ⊔

Consider an instance of the judgment (6) for substitution ρ. In order to apply the rule (rec) with that instance as premise, the fixpoint inference stage variable α must be mapped to a fresh stage variable ı. Moreover, we must have ı ∉ \overline{Γ}ρ,\overline{θ}ρ. This imposes that no inference stage variable occurring in \overline{Γ},\overline{θ} can be mapped to a stage expression with base stage ı. Let V^{≠} =_{def} 𝒱_{ℐ}(\overline{Γ},\overline{θ}).

The algorithm works on a representation of C as a graph whose nodes are inference stages variables and ∞, and whose edges are integers. Each constraint in C is of the form ∞ ≤ β̂^{n}, or α̂_{1}^{n_{1}} ≤ α̂_{2}^{n_{2}}. In the first case, one adds an edge from β to ∞ labeled with 0, in the second case one adds an edge from α_{2} to α_{1} labeled with n_{2} − n_{1}. We do not represent edges for constraints of the form β̂^{n} ≤ β̂^{n}.

\begin{matrix}[figure: α; −1; γ; δ; −1; β] & [figure: δ; −1; α; −1; γ] \\ α̂ ≤ γ, δ̂ ≤ β & δ̂ ≤ α, α̂ ≤ γ \\ C_{1} & C_{2} \end{matrix}

Fig. 8. The graphs of the constraints C_{1} and C_{2}.

Example 4.9. The graphs representing C_{1} and C_{2} are depicted in Fig. 8. ⊓ ⊔

Before explaining the algorithm, let us make an important remark on the graph of constraints. It may happen that the graph contains a negative cycle, i.e. a cycle where the sum of the edges is strictly negative. Such cycles imply β̂^{k+1} ≤ β, or equivalently ∞ ≤ β, for the variable β in the cycle. Hence, every variable in a negative cycle must be mapped to ∞. Therefore, at some stage in the algorithm, it is necessary to compute negative cycles. This can be done using Bellman’s algorithm, which runs n^{2}, where n is number of edges of the graph, hence the number of inference stage variables in C.

The algorithm runs in two phases. The first phase ensures that the fixpoint inference stage variable α can be mapped to ı, and the second phase ensures that no variable in V^{≠} must be mapped to a stage expression with base stage ı.

First phase: variables that must be mapped to ı. First, note that the constraint δ̂ ≤ α, α̂ ≤ γ of fix_{2} can not be satisfied by a substitution which sends α to the stage variable ı. Indeed, the constraint δ̂ ≤ α would lead to a stage inequality of the form ŝ≤ ı, which is not derivable.

Let us see how we can detect this kind of situation. Observe that constraints of the form β̂^{n} ≤ α̂^{m} force β to be mapped to a stage expression with base stage ı. This is the case of the variable δ in the constraint C_{2}. So, we define S^{ı}, the set of inference stage variable that must be mapped to a stage expression with base stage ı, as the downward closure of {α}:

α ∈ S^{ı} and β ∈ S^{ı} if β̂^{n} ≤ γ̂^{m}∈ C with γ ∈ S^{ı}

Example 4.10. For fix_{1} we have S^{ı}= {α} and for fix_{2} we have S^{ı}= {α,δ}. ⊓ ⊔

Note that if β ∈ S^{ı}is mapped to a s depending on ı, then we must have ı ≤ s. We represent this by computing a new set of constraints C^{1} =_{def} C ∪ {α ≤ β | β ∈ S^{ı}}.

Example 4.11. These constraints for fix_{1} and fix_{2}, denoted respectively C_{1}^{1} and C_{2}^{1}, are depicted in Fig. 9. We have C_{1}^{1} = C_{1}. On the other hand, the graph of C_{2}^{1} contains a negative cycle which forces α to be mapped to ∞. Hence α can not be mapped to ı. ⊓ ⊔

\begin{matrix}[figure: α; −1; γ; δ; −1; β] & [figure: δ; −1; α; 0; −1; γ] \\ α̂ ≤ γ, δ̂ ≤ β & δ̂ ≤ α, α̂ ≤ γ, α ≤ δ \\ C_{1}^{1} & C_{2}^{1} \end{matrix}

Fig. 9. The graphs of the constraints C_{1}^{1} and C_{2}^{1}.

Therefore, we now have to check for negative cycles in the graph of C^{1}. For each such cycle starting from β, we compute the set V_{β≤} of variables greater or equal to β, removes all inequalities about variables in V_{β≤} and adds the constraints ∞ ≤ γ for γ ∈ V_{β≤} . Hence, we get a new set of constraints C^{2} that does not contain cycles.

Example 4.12. The sets C_{1}^{2} and C_{2}^{2} for fix_{1} and fix_{2} are depicted on Fig. 10. The negative cycle involving α in C_{2}^{1} implies that C_{2}^{2} forces α to be mapped to ∞, which makes impossible to map α to ı. Therefore, we can already discard fix_{2} at this point, and put C_{2}^{Rec} =_{def} ⊥. On the other hand, the constraint C_{1}^{2} poses no problem. ⊓ ⊔

\begin{matrix}[figure: α; −1; γ; δ; −1; β] & [figure: ∞; 0; 0; 0; δ; γ; α] \\ α̂ ≤ γ, δ̂ ≤ β & ∞ ≤ δ, ∞ ≤ α, ∞ ≤ γ \\ C_{1}^{2} & C_{2}^{2} \end{matrix}

Fig. 10. The graphs of the constraints C_{1}^{2} and C_{2}^{2}.

Second phase: ensuring that ı ∉ \overline{Γ}ρ,\overline{θ}ρ. Since we must have ı ∉ \overline{Γ}ρ,\overline{θ}ρ, no inference stage variables occurring in \overline{Γ},\overline{θ} can be mapped by ρ to a stage expression with base stage ı. Moreover, if β is such a variable and β̂^{n} ≤ δ̂^{m} is derivable from C^{2} (i.e. if there is a path from δ to β in the graph of C^{2}), then δ can not be mapped to a stage expression with base stage ı. Indeed, s ≤ î^{p}implies that s is of the form î^{q}. Hence, mapping δ to î^{p} for some p forces to map β to î^{q}some q. Therefore, we let S^{¬ı}, the set of variables that can not be mapped to a stage expression with base stage ı, be the upward closure of V^{≠} :

V^{≠} ⊆ S^{¬ı} and δ ∈ S^{¬ı} if β̂^{n} ≤ δ̂^{m}∈ C^{2} with β ∈ S^{¬ı}

(recall that V^{≠} = 𝒱_{ℐ}(\overline{Γ},\overline{θ})).

Example 4.13. For fix_{1} and fix_{2} we have S_{1}^{¬ı} = S_{2}^{¬ı} = {β} = V_{1}^{≠} = V_{2}^{≠} . ⊓ ⊔

Now, assume that there is in C^{2} a path from a variable δ ∈ S^{¬ı} to a variable β ∈ S^{ı} (hence that β̂^{n} ≤ δ̂^{m} is derivable from C^{2}). Since β must be mapped to an expression with base stage ı, there are two possibilities for δ: it must be mapped either to a stage expression with base stage ı or to ∞. But δ can not be mapped to a stage expression with base stage ı. It must therefore be mapped to ∞, which is expressed by the constraint ∞ ≤ δ. Now, it may happen that such new constraints force a variable γ ∈ S^{ı} to be mapped to ∞ (see for instance Ex. 4.14below). In this case the algorithm fails, otherwise it succeeds.

Formally, we proceed as follows.

1. We compute the upward closed set S^{ı≤} of stage variables that must be mapped to ∞ or to a stage expression with base stage ı:

S^{ı}⊆ S^{ı≤} and δ ∈ S^{ı≤} if β̂^{n} ≤ δ̂^{m}∈ C^{2} with β ∈ S^{ı≤}

For fix_{1}, we have S_{1}^{ı≤} = {α,γ}.

2. Proceeding as for computing C^{2}, we set all variables β ∈ S^{¬ı}∩ S^{ı≤} to ∞. This generates a new set of constraints C^{3}. For fix_{1}, we have S_{1}^{¬ı}∩ S_{1}^{ı≤} = ∅, hence C_{1}^{3} = C_{1}^{2}.

3. We compute the upward closed set S^{∞} of stage variables that must be mapped to ∞:

β ∈ S^{∞} if ∞ ≤ β̂^{k} ∈ C^{3} or ( δ̂^{n} ≤ β̂^{m} ∈ C^{3} with δ ∈ S^{∞} )

Now, if S^{ı}∩ S^{∞} = ∅, then the algorithm succeeds and we put C^{Rec} := C^{3}, otherwise it fails and we put C^{Rec} := ⊥.

This second phase succeeds for fix_{1}. On the other hand, the failure of the algorithm for fix_{2} was already known at the end of the first phase. In Ex. 4.14 below, we give an expression for which the algorithm succeeds on the first phase and fails on the second.

In the case of fix_{1}, the algorithm succeeds and we have C_{1}^{Rec} = C_{1}^{2} = C_{1}^{1} = C_{1}. We arrive at the following inference derivation:

\frac{α̂ ≤ γ, δ̂ ≤ β ; f : Nat^{α} → Nat^{β} ⊢ λx: Nat. o ↓ Natα̂ → Nat^{β}}{α̂ ≤ γ, δ̂ ≤ β ; ⊢ (letrec_{Nat→Nat} f = λx: Nat. o) ↑ Nat^{α} → Nat^{β}}

We check that the constraint C_{1}^{Rec} specifies what is needed to apply the rule (rec):

(rec) \frac{f : Nat^{ı}→ Nat^{r} ⊢ λx: Nat. o : Natî→ Nat^{r}}{⊢ (letrec_{Nat→Nat} f = λx: Nat. o) : Nat^{s} → Nat^{r}} if ı ∉ r

Let ρ such that ρ̂(α) ≤ ρ(γ) and ρ̂(δ) ≤ ρ(β). Moreover, let s =_{def} ρ(α) and r =_{def} ρ(β). Let ı ∉ ρ(β),ρ(δ) and define ρ′such that

ρ′(α) = ı  ρ′(γ) = î ρ′(β) = ρ(β)  ρ′(δ) = ρ(δ)

We thus have { \atop ρ′(α)} ≤ ρ′(γ) and { \atop ρ′(δ)} ≤ ρ′(β). It follows that

f : Nat^{ı}→ Nat^{r} ⊢ λx: Nat. o : Natî→ Nat^{r}

Since ı ∉ r, by (rec) deduce that ⊢ (letrec_{Nat→Nat} f = λx: Nat. o) : Nat^{s} → Nat^{r}, hence ⊢ (letrec_{Nat→Nat} f = λx: Nat. o) : Nat^{ρ(α)} → Nat^{ρ(β)}.

Example 4.14 (The second phase of RecCheck). Consider the following expressions:

fix_{3} := λv: V. λy: Nat. (letrec f = λx: Nat.
case_{V} x of {o ⇒ v | s ⇒ λz: Nat. f z})
fix_{4} := λv: V. λy: Nat. (letrec f = λx: Nat.
case_{V} y of {o ⇒ v | s ⇒ λz: Nat. f z})

If we forget stages, both fix_{3} and fix_{4} would have type V → Nat → Nat → V, hence

v: V ⊢ fix_{3} v (s o) o : V and v: V ⊢ fix_{4} v (s o) o : V

The only difference between fix_{3} and fix_{4} is the variable subject to the case-analysis: in fix_{3}, this is the variable x, bound inside the fixpoint, while in fix_{4}, this is the variable y, bound outside the fixpoint. This leads to very different behaviors: fix_{3}v(so)o is strongly normalizing and reduces to v, whereas fix_{4}v(so)o has no normal form. Indeed, we have fix_{4}v(so)o →^{∗} fix′_{4}o and

fix′_{4} o →^{∗} case_{V} (so) of {o ⇒ v | s ⇒ λz: Nat. fix′_{4}z} → fix′_{4} o → ...

where fix′_{4} := (letrec f = λx : Nat. case_{V} (so) of {o ⇒ v | s ⇒ λz : Nat. f z}). Let us have a look at the constraints generated during the typechecking of fix_{3} and fix_{4}. Reasoning as in Ex. 4.7 (and doing the same simplifications), we obtain the following judgment for fix_{3}:

β ≤ α̂ ; v: V, y: Nat^{γ}, f : Nat^{α} → V, x: Nat^{β} ⊢ case_{V} x of {0 ⇒ v | s ⇒ λz: Nat^{α}. f z} ↑ V

and for fix_{4}:

γ ≤ α̂ ; v: V, y: Nat^{γ}, f : Nat^{α} → V, x: Nat^{β} ⊢ case_{V} y of {0 ⇒ v | s ⇒ λz: Nat^{α}. f z} ↑ V

This leads to the following premises to the type inference rule (rec): for fix_{3}, we have

β ≤ α̂, α̂ ≤ β ; v: V, y: Nat^{γ}, f : Nat^{α} → V ⊢

λx: Nat^{β}. case_{V} x of {0 ⇒ v | s ⇒ λz: Nat^{α}. f z} ↓ Natα̂ → V

and for fix_{4}, we have

γ ≤ α̂, α̂ ≤ β ; v: V, y: Nat^{γ}, f : Nat^{α} → V ⊢

λx: Nat^{β}. case_{V} y of {0 ⇒ v | s ⇒ λz: Nat^{α}. f z} ↓ Natα̂ → V

Let C_{3} =_{def} β ≤ α̂, α̂ ≤ β and C_{4} =_{def} γ ≤ α̂, α̂ ≤ β. In both cases, when checking the body of the recursive definition, α is the fixpoint stage variable (i.e. it must be mapped to ı), while γ can not be mapped to a stage expression with base stage ı. The variable β must normally not appear as an annotation of Nat under the λ-abstraction; we write it just for convenience. We have V_{3}^{≠} = V_{4}^{≠} = {γ}, hence there is a priori no restriction on β. The constraint C_{4} impose γ to be mapped to ı, and the algorithm will fail on fix_{4} for this reason. We display on Fig.11 the runs of the algorithm on fix_{3} and fix_{4}. The algorithm succeeds on fix_{3}. On fix_{4}, the first phase succeeds but the second fails. ⊓ ⊔

C_{3} = β ≤ α̂, α̂ ≤ β  C_{4} = γ ≤ α̂, α̂ ≤ β
S_{3}^{ı} = {α,β}  S_{4}^{ı} = {α,γ}
V_{3}^{≠} = {γ}  V_{4}^{≠} = {γ}
[figure: C_{3}^{2} = C_{3}^{1} =; α; −1; 0; 1; β; C_{4}^{2} = C_{4}^{1} =; γ; 1; 0; α; −1; β]
S_{3}^{¬ı} = {γ}  S_{4}^{¬ı} = {α,γ}
S_{3}^{ı≤} = {α,β}  S_{4}^{ı≤} = {α,β,γ}
S_{3}^{¬ı}∩ S_{3}^{ı≤} = ∅  S_{4}^{¬ı}∩ S_{4}^{ı≤} = {α,γ}
[figure: C_{3}^{3} = C_{3}^{2} =; α; −1; 0; 1; β; C_{4}^{3} =; γ; α; −1; β; ∞; 0; 0]

S_{3}^{∞} = ∅  S_{4}^{∞} = {α,β,γ}
S_{3}^{∞} ∩ S_{3}^{ı} = ∅  S_{4}^{∞} ∩ S_{4}^{ı} = {α,γ}
fix_{3}  fix_{4}

Fig. 11. Runs of RecCheck on fix_{3} and fix_{4} of Ex. 4.14.

4.4 Type inference in System F

We now turn to the formal and precise description of the type inference algorithm for F . Our presentation follows [4], where more details can be found.

System F ^{⋆}. When we discussed the typing rule of fixpoint in the last section (Sect. 4.3), we silenced one issue concerning the types appearing as tags in terms. Consider the typing rule (rec)

(rec) \frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}[ı:= î] ı pos \overline{θ}}{\overline{Γ} ⊢ (letrec_{d|\overline{τ}|→|\overline{θ}|} f = e) : d^{s}\overline{τ}→ \overline{θ}[ı:= s]} if ı ∉ \overline{Γ},\overline{τ}

In the general case, the stage variable may appear in \overline{θ}. But when inferring the type of a fixpoint ? ; \overline{Γ} ⊢ (letrec_{d \overline{τ}→θ} f = e) ↑? we have a priori no indication on how the θ should be decorated. Therefore, type inference is performed in a system F ^{⋆} such that the type appearing in fixpoints convey an indication, symbolized by the tag ⋆, of the positions at which the fixpoint stage variable must appear. Such types are called position types and are given by the abstract syntax:

𝒯^{⋆} ::= 𝒱_{𝒯} | 𝒯^{⋆} → 𝒯^{⋆} | Π𝒱_{𝒯} . 𝒯^{⋆} | 𝒟^{⋆} 𝒯⃗^{⋆} | 𝒟 𝒯⃗^{⋆}

where in the clause for datatypes, it is assumed that the length of the vector 𝒯⃗^{⋆} is exactly the arity of the datatype. We let |.|: 𝒯^{⋆} → 𝒯 be the obvious erasure map from 𝒯^{⋆} to 𝒯.

The terms of F ^{⋆} are those of F , excepted that fixpoints are now of the form (letrec_{τ^{⋆}} f = e) where τ^{⋆} ∈ 𝒯^{⋆} is a position type.

The typing rules of F ^{⋆} are those of F , excepted that the typing rule (rec) of fixpoints is now

\frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}[ı:= î]}{\overline{Γ} ⊢ (letrec_{τ^{⋆}} f = e) : d^{s}\overline{τ}→ \overline{θ}[ı:= s]} if \{ \begin{matrix}ı ∉ \overline{Γ},\overline{τ}and ı pos \overline{θ} \\ τ^{⋆} is ı-compatible with d^{ı}\overline{τ}→ \overline{θ} \end{matrix}

where we say that a position type σ^{⋆} is ı-compatible with a sized type \overline{σ} if σ^{⋆} can be obtained from \overline{σ} by replacing all stage annotations containing ı by ⋆ and by erasing all other size annotations. For instance, Nat^{ı}→ Nat^{ȷ}→ Natîis ı-compatible with Nat^{⋆} → Nat → Nat^{⋆}, while Nat^{ı}→ Nat^{ı}→ Natîis not.

Remark 4.15 (The shape of τ^{⋆}). Note that the conjunction of the conditions ı ∉ \overline{τ} and τ^{⋆} ı-compatible with d^{ı}\overline{τ}→ \overline{θ} implies that τ^{⋆} is of the form d^{⋆}τ⃗→ θ^{⋆}, where τ⃗ are not position types (i.e. they convey no tag ⋆).

Doing type inference without position types would have been be very difficult, if not impossible. The cause is that in the rule (rec) of F

(rec) \frac{\overline{Γ},f : d^{ı}\overline{τ}→ \overline{θ} ⊢ e : dî\overline{τ}→ \overline{θ}[ı:= î] ı pos \overline{θ}}{\overline{Γ} ⊢ (letrec_{d|\overline{τ}|→|\overline{θ}|} f = e) : d^{s}\overline{τ}→ \overline{θ}[ı:= s]} if ı ∉ \overline{Γ},\overline{τ}

the type θ may not have a most general decoration.

Example 4.16. Consider the most general typings

(letrec_{Nat^{⋆}→Nat^{⋆}} f = λx: Nat. o) : Nat^{ı}→ Nat^{ı}
(letrec_{Nat^{⋆}→Nat} f = λx: Nat. o) : Nat^{ı}→ Natĵ

Would we omit ⋆ in the tags of the recursive definitions, then (letrec_{Nat→Nat} f = λx : Nat. o) would not have a most general typing. Indeed, such a most general typing would be of the form

C ; ⊢ (letrec_{Nat→Nat} f = λx: Nat. o) ↑ Nat^{ı_{1}}→ Nat^{ı_{2}}

with the substitutions [ı_{1} := ı,ı_{2} := ı] ⊧ C and [ı_{1} := ı,ı_{2} := ĵ] ⊧ C. By elementary reasoning, we can show that it is impossible. In order to recover a most general typing, it will be required to allow both disjunctions and conjunctions of constraints in C. Unfortunately, disjunction makes types more complex to compute and to grasp. ⊓ ⊔

The annotation of a position type τ^{⋆} is performed by a function Annot^{⋆}, which is similar to Annot but takes as input a position type instead of a bare type. It is specified as follows. If V is a set of inference stage variables and σ^{⋆} ∈ 𝒯^{⋆} is a position type, then Annot^{⋆}(σ^{⋆},V) returns a tuple (\overline{σ},V′,V^{⋆}) such that:

– as with Annot, each occurrence of an inductive datatype (tagged or not) in σ^{⋆} is annotated with a distinct inference stage variable α ∉ V (so that α occurs at most once in σ^{⋆}), and V′= V ∪ 𝒱_{ℐ}(\overline{σ}),

– |σ^{⋆}| = |\overline{σ}|,

– V^{⋆} is the set of inference stages variables occurring in \overline{σ} at positions that where tagged in σ.

For inst., Annot^{⋆}(Nat^{⋆} → Nat,{α_{1},α_{2}}) = (Nat^{α_{3}} → Nat^{α_{4}},{α_{1},α_{2},α_{3},α_{4}},{α_{3}}). Therefore, the inference rule for fixpoints will have the following shape:

\frac{C ; \overline{Γ},f : d^{α} \overline{τ}→ \overline{θ} ⊢ e ↓ dα̂ → \overline{θ} (d^{α} \overline{τ}→ \overline{θ},V′,V^{⋆}) = Annot^{⋆}(d^{⋆}τ⃗→ θ^{⋆},V)}{C^{Rec} ; \overline{Γ} ⊢ (letrec_{d^{⋆}τ⃗→θ^{⋆}} f = e) ↑ d^{α} \overline{τ}→ \overline{θ}}

where C^{Rec} is computed by RecCheck and V = 𝒱_{ℐ}(\overline{Γ}). Before giving the formal definition of RecCheck, let us stress some important points. Recall that there must be a fresh stage variable ı such that the variables β ∈ V^{⋆} must all be mapped to a stage expression of base stage ı, and moreover the fixpoint variable α, which belongs to V^{⋆}, must be mapped to ı. Note that V^{⋆}\{α} contains exactly the set of inference variables occurring in \overline{θ} that must be mapped to a stage expression with base stage ı.

Therefore, the variables β ∈ V \ V^{⋆} are annotations of untagged datatypes occurrences in τ^{⋆}. Hence they can not be mapped to stage expressions depending on ı.

Moreover the typing rule of fixpoint imposes that for all substitution ρ, all occurrences of ı in \overline{θ}ρ must be positive. It follows that all occurrences of β ∈ V^{⋆} \ \{α\} in \overline{θ} must be positive. The type inference algorithm check this by encoding positivity tests in constraints. This is possible thanks to the following Lemma.

Lemma 4.17. ı pos \overline{τ} if and only if \overline{τ}⊑ \overline{τ}[ı:= î].

Note that by definition of Annot^{⋆}, the fixpoint variable α does not occur in \overline{θ}. Hence the positivity test for the occurrences of variables β ∈ V^{⋆} in \overline{θ} can be coded by the constraint ⦇\overline{θ} ⊑ θ̂⦈ where θ̂ is defined as θ̂ =_{def} \overline{θ}[β:= β̂]_{β∈V^{⋆}}. Therefore, in addition to the constraint C^{Rec} computed by RecCheck, the type inference rule of fixpoints produces a constraint ⦇\overline{θ} ⊑ θ̂⦈:

\frac{C ; \overline{Γ},f : d^{α} \overline{τ}→ \overline{θ} ⊢ e ↓ dα̂ → \overline{θ} (d^{α} \overline{τ}→ \overline{θ},V′,V^{⋆}) = Annot^{⋆}(d^{⋆}τ⃗→ θ^{⋆},V)}{C^{Rec} ∪_{⊥} ⦇\overline{θ} ⊑ θ̂⦈ ; \overline{Γ} ⊢ (letrec_{d^{⋆}τ⃗→θ^{⋆}} f = e) ↑ d^{α} \overline{τ}→ \overline{θ}}

where V = 𝒱_{ℐ}(\overline{Γ}).

The RecCheck algorithm. We now turn to the computation of RecCheck. This algorithm is at the core of guaranteeing termination. As we have in Sect.4.3, it takes as input the set of constraints that has been inferred for the body of the recursive definition, and either returns an error if the definition is unsound w.r.t. the type system, or the set of constraints for the recursive definition, if the definition is sound w.r.t. the type system. The formal definition of the function is given below. Let us look at its signature. Starting from (d^{α} \overline{τ}→ \overline{θ},V,V^{⋆}) := Annot^{⋆}(d^{⋆}τ⃗→ θ^{⋆},𝒱_{ℐ}(\overline{Γ})), we have

– an inference fixpoint variable α which must be mapped to a fresh stage variable ı,

– a set of inference stage variables V^{⋆}, containing α, which must be mapped to a stage expression with base stage ı,

– and a set V \ V^{⋆} which can not be mapped to stage expressions with base stage ı.

This corresponds to the first three arguments of RecCheck. The last one is the constraint C generated by typechecking the body of the recursive definition. Formally, the function RecCheck takes as input a tuple (α,V^{⋆},V^{≠} ,C), where

– α is the fixpoint inference stage variable of the recursive definition ; it must be mapped to a fresh base stage ı;

– V^{⋆} is a set of inference stage variables that must be mapped to a stage expression with the same base stage as α. The set V^{⋆} is determined by the position types in the tag of the recursive definition. In particular, we have α ∈ V^{⋆};

– V^{≠} is a set of inference stage variables that must be mapped to a stage expression with a base stage different from ı;

– C is the constraint inferred by typechecking the body of the recursive definition.

The algorithm RecCheck(α,V^{⋆},V^{≠} ,C) returns ⊥ or a set of constraints subject to conditions that will be presented later.

We now turn to the computation of RecCheck(α,V^{⋆},V^{≠} ,C). Assuming that we intend to map α to a fresh stage variable ı, the computation proceeds as follows:

1. it computes the downwards closed set S^{ı} of stage variables that must be mapped to a stage expression with base stage ı. The rules are V^{⋆} ⊆ S^{ı}, and if α_{1} ∈ S^{ı} and α̂_{2}^{n_{2}} ≤ α̂_{1}^{n_{1}} ∈ C then α_{2} ∈ S^{ı};

2. the algorithm must enforce that α is the smallest variable in S^{ı}. It does so by adding to C the constraints α ≤ S^{ı}. Let C_{1} = C ∪ α ≤ S^{ı};

3. the algorithm checks for negative cycles in the graph representation of C_{1}. Each time it finds such a cycle starting from β, the algorithm computes the set V_{⊒β} of variables greater or equal to β, removes all inequalities about variables in V_{⊒β} and adds the constraints ∞ ≤ V_{⊒β} . At the end of this step there are no more negative cycles in the graph, and we get a new set of constraints C_{2}; 4. the algorithm computes the upwards closed set S^{ı≤} of stage variables that must be

mapped to ∞ or to a stage expression with base stage ı. The rules are S^{ı}⊆ S^{ı≤} and if α_{1} ∈ S^{ı≤} and α̂_{1}^{n_{1}} ≤ α̂_{2}^{n_{2}} ∈ C_{2} then α_{2} ∈ S^{ı≤};

5. the algorithm computes the upwards closed set S^{¬ı} of stage variables that cannot be mapped to a stage expression with base stage ı. The rules are V^{≠} ⊆ S^{¬ı} and if α_{1} ∈ S^{¬ı} and α̂_{1}^{n_{1}} ≤ α̂_{2}^{n_{2}} ∈ C_{2} then α_{2} is in S^{¬ı};

6. the algorithm sets all variables β ∈ S^{¬ı}∩ S^{ı≤} to ∞ (as in Step 3). At the end of this step we get a new set of constraints C_{3};

7. the algorithm computes the upwards closed set S^{∞} of stage variables that must be mapped to ∞. If ∞ ≤ β̂^{k} ∈ C_{3} then β is in S^{∞}, and if α_{1} ∈ S^{∞} and α̂_{1}^{n_{1}} ≤ α̂_{2}^{n_{2}} ∈ C_{3} then α_{2} is in S^{∞}.

8. if S^{∞} ∩ S^{ı}= ∅ the algorithm returns the new set of constraints, else it fails.

We have already explained this algorithm in Sect. 4.3. Note that at the end of step 3, the algorithm can already stop and fail if C_{2} ⊢ ∞ ≤ α.

The inference algorithm. We now turn to the formal definition of the inference algorithm. Contrary to what we have done up to now, it is not presented by inference rules. The cause is that we want to have a very precise control on the fresh variables introduced during type inference. The defect of the presentation by inference rules can be seen on the inference rule (app) for the application:

(app) \frac{C_{1} ; \overline{Γ} ⊢ e ↑ \overline{τ}→ \overline{σ}  C_{2} ; \overline{Γ} ⊢ e′↓ \overline{τ}}{C_{1}∪_{⊥} C_{2} ; \overline{Γ} ⊢ e e′↑ \overline{σ}}

Assume that the derivation of C_{1} ; \overline{Γ} ⊢ e ↑ \overline{τ}→ \overline{σ} have generated fresh inference variables α⃗ occurring in C_{1} but not in \overline{Γ}. If we need fresh inference variables in the derivation of C_{2} ; \overline{Γ} ⊢ e′↓ \overline{τ}, then we must ensure that these variables are not taken among α⃗. Hence, we have to transmit the current set of non-fresh inference variable along the derivations of type inference. The easiest to do this is to use two functions Infer and Check such that

– Infer takes as input a tuple (V,\overline{Γ},e), where V is a set of already used inference variables such that 𝒱_{ℐ}(\overline{Γ}) ⊆ V. It returns a tuple (V′,C,\overline{τ}) such that C ; \overline{Γ} ⊢ e ↑ \overline{τ} and 𝒱_{ℐ}(C,\overline{τ}) ∪ V ⊆ V′.

– Check takes as input a tuple (V,\overline{Γ},e), where V is a set of already used inference variables such that 𝒱_{ℐ}(\overline{Γ},\overline{τ}) ⊆ V. It returns a tuple (V′,C) such that C ; \overline{Γ} ⊢ e ↓ \overline{τ} and 𝒱_{ℐ}(C,\overline{τ}) ∪ V ⊆ V′.

For instance, the inference rule for the application now becomes:

Infer(V,\overline{Γ},e_{1}e_{2}) = V_{2},C_{1}∪ C_{2},\overline{τ}
where (V_{1},C_{1},\overline{τ}_{2} → \overline{τ}) := Infer(V,\overline{Γ},e_{1})
(V_{2},C_{2}) := Check(V_{1},\overline{Γ},e_{2},\overline{τ}_{2})

Hence, if the derivation of C_{1} ; \overline{Γ} ⊢ e ↑ \overline{τ}→ \overline{σ} uses stage variables in V_{1}, then no fresh variable used in the derivation of C_{2} ; \overline{Γ} ⊢ e′↓ \overline{τ} belongs to V_{1}. The whole inference algorithm is presented in Fig. 12.

Check(V,\overline{Γ},e,\overline{τ})  = V_{e},C_{e}∪_{⊥} ⦇\overline{τ}_{e} ⊑ \overline{τ}⦈
where (V_{e},C_{e},\overline{τ}_{e}) := Infer(\overline{Γ},e)
Infer(V,\overline{Γ},x)  = V,∅,\overline{Γ}(x)
Infer(V,\overline{Γ},λx: τ_{1}. e)  = V_{e},C_{e},\overline{τ}_{1} → \overline{τ}_{2}
where V_{1},\overline{τ}_{1} := Annot(V,τ_{1})

(V_{e},C_{e},\overline{τ}_{2}) := Infer(V_{1},\overline{Γ},x : \overline{τ}_{1},e)

Infer(V,\overline{Γ},ΛA. e)  = V_{e},C_{e},ΠA. \overline{τ}
where (V_{e},C_{e},\overline{τ}) := Infer(V,\overline{Γ},e)
if A does not occur in\overline{Γ}
Infer(V,\overline{Γ},e_{1}e_{2})  = V_{2},C_{1}∪_{⊥} C_{2},\overline{τ}
where (V_{1},C_{1},\overline{τ}_{2} → \overline{τ}) := Infer(V,\overline{Γ},e_{1})
(V_{2},C_{2}) := Check(V_{1},\overline{Γ},e_{2},\overline{τ}_{2})
Infer(V,\overline{Γ},e τ)  = V_{e},C_{e},\overline{τ}_{e}[A:= \overline{τ}]
where V_{1},\overline{τ}:= Annot(V,τ)
(V_{e},C_{e},ΠA. \overline{τ}_{e}) := Infer(V_{1},\overline{Γ},e)
Infer(V,\overline{Γ},c)  = V ∪ \{α\},,Type(c,α)
with α ∉ V
Infer(V,\overline{Γ},case_{θ} e of \{c⃗ ⇒ e⃗\}) = V_{n},\{s ≤ α̂\} ∪_{⊥} C_{e}∪_{⊥} ⋃ _{i=1}^{n} C_{i},\overline{θ}
where α ∉ V
V_{θ},\overline{θ}:= Annot(V ∪ \{α\},θ)
(V_{0},C_{e},d^{s}\overline{τ}) := Infer(V_{θ},\overline{Γ},e)

(V_{i},C_{i}) := Check(V_{i−1} ,\overline{Γ},e_{i},Inst(c_{i},α,\overline{τ},\overline{θ}))

if 𝒞(d) = {c_{1},...,c_{n}}
Infer(V,\overline{Γ},(letrec_{d^{⋆}τ⃗→θ} f = e)) = V_{e},C_{f} ,d^{α} \overline{τ}→ \overline{θ}

where (V_{1},V^{⋆},d^{α} \overline{τ}→ \overline{θ}) := Annot^{⋆}(V,d^{⋆}τ⃗→ θ)

θ̂:= \overline{θ}[α_{i} := α̂_{i}]_{α_{i}∈V^{⋆}}

(V_{e},C_{e}) := Check(V_{1},\overline{Γ},f : d^{α} \overline{τ}→ \overline{θ},e,dα̂ \overline{τ}→ θ̂) C_{f} := RecCheck(α,V^{⋆},V_{1}\V^{⋆},C_{e}∪_{⊥} ⦇\overline{θ} ⊑ θ̂⦈)

Fig. 12. Inference algorithm

We end the description of the type inference algorithm by the following observation about constraints.

Remark 4.18. The principal type returned by the inference algorithm may not be represented in its most compact form: for example, the inference algorithm will infer for the usual definition of addition the unconstrained type Nat^{ı}→ Nat^{ȷ}→ Nat^{∞} whereas it would be more readable to use the equivalent type Nat^{∞} → Nat^{∞} → Nat^{∞}. Formally, we can define a notion of equivalence between pairs of types and constraint: we say (C,\overline{τ}) ⪯ (C′,\overline{τ′}) iff for every ρ s.t. ρ ⊧ C there exists ρ′ s.t. ρ′⊧ C′ and ρ′\overline{τ′}⊑ ρ\overline{τ}. Then, we define (C,\overline{τ}) ≃ (C′,\overline{τ′}) iff (C,\overline{τ}) ⪯ (C′,\overline{τ′}) and (C′,\overline{τ′}) ⪯ (C,\overline{τ}). Now, we can define a set of heuristics that transform a pair (C,\overline{τ}) into simpler ones. For example, one can replace by ∞ all size variables that only occur in negative positions in the type component of such pairs. One can also perform simplifications in the constraint, in the spirit of the rules that are used in the algorithm that checks the correctness of recursive definitions. We do not formalize the notion of simplification, but it is possible to define a notion of canonical form and provide a set of rules that transform every such pair to an equivalent, canonical one.

The soundness and completeness of the algorithm, which is stated in Proposition 4.1, is proved by induction on derivations, and relies on a proof that the algorithm RecCheck is itself sound and complete.

5 Further reading

The material presented in this paper is based on the research papers [3,4]; the first paper introduces λ , a simply typed fragment of the F , and shows that it enjoys strong normalization, whereas the second paper introduces F and presents the inference algorithm.

Type-based termination has its origins in Mendler’s formulation of recursion in the style of fixpoints [10]. Mendler’s ideas were further developed in a series of works, including [5,15], and adapted to reactive programming by Pareto, Hughes, and Sabry [9], and to type theory by Giménez [?]. Abel [2] and Barthe et al provide a more detailed account of related work in the area of type-based termination. Coquand and Dybjer [?] provide an historical account of inductive definitions in type theory, whereas Aczel [?] provides an introduction to inductive definitions in a set-theoretical setting.

References

1. A. Abel. Termination Checking with Types. RAIRO – Theoretical Informatics and Applications, 38(4):277–319, 2004. Special Issue (FICS’03).

2. A. Abel. Type-Base Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, LMU University, Munich, 2006.

3. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-Based Termination of Recursive Definitions. Mathematical Structures in Computer Science, 14(1):97–141, 2004.

4. G. Barthe, B. Grégoire, and F. Pastawski. Practical Inference for Type-Based Termination in a Polymorphic Setting. In Proceedings of TLCA’05, pages 71–85, 2005.

5. W.-N. Chin and S.-C. Khoo. Calculating Sized Types. Higher-Order and Symbolic Computation, 14(2–3):261–300, 2001.

6. J.H. Gallier. What’s So Special About Kruskal’s Theorem and the Ordinal Γ_{0}? A Survey of Some Results in Proof Theory. Annals of Pure and Applied Logic, 53(3):199–260, 1991.

7. J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. PhD thesis, Université Paris 7, 1972.

8. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

9. J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of POPL’96, pages 410–423. ACM, 1996.

10. N. P. Mendler. Recursive Types and Type Constraints in Second Order Lambda-Calculus. In Proceedings of LiCS’87, pages 30–36. IEEE Computer Society, 1987.

11. M. Parigot. On the Representation of Data in Lambda-Calculus. In Proceedings of CSL’89, volume 440 of LNCS, pages 309–321, 1989.

12. Z. Sp�awski and P. Urzyczyn. Type Fixpoints: Iteration vs. Recursion. In Proceedings of ICFP’99, pages 102–113. ACM, 1999.

13. M. Steffen. Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen, 1997.

14. W. W. Tait. A Realizability Interpretation of the Theory of Species. In R. Parikh, editor, Logic Colloquium, volume 453 of LNCS, pages 240–251, 1975.

15. H. Xi. Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation, 15(1):91–131, 2002.

Table of Contents

A tutorial on type-based termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Gilles Barthe Benjamin Grégoire Colin Riba

1 Introduction ....................................................... 1
2 Computations in polymorphic type systems ............................ 3
2.1 System F .................................................... 4
2.2 A polymorphic calculus with datatypes and general recursion......... 6
2.3 Inductive datatypes ............................................ 14
2.4 Guarded reduction for strong normalization........................ 16
2.5 Syntactic termination criteria .................................... 16
3 The system F of type-based termination ............................... 18
3.1 Semantical ideas for a type-based termination criterion .............. 18
3.2 Formal definition.............................................. 20
3.3 Some important properties ...................................... 28
3.4 A reducibility interpretation ..................................... 30
4 Type inference ..................................................... 32
4.1 Preliminaries: Type inference in system F ......................... 34
4.2 Adding sized inductive datatypes ................................ 34
4.3 Checking the correctness of recursive definitions ................... 39
4.4 Type inference in System F .................................... 47
5 Further reading .................................................... 53