Type-Based Termination of Generic Programs

Andreas Abel

Institut für Informatik Ludwig-Maximilians-Universität München Oettingenstr. 67, D-80538 München, GERMANY

Abstract

Instances of a polytypic or generic program for a concrete recursive type often exhibit a recursion scheme that is derived from the recursion scheme of the instantiation type. In practice, the programs obtained from a generic program are usually terminating, but the proof of termination cannot be carried out with traditional methods as term orderings alone, since termination often crucially relies on the program type. In this article, it is demonstrated that type-based termination using sized types handles such programs very well. A framework for sized polytypic programming is developed which ensures (typebased) termination of all instances.

1 Introduction

In the last decade, polytypic or generic programming has been explored for functional programming languages [26,19,22,23]. With polytypic programming, repetitive tasks, like writing a size-function for data structures of type A, can be mechanized by writing a generic size-function which then can be instantiated to all sorts of types A. Over the years, many useful examples of generic programs have been put forth, like parsing and unparsing, map and zip functions, and even finite maps for key type A. When generic programs are defined by recursion on type A, then the resulting programs often exhibit a recursion structure that corresponds to the recursion structure of type A; and it is the rule that they terminate, if applied to finite input. However, because of the high degree of abstraction that generic programs usually involve, termination cannot be proven with conventional methods like term orderings alone. It is the purpose of this article to outline a systematic solution to the termination problem of many generic programs.

  Email address: abel@informatik.uni-muenchen.de (Andreas Abel).

Preprint submitted to Elsevier 26 September 2007

As an example, we take Hinze’s [18] generic definition of finite maps. If instantiated to key type list of A, in Haskell syntax [a], we get the following definition of a finite map:

data MapList f v = Leaf
                   | Node (Maybe v) (f (MapList f v))

Herein, v is the range of the finite map, and f w represents the finite maps from a to w. Instantiating a with Char and f w with Char→w, we would get finite maps over strings. Such a finite map is either totally undefined (Leaf) or a pair of maybe a piece of data associated with the current key (Maybe v) plus a finite map for each extension of the current key by one character (f (MapList f v)).

Merging finite maps is a completely generic operation. Again for the key type of lists, we get the following instance. Let

comb :: (v -> v -> v) -> Maybe v -> Maybe v -> Maybe v

be a conflict resolution function for up to two candidate values of a finite map at a certain key. Then the following Haskell program merges two finite maps over lists:

mergeList ::
  (forall w. (w -> w -> w) -> f w -> f w -> f w) ->
  (v -> v -> v) ->
  MapList f v -> MapList f v -> MapList f v
mergeList mergeF c Leaf t = t
mergeList mergeF c t Leaf = t
mergeList mergeF c (Node m1 t1) (Node m2 t2) =
  Node (comb c m1 m2) (mergeF (mergeList mergeF c) t1 t2)

This function has an extraordinary recursion behavior: As a recursive “call”, the whole function mergeList mergeF c is passed to one of its arguments, mergeF. It is not immediately obvious that mergeList is a total function. Indeed, if we disregard its type, we can create a non-terminating execution: Define

mf m t1 t2 = m (Node Nothing t1) (Node Nothing t2)

and run:

mergeList mf fst (Node Nothing t1) (Node Nothing t2)

However, mf does not have the right type, and the polymorphic nature of the argument mergeF is a critical ingredient for termination.

This example shows that term-based termination arguments do not suffice for generic programs. We need a method for establishing termination which takes the type of a program into account. Such a method is type-based termination, which has been developed by Hughes, Pareto, and Sabry [24], and independently by Giménez [16] who advanced the pioneering work of Mendler [27]. Since then, type-based termination has been considered by several authors [2,8,9,12].

In this work, we show that type-based termination can be successfully applied to generic programs. We build on previous work, System F_{ω} [1], which is an extension of type-based termination to higher-order data types. Our contribution is an adaptation of Hinze, Jeuring, and Löh’s generic programming framework [23] to sized types, including a condition on the type of a generic program which ensures that all its instances are admissible recursion types in F_{ω}.

We will briefly introduce the necessary concepts to the reader in Section 2 and then outline a framework for total generic programming in Sect. 3. In Sect. 4 we prove that all instances of generic programs are well-typed which entails termination. More related work and directions for future research are discussed in Sect. 5.

This article is an extension of my MPC’06 conference paper [3].

1.1 Preliminaries

We assume that the reader is familiar with the higher-order polymorphic lambdacalculus, System F^{ω} (see Pierce’s text book [34]), or the functional programming language Haskell. Additionally, some familiarity with generic programming would be helpful [22].

Generic programming takes a minimalistic view on data types: Each ground type can be constructed using the unit type 1, disjoint sum type A + B, product type A × B and recursion. The following terms manipulate these types:

() : 1
pair : ∀A∀B. A → B → A × B
fst : ∀A∀B. A × B → A
snd : ∀A∀B. A × B → B
inl : ∀A∀B. A → A + B
inr : ∀A∀B. B → A + B
case : ∀A∀B∀C. A + B → (A → C) → (B → C) → C

Pairs pair r s are written (r, s). We assume the usual reduction rules, for instance, fst (r, s) ⟶ r. Multi-step reduction is denoted by ⟶^{+}. Sometimes it is convenient to introduce abbreviations for derived data constructors. For instance:

Nat = 1 + Nat
zero = inl ()
succ = λn. inr n

To improve readability, we will freely make use of the pattern matching notation

match r with p_{1} ↦ t_{1} | ⋯ | p_{n} ↦ t_{n}

for patterns p_{i} generated from both elementary and derived data constructors. We use a non-recursive let p=r in t as abbreviation for match r with p ↦ t.

2 Sized Types in a Nutshell

We use sized types for type-based termination checking, as described by Hughes, Pareto, and Sabry [24,32] and Barthe, Frade, Giménez, Pinto, and Uustalu [8]. In comparison with the cited works, our system, F_{ω}, also features higher-order polymorphism and heterogeneous (nested) and higher-order data types. In this section, we quickly introduce the most important features of F_{ω} [1], a summary of the rules can be found in the appendix.

Monotone type constructors and polarized kinds. Inductive types are recursively defined types which can only be unfolded finitely many times. The classical example are lists which are given as the least fixed-point of the type constructor λX. 1 + A × X, where A is the type of list elements. If the type constructor underlying an inductive type is not covariant (monotone), non-terminating programs can be constructed without explicit recursion [27]. Therefore we restrict inductive types to fixed-points of covariant constructors. We write

∗ →^{+} ∗ or +∗ → ∗ for the kind of covariant,
∗ →^{−} ∗ or −∗ → ∗ for the kind of contravariant, and
∗ →^{∘} ∗ or ∘∗ → ∗ for the kind of mixed-variant

type constructors, the last meaning constructors which are neither co- nor contravariant, or the absence of variance information. For example, λX. X → 1 is contravariant, and λX. X → X is mixed-variant. The notion of variance is extended to arbitrary kinds, and p-variant function kinds are written as

pκ → κ′ or κ →^{p} κ′.

For instance, we have the following kindings for disjoint sum, product, function, and polymorphic type constructor:

+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification

We assume a signature Σ that contains the above type constructor constants together with their kinding, plus some base types 1, Char, Int … The signature Σ is viewed as a function, so Σ(C) returns the kind of the constructor constant C. A bit sloppily, we write C ∈ Σ if C is in the domain of this function, C ∈ dom(Σ). Also, we usually write ∀X:κ.A for ∀_{κ}λX.A, or ∀XA, if the kind κ is inferable.

Kinding judgement. A kinding context Δ is a finite map from constructor variables X to pairs pκ of a polarity p and a kind κ. Kinding Δ ⊢ F : κ of constructors is given inductively by the following rules:

\frac{C:κ ∈ Σ}{Δ ⊢ C : κ}  \frac{X:pκ ∈ Δ  p ∈ \{+, ∘\}}{Δ ⊢ X : κ}

