Implementing a Normalizer Using Sized Heterogeneous Types

Andreas Abel^{1} Institut für Informatik Ludwig-Maximilians-Universität München Oettingenstr. 67, D-80538 München, GERMANY abel@tcs.ifi.lmu.de

Abstract

In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be defined by lexicographic induction on a and r, thus, giving rise to a structurally recursive normalizer for the simply-typed lambda-calculus. We generalize this scheme to simultaneous substitutions, preserving its simple termination argument. We further implement hereditary simultaneous substitutions in a functional programming language with sized heterogeneous inductive types, F_{ω}, arriving at an interpreter whose termination can be tracked by the type system of its host programming language.

Keywords: Sized Types, Heterogeneous Types, Nested Types, Interpreter, Normalization, De Bruijn Terms

1. INTRODUCTION

Inductive types T can be expressed as the least solution of the recursive equation F X = X for some suitable monotone type function F; we write T = μF and say that T is the least fixed-point of F. The least fixed point can be obtained in two ways: from above, using the theorem of Knaster and Tarski, and from below using transfinite iteration. Defining

\begin{aligned}μ^{0} & F & = & empty \\ μ^{α+1} & F & = & F (μ^{α}F) \\ μ^{λ} & F & = & ⋃_{α<λ} μ^{α}F, \end{aligned}

the least fixed-point of F is reached for some ordinal γ and we have F (μ^{γ}F) = μ^{γ}F. The construction of an inductive type from below is convenient if we want to define a function f : T → C over an inductive type; we can reason by transfinite induction that f is well-defined. This is especially the case if f is structurally recursive, i. e., refers in recursive calls only to smaller elements of the inductive type. Consider f = fix s being the fixed point of a functional s, i. e., fix s = s (fix s). Such functions can be introduced by the rule

\frac{s ∈ (μ^{α}F → C) → (μ^{α+1}F → C) for allα < β}{fix s ∈ μ^{β}F → C} .

The rule can be justified by transfinite induction up to β. Base case: Since μ^{0}F is empty, fix s ∈ μ^{0}F → C trivially. For the step case, assume fix s ∈ μ^{α}F → C. By the premise of the rule, s (fix s) ∈ μ^{α+1}F → C, and by the fix-point equation, fix s ∈ μ^{α+1}F → C. Finally, for the limit case, assume fix s ∈ μ^{α}F → C for all α < λ and assume t ∈ μ^{λ}F. By definition of iteration at a limit, t ∈ μ^{α}F for some α < λ, hence fix s t ∈ C. Since t was arbitrary, fix s ∈ μ^{λ}F → C.

Implementing a Normalizer using Sized Heterogeneous Types

Up to now, we have considered the semantics of inductive types and the justification of semantical functions. Mendler [22] first observed that by turning these semantical concepts into syntax,^{2} one gets a type system that accepts structurally recursive functions, hence, guarantees termination of well-typed programs. This idea has been taken up by Hughes, Pareto, and Sabry [17], Giménez [16], Amadio and Coupet-Grimal [9], Barthe et al. [10], Blanqui [14] and myself [1, 2]. My thesis [5] describes F_{ω}, an extension of the higher-order polymorphic lambda-calculus F_{ω} by sized inductive types and structural recursion. A sized inductive type μ^{a}F is the syntactic equivalent of an iteration stage μ^{α}F, only that a is now a syntactic ordinal expression and F is a syntactic type constructor whose monotonicity is established syntactically.

1Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).

2Another example where semantics has been successfully turned into syntax is the monad. Invented by Moggi as a tool to reason about impure features, it has become a device to program imperatively in Haskell.

In this article, we give a non-trivial example of a structurally recursive function whose termination is automatically established using sized types: a β-normalizer for simply-typed λ-terms. The heart of the normalizer are hereditary substitutions [25]: substitution of a normal form into another one, potentially triggering new substitutions, until a normal form is returned. Surprisingly, this process can be formulated by a lexicographic recursion on the type of the substituted value and the normal form substituted into. Our contribution is a generalization to hereditary simultaneous substitutions, necessary to handle de Bruijn-style λ-terms with static guarantee of well-scopedness. Such de Bruijn terms can be represented using a data structure of heterogeneous type [8, 13]. In F_{ω}, heterogeneous types can be expressed by higher-kinded inductive types, i. e., type μ^{a}F where F is an operator on type constructors instead of just types. As a result, we obtain an implementation of a normalizer in F_{ω} whose termination and well-scopedness is ensured by type-checking in F_{ω}.

The remainder of this article is organized as follows. In Section 2, we briefly present system F_{ω}. Then, we specify and verify hereditary substitutions and normalization for simply-typed λ-terms in Section 3. In Section 4 we modify the specification to account for simultaneous hereditary substitutions. An implementation in F_{ω} is provided in Section 5. We conclude by discussing related and further work.

2. F_{ω}: A POLYMORPHIC λ-CALCULUS WITH SIZED TYPES

In this section, we briefly introduce the most important concepts of F_{ω}. We assume familiarity with system F_{ω} and inductive types.

Kinds. Kinds classify type constructors. In F_{ω}, one has the kind ∗ of types and function kinds κ → κ′ for type constructors. In F_{ω} we additionally have a kind ord for syntactic ordinals. And we distinguish type constructors by their variance: they can be covariant (monotonic), contravariant (antitonic), or mixed-variant (no monotonicity information).

κ ::= ∗  kind of types
| ord  kind of ordinals
| κ →^{+} κ′  kind of covariant type constructors
| κ →^{−} κ′  kind of contravariant type constructors
| κ →^{∘} κ′  kind of mixed-variant type constructors

Type constructors. Type constructors are expressions of a type-level λ-calculus, given by the following grammar.

A, B, F, G ::= C | X | λX.F | F G

The constants C are drawn from a signature Σ (see Figure 1). We use +, ×, and → infix and write ∀X : κ.A for ∀_{κ}(λX.A). If clear from the context or inessential, we omit the kind annotation κ in ∀X : κ.A and μ_{κ}. We also write the first argument to μ_{κ}—the size index—superscript. For instance, μ^{a}(λX. 1 + A × X) denotes the lists of length < a containing elements of type A.

Constructors a : ord that denote ordinal expressions are essentially following the grammar

a, b ::= ı | ∞ | s a

where we use ı and ȷ for variables of kind ord. (Of course, there are non-normal expressions like (λX. ∞) G : ord, or neutral expression such as X G⃗ : ord, but they do not matter for our purposes.)

1 : ∗  unit type
+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification
μ_{κ} : ord →^{+} (κ →^{+} κ) →^{+} κ  inductive constructors
s : ord →^{+} ord  successor of ordinal
∞ : ord  infinity ordinal

FIGURE 1: Signature Σ.

The ordinal expression ∞ denotes an ordinal large enough such that all inductive types have reached their fixed-point, thus, we have

F (μ^{∞}F) = μ^{∞}F.

The ordinal expression s a denotes the ordinal successor of a. We also write a + n as shorthand for s (… (s a)) (n successors). In general, we have the type equation

μ^{a+1}F = F (μ^{a}F).

for sized inductive types.

Subtyping. The sized inductive type μ^{a}F : ∗ contains data trees of height < a (this can be seen from its semantics). Since the size index denotes an upper bound, we have a natural subtyping relation

μ^{a}F ≤ μ^{a+1}F ≤ ⋯ ≤ μ^{∞}F.

This relation is extended appropriately to all type constructors and to higher-order, taking the variance information into account. (For more details, see the article about higher-order subtyping in F_{ω} [4].)

Programs (terms). F_{ω} is a purely functional language with categorical datatypes^{3} and recursion. Programs are given by the following grammar.

e, f ::= x | λx.e | f e  λ-calculus
| ⟨⟩  inhabitant of type 1
| ⟨e_{1}, e_{2}⟩ | fst e | snd e  pairing and projections
| inl e | inr e | case e f_{1} f_{2}  injections into disjoint sum, case distinction
| fix f  recursion

The typing rules for the λ-calculus part are inherited from Curry-style system F_{ω}. Unit type, cartesian product and disjoint sum are introduced and eliminated using the respective terms given in the grammar. Inductive types can be introduced and eliminated using the above type equations. The outstanding feature of F_{ω} is the type-based recursion rule which has been semantically motivated in the introduction:

3Categorical datatypes do not contain names, just structure. Constructors of data structures are derived from the program primitives. This is in opposition to nominal languages where data constructors are themselves primitives (e. g., in Haskell).

\frac{f : ∀ı:ord. (∀X⃗. μ^{ı}F X⃗ → G ı) → ∀X⃗. μ^{ı+1}F X⃗ → G (ı + 1)  G : ord →^{+} ∗  a : ord}{fix f : ∀X⃗. μ^{a}F X⃗ → G a}

In comparison with the semantic rule given in the introduction, we now allow polymorphic recursion, and the result type G a may mention the ordinal index a, but only positively [10, 2, 14]. Note that the size index a in the conclusion can be arbitrary. (Alternatively, one could formulate the rule with conclusion fix f : ∀ı∀X⃗. μ^{ı}F X⃗ → G ı. This size-polymorphic function can then instantiated to any size a.)