\frac{Δ, X:pκ ⊢ F : κ′}{Δ ⊢ λXF : pκ → κ′}  \frac{Δ ⊢ F : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

The kinding judgement Δ ⊢ F : κ expresses that if Δ(X) = qκ′ then F is qvariant in X. In particular if q = + then F is monotone in X and if q = − then F is antitone in X. Since X is monotone in X, the judgement Δ ⊢ X : κ is valid if and only if Δ(X) is +κ or ∘κ; this justifies the variable rule. Special attention has to be paid to the application rule: the variance of the application H = F G depends not only on the variance of F and G in X, but also on the variance of the function F itself. The hypotheses of the rule are Δ ⊢ F : pκ → κ′ and p^{−1}Δ ⊢ G : κ. The operation p^{−1}Δ modifies the polarities of the free variables in G according to p. If p = +, then +^{−1}Δ = +Δ = Δ; this is because F G is monotone (antitone, resp.) in X if both F and G are. If p = −, then F G is monotone in X if F is monotone in X and G is antitone in X. This means that the polarities in the kinding context for G have to be reversed. We set (−^{−1}Δ)(X) = (−Δ)(X) = −(Δ(X)), where −+ = −, −− = +, and −∘ = ∘. Finally, if p = ∘ then F G is monotone (antitone, resp.) in X if F is monotone (antitone, resp.) in X and X does not appear in G. Hence ∘^{−1}Δ needs to erase all variables X : qκ′′ from Δ whose polarity q is + or −; only variables of mixed variance are kept. Thus (Δ^{−1})(X) = ∘κ if Δ(X) = ∘κ, otherwise (Δ^{−1})(X) is undefined.

Ordinary F^{ω} kinding Δ ⊢ F : κ is regained if all polarities in Δ and κ are ∘.

Further information on kinding can be found in the thesis of the author [1, Ch. 2].

Sized inductive types. We write inductive types as μ^{a}F, where F is a covariant constructor and a a constructor of special kind ord. This kind models the stage expressions of Barthe et al. [8], which are interpreted as ordinals, and has the following constructors:

s : ord →^{+} ord  successor of ordinal,
∞ : ord  infinity ordinal.

The infinity ordinal is the closure ordinal of all inductive types considered, i. e., an ordinal big enough such that the equation

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

holds for all type constructors which are allowed as basis for an inductive type. If F is first-order, i. e., does not mention function space, then the smallest infinite ordinal ω is sufficient. However, if we allow higher-order datatypes like the infinitely-branching μ^{∞}λX.1 + (Nat → X), higher ordinals are required.^{1}

In the following, we will only make use of ordinal constructors that are either ∞ or ı + n, where ı is a constructor variable of kind ord and n a natural number and a + n is a shorthand for prepending the constructor a with n successor constructors s.

Sized inductive types are explained by the equation μ^{a+1}F = F (μ^{a}F). Viewing inductive types as trees and F as the type of the node constructor, it becomes clear that the size index a is an upper bound on the height of trees in μ^{a}F. Hence, inductive types are covariant in the size index, and their instances stand in the subtyping relation

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

Some examples for sized inductive types are:

Nat : ord →^{+} ∗
Nat := λı. μ^{ı}λX. 1 + X
List : ord →^{+} ∗ →^{+} ∗
List := λıλA. μ^{ı}λX. 1 + A × X
Tree : ord →^{+} ∗ →^{−} ∗ →^{+} ∗
Tree := λıλBλA. μ^{ı}λX. 1 + A × (B → X)

1 More details can be found in the thesis of the author [1, Sect. 3.3.3].

Nat^{a} denotes the type of natural numbers < a, List^{a}A the type of lists of length < a, and Tree^{a}B A the type of B-branching A-labeled trees of height < a. For lists, we define the usual constructors:

nil := inl ()  : ∀ı∀A. List^{ı+1} A
cons := λaλas. inr (a, as) : ∀ı∀A. A → List^{ı} A → List^{ı+1}A.

Heterogeneous data types. Nothing prevents us from considering inductive types of higher kind, i. e., such μ^{a}F where F is not of kind ∗ →^{+} ∗, but, for instance, of kind (∗ →^{+} ∗) →^{+} (∗ →^{+} ∗). For such an F we get an inductive constructor, or a heterogeneous data type [6], in the literature often called nested type [4,11,18,31]. In general, the least-fixed point constructor μ_{κ} can be used on any F : κ →^{+} κ where κ must be a pure kind, i. e., must not mention special kind ord. Examples for heterogeneous types are:

PList : ord →^{+} ∗ →^{+} ∗
PList := λı. μ_{+∗→∗}^{ı}λXλA. A + X (A × A)
Bush : ord →^{+} ∗ →^{+} ∗
Bush := λı. μ_{+∗→∗}^{ı}λXλA. 1 + A × X (X A)

The type PList^{a} A implements lists with exactly 2^{n} elements of type A for some n < a. The second type, bushy lists, is an example of a truly nested type since X appears in an argument to X. It is well-defined since we can infer covariance of X (X A) in X from the assumption that X is covariant itself.^{2}

Example 1 (A powerlist) Let a_{0}, a_{1}, a_{2}, a_{3} : A and ı : ord. We can construct the powerlist PList^{ı+3} A containing these four elements as follows:

((a_{0}, a_{1}), (a_{2}, a_{3})) : ((A × A) × (A × A)) =: A^{4}
inl ((a_{0}, a_{1}), (a_{2}, a_{3})) : A^{4} + PList^{ı} (A^{4} × A^{4})
inl ((a_{0}, a_{1}), (a_{2}, a_{3})) : PList^{ı+1} A^{4}
inr (inl ((a_{0}, a_{1}), (a_{2}, a_{3}))) : A × A + PList^{ı+1} A^{4}
inr (inl ((a_{0}, a_{1}), (a_{2}, a_{3}))) : PList^{ı+2} (A × A)
inr (inr (inl ((a_{0}, a_{1}), (a_{2}, a_{3})))) : A + PList^{ı+2} (A × A)
inr (inr (inl ((a_{0}, a_{1}), (a_{2}, a_{3})))) : PList^{ı+3} A

Structural recursion. Since we are considering a terminating programming language, recursion cannot be available without restriction. In the following we give

2 The constructor underlying Bush fails a purely syntactical covariance test, like the test for strict positivity in Coq [25].

a typing rule for structurally recursive functions. Herein, we interpret structurally recursive in the context of sized types: A function is structurally recursive if the recursive instance is of smaller size than the calling instance. As typing rule, this definition reads:

\frac{Γ, ı:ord, f : A ı ⊢ t : A (ı + 1)}{Γ ⊢ fix^{μ}(λf.t) : ∀ı. A ı} A fix^{μ}-adm

Of course, the type A ı must mention the size variable ı in a sensible way; with the constant type A ı = Nat^{∞} → Nat^{∞} one immediately allows non-terminating functions. Barthe et al. [8,9] suggest types of the shape A ı = μ^{ı}F → C where ı does not occur in F and only positively in C. In this article, we want to consider recursive functions that simultaneously descend on several arguments, and also polymorphic recursion. Hence, we consider types of the shape

∀Y⃗^{0}. μ^{ı}F G⃗ → ∀Y⃗^{1}. B_{1} → ⋯ → ∀Y⃗^{m}. B_{m} → C,

where ı does not occur in F and G⃗, index ı occurs only positively in C, and each of the B_{i} is either contravariant in ı or of the shape μ^{ı}F′ G⃗′ with F′, G⃗′ ı-free. This condition is written A fix^{μ} -adm, or Γ ⊢ A fix^{μ} -adm if A has free variables whose types are recorded in Γ. More valid shapes for the type A ı are described by Hughes, Pareto, and Sabry [24], in Pareto’s thesis [32] and my thesis [1,2].

To obtain a strongly normalizing system, unrolling of fixed-points has to be restricted to the case

fix^{μ}s v ⟶ s (fix^{μ}s) v,

where v is a value (an injection, a pair, a λ-abstraction, an under-applied function symbol). For convenience, we define the fixed-point combinator fix_{n}^{μ} that takes n non-recursive arguments before the first recursive argument:

back_{n} := λgλt_{1} … λt_{n}λr. g r t_{1} … t_{n}
front_{n} := λgλrλt_{1} … λt_{n}. g t_{1} … t_{n} r
fix_{n}^{μ}[s] := back_{n} (fix^{μ} (λf. front_{n} (s (back_{n} f)))).
fix_{n}^{μ} := λs. fix_{n}^{μ}[s]

Lemma 2 (Reduction of defined fixed-points) If |t⃗| = n, then

fix_{n}^{μ}[s] t⃗v ⟶^{+} s (fix_{n}^{μ}[s]) t⃗v.

Proof. Easy. Observe, however, that fix_{n}^{μ} s t⃗v −̸→^{+} s (fix_{n}^{μ} s) t⃗v (would require one β-expansion step). □

Lemma 3 If Γ ⊢ s : (∀X⃗^{1}. A_{1} → ⋯ → ∀X⃗^{n}. A_{n} → ∀X⃗. B → C) → (∀Y⃗^{1}. A′_{1} → ⋯ → ∀Y⃗^{n}. A′_{n} → ∀Y⃗ . B′ → C′) then Γ ⊢ λf. front_{n} (s (back_{n} f)) : (∀X⃗^{1} … X⃗^{n}X⃗. B → A⃗ → C) → (∀Y⃗^{1} … Y⃗^{n}Y⃗ . B′ → A⃗′ → C′).

The admissibility condition is generalized to functions that have n non-recursive arguments before the recursive ones: We write Γ ⊢ A fix_{n}^{μ}-adm if A ı is of the shape

∀X⃗^{1}. A_{1} → ⋯ → ∀X⃗^{n}. A_{n} → ∀Y⃗^{0}. μ^{ı}F G⃗ → ∀Y⃗^{1}. B_{1} → ⋯ → ∀Y⃗^{m}. B_{m} → C,

where the ı may occur only negatively in the A_{j}, and for the other type expressions the same conditions hold as in the definition of A fix^{μ}-adm.

Lemma 4 (Typing of defined fixed-points) Let Γ ⊢ A fix_{n}^{μ}-adm. If Γ ⊢ s : ∀ı. A ı → A (ı + 1), then Γ ⊢ fix_{n}^{μ}[s] : ∀ı. A ı. Hence,

Γ ⊢ fix_{n}^{μ} : (∀ı. A ı → A (ı + 1)) → ∀ı. A ı.

Example 5 (Merge sort) Assume a type A with a comparison function ≤: A → A → Bool, a function merge : List^{∞}A → List^{∞}A → List^{∞}A which merges two ordered lists into an ordered output list and a function split : ∀ı. List^{ı}A → List^{ı}A × List^{ı}A which splits a list into two parts of roughly the same size. The type of split expresses that none of the output lists is bigger than the input. We can encode merge sort msort a as for non-empty lists cons a as in F_{ω} as follows:

msort : ∀ı. A → List^{ı}A → List^{∞}A
msort := fix_{1}^{μ} λmsortλaλxs. match xs with
nil  ↦ cons a nil
cons b l ↦ let (as, bs) = split l

in merge (msort a as) (msort b bs)

The recursive calls to msort are legal because of the typing of split. Indeed, we can assign the following types:

msort : A → List^{ı} A → List^{∞} A
a, b : A
xs  : List^{ı+1} A
l  : List^{ı} A
as, bs : List^{ı} A

The termination of msort depends on the fact that split is non size-increasing. This information could have been established by other means than typing, e. g., by a term ordering as usual for termination of term rewriting systems. However, for the instances of generic programs we consider in the next section, the typing will be essential for termination checking.

3 A Framework for Generic Programming with Sized Types

Hinze [19] describes a framework for generic programming which is later extended by Hinze, Jeuring, and Löh [23] and implemented in Generic Haskell [22]. In this framework, both types and values can be constructed by recursion on some index type. The behavior is only specified for the type and constructor constants like Int, 1, + and ×, and this uniquely defines the constructed type or value. In the following we propose an extension by sized types, sized polytypic programming, and demonstrate its strength by giving termination guarantees for Hinze’s generalized tries [18].

In the sequel we will employ the following typographic conventions:

Capital  Type⟨A⟩ generic datatypes type-indexed types
UPPERCASE TYPE⟨κ⟩ their kinds  kind-indexed kinds
lowercase  poly⟨A⟩ generic functions type-indexed values
Capital  Poly⟨κ⟩ their types  kind-indexed types

The definition of the framework will be grayed, example generic programs will be lightly grayed.

3.1 Type-indexed Types

In generic programming as proposed by Hinze, Jeuring, and Löh [23], one can define a family Type⟨A⟩ indexed by another type A. For instance, one can define the type Map⟨A⟩V of finite maps from A to V generically for all index types A, by analyzing the structure of A. To this end, one specifies what Map⟨A⟩ should be for base types A_{0} and for the standard type constructors, e. g., + and ×. Then, Map⟨A⟩ is computed for a specific instance of A, where recursion is interpreted as the infinite unfolding. We differ from this setting in that we deal with inductive types instead of recursive types, thus, in our case, Map⟨A⟩ for an inductive type A will be itself an inductive type.

Roughly, a type-indexed type Type⟨A⟩ is A where constructor constants C have been replaced by user-defined constructors Type⟨C⟩. More precisely, we define Type⟨A⟩ by recursion on A, using the equations to follow. We generalize this definition to TypeX⃗⟨F ⟩, where F is a constructor and X⃗ are the variables under whose binders we have stepped in the course of the definition. So, in fact, we are dealing with constructor-indexed constructors, but we stick to the sloppy terminology used by datatype-generic programmers.

Type⟨A⟩ can be fully computed if A is closed; if A contains a free variable Y, then Type⟨A⟩ will have occurrences of the subexpression Type⟨Y ⟩ that can be further reduced if we substitute a (closed) type constructor for Y.

TypeX⃗⟨C⟩ = Type⟨C⟩ (user-defined) for C ∈ {1, +, ×, Int, Char, … }
TypeX⃗⟨X⟩ = X  if X ∈ X⃗
TypeX⃗⟨λXF ⟩ = λX. Type_{X⃗,X}⟨F ⟩
TypeX⃗⟨F G⟩ = TypeX⃗⟨F ⟩ TypeX⃗⟨G⟩
TypeX⃗⟨μ_{κ}⟩ = μ_{?}

What should the kind index to μ be in the last equation? We can answer this question if we look at the kind TYPE⟨κ⟩ of a type-indexed type Type⟨F ⟩. The kind TYPE⟨κ⟩ depends on the kind κ of constructor F. The given equations for abstraction and application dictate the law for function kinds.

TYPE⟨∗⟩  = κ, user-defined
TYPE⟨κ_{1} →^{p} κ_{2}⟩ = TYPE⟨κ_{1}⟩ →^{p} TYPE⟨κ_{2}⟩

The kind TYPE⟨∗⟩ has to be chosen such that for the basic type constructors C ∈ Σ the user-defined Type⟨C⟩ : TYPE⟨Σ(C)⟩. (Of course, Type⟨C⟩ can be undefined for some C, typically for C = → and C = ∀_{κ}.) For instance, the kind MAP⟨κ⟩ for the type of finite maps Map⟨F : κ⟩ is defined by MAP⟨∗⟩ = ∗ →^{+} ∗. We can now complete the construction law for types indexed by inductive types.

TypeX⃗⟨μ_{κ}⟩ = μ_{TYPE⟨κ⟩}

Remark 6 Note that the presence of polarities in TYPE⟨Σ(C)⟩ restricts the choices for Type⟨C⟩. For instance, Type⟨→⟩ = λAλB.A × B or Type⟨×⟩ = λAλB.A → B are both impossible (and meaningless). However, I do not know any practical, meaningful type-indexed types that are excluded by the polarity restriction.

We extend the framework to sized types by giving homomorphic construction rules for everything that concerns sizes:

TYPE⟨ord⟩ = ord
TypeX⃗⟨s⟩ = s
TypeX⃗⟨∞⟩ = ∞

Since except for constants, the defining clauses for type-indexed types are homomorphic, type-indexed types are compositional.

Lemma 7 (Substitution in type indices) TypeX⃗⟨[G/X]F ⟩ = [TypeX⃗⟨G⟩/X]Type_{X⃗,X}⟨F ⟩.

Proof. By induction on F. □

As a consequence, type-indexed types preserve equality. Kinding and subtyping are also preserved, since TYPE⟨κ⟩ preserves the polarities in κ.

Theorem 8 (Well-kindedness, equality, and subtyping for type-indexed types) Let Σ be a signature of constructor constants and assume Type⟨C⟩ : TYPE⟨κ⟩ for all (C:κ) ∈ Σ.

(1) If X_{1} : p_{1}κ_{1}, …, X_{n} : p_{n}κ_{n} ⊢ F : κ, then X_{1} : p_{1}TYPE⟨κ_{1}⟩, …, X_{n} : p_{n}TYPE⟨κ_{n}⟩ ⊢ TypeX⃗⟨F ⟩ : TYPE⟨κ⟩.

(2) If X_{1} : p_{1}κ_{1}, …, X_{n} : p_{n}κ_{n} ⊢ F = F′ : κ, then X_{1} : p_{1}TYPE⟨κ_{1}⟩, …, X_{n} : p_{n}TYPE⟨κ_{n}⟩ ⊢ TypeX⃗⟨F ⟩ = TypeX⃗⟨F′⟩ : TYPE⟨κ⟩.

(3) If X_{1} : p_{1}κ_{1}, …, X_{n} : p_{n}κ_{n} ⊢ F ≤ F′ : κ, then X_{1} : p_{1}TYPE⟨κ_{1}⟩, …, X_{n} : p_{n}TYPE⟨κ_{n}⟩ ⊢ TypeX⃗⟨F ⟩ ≤ TypeX⃗⟨F′⟩ : TYPE⟨κ⟩.

Proof. Each by induction on the derivation. The rules are given in the appendix. □

Example: finite maps via generalized tries. Hinze [18] defines generalized tries Map⟨F ⟩ by recursion on F. In particular, Map⟨K : ∗⟩ V is the type of finite maps from domain K to codomain V. The following representation using type-level λ can be found in his article on type-indexed data types [23, page 139].

MAP⟨∗⟩ := ∗ →^{+} ∗
Map⟨Int⟩ := λV. efficient implementation ofInt →_{fin} V
Map⟨Char⟩ := λV. efficient implementation ofChar →_{fin} V
Map⟨1⟩ := λV. 1 + V
Map⟨+⟩ := λF λGλV. 1 + F V × G V
Map⟨×⟩ := λF λGλV. F (G V)

Well-kindedness of these definitions is immediate, except maybe for Map⟨×⟩ which must be of kind (∗ →^{+} ∗) →^{+} (∗ →^{+} ∗) →^{+} (∗ →^{+} ∗). For Map⟨+⟩ we have used the variant of spotted products (or lifted products) which Hinze mentions in section 4.1 of his article [18]. This way we avoid that certain empty tries have an infinite normal form (see [18, page 341]) which requires lazy evaluation. The constructor for finite maps over strings can now be computed as follows:

Map⟨λı. List^{ı} Char⟩
= Map⟨λı. μ_{∗}^{ı} λX. 1 + Char × X⟩
= λı. μ^{ı}_{∗→^{+}∗} λX. Map⟨+⟩ Map⟨1⟩ (Map⟨×⟩ Map⟨Char⟩ X)
= λı. μ^{ı}_{∗→^{+}∗} λXλV. 1 + (1 + V) × Map⟨Char⟩ (X V)

The matching kind is

MAP⟨ord →^{+} ∗⟩ = ord →^{+} ∗ →^{+} ∗.

Note that the type Map⟨λı. List^{ı} Char⟩ of sized, string-indexed tries involves a higherkinded inductive type μ_{∗→^{+}∗}. However, it is not heterogeneous, but homogeneous, meaning that X is always applied to the variable V. Thus, we have the option to simplify it using λ-dropping and obtain an ordinary inductive type:

Map⟨λı. List^{ı} Char⟩ = λıλV. μ_{∗}^{ı} λY. 1 + (1 + V) × Map⟨Char⟩ Y

It is easy to interpret this type as a trie for strings with prefix p: The trie is either “()” (first 1), meaning that strings with this prefix are undefined in the finite map, or it is a pair of maybe a value v (the value mapped to p) and of one trie for strings with prefix p · c for each c ∈ Char. A trie for strings with empty prefix is then a finite map over all strings.

Remark 9 (λ-dropping) We use λ-dropping in some places in this article to simplify types or values computed by the generic programming framework. However, it has no official status and is not essential for our results.

3.2 Type-indexed Values

The key ingredient to generic programming are type-indexed values, meaning, programs poly⟨F ⟩ which work for different type constructors F but are uniformly (generically) constructed by recursion on F. Again, the user supplies the desired behavior poly⟨C⟩ on base types and type constructors C, and the polytypic program poly⟨F ⟩ is then constructed by the following laws.

poly⟨C⟩ = user-defined
poly⟨X⟩ = X
poly⟨λXF ⟩ = λX. poly⟨F ⟩
poly⟨F G⟩ = poly⟨F ⟩ poly⟨G⟩
poly⟨μ_{κ}⟩ = fix

The handling of variables is still sloppy in this definition; we assume that we can reuse type variables as special term variables. Here we just want to convey the idea, later we will make the variable handling water proof.

Hinze [20] has observed that type-indexed values poly⟨F : κ⟩ have kind-indexed types Poly⟨F, …, F : κ⟩ : ∗ with possibly several copies of the parameter F, obeying the following laws:

Poly⟨A_{1}, …, A_{n} : ∗⟩  = user-defined, parametric in A⃗
Poly⟨F_{1}, …, F_{n} : κ →^{p} κ′⟩ = ∀G_{1} :κ … ∀G_{n}:κ.

Poly⟨G_{1}, …, G_{n} : κ⟩ → Poly⟨F_{1} G_{1}, …, F_{n} G_{n} : κ′⟩

For example, three copies of F are required for a generic definition of zipping functions [20, Sect. 7.2].

Hinze works in a framework where only covariant type constructors serve as indices, i. e., p = + in the above equation. However, with polarity information at hand, it is sometimes useful to depart from Hinze’s scheme. One example is a generic map function (monotonicity witness, functoriality witness):

GMap⟨A, B : ∗⟩  := A → B
GMap⟨F, G : κ →^{−} κ′⟩ := ∀X∀Y. GMap⟨Y, X : κ⟩ → GMap⟨F X, G Y : κ′⟩
GMap⟨F, G : κ →^{p} κ′⟩ := ∀X∀Y. GMap⟨X, Y : κ⟩ → GMap⟨F X, G Y : κ′⟩
for p ∈ {+, ∘}

With this refined definition of kind-indexed type, a generic map function is definable which also works for data types with embedded function spaces, e. g., Tree.

gmap⟨1 : ∗⟩  := λu. u
gmap⟨+ : ∗ →^{+} ∗ →^{+} ∗⟩ := λfλgλs. case s (λx. inl (fx)) (λy. inr (g y))
gmap⟨× : ∗ →^{+} ∗ →^{+} ∗⟩ := λfλgλp. (f (fst p), g (snd p))
gmap⟨→ : ∗ →^{−} ∗ →^{+} ∗⟩ := λfλgλhλx. g (h (f x))

For the main example we want to consider, generic operations for tries, types Poly⟨F : κ⟩ indexed by a single constructor F are sufficient, hence, we will restrict the following development to this case. Formally, our framework contains rules to compute

Poly⟨κ⟩ : κ →^{∘} ∗

from the user-defined type constructor Poly⟨∗⟩ : ∗ →^{∘} ∗. The notation Poly⟨F : κ⟩ shall be a shorthand for the β-normal form of Poly⟨κ⟩ F (thus, removing administrative redexes). If the kind κ of F is clear from the context of discourse, we abbreviate Poly⟨F : κ⟩ by Poly⟨F ⟩. The computation rules for Poly⟨κ⟩ are the following:

Poly⟨∗⟩  = λXA : ∗ →^{∘} ∗, user-defined
Poly⟨ord⟩  = λ_1
Poly⟨κ_{1} →^{p} κ_{2}⟩ = λF ∀G:κ_{1}. Poly⟨κ_{1}⟩ G → Poly⟨κ_{2}⟩(F G)

The second line treats base kind ord which is new in F_{ω}. Since ordinals are only used to increase the static information about programs, they have no computational significance and can be mapped to inhabitants of the unit type.

Theorem 10 (Well-kindedness of kind-indexed types) If Γ ⊢ Poly⟨∗⟩ : ∗ →^{∘} ∗, then Γ ⊢ Poly⟨κ⟩ : κ →^{∘} ∗.

Proof. By induction on κ. □

The defined notion Poly⟨F : κ⟩ is trivially substitutive, meaning Γ ⊢ Poly⟨[G/X]F : κ⟩ = [G/X]Poly⟨F : κ⟩ : ∗ when Γ ⊢ G : κ′ and Γ, X: κ′ ⊢ F : κ. And likewise trivially, it respects equality: Γ ⊢ F = F′ : κ implies Γ ⊢ Poly⟨F : κ⟩ = Poly⟨F′ : κ⟩ : ∗.

We can refine the generation laws for type-indexed programs as follows. Formally, we define poly_{n,ϕ}⟨F ⟩ where n is a natural number and ϕ maps type variables to term variables.

poly⟨C⟩  = t : Poly⟨C⟩, user-defined
poly_{n,ϕ}⟨C⟩  = poly⟨C⟩
poly_{n,ϕ}⟨X⟩ = ϕ(X)
poly_{n,ϕ}⟨λXF ⟩ = λx. poly_{n,ϕ[X↦x]}⟨F ⟩, x fresh
poly_{n,ϕ}⟨F G⟩ = poly_{n,ϕ}⟨F ⟩ poly_{n,ϕ}⟨G⟩
poly_{n,ϕ}⟨μ_{p⃗κ⃗→∗}⟩ = λ_. fix_{n+|κ⃗|}^{μ}

In the last equation there is a void abstraction to take care of the argument of unit type which arises from the ordinal argument a of μ_{κ}^{a}. Also, n has to be chosen such that the nth argument to the resulting recursive function is of an inductive type whose size is associated to a. The choice of n depends on the definition of the type Poly⟨A:∗⟩ of the type-indexed program given by the user. For the example of map lookup functions (see below), the polytypic program is of type

Lookup⟨K:∗⟩ := ∀V. K → Map⟨K⟩ V → 1 + V.

Hence, we set n = 0, because the recursive argument of the function that is generated in case K = μ^{a}F is the first one, of type K. In the example of finite map merging to follow, we will have the type

Merge⟨K:∗⟩ := ∀V. Bin V → Bin (Map⟨K⟩ V)

with Bin V = V → V → V. Since Map⟨K⟩ is an inductive type for inductive K, the second argument is the recursive one and we have n = 1. The choice of n will be formally determined in the next section.

Example: generic finite map lookup. In the following, we implement Hinze’s generic lookup function in our framework. The definitions on the program level are unchanged, only the types are now sized, and we give termination guarantees. The lookup function is polymorphic in the value type V, it takes a key of type K and a finite map from K to V and returns maybe a value.

Lookup⟨K:∗⟩ := ∀V. K → Map⟨K⟩ V → 1 + V

In the definition of the generic lookup function, we use the bind operation ≫= for the Maybe monad λV. 1 + V. It obeys the laws (inl() ≫= f) ⟶ inl() and (inr v ≫= f) ⟶ f v.

lookup⟨1⟩ : ∀V. 1 → 1 + V → 1 + V
lookup⟨1⟩ := λkλm. m
lookup⟨+⟩ : ∀A:∗. Lookup⟨A⟩ → ∀B:∗. Lookup⟨B⟩ →
∀V. A + B → 1 + (Map⟨A⟩ V) × (Map⟨B⟩ V) → 1 + V
lookup⟨+⟩ := λlaλlbλabλtab. tab ≫= λ(ta, tb).
match ab with
inl a ↦ la a ta
inr b ↦ lb b tb
lookup⟨×⟩ : ∀A:∗. Lookup⟨A⟩ → ∀B:∗. Lookup⟨B⟩ →
∀V. A × B → Map⟨A⟩ (Map⟨B⟩ V) → 1 + V
lookup⟨×⟩ := λlaλlbλ(a, b)λtab. la a tab ≫= λtb. lb b tb

All these definitions are well-typed, which is easy to check since there are no references to sizes.

Example: lookup for list-shaped keys. The previous definitions determine the instance of the generic lookup function for the type constructor of lists.The kindindexed type unfolds to:

Lookup⟨List : ord →^{+} ∗ →^{+} ∗⟩
= ∀ı. 1 → ∀K. Lookup⟨K : ∗⟩ → Lookup⟨List^{ı} K : ∗⟩
= ∀ı. 1 → ∀K. Lookup⟨K : ∗⟩ → ∀V. List^{ı}K → Map⟨List^{ı}K⟩ → 1 + V
= ∀ı. 1 → ∀K. Lookup⟨K : ∗⟩ → ∀V. List^{ı}K →
(μ_{∗}^{ı}λY. 1 + (1 + V) × Y) → 1 + V

Note that the type Lookup⟨List⟩ mentions the size variable ı twice, as index to both inductive arguments. This makes sense, since the length of the search keys determines the depth of the trie. The lookup function is computed as follows:

lookup_{0}⟨List⟩ = lookup_{0}⟨λıλK. μ_{∗}^{ı}λX. 1 + K × X⟩
= λiλlookup_{K} . (λ_. fix_{0}^{μ}) i (λlookup. lookup⟨+⟩ lookup⟨1⟩

(lookup⟨×⟩ lookup_{K} lookup))

= λiλlookup_{K} . fix_{0}^{μ} λlookupλlλm. m ≫= λ(n, c).

match l with

nil  ↦ n
cons k l′ ↦ lookup_{K} k c ≫= λm′. lookup l′ m′

Well-typedness follows as the type Lookup⟨List^{ı}K⟩ is valid for recursion with fix_{0}^{μ}, according to criterion given in Sect. 2. We reason on an abstract level:

lookup_{K}  : Lookup⟨K⟩
lookup  : Lookup⟨List^{ı}K⟩
lookup⟨×⟩ lookup_{K} lookup =: r : Lookup⟨K × List^{ı}K⟩
lookup⟨+⟩ lookup⟨1⟩ r =: s : Lookup⟨1 + K × List^{ı}K⟩
: Lookup⟨List^{ı+1}K⟩
fix_{0}^{μ} λlookup. s  : Lookup⟨List^{ı}K⟩
lookup⟨List⟩  : Lookup⟨List⟩

Example: generic trie merging. Hinze [18] presents three elementary operations to construct finite tries: empty, single, and merge. In the following we replay the construction of merge in our framework, since it exhibits a very interesting recursion scheme.

We first define the type Bin V for binary operations on V and a function comb which lifts a merging function for V to a merging function for 1 + V:

Bin : ∗ →^{∘} ∗
Bin := λV. V → V → V
comb : ∀V. (V → V → V) → (1 + V → 1 + V → 1 + V)
comb := λcλm_{1}λm_{2}. match (m_{1}, m_{2}) with
(inl(), _)  ↦ m_{2}
(_, inl())  ↦ m_{1}
(inr v_{1}, inr v_{2}) ↦ inr (c v_{1} v_{2})

When merging two finite maps of type Map⟨K⟩ V, one has to resolve a conflict when both maps assign a value to the same key. This conflict resolution function c : Bin V is abstracted out, leading to the following kind-indexed type:

Merge⟨K:∗⟩ := ∀V. Bin V → Bin (Map⟨K⟩ V)

The following definitions determine a generic merging function for finite maps over key whose type is composed from 1, +, ×, and μ.

merge⟨1⟩ : Merge⟨1⟩
merge⟨1⟩ := comb
merge⟨+⟩ : ∀A. Merge⟨A⟩ → ∀B. Merge⟨B⟩ →
∀V. Bin V → Bin (1 + Map⟨A⟩ V × Map⟨B⟩ V)
merge⟨+⟩ := λmaλmbλc. comb
λ(ta_{1}, tb_{1})λ(ta_{2}, tb_{2}). (ma c ta_{1} ta_{2}, mb c tb_{1} tb_{2})
merge⟨×⟩ : ∀A. Merge⟨A⟩ → ∀B. Merge⟨B⟩ →
∀V. Bin V → Bin (Map⟨A⟩ (Map⟨B⟩ V))
merge⟨×⟩ := λmaλmbλc. ma (mb c)

In the last line, mb c : Bin (Map⟨B⟩ V) merges finite maps over key type B. This function serves as conflict resolver to merge finite maps from A to Map⟨B⟩ V, arriving at the elegant λc. ma (mb c) : Merge⟨A × B : ∗⟩.

Example: list-trie merging. The type of the merge function for finite maps over list-shaped keys is derived as follows:

Merge⟨List : ord →^{+} ∗ →^{+} ∗⟩ = ∀ı. 1 → ∀K. Merge⟨K⟩ → Merge⟨List^{ı}K⟩
= ∀ı. 1 → ∀K. (∀V. Bin V → Bin (Map⟨K⟩ V))

→ ∀W. Bin W → Bin (Map⟨List^{ı}K⟩ W)

Mechanically, we compute the merge function for list-tries:

merge_{1}⟨List⟩

= merge_{1}⟨λıλK. μ^{ı}λX. 1 + K × X⟩
= λiλmerge_{K} . (λ_fix_{1}^{μ}) i merge_{1}⟨λX. 1 + K × X⟩
= λiλmerge_{K} . fix_{1}^{μ}(λmerge. merge⟨+⟩ merge⟨1⟩ (merge⟨×⟩ merge_{K} merge))
= λiλmerge_{K} . fix_{1}^{μ} λmergeλc. comb
λ(mv_{1}, t_{1})λ(mv_{2}, t_{2}). (comb c mv_{1} mv_{2}, merge_{K} (merge c) t_{1}t_{2})
[= λiλmerge_{K} λc. fix_{0}^{μ} λmerge. comb
λ(mv_{1}, t_{1})λ(mv_{2}, t_{2}). (comb c mv_{1} mv_{2}, merge_{K} merge t_{1} t_{2})]

In the last step (enclosed in [brackets]), we have decreased the rank of recursion by λ-dropping.

Surprisingly, recursion happens not by invoking merge on structurally smaller arguments, but by passing the function itself to a parameter, merge_{K} . Here, type-based termination reveals its strength; it is not possible to show termination of merge⟨List⟩ disregarding its type. With sized types, however, the termination proof is again just a typing derivation, as easy as for lookup⟨List⟩. We reason again on the abstract level:

merge_{K}  : Merge⟨K⟩
merge  : Merge⟨List^{ı}K⟩
merge⟨×⟩ merge_{K} merge =: r : Merge⟨K × List^{ı}K⟩
merge⟨+⟩ merge⟨1⟩ r =: s : Merge⟨1 + K × List^{ı}K⟩
: Merge⟨List^{ı+1}K⟩
fix_{1}^{μ} λmerge. s  : Merge⟨List^{ı}K⟩

The type Merge⟨List^{ı}K⟩ is admissible for recursion on the second argument (the first argument is of type Bin V): The whole type is of shape ∀V. Bin V → μ^{ı}F → μ^{ı}F → μ^{ı}F for some F which does not depend on the size variable ı. Hence, the type has the required shape.

Example: merging bushy tries. An even more dazzling recursion pattern is exhibited by the merge function for “bushy” tries, i. e., finite maps over bushy lists.

Bush  : ord →^{+} ∗ →^{+} ∗
Bush  := λı. μ^{ı}_{∗→^{+}∗} λXλK. 1 + K × X (X K)
Map⟨Bush⟩ : ord →^{+} (∗ →^{+} ∗) →^{+} (∗ →^{+} ∗)
Map⟨Bush⟩ = λı. μ^{ı}_{(∗→^{+}∗)→^{+}(∗→^{+}∗)} λXλF λV. 1 + (1 + V) × F (X (X F) V)

The merge function for bush-indexed tries can be derived routinely:

merge_{1}⟨Bush⟩
= merge_{1}⟨λı. μ^{ı}_{∗→^{+}∗}λXλK. 1 + K × X (X K)⟩
= λi. (λ_fix_{2}^{μ}) i (λmergeλmerge_{K} .

merge⟨+⟩ merge⟨1⟩ (merge⟨×⟩ merge_{K} (merge (merge merge_{K} ))))

= λi. fix_{2}^{μ} λmergeλmerge_{K}

λc. comb λ(mv_{1}, t_{1})λ(mv_{2}, t_{2}).

(comb c mv_{1} mv_{2}, merge_{K} (merge (merge merge_{K} ) c) t_{1} t_{2})

The recursion pattern of merge⟨Bush⟩ is adventurous. Not only is the recursive instance merge passed to an argument to the function merge_{K} , but also this function is modified during recursion: it is replaced by (merge merge_{K} ), which involves the recursive instance again! All these complications are coolly handled by type-based termination!

We have now seen how termination of some specific programs, which happened to be instances of generic programs, can be established using types. In the next section we develop a criterion on generic programs which entails termination of all of their instances.

4 Termination of Generic Programs

In this section, we establish the soundness of the framework presented in the last section, i. e., we prove that all instances of generic programs are indeed terminating. It suffices to show that they are well-typed in F_{ω}, since this type system only accepts total programs. Critical is the typing of fixed-points

poly_{n,ϕ}⟨μ_{κ} : ord →^{+} (κ →^{+} κ) →^{+} κ⟩ = λ_. fix_{n+m}^{μ}, where κ = p⃗κ⃗ → ∗, m = |κ⃗|

or more perspicuously, poly_{n,ϕ}⟨μ_{κ}^{ı}⟩ = fix_{n+m}^{μ} : ∀F. Poly⟨F : κ →^{+} κ⟩ → Poly⟨μ^{ı} F ⟩. It is easily established that the step term s, the first argument to fix_{n+m}^{μ}, can be instantiated to the correct type.

Lemma 11 If Γ ⊢ s : Poly⟨F : κ →^{+} κ⟩ then Γ ⊢ s : Poly⟨μ^{ı}F ⟩ → Poly⟨μ^{ı+1}F ⟩.

Proof. We have Poly⟨F : κ →^{+} κ⟩ = ∀G:κ.Poly⟨G : κ⟩ → Poly⟨F G : κ⟩, hence, instantiating G to μ^{ı}F and using the equation F (μ^{ı}F) = μ^{ı+1}F, we get the typing Γ ⊢ s : Poly⟨μ^{ı}F ⟩ → Poly⟨μ^{ı+1}F ⟩. □

So poly_{n,ϕ}⟨F ⟩ is a candidate for a step term s of a recursive function fix_{n+m}^{μ} s. If we can ensure that λı. Poly⟨μ^{ı}F ⟩ is admissible for recursion, we have ensured termination of all generic programs in our framework. Let us recall admissible recursion types, this time in form of an inductive definition.

Lemma 12 (Inductive definition of fix_{n}^{μ} -adm) The following rules define fix_{n}^{μ} -adm inductively.

\frac{Γ, ı:+ord ⊢ A : ∗}{Γ ⊢ λı. A fix_{−∞}^{μ} -adm}  (1)

\frac{Γ, Y :∘κ ⊢ λı.A fix_{n}^{μ} -adm}{Γ ⊢ λı. ∀Y :κ. A fix_{n}^{μ} -adm}  (2)

\frac{Γ ⊢ F : (p⃗κ⃗ → ∗) →^{+} (p⃗κ⃗ → ∗)  p_{i}^{−1}Γ ⊢ G_{i} : κ_{i} (all i)  Γ ⊢ λı.A fix_{n}^{μ} -adm}{Γ ⊢ λı.μ^{ı}F G⃗ → A fix_{0}^{μ} -adm}

(3)

\frac{−Γ, ı:−ord ⊢ A_{0} : ∗  Γ ⊢ λı.A fix_{n}^{μ} -adm}{Γ ⊢ λı. A_{0} → A fix_{n+1}^{μ} -adm}  (4)

Each admissible function type Γ ⊢ λı.A fix_{n}^{μ} -adm with n ≥ 0 must end in a covariant codomain (1), which is preceded by at least one inductive domain (3) and by an arbitrary number of contravariant domains (4). Universal quantification can come in at any point (2). The first inductive domain counts as the recursive argument, and the number of domains preceding it make up n.

With the judgement Γ ⊢_{n}^{X} B to follow, we characterize such user-defined types Poly⟨∗⟩ of generic programs that give rise to admissible recursion types. More precisely, if ⋄ ⊢_{n}^{X} Poly⟨X : ∗⟩ and κ = p⃗κ⃗ → ∗ with m = |κ⃗|, then λı. Poly⟨μ_{κ}^{ı}F : κ⟩ fix_{n+m}^{μ} -adm (Lemma 16). Simultaneously, the judgement determines the n in the number n + m of non-recursive arguments in fix_{n+m}^{μ}.

Definition 13 (Admissible types of recursive generic programs) Let Γ be a kinding context, X a variable not assigned in Γ, n a natural number or −∞, and B a type. The judgement Γ ⊢_{n}^{X} B is inductively given by the following rules.

\frac{Γ, X:+∗ ⊢ B : ∗}{Γ ⊢_{−∞}^{X} B} p ≤ + (1)

\frac{Γ, Y :∘κ ⊢_{n}^{X} B}{Γ ⊢_{n}^{X} ∀Y :κ. B} (2)

\frac{p_{i}^{−1}Γ ⊢ H_{i} : κ_{i} (for all i = 1..|κ⃗|) Γ ⊢_{n}^{X} B}{Γ ⊢_{0}^{X} Type⟨X⟩ H⃗ → B} TYPE⟨∗⟩ = p⃗κ⃗ → ∗

\frac{Γ ⊢_{n}^{X} B}{Γ ⊢_{0}^{X} X → B} (3)

\frac{−Γ, X:−∗ ⊢ A : ∗  Γ ⊢_{n}^{X} B}{Γ ⊢_{n+1}^{X} A → B} p ≤ +  (4)

In Γ ⊢_{n}^{X} B, we assume that X ∉ Γ and maintain the invariant Γ, X:∘∗ ⊢ B : ∗. If n = −∞, then even Γ, X: +∗ ⊢ B : ∗. We use the subscript −∞ to indicate that an occurrence of X or Type⟨X⟩ has not yet been encountered, which means that there is no recursive argument yet. (Note that −∞ + 1 = −∞.)

The rules of ⊢_{n}^{X} correspond to the ones of fix_{n}^{μ} -adm and have been numbered accordingly. The placeholder X will be instantiated to an inductive type μ^{ı}F G⃗. Rule (1): Since B is monotone in X, its instantiation will be monotone in ı. Remember that admissible function types need at least one inductive domain (3). This can either come from X or from a type-indexed type Type⟨X⟩, since a type indexed by an inductive type is again an inductive type. Finally, leading non-recursive arguments must be in contravariant domains (4).

Example 14 The kind-indexed types of the last section satisfy this judgement.

⊢_{0}^{K} Lookup⟨K : ∗⟩ = ∀V. K → Map⟨K⟩ V → 1 + V
⊢_{1}^{K} Merge⟨K : ∗⟩ = ∀V. Bin V → Bin (Map⟨K⟩ V)

Lemma 15 (Soundness of Γ ⊢_{n}^{X} B) Let Γ ⊢ F : κ →^{+} κ for κ = p⃗κ⃗ → ∗ and p_{j}^{−1}Γ ⊢ G_{j} : κ_{j} for 1 ≤ j ≤ |κ⃗|. Let ı ∉ dom(Γ) and A = λı.[μ^{ı}F G⃗/X]B. If Γ ⊢_{n}^{X} B then Γ ⊢ A fix_{n}^{μ} -adm.

Proof. By induction on Γ ⊢_{n}^{X} B.

• Case (1)

\frac{Γ, X:+∗ ⊢ B : ∗}{Γ ⊢_{−∞}^{X} B} p ≤ +

Since λı. μ^{ı}F G⃗ : ord →^{+} ∗ and X appears only positively in B, we have Γ ⊢ A :

ord →^{+} ∗.

• Case (3)

\frac{Γ ⊢_{n}^{X} B}{Γ ⊢_{0}^{X} X → B}

By induction hypothesis, Γ ⊢ A fix_{n}^{μ} -adm. Thus, Γ ⊢ λı. μ^{ı}F G⃗ → A ı fix_{0}^{μ} -adm.

• Case (3)

\frac{p_{i}^{−1}Γ ⊢ H_{i} : κ_{i} (for all i = 1..|κ⃗|) Γ ⊢_{n}^{X} B}{Γ ⊢_{0}^{X} Type⟨X⟩H⃗ → B} TYPE⟨∗⟩ = p⃗κ⃗ → ∗

Let A := [μ^{ı}F G⃗/X]B. By induction hypothesis, Γ ⊢ λı. A fix_{n}^{μ} -adm. Since X not free in H⃗, we have [μ^{ı}F G⃗/X](Type⟨X⟩H⃗ → B) = Type⟨μ^{ı}F G⃗⟩ H⃗ → A. By definition of type-indexed types Type⟨μ^{ı}F G⃗⟩ = μ^{ı}F′ G⃗′ for some ı-free F′, G⃗′, hence, Γ ⊢ λı. μ^{ı}F′ G⃗′ H⃗ → A fix_{0}^{μ} -adm.

The remaining two cases for Γ ⊢_{n}^{X} B follow by induction hypothesis and the matching rule for fix_{n}^{μ} -adm. □

The previous lemma implies that if ⊢_{n}^{X} Poly⟨X : ∗⟩ then Poly⟨μ_{∗}^{ı}F : ∗⟩ fix_{n}^{μ} -adm. The next lemma extends this result to higher kinds, such that we can treat programs indexed by nested data types.

Lemma 16 Let κ = p_{1}κ_{1} → ⋯ → p_{m}κ_{m} → ∗. If ⊢_{n}^{X} Poly⟨X : ∗⟩ for some n ≥ 0 and Γ ⊢ F : κ →^{+} κ then Γ ⊢ Poly⟨μ_{κ}^{ı}F : κ⟩ fix_{m+n}^{μ} -adm.

Proof. From the previous lemma, by induction on m. □

Now we are able to show that all instances poly_{n,ϕ}⟨F ⟩ of a generic program are well-typed, hence, terminating, if their type Poly⟨F ⟩ is of suitable shape.

Theorem 17 (Termination of generic programs) Let Γ ⊢ poly⟨C⟩ : Poly⟨C : κ⟩ for all constants (C : κ) ∈ Σ and ⊢_{n}^{X} Poly⟨X : ∗⟩ for some n ≥ 0. Let Δ := (X_{i} : p_{i}κ_{i})_{i=1..l} and Δ′ := (X_{i} : p_{i}κ_{i}, x_{i} : Poly⟨X_{i} : κ_{i}⟩)_{i=1..l}. If Δ ⊢ F : κ and ϕ(X_{i}) = x_{i} for i = 1..l, then Γ, Δ′ ⊢ poly_{n,ϕ}⟨F ⟩ : Poly⟨F : κ⟩.

Proof. By induction on Δ ⊢ F : κ. The interesting case is Δ ⊢ μ_{κ} : ord →^{+} (κ →^{+}

κ) →^{+} κ with κ = p′_{1}κ′_{1} → … p′_{m}κ′_{m} → ∗.

poly_{n,ϕ}⟨μ_{κ}⟩ = λ_. fix_{m+n}^{μ} = λ_λs. fix_{m+n}^{μ}[s]
Poly⟨μ_{κ}⟩ = ∀ı. 1 → ∀F. Poly⟨F : κ →^{+} κ⟩ → Poly⟨μ_{κ}^{ı}F ⟩

Let A := λı. Poly⟨μ_{κ}^{ı}F ⟩. By Lemma 16, Δ ⊢ A fix_{m+n}^{μ}-adm. By Lemma 11, Δ, ı : ∘ord, _: 1, F : ∘(κ →^{+} κ), s : Poly⟨F ⟩ ⊢ s : A ı → A (ı + 1), hence, Δ, _: 1, F : ∘(κ →^{+} κ), s : Poly⟨F ⟩ ⊢ s : ∀ı. A ı → A (ı + 1). By Lemma 4, Δ, ı: ∘ord, _: 1, F : ∘(κ →^{+} κ), s: Poly⟨F ⟩ ⊢ fix_{m+n}^{μ}[s] : A ı. Thus, by abstraction, generalization, and weakening, we conclude Γ, Δ′ ⊢ poly_{n,ϕ}⟨μ_{κ}⟩ : Poly⟨μ_{κ}⟩. □

5 Conclusions and Related Work

We have seen a polymorphic λ-calculus with sized higher-order data types, F_{ω}, in which all programs are terminating. This calculus is strong enough to certify termination of arbitrary instances of generic programs, provided the generic programs themselves do not use unrestricted recursion. A systematic method to certify termination using the framework of sized polytypic programming has been presented. The approach of type-based termination we have seen can handle convoluted recursion patterns that go far beyond schemes of iteration and primitive recursion stemming from the initial algebra semantics of data types. The recursion patterns of many examples for generic programming [21,22] can be treated in F_{ω}, and I am still looking for sensible examples that exceed the capabilities of F_{ω}. It seems promising to pursue this approach further.

In this article, we have not addressed the problem of type-checking sized types. However, some solutions exist in the literature: Pareto [32], Barthe, Grégoire, and Pastawski [9], and Blanqui [12] have given constraint-based inference algorithms for sized types.

System F_{ω} is strongly normalizing [1], as is its non-polymorphic predecessor λ [8]. More suitable for functional programming seems an interpretation of types as sets of closed values or finite observations—this, however, is future work. Hughes, Pareto, and Sabry [24] have presented a similar calculus, with ML-polymorphism, and given it a domain-theoretic semantics. What is not so pretty in this approach is that one constructs the semantics using undefinedness (⊥), but then later shows that each well-typed program is totally defined. One wonders why one has to speak about ⊥ in the first place.

Related Work on Termination. The research on size-change termination (SCT), which is led by Neil Jones, has received much attention. Recently, Sereni and Jones have extended this method to higher-order functions [36]. Is SCT able to check termination of the generic programs presented in this work? No, because SCT analyses only the untyped program, and without typing information termination of, e. g., mergeList cannot be established, as explained in the introduction (mergeList diverges on ill-typed arguments). Neither can the methods developed for higherorder term rewriting systems, as for instance bundled in the tool AProve [15], be applied to the generic program, since they disregard typing. (I conducted my experiments in Fall 2005.)

Related Work on Generic Programming. We have considered generic programming in the style of Generic Haskell which has been formulated by Hinze, Jeuring, and Löh [19–23]. Another philosophy of generic programming is rooted in the initial algebra semantics for data types (see the introductory text by Backhouse, Jansson, Jeuring, and Meertens [7]). Jansson and Jeuring [26] present PolyP, a polytypic extension for Haskell which gives more control in defining polytypic functions, for instance, “recursion” is a type constructor one can treat in a clause of the polytypic program, whereas in Generic Haskell and our extension to sized types, recursion on types is always mapped to a recursive program.

Pfeifer and Rueß [33] study polytypic definitions in dependent type theory where all expressions are required to terminate. Termination is achieved by limiting recursion to the elimination combinators for inductive types, which correspond to the scheme of primitive recursion or paramorphisms. This excludes many interesting generic programs we can treat, like merging of tries, that do not fit into this scheme. Benke, Dybjer, and Jansson [10] extend the approach of Pfeifer and Rueß to generic definitions over inductive families. They also restrict recursion to iteration and primitive recursion. Altenkirch and McBride [5] pursue a similar direction; they show that generic programming is dependently typed programming with tailored type universes. They construct a generic fold for members of the universe of Haskell types, which allows to define generic iterative functions (catamorphisms).

Norell and Jansson [29] exploit the type class mechanism to enable polytypic programming in Haskell without language extensions. They also present an approach to generic programming using template Haskell [30]. Finally, Norell [28] describes an encoding of generic programs in dependent type theory. None of these works considers the problem of termination of the generated programs.

Generic programming within an intermediate language of a typed compiler has been studied under the names intensional polymorphism and intensional type analysis by Harper and Morrisett [17] and Crary, Weirich, and Morrisett [14]. The gist of this approach is to have a type case construct on the level of programs, in later developments even also on the level of types. This way, certain compiler optimizations such as untagging and unboxing can be performed in a type-safe way. Crary and Weirich [13] even enrich the kind language by inductive kinds and the constructor language by primitive recursion. Saha, Trifonov, and Shao [35] consider intensional analysis of polymorphism. To this end, they introduce polymorphic kinds. For our purposes, this would be counterproductive since a language with two impredicative universes on top of each other is non-normalizing (Girard’s paradox).

Acknowledgments. The idea to apply type-based termination to generic programming was born in discussions with Ralph Matthes. Thanks to the anonymous referees for helpful comments which helped to improve the presentation.

Research 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).