This has been a short introduction to F_{ω}, more details can be found in my thesis [5]. In the next section, we start developing an interpreter for some object language, in our case, the simply-typed λ-calculus, which we will later implement in our meta language, F_{ω}.

3. A TERMINATING NORMALIZER FOR SIMPLY-TYPED LAMBDA-TERMS

In this section, we formally define hereditary substitution for the simply-typed λ-calculus. We show its termination, soundness, and completeness.

Types and terms. The following grammars introduce our object language, the simply-typed λcalculus. To distinguish it from our meta-language, F_{ω}, we use lower case letters for the types.

a, b, c ::= o | a → b  simple types
r, s, t ::= x | λx:a.t | r s  simply-typed terms
n  ::= x | n s  neutral terms (required in Section 3.3)
Γ  ::= ⋄ | Γ, x:a  typing contexts

Ordinary (capture-avoiding) substitution [s/x]t of s for x in t, the set FV(t) of free variables of term t, and β-equality t =_{β} t′ of terms t, t′ are defined as usual, as well as the typing judgement Γ ⊢ t : a. Let |a| ∈ ℕ denote a measure on types with |b| < |b → c| and |c| ≤ |b → c| (e. g., size, or order).

3.1. Hereditary substitution

We define a 4-ary function [s^{a}/x]t, called hereditary substitution, which returns a result r̂. A result is either just a term r or a term annotated with a type, written r^{a}. The intention is that if s and t are β-normal and well-typed terms, then the result will also be β-normal (and well-typed). Our definition is a simplification of Watkins et al.’s hereditary substitutions for terms of the logical framework LF extended to linearity and concurrency [25]. Implicitly, hereditary substitutions are present already in Joachimski and Matthes’ normalization proof for the simply-typed λ-calculus [18].

Let us first introduce some overloaded notation on results r̂. The operation \underline{r̂} discards the type annotation on the result if present, i. e., \underline{r^{a}} = r and \underline{r} = r. This operation is to be applied implicitly when the context demands it. For example, application of two results r̂ and ŝ implicitly discards the type annotations: r̂ŝ = \underline{r̂}\underline{ŝ}. Similarly for abstraction: λx: a.r̂ = λx: a.\underline{r̂}. Finally, reannotation r̂^{a} = (\underline{r̂})^{a} puts a fresh type annotation a onto a result.

Using these notations, we can compactly define hereditary substitution:

[s^{a}/x]x  = s^{a}
[s^{a}/x]y = y ifx ≠ y
[s^{a}/x](λy:b.r) = λy:b. [s^{a}/x]r where y fresh for s, x
[s^{a}/x](t u)  = ([û^{b}/y]r′)^{c}  if t̂= (λy:b′.r′)^{b→c}
t̂û  otherwise
where t̂ = [s^{a}/x]t
û = [s^{a}/x]u

Lemma 1 (Invariant) If [s^{a}/x]t = r^{c} then |c| ≤ |a|.

Proof. By induction on t. There are only two cases which return an annotated term:

• [s^{a}/x]x = s^{a}. Trivially |a| ≤ |a|.

• [s^{a}/x](t u) = ([û^{b}/y]r′)^{c} where [s^{a}/x]t = (λy: b′.r′)^{b→c}. By induction hypothesis, |b → c| ≤ |a|. This proves the invariant, since |c| ≤ |b → c| by definition of the measure | · |.

□

Lemma 2 (Termination and soundness) [s^{a}/x]t =_{β} [s/x]t for all a, s, x, t.

Proof. By lexicographic induction on (|a|, t). We consider the case of application, [s^{a}/x](t u): By induction hypothesis, t̂ = [s^{a}/x]t and û = [s^{a}/x]u are both defined. We consider the subcase t̂ = (λy : b′.r′)^{b→c}. Using the invariant, we infer |b| < |b → c| ≤ |a|. Hence, we can again apply the induction hypothesis to infer that [û^{b}/y]r′ terminates, thus, by definition, also [s^{a}/x](t u). Soundness holds by the induction hypotheses, since (λy:b′.r′) û =_{β} [û/y]r′. □

3.2. Full Normalization

We define a function [[t]] which β-normalizes term t, provided it is well-typed. Even if it is not well-typed, the normalizer terminates and returns a term which is β-equal to the input.

[[x]]  = x
[[λx:a.r]] = λx:a. [[r]]
[[r s]]  = [[[s]]^{a}/x]t if[[r]] = λx:a.t
[[r]] [[s]]  otherwise