A System F_{ω}

This section gives a short overview over system F_{ω} and lists typing, subtyping, and kinding rules. In comparison to the author’s thesis [1], the version of F_{ω} presented here has no coinductive types, but only inductive types.

A.1 Kinds and Constructors

Polarities. To track the monotonicity of type constructors, we introduce polarities p, which range over the three values + (covariant), − (contravariant), and ∘ (mixedvariant). They are partially ordered; the order is given by ∘ ≤ p and p ≤ p.

Kinds κ are the “types” of type constructors. In F_{ω}, size expressions belong to the type language and have kind ord.

κ ::= ∗  types
| ord  ordinals
| pκ_{1} → κ_{2}  co-/contra-/mixed-variant constructor transformers

Notation: κ →^{p} κ′ for pκ → κ′. Pure kinds κ_{∗} are kinds that do not mention ord.

Constructors are λ-terms over some constants C.

a, b, A, B, F, G ::= C | X | λXF | F G

The constructor constants C are taken from a fixed signature Σ_{0} which contains at least the following constants together with their kinding.

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

We sometimes write the size index superscript, e. g., μ^{ı} instead of μ ı.

Polarized contexts. A kinding context usually records the kinds of the free variables of a type constructor; a polarized context additionally records variance information for each variable to distinguish whether this free variable occurs only positively (p = +), only negatively (p = −), or arbitrarily (p = ∘) in the type constructor under consideration.