Lemma 3 (Termination and soundness) [[t]] =_{β} t for all t.

Proof. By induction on t, using termination and soundness of hereditary substitution. □

Example 4 (Behavior of normalizer)

[[(λx:o → o.λy:b. x y) (λz:a.z)]] = λy:b.y

Hereditarily substituting (λz:a.z) at function type o → o for x into x y triggers another substitution of y for z in z. However, if variable x is annotated with base type o only, this second substitution is not invoked and we get a non-normal result:

[[(λx:o.λy:b. x y) (λz:a.z)]] = λy:b. (λz:a.z) y

Evaluation of terms that are diverging under β-reduction also stops, e.g.,

[[(λx:o. x x) (λx:o. x x)]] = (λx:o. x x) (λx:o. x x).

3.3. Completeness of the Normalizer

In the following we show that the normalizer actually computes normal forms for well-typed terms.

Typed normal forms. We introduce a judgement Γ ⊢ t ⇓ a which expresses that t is a β-normal form of type a in context Γ.

\frac{(x:a) ∈ Γ}{Γ ⊢ x ⇓ a}  \frac{Γ ⊢ n ⇓ a → b  Γ ⊢ s ⇓ a}{Γ ⊢ n s ⇓ b}  \frac{Γ, x:a ⊢ r ⇓ b}{Γ ⊢ λx:a.r ⇓ a → b}

Note that in the second rule, the head n of the application n s is a neutral term, in particular, not an abstraction.

Lemma 5 (Completeness of hereditary substitution) Let Γ ⊢ s ⇓ a and Γ, x: a ⊢ t ⇓ c. Then exists an r with the following properties: If t is neutral then either [s^{a}/x]t = r^{c}, or r is also neutral and [s^{a}/x]t = r. Otherwise, if t is not neutral, [s^{a}/x]t = r. In all cases, Γ ⊢ r ⇓ c.

Proof. By lexicographic induction on (|a|, t). We consider the interesting case t = n u:

\frac{Γ, x:a ⊢ n ⇓ b → c Γ, x:a ⊢ u ⇓ b}{Γ, x:a ⊢ n u ⇓ c}

Let û = [s^{a}/x]u. If [s^{a}/x]n = r and r is neutral, then Γ ⊢ r û : c follows easily by induction hypothesis. Otherwise, [s^{a}/x]n = r^{b→c}. If r is neutral then we conclude as before, otherwise r = λy:b.r′. By the invariant, |b| < |b → c| ≤ a, and we can apply the induction hypothesis to infer Γ ⊢ [û^{b}/y]r′ ⇓ c, which is by definition equivalent to Γ ⊢ [s^{a}/x](n u) ⇓ c. □

Theorem 6 (Completeness of the normalizer) If Γ ⊢ t : a then Γ ⊢ [[t]] ⇓ a.

Proof. By induction on t, using the previous lemma in case of a β-redex. □

4. ADAPTATION TO SIMULTANEOUS SUBSTITUTIONS

Our aim is to implement the normalizer of the last section for a representation of terms using de Bruijn indices. Following Altenkirch and Reus [8] and Bird and Paterson [13], untyped λ-terms over the set of free variables A can be implemented by a nested datatype Tm A with the three constructors:

var : ∀A. A → Tm A
abs : ∀A. Tm (1 + A) → Tm A
app : ∀A. Tm A → Tm A → Tm A

The second constructor, abs, expects a term with one more free variable (1 + A) and binds this variable such that the result will only have free variables in A.

In this representation of de Bruijn terms, which statically ensures well-scoping, substitution [s/x]t for a single variable x is not directly implementable. Instead, one has to define the simultaneous substitution tρ for all free variables in t: If t has type Tm A and ρ has type A → Tm B, the result tρ of the substitution has type Tm B.^{4}

Hereditary simultaneous substitution. A valuation ρ is a function from variables to results r̂. Let the update ρ[x ↦ r̂] of valuation ρ in x by result r̂ be defined as usual:

\begin{aligned}ρ[x ↦ r̂](x) & = & r̂ \\ ρ[x ↦ r̂](y) & = & ρ(y) & ifx ≠ y \end{aligned}

The singleton valuation which maps x to r̂ and all other variables to themselves shall be denoted by (x ↦ r̂). A single substitution [s/x]t can be implemented using the simultaneous substitution t(x ↦ s) with a singleton valuation.

The hereditary simultaneous substitution t!ρ returns a result r̂ and is defined by the following equations:

x!ρ = ρ(x)
(λy:b.r)!ρ = λy:b. (r!ρ[y ↦ y]) where y fresh for any ρ(x) withx ∈ FV(r) \ {y}
(t u)!ρ = (r′!(y ↦ û^{b}))^{c}  if t̂= (λy:b′.r′)^{b→c}
t̂û  otherwise
where t̂ = t!ρ
û = u!ρ

4The type constructor Tm forms a Kleisli triple with unit var and simultaneous substitution as the bind-operation [8].

A closer look reveals that we use only three operations on valuations: lookup, ρ(x), lifting, ρ[y ↦ y] for y fresh, and creation of a singleton valuation, (y ↦ û^{b}). In particular, if t!ρ is invoked with a singleton valuation ρ, all recursive calls will also just involve a singleton valuation. We could therefore restrict ourselves to singleton valuations. However, for termination, a weaker requirement is sufficient:

In the following we consider only valuations ρ where ρ(x) = r^{a} for only finitely many variables x. For such valuations,

|ρ| := max{|a| | ρ(x) = r^{a}}

is a well-defined measure, |ρ| ∈ ℕ. Trivially, |(y ↦ s^{a})| = |a| for a singleton valuation.

Hereditary simultaneous substitutions always terminate, and the respective proof for hereditary singleton substitutions can be adopted:

Lemma 7 (Invariant) If t!ρ = r^{c}, then |c| ≤ |ρ|.

Proof. By induction on t. □

Lemma 8 (Termination and soundness of hereditary simultaneous substitutions) For all terms r and valuations ρ such that |ρ| exists, we have r!ρ =_{β} rρ.

Proof. By lexicographic induction on (|ρ|, r). In case r = t u and t̂ = t!ρ = (λy:b′.r′)^{b→c}, use the invariant to establish |(y ↦ û^{b})| = |b| < |b → c| ≤ |ρ| and apply the induction hypothesis. □

By setting [s^{a}/x]t := t!(x ↦ s^{a}) we can reuse the code for the normalization function [[r]] from the last section.

5. IMPLEMENTATION USING SIZED HETEROGENEOUS TYPES

In this section, we implement hereditary substitutions in F_{ω}. As a result, we will get a normalizer whose termination is certified by the type system of F_{ω}.

Simple types over a single base type o can be defined as follows in F_{ω}:

Ty : ord →^{+} ∗_{Ty := λı. μ_{∗}^{ı}λX. 1 + X × X} o : ∀ı. Ty^{ı+1}

o := inl ⟨⟩
arr : ∀ı. Ty^{ı} → Ty^{ı} → Ty^{ı+1}
arr := λaλb. inr ⟨a, b⟩

The size index ı in Ty^{ı} implements a measure on simple types. The requirements |b| < |arr b c| and |c| ≤ |arr b x| hold since b, c : Ty^{ı} implies arr b c : Ty^{ı+1}. But note that the only kind of measure that can be captured by the type system of F_{ω} is the structural one.

We can express the sized type constructor Tm for de Bruijn terms by a least fixed point of kind

∗ →^{+} ∗.

Tm : ord →^{+} ∗ →^{+} ∗
Tm := λı. μ^{ı}_{∗→^{+}∗}λXλA. A + (X A × X A + Ty^{∞} × X (1 + A))
var : ∀ı∀A. A → Tm^{ı+1} A
var := λx. inl x
app : ∀ı∀A. Tm^{ı} A → Tm^{ı} A → Tm^{ı+1} A
app := λrλs. inr (inl ⟨r, s⟩)
abs : ∀ı∀A. Ty^{∞} → Tm^{ı} (1 + A) → Tm^{ı+1} A
abs := λaλr. inr (inr ⟨a, r⟩)

Note that the first argument to abs is the object-level type of the abstraction: abs a r represents λx:a. r.

A whole article [6] has been devoted to functions defined by iteration over heterogeneous data types such as Tm. F_{ω} can simulate all the systems discussed in that article, hence, all examples in that article can be replayed in F_{ω}. Even more, in F_{ω}, some functions can be given more precise typings, e. g., the functoriality/monotonicity witness of Tm:

map : ∀ı∀A∀B. (A → B) → Tm^{ı}A → Tm^{ı}B
map := λfλr. map′ r f
map′ : ∀ı∀A. Tm^{ı}A → ∀B. (A → B) → Tm^{ı}B
map′ := fix λmap′λtλf. match t with
var x ↦ var (f x)
app r s ↦ app (map′ r f) (map′ s f)
abs a r ↦ abs a (map′ r (lift f))
lift : ∀A∀B. (A → B) → (1 + A → 1 + B)
lift := λfλt. match t with
inl ⟨⟩ ↦ inl ⟨⟩
inr x ↦ inr (f x)