Δ ::= ⋄ | Δ, X:pκ

Negation of a polarity −p is given by the three equations −(+) = −, −(−) = + and −(∘) = ∘. We define inverse application p^{−1}Δ of a polarity p to a polarized context Δ.

\begin{aligned}+^{−1}Δ & = & Δ \\ −^{−1}(⋄) & = & ⋄ \\ −^{−1}(Δ, X:pκ) & = & −^{−1}Δ, X:(−p)κ \end{aligned}  \begin{aligned}∘^{−1}(⋄) & = & ⋄ \\ ∘^{−1}(Δ, X:∘κ) & = & ∘^{−1}Δ, X:∘κ \\ ∘^{−1}(Δ, X:+κ) & = & ∘^{−1}Δ \\ ∘^{−1}(Δ, X:−κ) & = & ∘^{−1}Δ \end{aligned}

Inverse application is used in the kinding judgement.

Kinding. Δ ⊢ F : κ

\frac{C:κ ∈ Σ_{0}}{Δ ⊢ C : κ}  \frac{X:pκ ∈ Δ  p ≤ +}{Δ ⊢ X : κ}

\frac{Δ, X:pκ ⊢ F : κ′}{Δ ⊢ λXF : pκ → κ′}  \frac{Δ ⊢ F : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

Constructor equality. Constructors are identified modulo β and η. Furthermore, there are two axioms for sizes and inductive types.

Computation axioms.

\frac{Δ, X:pκ ⊢ F : κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ (λXF) G = [G/X]F : κ′}  \frac{Δ ⊢ F : pκ → κ′}{Δ ⊢ (λX. F X) = F : pκ → κ′}

\overline{Δ ⊢ s ∞ = ∞ : ord}  \frac{Δ ⊢ a : ord}{Δ ⊢ μ_{κ}^{s a} = λF. F (μ_{κ}^{a} F) : (κ →^{+} κ) →^{+} κ}

Congruences.

\frac{X:pκ ∈ Δ  p ≤ +}{Δ ⊢ X = X : κ}  \frac{Δ, X:pκ ⊢ F = F′ : κ′}{Δ ⊢ λXF = λXF′ : pκ → κ′}

\frac{C:κ ∈ Σ_{0}}{Δ ⊢ C = C : κ}  \frac{Δ ⊢ F = F′ : pκ → κ′  p^{−1}Δ ⊢ G = G′ : κ}{Δ ⊢ F G = F′ G′ : κ′}

Symmetry and transitivity.

\frac{Δ ⊢ F = F′ : κ}{Δ ⊢ F′ = F : κ}  \frac{Δ ⊢ F_{1} = F_{2} : κ  Δ ⊢ F_{2} = F_{3} : κ}{Δ ⊢ F_{1} = F_{3} : κ}

Higher-Order Subtyping. Subtyping captures the natural inclusion order μ^{a}F ≤ μ^{s a}F between sized inductive types.

Reflexivity, transitivity, antisymmetry.

\frac{Δ ⊢ F = F′ : κ}{Δ ⊢ F ≤ F′ : κ}  \frac{Δ ⊢ F_{1} ≤ F_{2} : κ  Δ ⊢ F_{2} ≤ F_{3} : κ}{Δ ⊢ F_{1} ≤ F_{3} : κ}

\frac{Δ ⊢ F ≤ F′ : κ Δ ⊢ F′ ≤ F : κ}{Δ ⊢ F = F′ : κ}

Abstraction and application.

\frac{Δ, X:pκ ⊢ F ≤ F′ : κ′}{Δ ⊢ λXF ≤ λXF′ : pκ → κ′}  \frac{Δ ⊢ F ≤ F′ : pκ → κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G ≤ F′ G : κ′}

\frac{Δ ⊢ F : +κ → κ′ Δ ⊢ G ≤ G′ : κ}{Δ ⊢ F G ≤ F G′ : κ′} \frac{Δ ⊢ F : −κ → κ′ −Δ ⊢ G′ ≤ G : κ}{Δ ⊢ F G ≤ F G′ : κ′}

Successor and infinity.

\frac{Δ ⊢ a : ord}{Δ ⊢ a ≤ s a : ord}  \frac{Δ ⊢ a : ord}{Δ ⊢ a ≤ ∞ : ord}

A.2 Terms and Typing

Terms.

Tm ∋ r, s, t ::= c | x | λxt | r s | fix^{μ}
Const ∋ c  ::= () | pair | fst | snd | inl | inr | case

The signature Σ_{0} contains the types for the constants in Const.

Typing contexts.

Γ ::= ⋄ | Γ, x:A | Γ, X:pκ

Wellformed contexts.

\overline{⋄ cxt} \frac{Γ cxt}{Γ, X:∘κ cxt} \frac{Γ cxt  Γ ⊢ A : ∗}{Γ, x:A cxt}

Typing. Γ ⊢ t : A Lambda-calculus.

\frac{(x:A) ∈ Γ  Γ cxt}{Γ ⊢ x : A}  \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : A → B}  \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B}

Quantification.

\frac{Γ, X:∘κ ⊢ t : F X}{Γ ⊢ t : ∀_{κ}F} X ∉ FV(F)  \frac{Γ ⊢ t : ∀_{κ} F  Γ ⊢ G : κ}{Γ ⊢ t : F G}

Subsumption.

\frac{Γ ⊢ t : A Γ ⊢ A ≤ B : ∗}{Γ ⊢ t : B}

Recursion and further constants.

\frac{Γ ⊢ A fix^{μ}-adm  Γ ⊢ a : ord}{Γ ⊢ fix^{μ} : (∀ı:ord. A ı → A (ı + 1)) → A a}  \frac{(c:A) ∈ Σ_{0}}{Γ ⊢ c : A}

Γ ⊢ A fix^{μ}-adm means that Γ ⊢ A = λı. ∀X⃗^{0}.μ^{ı}F G⃗ → ∀X⃗^{1}.B_{1} ⋯ → ∀X⃗^{m}.B_{m} → C : ord →^{∘} ∗ where the ı does not occur in F and G⃗ and only positively in C. Each B_{j} either is of the form μ^{ı}F′ G⃗′ where ı does not occur in F′, G⃗′ or ı occurs only negatively in B_{j}.

A.3 Values and Reduction

Values are weak-head normal forms.