Note our use of pattern matching over t distinguishing the defined constructors var, app, and abs. Assuming the patterns resulting from expanding the constructors are non-overlapping, mutually exclusive, and complete, this can be mechanically translated into case expressions. For the sake of readability, we prefer pattern matching as syntactic sugar.

The call map f t renames all free variables in t according to f; the structure of t remains unchanged, which is partially reflected in the type of map: it expresses that the output term is not higher than the input term.

The type of recursion in map′ is polymorphic:

C(ı) := ∀A. Tm^{ı}A → ∀B. (A → B) → Tm^{ı}B.

This is typical for functions over heterogeneous data types; in our example, since in the recursive call map r (lift f) the argument r has type Tm^{ı} (1 + A), the variable A of the recursion type C(ı) has to be instantiated to 1 + A.

The result of a hereditary substitution of a normal term into a neutral term is either a neutral term r or a normal term r plus (its) type a, which we have written as r^{a}. We encode these alternatives in the type Res^{ı} A, where ı is an upper bound on the size of the type a and A is the set of free variables that might occur in the result term r. We define two constructors: ne_{Res} r for the first alternative, and nf_{Res} r a for the second alternative.

Res : ord →^{+} ∗ →^{+} ∗
Res := λıλA. Tm^{∞} A × (1 + Ty^{ı})
ne_{Res} : ∀ı. Tm^{∞} A → Res^{ı} A
ne_{Res} := λr. ⟨r, inl ⟨⟩⟩
nf_{Res} : ∀ı. Tm^{∞} A → Ty^{ı} → Res^{ı} A
nf_{Res} := λrλa. ⟨r, inr a⟩

The destructor tm just extracts the term component. The function weak_{Res} lifts the free variables in a result term by one.

tm  : ∀ı∀A. Res^{ı}A → Tm^{∞} A
tm  := λ⟨r, a⟩. r
weak_{Res} : ∀ı∀A. Res^{ı} A → Res^{ı} (1 + A)
weak_{Res} := λ⟨r, a⟩. ⟨map inr r, a⟩

Finally, we can mimic all term constructors on Res. They should all discard the type component, if present. This is why the size index ı on the result of these operations is arbitrarily small:

var_{Res} : ∀ı∀A. A → Res^{ı} A
var_{Res} := λa. ne_{Res} (var a)
abs_{Res} : ∀ı∀A. Ty^{∞} → Res^{∞}(1 + A) → Res^{ı}A
abs_{Res} := λaλr. ne_{Res} (abs a (tm r))
app_{Res} : ∀A. Res^{∞} A → Res^{∞} A → Res^{ı} A
app_{Res} := λtλu. ne_{Res} (app (tm t) (tm u))

We represent valuations ρ which map all variables in A to a result with variables in B by the sized type Val^{ı} A B. The size index ı is an upper bound for |ρ|.

Val : ord →^{+} ∗ →^{−} ∗ →^{+} ∗
Val := λıλAλB. A → Res^{ı}B
sg_{Val} : ∀ı∀A. Tm^{∞}A → Ty^{ı} → Val^{ı} (1 + A) A
sg_{Val} := λsλaλmy. match my with
inl ⟨⟩ ↦ nf_{Res} s a
inr y ↦ var_{Res} y
lift_{Val} : ∀ı∀A∀B. Val^{ı} A B → Val^{ı} (1 + A) (1 + B)
lift_{Val} := λρλmx. match mx with
inl ⟨⟩ ↦ var_{Res} (inl ⟨⟩)
inr x ↦ weak_{Res} (ρ x)

The expression sg_{Val} s a : Val^{ı} (1 + A) A corresponds to the singleton valuation (x ↦ s^{a}); it generates a valuation which maps the variable x in 1 to nf_{Res} s a and the variables y in A to ne_{Res} (var y). The extension ρ[y ↦ y] of a valuation ρ is implemented by lift_{Val} ρ.

For implementing hereditary substitutions, we have to take into account the limitations of recursion in F_{ω}. Lexicographic recursion on type and term, Ty^{ı} × Tm^{ȷ} A, needs to be split up into an outer recursion on Ty^{ı} and an inner recursion on Tm^{ȷ}.

Thus, we define hereditary substitution [s^{a}/x]r by a function subst a s r recursive in a. This outer function calls an inner function simsubst r (sg_{Val} a s) recursive in r, which performs hereditary simultaneous substitutions in r, starting with the singleton valuation (x ↦ s^{a}). In one case, the inner function calls the outer function, albeit with a smaller type b. That b is in fact smaller than a is tracked by the type system.