v ::= λxt | pair t_{1} t_{2} | inl t | inr t  proper values
| fix^{μ} | fix^{μ} s | pair | pair t | inl | inr | fst | snd | case under-applied functions

Reduction. The one-step reduction relation t ⟶ t′ is the closure of the following axioms under all term constructors.

(λxt) s ⟶ [s/x]t
fix_{n}^{μ} s v ⟶ s (fix_{n}^{μ} s) v
fst (r, s) ⟶ r
snd (r, s) ⟶ s
case (inl r) ⟶ λxλy. x r
case (inr r) ⟶ λxλy. y r

Well-typed terms are strongly normalizing under this reduction.

References

[1] A. Abel, A polymorphic lambda-calculus with sized higher-order types, Ph.D. thesis, Ludwig-Maximilians-Universität München (2006).

[2] A. Abel, Semi-continuous sized types and termination, in: Z. Ésik (ed.), Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 21-24, 2006, Proceedings, vol. 4207 of Lecture Notes in Computer Science, Springer-Verlag, 2006.

[3] A. Abel, Towards generic programming with sized types, in: T. Uustalu (ed.), Mathematics of Program Construction: 8th International Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006. Proceedings, vol. 4014 of Lecture Notes in Computer Science, Springer-Verlag, 2006.

[4] A. Abel, R. Matthes, T. Uustalu, Iteration schemes for higher-order and nested datatypes, Theoretical Computer Science 333 (1–2) (2005) 3–66.