subst : ∀ı. Ty^{ı} → ∀A. Tm^{∞} A → Tm^{∞}(1 + A) → Tm^{∞} A
subst := fix λsubstλaλsλt. tm (simsubst t (sg_{Val} s a))

where

simsubst : ∀ȷ. ∀A∀B. Tm^{ȷ}A → Val^{ı+1} A B → Res^{ı+1}B
simsubst := fix λsimsubstλtλρ. match t with
var x ↦ ρ x
abs b r ↦ abs_{Res} b (simsubst r (lift_{Val} ρ))
app t u ↦ let t̂ = simsubst t ρ û = simsubst u ρ
in match t̂with
nf_{Res} (abs b′ r′) (arr b c) ↦ nf_{Res} (subst b (tm û) r′) c
_↦ app_{Res} t̂û

The outer function is defined by induction on size ı; we have the following important types of bound variables:

subst : Ty^{ı} → ∀A. Tm^{∞} A → Tm^{∞}(1 + A) → Tm^{∞} A
a  : Ty^{ı+1}

This explains why in the type of the inner function, we have used size index ı + 1 to Val and Res. The inner function is defined by induction on ȷ. It is important that lift_{Val} does not touch the size argument to Val. Also, abs_{Res} and app_{Res} can return results Res with any size argument, thus, ı + 1 is fine. In the application ρ x, the size index on Val is returned as the size of Res. Finally, when we match t̂: Res^{ı+1} B as the result of a recursive call to simsubst, the expression arr b c has sized type Ty^{ı+1}, hence, b : Ty^{ı}, and the recursive call to subst is legal. Since c : Ty^{ı} ≤ Ty^{ı+1} by subtyping, the result nf_{Res} (…) c is well-typed.

The evaluator [[−]] can now be implemented straightforwardly. Its termination is guaranteed by sized types!

6. RELATED WORK

Type-based termination and sized types. Mendler [23] first devised a typing rule for general recursive programs that would single out the ones that are iterative—like fold for lists. Mendler’s system was extended by Giménez [16] and Barthe et al. [10, 11] to account for course-of-value recursion—covering functions like quicksort. I have explored how the type of a recursive function may depend on the size index [1]—now functions like breadth-first traversal are recognized as terminating by the type system. In my thesis [5], I cover also heterogeneous types like this article’s Tm. Blanqui [14, 15] extended type-based termination to dependent types and rewriting.

Independently of these “type-theoretic” developments, Hughes, Pareto, and Sabry [17, 24] have explored sized types for preventing crashes of functional programs. They arrived at a similar rule for type-based terminating recursion.

De Bruijn representation by a heterogeneous type. Since the 1960s it is known that simultaneous substitution can be viewed as the bind operation of a suitable monad [19, VI.4] [20]. For terms with binders, the idea was taken up by Bird and Paterson [13] as a case study for heterogeneous (nested, resp.) types in Haskell. Altenkirch and Reus [8] implement simultaneous substitutions for de Bruijn terms in a more type-theoretic setting; they carry out the renaming— performed in substitution under a binder—also by an invocation of substitution. Thus, termination of substitution becomes more complicated; they justify it by a lexicographic argument. McBride [21] stratifies this situation by exhibiting a common scheme which substitution and renaming as special instances. This scheme is again structurally recursive. McBride considers the object language of simply-typed terms in a dependently typed meta language; this way, he even establishes that substitution and renaming are type-preserving.

Adams [7] has carried out metatheory of pure type systems using de Bruijn representations as a heterogeneous type. He found that he had to pass from small-step statements, which speak about a single variable, e.g., a single substitution, to big-step statements, that take all variables into account at the same time, like simultaneous substitution. We can only confirm his findings.

Arithmetic normalization proofs and functions. Joachimski and Matthes [18] present strong and weak normalization proofs of the simply-typed λ-calculus using a lexicographic induction on types and derivations, similar to the one we have given in Section 3. They hand-extract a general recursive normalization algorithm which may diverge on ill-typed input. Berghofer [12] implemented the weak normalization proof in Isabelle and automatically extracted a normalizer, being much more complicated and keeping some intermediate data structures. I have implemented a similar proof in Twelf [3]. The termination checker of Twelf is capable to certify termination of the normalization proof, if viewed as a recursive function.