[5] T. Altenkirch, C. McBride, Generic programming within dependently typed programming., in: J. Gibbons, J. Jeuring (eds.), Generic Programming, IFIP TC2/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl, Germany, vol. 243 of IFIP Conference Proceedings, Kluwer, 2003.

[6] T. Altenkirch, B. Reus, Monadic presentations of lambda terms using generalized inductive types, in: J. Flum, M. Rodríguez-Artalejo (eds.), Computer Science Logic, 13th International Workshop, CSL ’99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, vol. 1683 of Lecture Notes in Computer Science, Springer-Verlag, 1999.

[7] R. Backhouse, P. Jansson, J. Jeuring, L. Meertens, Generic programming — an introduction, in: S. D. Swierstra, P. R. Henriques, J. N. Oliveira (eds.), Revised Lectures from the Third International School on Advanced Functional Programming, AFP ’98, vol. 1608 of Lecture Notes in Computer Science, Springer-Verlag, 1999.

[8] G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science 14 (1) (2004) 1– 45.

[9] G. Barthe, B. Grégoire, F. Pastawski, Practical inference for type-based termination in a polymorphic setting, in: P. Urzyczyn (ed.), Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan, vol. 3461 of Lecture Notes in Computer Science, Springer-Verlag, 2005.

[10] M. Benke, P. Dybjer, P. Jansson, Universes for generic programs and proofs in dependent type theory, Nordic Journal of Computing 10 (4) (2003) 265–289.

[11] R. Bird, L. Meertens, Nested datatypes, in: J. Jeuring (ed.), Mathematics of Program Construction, MPC’98, Proceedings, vol. 1422 of Lecture Notes in Computer Science, Springer-Verlag, 1998.

[12] F. Blanqui, Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations., in: C.-H. L. Ong (ed.), Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, vol. 3634 of Lecture Notes in Computer Science, Springer-Verlag, 2005.

[13] K. Crary, S. Weirich, Flexible type analysis, in: Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, vol. 34 of SIGPLAN Notices, ACM Press, 1999.

[14] K. Crary, S. Weirich, J. G. Morrisett, Intensional polymorphism in type-erasure semantics, in: Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998, vol. 34 of SIGPLAN Notices, ACM Press, 1999.

[15] J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke, Automated termination proofs with AProVE, in: V. van Oostrom (ed.), Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 – 5, 2004, Proceedings, vol. 3091 of Lecture Notes in Computer Science, Springer-Verlag, 2004.

[16] E. Giménez, Structural recursive definitions in type theory, in: K. G. Larsen, S. Skyum, G. Winskel (eds.), Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, vol. 1443 of Lecture Notes in Computer Science, Springer-Verlag, 1998.

[17] R. Harper, J. G. Morrisett, Compiling polymorphism using intensional type analysis, in: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’95, San Francisco, California, January 23-25, 1995, ACM Press, 1995.

[18] R. Hinze, Generalizing generalized tries, Journal of Functional Programming 10 (4) (2000) 327–351.

[19] R. Hinze, A new approach to generic functional programming, in: Proceedings of the 27th ACM SIGPLAN-SIGACT on Principles of Programming Languages, POPL 2000, Boston, Massachusetts, USA, January 19-21, 2000, ACM Press, 2000.

[20] R. Hinze, Polytypic values possess polykinded types, MPC Special Issue, Sci. Comput. Programming 43 (2002) 129–159.

[21] R. Hinze, J. Jeuring, Generic Haskell: Applications, in: R. C. Backhouse, J. Gibbons (eds.), Generic Programming - Advanced Lectures, vol. 2793 of Lecture Notes in Computer Science, Springer-Verlag, 2003.

[22] R. Hinze, J. Jeuring, Generic Haskell: Practice and Theory, in: R. C. Backhouse, J. Gibbons (eds.), Generic Programming - Advanced Lectures, vol. 2793 of Lecture Notes in Computer Science, Springer-Verlag, 2003.

[23] R. Hinze, J. Jeuring, A. Löh, Type-indexed data types, MPC Special Issue, Sci. Comput. Programming 51 (2004) 117–151.

[24] J. Hughes, L. Pareto, A. Sabry, Proving the correctness of reactive systems using sized types, in: 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’96, 1996.

[25] INRIA, The Coq Proof Assistant, Version 8.1, http://coq.inria.fr/ (2007).

[26] P. Jansson, J. Jeuring, PolyP—a polytypic programming extension, in: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’97, Paris, France, ACM Press, 1997.

[27] N. 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., IEEE Computer Society Press, 1987.

[28] U. Norell, Functional generic programming and type theory, Master’s thesis, Computing Science, Chalmers University of Technology, available

from http://www.cs.chalmers.se/~ulfn (2002).

[29] U. Norell, P. Jansson, Polytypic programming in Haskell, in: P. W. Trinder, G. Michaelson, R. Pena (eds.), Implementation of Functional Languages (IFL’03), Lecture Notes in Computer Science, 2004.

[30] U. Norell, P. Jansson, Prototyping generic programming in Template Haskell, in: D. Kozen, C. Shankland (eds.), Proceedings of the Seventh International Conference on Mathematics of Program Construction, MPC ’04, vol. 3125 of Lecture Notes in Computer Science, Springer-Verlag, 2004.

[31] C. Okasaki, From fast exponentiation to square matrices: An adventure in types, in: Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, 1999.

[32] L. Pareto, Types for crash prevention, Ph.D. thesis, Chalmers University of Technology (2000).

[33] H. Pfeifer, H. Rueß, Polytypic proof construction, in: Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, , L. Théry (eds.), Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99, Nice, France, vol. 1690 of Lecture Notes in Computer Science, Springer-Verlag, 1999.

[34] B. C. Pierce, Types and Programming Languages, MIT Press, 2002.

[35] B. Saha, V. Trifonov, Z. Shao, Intensional analysis of quantified types, ACM Transactions on Programming Languages and Systems 25 (2) (2003) 159–209.

[36] D. Sereni, N. D. Jones, Termination analysis of higher-order functional programs, in: K. Yi (ed.), Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, vol. 3780 of Lecture Notes in Computer Science, Springer-Verlag, 2005.