Watkins et al. [25] define hereditary substitutions for terms of the logical framework LF, and its extensions to linearity and concurrency. These substitutions are terminating by a lexicographic induction on type and term—as in this article. Hereditary substitutions enable us to specify a framework which only treats canonical forms (β-normal η-long objects), thus, simplifying its metatheory considerably.

7. CONCLUSION

We have presented F_{ω}, a pure polymorphic programming language with sized heterogeneous inductive types and type-based termination. As a non-trivial example, we have implemented a normalizer for simply-typed λ-terms in F_{ω}. The termination of the normalizer is statically ensured in F_{ω}. Additionally, the normalizer is well-scoped, by virtue of an implementation of λ-terms using a heterogeneous type.

One could go further and aim for a normalizer for statically well-typed λ-terms, “well-typed” referring here to typing in the object language of simple types. McBride has done a first step and implemented type-preserving renaming and substitution for the object language using a dependently-typed meta language [21]. Pursuing this approach, one could modify the normalizer such that it does not any more explicitly manipulate object-level types but considers only objectlevel terms. The object-level types would be visible only in the meta-level typing of the normalizer. The normalizer, viewed purely operationally, would have the possibility to diverge on ill-typed terms, but the static well-typedness condition would guarantee its termination for all actual inputs.

Acknowledgments. Thanks to the anonymous referees for their careful reading and their helpful and encouraging comments.

REFERENCES

[1] Andreas Abel. Termination and guardedness checking with continuous types. In M. Hofmann, editor, Typed Lambda Calculi and Applications (TLCA 2003), Valencia, Spain, volume 2701 of Lecture Notes in Computer Science, pages 1–15. Springer-Verlag, June 2003.

[2] Andreas Abel. Termination checking with types. RAIRO – Theoretical Informatics and Applications, 38(4):277–319, 2004. Special Issue: Fixed Points in Computer Science (FICS’03).

[3] Andreas Abel. Weak normalization for the simply-typed lambda-calculus in Twelf. In Logical Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland, 2004.

[4] Andreas Abel. Polarized subtyping for sized types. In D. Grigoriev, J. Harrison, and E. A. Hirsch, editors, Computer Science Symposium in Russia (CSR 2006), St. Petersburg, June 8-12, 2006, volume 3967 of Lecture Notes in Computer Science, pages 381–392. Springer-Verlag, 2006.

[5] Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006. Draft available under

http://www.tcs.ifi.lmu.de/˜ abel/diss.pdf.

[6] Andreas Abel, Ralph Matthes, and Tarmo Uustalu. Iteration schemes for higher-order and nested datatypes. Theoretical Computer Science, 333(1–2):3–66, 2005.

[7] Robin Adams. Formalized metatheory with terms represented by an indexed family of types. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, volume 3839 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 2006.

[8] Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL ’99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453–468. Springer-Verlag, 1999.

[9] Roberto M. Amadio and Solange Coupet-Grimal. Analysis of a guard condition in type theory. In Maurice Nivat, editor, Foundations of Software Science and Computation Structures, First International Conference, FoSSaCS’98, volume 1378 of Lecture Notes in

Computer Science, pages 48–62. Springer-Verlag, 1998.

[10] 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):1–45, 2004.

[11] Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. Practical inference for typebased termination in a polymorphic setting. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan, volume 3461 of Lecture Notes in Computer Science, pages 71–85. Springer-Verlag, 2005.

[12] Stefan Berghofer. Extracting a normalization algorithm in Isabelle/HOL. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, volume 3839 of Lecture Notes in Computer Science, pages 50–65. Springer-Verlag, 2006.

[13] Richard S. Bird and Ross Paterson. De Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77–91, 1999.

[14] Frédéric Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 – 5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 24–39. Springer-Verlag, 2004.

[15] Frédéric Blanqui. Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 135–150. Springer-Verlag, 2005.

[16] Eduardo Giménez. Structural recursive definitions in type theory. In K. G. Larsen, S. Skyum, and G. Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 397–408. Springer-Verlag, 1998.

[17] John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In 23rd Symposium on Principles of Programming Languages, POPL’96, pages 410–423, 1996.

[18] Felix Joachimski and Ralph Matthes. Short proofs of normalization. Archive of Mathematical Logic, 42(1):59–87, 2003.

[19] Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[20] E. Manes. Algebraic Theories. Springer-Verlag, 1976.

[21] Conor McBride. Type-preserving renaming and substitution. Journal of Functional Programming, 2006. Functional Pearl. To appear.

[22] Nax P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30–36. IEEE Computer Society Press, 1987.

[23] Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1–2):159–172, 1991.

[24] Lars Pareto. Types for Crash Prevention. PhD thesis, Chalmers University of Technology, 2000.

[25] Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.