Fixed Points of Type Constructors and Primitive Recursion

Andreas Abel^{⋆}^{1} and Ralph Matthes^{2}

1 Department of Computer Science, Chalmers University of Technology

                           abel@cs.chalmers.se

2 Department of Computer Science, University of Munich

                    matthes@informatik.uni-muenchen.de

Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive nonstrictly positive type constructors of arbitrary finite kinds, where fixedpoint unfolding is computationally invisible due to its treatment on the level of type equality. Positivity is ensured by a polarized kinding system, and strong normalization is proven by a model construction based on saturated sets. The second solution is a formulation of primitive recursion for arbitrary type constructors of any rank. Although without positivity restriction, the second system embeds—even operationally—into the first one.

1 Introduction

Recently, higher-rank datatypes have drawn interest in the functional programming community [Oka96,Hin01]. Rank-2 non-regular types, so-called nested datatypes, have been investigated in the context of the functional programming language Haskell. To define total functions which traverse nested datastructures, Bird et al. [BP99a] have developed generalized folds which implement an iteration scheme and are strong enough to encode most of the known algorithms for nested datatypes. In this work, we investigate schemes to overcome some limitations of iteration which we expound in the following.

Since the work of Böhm et al. [BB85] it is well-known that iteration for rank-1 datatypes can be simulated in typed lambda calculi. The easiest examples are iterative definitions of addition and multiplication for Church numerals. The iterative definition of the predecessor, however, is inefficient: It traverses the whole numeral in order to remove one constructor. Surely, taking the predecessor should run in constant time.

Primitive recursion is the combination of iteration and efficient predecessor. A typical example for a primitive recursive algorithm is the natural definition

⋆ The first author gratefully acknowledges the support by both the PhD Programme Logic in Computer Science (GKLI) of the Deutsche Forschungs-Gemeinschaft and the CoVer project by the Stiftelsen för Strategisk Forskning (SSF).

of the factorial function. It is common belief that primitive recursion cannot be reduced to iteration in a computationally faithful manner. This is because no encoding of natural numbers in the polymorphic lambda-calculus (System F) seems possible which supports a constant-time predecessor operation (see Spławski and Urzyczyn [SU99]).

In this article, we present two approaches to overcome the predecessor dilemma for higher-rank datatypes. A first solution, presented in Section 2, is System Fix^{ω} of non-strictly positive equi-recursive type constructors, which handles folding and unfolding for fixed points on the level of types, trivially yielding an efficient predecessor. Fix^{ω} is proven strongly normalizing in Section 3. Even though the system has no native means of recursion, a powerful scheme of primitive recursion is definable in Fix^{ω}. This schema is embodied in our formulation of a second system MRec^{ω}, given in Section 4. In Section 4.2 we give an extensive example of a function which can most naturally be implemented with primitive recursion—redecoration for triangular matrices. Finally, we give the details of the definition of MRec^{ω} within Fix^{ω}, hence establishing strong normalization of the primitive recursion scheme as well (Section 5).

2 System Fix^{ω}

Since Mendler [Men87], it is known that type equations of the form X = A with X a type variable and A a type expression, can only be added to system F in case X only occurs positively in A. Otherwise, strong normalization of typable terms is lost. In this section, we show that the positive part of Mendler’s finding, namely strong normalization in the case where X only occurs positively in A, can be extended to equations for type constructors of arbitrary finite kind, hence within the framework F^{ω} of higher-order parametric polymorphism.

Equations in solved form, i. e., with a constructor variable on the left-hand side, can equivalently be treated by an explicit type constructor for fixed-points [Urz96]. In the case of fixed-points of types, the purported solution of X = C would be written as the type fix X.C, with its characteristic equation being fix X.C = [fix X.C/X]C. In the case of nested datatypes, we are interested in equations like X A = A+X(A×A), where X now denotes a type transformation. This would be solved by PList = fix X.λA. A + X(A × A). PList A stands for powerlists over A, i. e., lists with 2^{n} elements of type A, for some (unspecified) n, which can clearly be seen to be the least fixed-point of the above equation. With function kinds at hand, we can pass from fix X.C to fix F with F := λX.C, which is a type transformer.

A manifest idea to isolate positive constructors systematically is to distinguish covariant (monotone), contravariant (antitone) and invariant (no information about monotonicity) constructors through the kinding system. Such systems have been found independently by L. Cardelli, B. C. Pierce, the first author and others, but published only by Steffen [Ste98] and Duggan and Compagnoni [DC98]. In both publications, polarized kinds are used to model subtyping of container types like lists and arrays in object-oriented calculi. We are reusing

Polarities  p  ::= +  covariant
| −  contravariant
| ∘  invariant
Kinds  κ  ::= ∗ | pκ → κ′
Constructors  A, B, F, G ::= X | λX^{pκ}. F | F G | A → B | ∀X^{κ}. A | fix F
Objects (terms) r, s, t  ::= x | λx.t | r s
Contexts  Δ  ::= ⋄ | Δ, x:A | Δ, X^{pκ}

Table 1. Language of Fix^{ω}

their ideas to formulate positive recursive constructors in a strongly normalizing language.

Each function kind κ → κ′ is decorated with a polarity, yielding pκ → κ′ in Duggan and Compagnoni’s notation. For covariant constructors, p = +, for contravariant, p = −, and p = ∘ if the constructor is neither co- nor contravariant or its variance is unknown. Consequently, abstracted variables now carry kinding and polarity information. For instance, we have

λX^{+(+∗→∗)}λA^{+∗}. X (X A) : +(+∗ → ∗) → (+∗ → ∗).

The kinding expresses that X ∘ X is covariant if X is, and that the “twice” operation λX.X ∘ X is itself covariant on covariant arguments, meaning that we may form its fixed point, which would in turn be covariant.^{1} We can also classify invariant constructors, e. g., λA^{∘∗}. A → X (A × A) : ∘∗ → ∗ for invariant X that occurs covariantly, indicated by X^{+(∘∗→∗)} in the context, and contravariant constructors like λX^{−∗}. X → ⊥ : −∗ → ∗. Consequently, λX^{+∗}. (X → ⊥) → ⊥ : +∗ → ∗, which hence includes non-strictly positive type transformers.^{2}

Language of Fix^{ω}. Table 1 shows the syntactic entities of System Fix^{ω}, an extension of F^{ω} by polarized kinds and fixed-points of constructors. Typically, the empty context “⋄” will be suppressed. Furthermore we assume all variables in a context Δ to be pairwise distinct. Capture-avoiding substitution of constructor G for variable X in constructor F is written as [G/X]F, likewise substitution in terms is denoted by [s/x]t. As usual, it is assumed that constructor application and term application associate to the left, e. g., F G X denotes (F G) X and (λx.r) s t denotes ((λx.r) s) t. Iterated applications may be “vectorized”, i. e., r t_{1} … t_{n} will be written as rt with t := t_{1}, …, t_{n}. Then, |t| := n.

While we are using Curry-style objects to express solely the operational behavior, for the type constructors we decided on Church style in order to simplify

1 The kind of λX.X ∘ X obtained here is a syntactic approximation and simplification

of the more logic-based concept of rank-2 monotonicity introduced in [Mat01]. 2 Most dependently typed systems such as Coq do not allow non-strict positivity for

their native fixed points due to the consistency problem reported in [CP88].

the semantics definition in Section 3. The same decision has been taken by Giannini et al. [GHR93], where equivalence with pure Church typing is also established. Note, however, that impredicative systems with dependent types are richer in this mixed style [vBL^{+}97].

Operations on polarities and contexts. Negation of a polarity −p is given by the three equations −(+) = −, −(−) = + and −(∘) = ∘. We define application pΔ of a polarity p to a polarized context Δ. Positive polarity is neutral and changes nothing: +Δ = Δ. The operation −Δ reverses all polarities in Δ. Furthermore ∘Δ discards all co- and contravariant type variable bindings.

Kinding. We introduce a judgement Δ ⊢ F : κ which combines the usual notions of wellkindedness and positive and negative occurrences of type variables. It assures that fixed-points can only be formed over positive type constructors.

\frac{X^{pκ} ∈ Δ p ∈ \{+, ∘\}}{Δ ⊢ X : κ} \frac{Δ, X^{pκ} ⊢ F : κ′}{Δ ⊢ λX^{pκ}. F : pκ → κ′} \frac{Δ ⊢ F : pκ → κ′ pΔ ⊢ G : κ}{Δ ⊢ F G : κ′}
\frac{−Δ ⊢ A : ∗  Δ ⊢ B : ∗}{Δ ⊢ A → B : ∗}  \frac{Δ, X^{∘κ} ⊢ A : ∗}{Δ ⊢ ∀X^{κ}. A : ∗}  \frac{Δ ⊢ F : +κ → κ}{Δ ⊢ fix F : κ}

Kinding is syntax-directed, and, since we are using Church-style constructors, for given Δ and F, the kind κ of F can be computed by structural recursion on F. As a consequence, all rules are invertible in the strong sense that we can recover the applied rule and all the parts of its premises from a given kinding judgement.

The arrow in kinds and in types is assumed to associate to the right, e. g., A → B → C stands for A → (B → C) and +∗ → −κ → κ′ stands for +∗ → (−κ → κ′).

Example 1. We can define standard type constructors via the usual impredicative encodings and get more informative kinds:

\begin{aligned}× & : & +∗ → +∗ → ∗ \\ × & := & λX^{+∗}λY^{+∗}∀Z^{∗}. (X → Y → Z) → Z \\ + & : & +∗ → +∗ → ∗ \\ + & := & λX^{+∗}λY^{+∗}∀Z^{∗}. (X → Z) → (Y → Z) → Z \\ ∃^{κ} & : & +(∘κ → ∗) → ∗ \\ ∃^{κ} & := & λF^{+(∘κ→∗)}∀Z^{∗}. (∀X^{κ}. F X → Z) → Z \end{aligned}

Notice that all these examples use non-strict positivity. We will use + and × infix.

Example 2. The reader is invited to check the examples in the introduction, using ⊥ := ∀X^{∗}. X of kind ∗.

Kinding enjoys the usual properties of weakening and strengthening, as well as substitution which respects polarities: Lemma 1 (Substitution). If Δ, X^{pκ} ⊢ F : κ′ and pΔ ⊢ G : κ then Δ ⊢ [G/X]F : κ′.

Proof. By induction on Δ, X^{pκ} ⊢ F : κ′.

Constructor equality. The β-equality F = F′ of constructors F, F′ is given by the following rules, hence only in the qualified form with contexts:

Computation axioms.

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

Congruences.

\frac{X^{pκ} ∈ Δ  p ∈ \{+, ∘\}}{Δ ⊢ X = X : κ}  \frac{Δ ⊢ F = F′ : pκ → κ′  pΔ ⊢ G = G′ : κ}{Δ ⊢ F G = F′ G′ : κ′}

\frac{Δ, X^{pκ} ⊢ F = F′ : κ′}{Δ ⊢ λX^{pκ}. F = λX^{pκ}. F′ : pκ → κ′}  \frac{Δ, X^{∘κ} ⊢ A = A′ : ∗}{Δ ⊢ ∀X^{κ}. A = ∀X^{κ}. A′ : ∗}
\frac{−Δ ⊢ A′ = A : ∗  Δ ⊢ B = B′ : ∗}{Δ ⊢ A → B = A′ → B′ : ∗}  \frac{Δ ⊢ F = F′ : +κ → κ}{Δ ⊢ fix F = fix F′ : κ}

Symmetry and transitivity.

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

Lemma 2 (Reflexivity). If Δ ⊢ F : κ then Δ ⊢ F = F : κ.

Lemma 3 (Kindedness). If Δ ⊢ F = F′ : κ then Δ ⊢ F : κ and Δ ⊢ F′ : κ.

Wellformed contexts. Δ cxt

\overline{⋄ cxt}  \frac{Δ cxt}{Δ, X^{pκ} cxt}  \frac{Δ cxt  Δ ⊢ A : ∗}{Δ, x:A cxt}

Welltyped terms. Δ ⊢ t : A

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

\frac{Δ, X^{∘κ} ⊢ t : A}{Δ ⊢ t : ∀X^{κ}. A} \frac{Δ ⊢ t : ∀X^{κ}. A ∘Δ ⊢ F : κ}{Δ ⊢ t : [F/X]A} \frac{Δ ⊢ t : A Δ ⊢ A = B : ∗}{Δ ⊢ t : B}

Welltyped terms are closed under substitution (as are constructors, cf. Lemma 1).

As opposed to iso-recursive types with “verbose” folding and unfolding, equirecursive types yield a leaner term language and hence a more succinct semantics.

Lemma 4. If Δ ⊢ t : A then Δ cxt and Δ ⊢ A : ∗.

Proof. By induction on Δ ⊢ t : A.

Reduction. The one-step reduction relation t ⟶ t′ between terms t and t′ is defined as the closure of the β-axiom (λx.t) s ⟶_{β} [s/x]t under all term constructors. We denote the transitive closure of ⟶ by ⟶^{+}. In the next section, we will see that welltyped terms t_{0} admit no infinite reduction t_{0} ⟶ t_{1} ⟶ … Constant-time predecessor. For the type Nat := fix λA^{+∗}. 1+A (using +, defined above, and 1 := ∀A^{∗}. A → A), it is an easy exercise to define closed terms O : Nat and S : Nat → Nat (using the injections into sums) that represent the natural numbers, and a closed term P : Nat → Nat (using the definable case analysis construct) such that P O ⟶^{+} O and P (S x) ⟶^{+} x.

3 Strong Normalization of Fix^{ω}

In this section we prove strong normalization of Fix^{ω} by a model construction where constructors are interpreted as operators on saturated sets. Due to space constraints, the proof necessarily remains sketchy, but all definitions and facts are given which are required to recover the detailed proof.

As is usual for proving (strong) normalization by a model, only the type system has to be reflected in its construction. In System F^{ω}, this is just a simply-typed lambda calculus, namely the (simply-)kinded type constructors. Our system Fix^{ω} additionally has the notions of monotonicity and fixed point. Essentially, we therefore have to give a model of a simply-typed calculus of “syntactically monotone lambda terms”. Although the reader will not be surprised by our solution, the authors were surprised that they were not able to find it in the literature.

Following van Raamsdonk and Severi [vRS95,vRS^{+}99] we define the set of strongly normalizing lambda-terms inductively by the following rules (which are implicity also contained in [Gog95]).

\frac{t_{i} ∈ SN for 1 ≤ i ≤ |t|}{x t ∈ SN}  \frac{t ∈ SN}{λx.t ∈ SN}  \frac{[s/x]t s ∈ SN  s ∈ SN}{(λx.t) s s ∈ SN}

This characterization is sound, i.e., if t_{0} ∈ SN then there is no infinite reduction sequence t_{0} ⟶ t_{1} ⟶ …, for a proof see loc. cit. Our aim is to show t ∈ SN for each welltyped term t.

3.1 Lattices of Operators on Saturated Sets

A set of terms A is called saturated, A ∈ SAT^{∗}, if it contains only strongly normalizing terms, A ⊆ SN, and A is closed under addition of strongly normalizing neutral terms and strongly normalizing weak head expansion:

\frac{t_{i} ∈ SN for 1 ≤ i ≤ |t|}{x t ∈ A}  \frac{[s/x]t s ∈ A  s ∈ SN}{(λx.t) s s ∈ A}

For sets of terms A, B we define the function space A → B := {r ∈ SN | r s ∈ B for all s ∈ A}. If A and B are saturated, so is A → B. Furthermore the function space construction is antitone in the domain and monotone in the codomain: if A′ ⊆ A and B ⊆ B′ then A → B ⊆ A′ → B′.

Given an index set I and a family A_{i} (i ∈ I) of saturated sets, the infimum ⋂_{i∈I} A_{i} is also saturated. Formation of the infimum is monotone: Given a second family A′_{i} of pointwise greater members, A_{i} ⊆ A′_{i}, the infimum is also greater ⋂_{i∈I} A_{i} ⊆ ⋂_{i∈I} A′_{i}. Taking set SN as top element, the saturated sets, together with inclusion, (SAT^{∗}, ⊆), constitute a complete lattice.

In our model for Fix^{ω}, types (= constructors of kind “∗”) will be interpreted as saturated sets. To model constructors of higher kinds κ, we need to define a poset (SAT^{κ}, ⊑^{κ}) of (higher-order) operators on saturated sets for each kind κ. For the base kind, let A ⊑^{∗} A′ :⟺ A, A′ ∈ SAT^{∗} and A ⊆ A′. To require A, A′ ∈ SAT^{∗} is convenient because the reflexive elements of ⊑^{∗} are now exactly the saturated sets: A ∈ SAT^{∗} ⟺ A ⊑^{∗} A. The notion of saturated set SAT^{pκ→κ′} and inclusion ⊑^{pκ→κ′} for higher kinds is defined by induction on the kind. Let F, F′ ∈ SAT^{κ} → SAT^{κ′} be set-theoretic functions.

F ⊑^{pκ→κ′} F′ :⟺ F(G) ⊑^{κ′} F′(G′) for all G, G′ ∈ SAT^{κ} with G ⊑^{pκ} G′
F ∈ SAT^{pκ→κ′} :⟺ F ⊑^{pκ→κ′} F

Here, we used the abbreviations

\begin{aligned}G ⊑^{+κ} G′ & :⟺ & G ⊑^{κ} G′, \\ G ⊑^{−κ} G′ & :⟺ & G′ ⊑^{κ} G, \\ G ⊑^{∘κ} G′ & :⟺ & G ⊑^{κ} G′ and G′ ⊑^{κ} G. \end{aligned}

(An easy induction on κ shows that G ⊑^{∘κ} G′ implies G = G′, but the present definition is more suitable for a uniform treatment of all variances in the proofs to follow.)

Each SAT^{κ} has a top element and infima: For the base kind, ⊤^{∗} = SN and ⨅^{∗} = ⋂; for higher kinds they are defined pointwise: Let F_{i} ∈ SAT^{pκ→κ′} for each i ∈ I. Then ⊤^{pκ→κ′} ∈ SAT^{pκ→κ′} with ⊤^{pκ→κ′}(G) := ⊤^{κ′}, and ⨅_{i∈I}^{pκ→κ′} F_{i} ∈ SAT^{pκ→κ′} with (⨅_{i∈I}^{pκ→κ′} F_{i})(G) := ⨅_{i∈I}^{κ′} F_{i}(G). With these definitions, each poset (SAT^{κ}, ⊑^{κ}) forms a complete lattice.

By Tarski’s fixed-point theorem, each monotone operator F on a complete lattice has a least fixed point lfp F. Indeed, given F ∈ SAT^{+κ→κ}, we can define the least fixed point by lfp F := ⨅^{κ}{G ∈ SAT^{κ} | F(G) ⊑^{κ} G}, i.e., as the least pre-fixed point of F, which, by the theorem, is indeed a pre-fixed point of F, and also a post-fixed point: lfp F ⊑^{κ} F(lfp F). We will use lfp to interpret fixed points fix F of wellkinded constructors F.

3.2 Interpretation of Constructors

In the following part we will define an interpretation [[F]]_{θ} ∈ SAT^{κ} for each constructor of kind κ, where θ is a valuation for the free constructor variables in F. For convenience, a valuation θ is a set-theoretical object which maps both constructor variables X to sets F and term variables x to terms t. Update of a valuation is written as θ[X ↦ F] resp. θ[x ↦ t]. We extend inclusion and saturatedness to valuations by defining:

θ ⊑^{Δ} θ′ :⟺ θ(X) ⊑^{pκ} θ′(X) for all X^{pκ} ∈ Δ
θ ∈ SAT^{Δ} :⟺ θ ⊑^{Δ} θ

Lemma 5. If θ ⊑^{Δ} θ′, then θ ⊑^{+Δ} θ′, θ′ ⊑^{−Δ} θ, θ ⊑^{∘Δ} θ′ and θ′ ⊑^{∘Δ} θ.

Proof. By induction on the generation of Δ.

For the following definition and lemma which is the crucial part of this normalization proof, let Δ ⊢ F : κ. For θ ∈ SAT^{Δ}, we define the interpretation [[F]]_{θ} ∈ SAT^{κ} by induction on the structure of F. Simultaneously we need to prove monotonicity of [[F]], the cases for definition and proof are given below.

Lemma 6 (Monotonicity). If θ ⊑^{Δ} θ′ then [[F]]_{θ} ⊑^{κ} [[F]]_{θ′}.

For θ = θ′, immediate consequence of monotonicity is welldefinedness of the interpretation, [[F]]_{θ} ∈ SAT^{κ}.

Corollary 1 (p-Monotonicity). Let pΔ ⊢ F : κ. If θ ⊑^{Δ} θ′ then [[F]]_{θ} ⊑^{pκ} [[F]]_{θ′}.

Proof (of the corollary). In case p = + the corollary just restates monotonicity (Lemma 6). If p = − then θ′ ⊑^{−Δ} θ by Lemma 5. Using monotonicity, [[F]]_{θ′} ⊑^{κ} [[F]]_{θ}. This is by definition equivalent to [[F]]_{θ} ⊑^{−κ} [[F]]_{θ′}. If otherwise p = ∘, then by Lemma 5 both θ ⊑^{∘Δ} θ′ and θ′ ⊑^{∘Δ} θ. By monotonicity [[F]]_{θ} ⊑^{κ} [[F]]_{θ′} and [[F]]_{θ′} ⊑^{κ} [[F]]_{θ} which entail by definition [[F]]_{θ} ⊑^{∘κ} [[F]]_{θ′}.

Definition of [[F]]_{θ} and proof of monotonicity. By induction on the shape of F.

– Δ ⊢ X : κ. Set [[X]]_{θ} := θ(X). By assumption, X^{pκ} ∈ Δ with p ∈ {+, ∘}. The requirement θ ⊑^{Δ} θ′ implies θ(X) ⊑^{κ} θ′(X), hence [[X]]_{θ} ⊑^{κ} [[X]]_{θ′} by definition.

– Δ ⊢ λX^{pκ}. F : pκ → κ′. The interpretation is a set-theoretic function [[λX^{pκ}. F]]_{θ} ∈ SAT^{κ} → SAT^{κ′}, [[λX^{pκ}. F]]_{θ}(G) := [[F]]_{θ[X↦G]} . To show monotonicity, assume G, G′ ∈ SAT^{κ} with G ⊑^{pκ} G′. By inversion of the typing derivation, Δ, X^{pκ} ⊢ F : κ′, and, since θ[X ↦ G] ⊑^{Δ,X^{pκ}} θ′[X ↦ G′], by induction hypothesis [[F]]_{θ[X↦G]} ⊑^{κ′} [[F]]_{θ′[X↦G′]}. Hence, [[λX^{pκ}. F]]_{θ}(G) ⊑^{κ′} [[λX^{pκ}. F]]_{θ′}(G′) by definition. To conclude, [[λX^{pκ}. F]] is monotone.

– Δ ⊢ F G : κ′. Set [[F G]]_{θ} := [[F]]_{θ}([[G]]_{θ}). Monotonicity and welldefinedness can be seen as follows. By inversion of the kinding derivation, Δ ⊢ F : pκ → κ′ and pΔ ⊢ G : κ. Assume θ ⊑^{Δ} θ′. By the first induction hypothesis, [[F]]_{θ} ⊑^{pκ→κ′} [[F]]_{θ′}. By the second induction hypothesis, with Corollary 1, [[G]]_{θ} ⊑^{pκ} [[G]]_{θ′}. Putting things together, [[F]]_{θ}([[G]]_{θ}) ⊑^{κ′} [[F]]_{θ′}([[G]]_{θ′}), which by definition entails our goal.

– Δ ⊢ A → B : ∗. Set [[A → B]]_{θ} := [[A]]_{θ} → [[B]]_{θ}. By inversion, −Δ ⊢ A : ∗ and Δ ⊢ B : ∗. By induction hypothesis and Corollary 1, [[A]]_{θ} ⊑^{−∗} [[A]]_{θ′}, hence [[A]]_{θ′} ⊆ [[A]]_{θ}. Again, by induction hypothesis, [[B]]_{θ} ⊑^{∗} [[B]]_{θ′}, hence [[B]]_{θ} ⊆ [[B]]_{θ′} Together, [[A → B]]_{θ} ⊆ [[A → B]]_{θ′}. Since the functional construction is saturated, we conclude with [[A → B]]_{θ} ⊑^{∗} [[A → B]]_{θ′}.

– Δ ⊢ ∀X^{κ}. A : ∗. Set [[∀X^{κ}. A]]_{θ} := ⋂_{F∈SAT^{κ}}[[A]]_{θ[X↦F]}. By inversion, Δ, X^{∘κ} ⊢ A : ∗. For arbitrary F ∈ SAT^{κ}, θ[X ↦ F] ⊑^{Δ,X^{∘κ}} θ′[X ↦ F], hence [[A]]_{θ[X↦F]} ⊑^{∗} [[A]]_{θ′[X↦F]} by induction hypothesis. This entails [[∀X^{κ}. A]]_{θ} ⊑^{∗} [[∀X^{κ}. A]]_{θ′} by monotonicity and saturatedness of the infimum.

– Δ ⊢ fix F : κ. Set [[fix F]]_{θ} := lfp([[F]]_{θ}). By inversion, Δ ⊢ F : +κ → κ, hence, by induction hypothesis, F := [[F]]_{θ} ∈ SAT^{+κ→κ} is a monotone operator on SAT^{κ}, and by Tarski’s theorem the least fixed-point lfp F ∈ SAT^{κ} exists. To show monotonicity, we assume θ ⊑^{Δ} θ′ and define F′ := [[F]]_{θ′}. By monotonicity of [[F]], F ⊑^{+κ→κ} F′. In particular, F(G) ⊑^{κ} F′(G) for every G ∈ SAT^{κ}. Since lfp F is a monotone function in its argument F, we are done. ⊓ ⊔

The interpretation is compatible with substitution and constructor equality, as we show in the following lemmata.

Lemma 7 (Soundness of substitution). If Δ, X^{pκ} ⊢ F : κ′ and pΔ ⊢ G : κ, then [[[G/X]F]]_{θ} = [[F]]_{θ[X↦[[G]]_{θ}]} for all θ ∈ SAT^{Δ}.

Proof. By induction on the structure of F.

Lemma 8 (Soundness of equality). If Δ ⊢ F = F′ : κ then [[F]]_{θ} = [[F′]]_{θ} for all θ ∈ SAT^{Δ}.

Proof. By induction on constructor equality, using the previous lemma for the first computation rule.

3.3 Interpretation of Terms

To complete our model, we define an interpretation ⦇t⦈_{θ} of terms and then show ⦇t⦈_{θ} ∈ [[A]]_{θ} for welltyped terms Δ ⊢ t : A and sound valuations θ. For wellformed contexts Δ cxt a valuation is sound, θ ∈ [[Δ]], if θ ∈ SAT^{Δ} and θ(x) ∈ [[A]]_{θ} for each (x:A) ∈ Δ. The term interpretation ⦇t⦈_{θ} is simply the term t itself where all free variables x have been replaced by their value θ(x) in valuation θ. Note that theses values are strongly normalizing for sound valuations already; it remains to show that the full term ⦇t⦈_{θ} is strongly normalizing for well-typed θ. This is a consequence of the following theorem.

Theorem 1 (Soundness of typing). If Δ ⊢ t : A and θ ∈ [[Δ]] then ⦇t⦈_{θ} ∈ [[A]]_{θ}.

Proof. By induction on Δ ⊢ t : A. Note that by Lemma 4 the context Δ and the type A are wellformed if the typing judgement is derivable. Since our term language is just pure lambda calculus, the proof is standard, for the rule of type equality use Lemma 8.

Corollary 2. If Δ ⊢ t : A, the term t is strongly normalizing.

Proof. By Theorem 1, choosing a valuation θ with θ(X) = ⊤^{κ} for all X^{pκ} ∈ Δ and θ(x) = x for all (x : B) ∈ Δ. This valuation is sound since the type interpretation [[B]]_{θ} is saturated, hence, contains x.

4 Primitive Recursion for Heterogeneous Datatypes

In this section, we propose a second way to equip System F^{ω} with fixed points of higher rank. Therein, we follow Mendler [Men87] who also—besides considering type equations in System F—gave an extension of F by least and greatest fixed points, together with elimination schemes which we refer to as Mendler (co)recursion. We carry Mendler’s schemes to higher ranks and define a system MRec^{ω} as an extension of F^{ω} by least fixed points of type constructors, also called higher-order inductive types. In contrast to Fix^{ω} which possesses equi-recursive types, MRec^{ω} is in the style of iso-recursive type systems and has explicit introduction and elimination terms for inductive types. In analogy to Spławski and Urzyczyn [SU99] we conjecture that MRec^{ω} has no reduction preserving embedding into F^{ω}. However, it embeds into Fix^{ω}, as we will show in Section 5.

Our starting point is Curry-style System F^{ω}, enriched with unit type 1, binary products A × B and sums A + B and the usual term constructors: ⟨⟩ for the inhabitant of the unit type, ⟨t_{1}, t_{2}⟩, fst r and snd r for pairs and left and right projection, and inl t, inr t and case (r, x. s, y. t) for left and right injection and case distinction. Note that there are no polarized kinds and no fixed-point constructors. An exposition of the exact rules for typing Γ ⊢ t : A and reduction t ⟶ t′ can be found in the appendix of Abel et al. [AMU03]. Since F^{ω}’s notion of constructor equivalence is just plain β-equality, we even identify constructors with their β-normal form on the syntactic level.

4.1 Definition of System MRec ^{ω}

For every kind κ of F^{ω}, we add the constructor constant μ^{κ} of kind (κ → κ) → κ to the system of constructors of F^{ω}, denoting least fixed-point formation. The term system of F^{ω} is extended by two families of constants: in^{κ} (fixed-point introduction) and MRec^{κ} (fixed-point elimination) for every kind κ. In order to give their types, we need a notion of constructor containment: Every kind κ can uniquely be written in the form κ_{1} → … κ_{n} → ∗, in short κ → ∗. Define

F ⊆^{κ} G := ∀X^{κ}. F X → GX : κ → κ → ∗,

for constructors F, G : κ = κ → ∗. The typing of the constants can now be given by in^{κ} : ∀F^{κ→κ}. F (μ^{κ}F) ⊆^{κ} μ^{κ}F and

MRec^{κ} : ∀F^{κ→κ}∀G^{κ}. (∀X^{κ}. X ⊆^{κ} μ^{κ}F → X ⊆^{κ} G → F X ⊆^{κ} G) → μ^{κ}F ⊆^{κ} G.

The notion ⟶ of reduction for untyped terms is extended by the additional basic reduction rule of primitive recursion

MRec^{κ} s (in^{κ} t) ⟶_{β} s id (MRec^{κ} s) t,

where id := λx.x is the identity. Intuitively, subject reduction still holds because the type ∀X^{κ}. X ⊆^{κ} μ^{κ}F → X ⊆^{κ} G → F X ⊆^{κ} G of the term s is instantiated with the fixed-point constructor μ^{κ}F itself. Therefore, the identity id qualifies as first argument to s. In general, the transformation from the blank type X back into the fixed-point, i. e., of type X ⊆^{κ} μ^{κ}F, which is the first formal argument of s, provides access to the predecessor of the recursion argument. This is the feature which distinguishes primitive recursion from iteration.

For κ = ∗, we have just restated Mendler’s rules for recursive types [Men87]. At this point, let us remark that Mendler-style inductive types μ^{κ}F —although not observed by Mendler—do not require positivity for F. This contrasts with the recursive types of Fix^{ω}. It also contrasts with formulations of primitive recursion in conventional style that have to rely on positivity or, less syntactically, on a monotonicity requirement such as that in [Mat01] for κ = ∗ or ∗ → ∗.

4.2 Example: Redecoration of Finite Triangular Matrices

As a non-trivial example of the use of MRec^{ω} for heterogeneous datatypes, we consider a redecoration operation for the diagonal elements of finite triangular matrices. In previous work with Uustalu, we have treated redecoration for infinite triangular matrices by higher-order coiteration [AMU03], and the finite ones by a computationally unsatisfactory encoding of recursion within iteration [AMU04].

Fix a type E : ∗ of matrix elements. The type Tri A of finite triangular matrices with diagonal elements in A and ordinary elements E can be obtained as follows, with κ1 := ∗ → ∗:

TriF := λX^{κ1}λA^{∗}. A × (1 + X (E × A)) : κ1 → κ1
Tri := μ^{κ1}TriF  : κ1

We think of these triangles decomposed columnwise: The first column is a singleton of type A, the second a pair of type E × A, the third a triple of type E × (E × A), the fourth a quadruple of type E × (E × (E × A)) etc. Hence, if some column has some type A′ we obtain the type of the next column as E ×A′. By taking the left injection into the sum 1 + …, one can construct an element without further recurrence, the last column. We can visualize triangles like this:

\begin{aligned}A & E & E & E & E \\ & A & E & E & E \\ & & A & E & E \\ & & & A & E \\ & & & & A \end{aligned}

The vertical lines hint at the decomposition scheme. In general, elements of type Tri A are constructed by means of

sg := λa. in^{κ1} ⟨a, inl ⟨⟩⟩ : ∀A^{∗}. A → Tri A
cons := λaλt. in^{κ1} ⟨a, inr t⟩ : ∀A^{∗}. A → Tri (E × A) → Tri A

The function top : ∀A^{∗}. Tri A → A = Tri ⊆^{κ1} λA^{∗}. A that yields the topmost diagonal element, is defined as top := MRec^{κ1}(λiλtopλp. fst p). As reduction behavior, we get

top (sg a) ⟶^{+} a
top (cons a t) ⟶^{+} a

If we remove the first column of a triangle Tri A, we obtain a trapezium Tri (E × A). We can get back a (smaller) triangle if we cut off the top row of the trapezium using the function cut : ∀A^{∗}. Tri (E × A) → Tri A. The exact definition of this function, which is like fcut in [AMU04, Example 34], has to be omitted due to lack of space.

Let T A denote some sort of A-decorated (or A-labelled) trees. Redecoration [UV02] is an operation that takes an A-decorated tree t : T A and a redecoration rule f : T A → B and returns a B-decorated tree t′ : T B. For triangles, redecoration works as follows: In the triangle

\begin{aligned}A & E & E & E & E \\ & A & E & E & E \\ & & \underline{A} & E & E \\ & & & A & E \\ & & & & A \end{aligned}

the underlined A (as an example) gets replaced by the B assigned by the redecoration rule to the sub triangle cut out by the horizontal line; similarly, every other A is replaced by a B.

For the definition of redecoration, we will need a means of lifting a redecoration rule on triangles to one on trapeziums.

lift := λfλt. ⟨fst (top t), f (cut t)⟩
: ∀A^{∗}∀B^{∗}. (Tri A → B) → Tri (E × A) → E × B

For a detailed explanation in which sense this is a lifting, see [AMU04]. Finally, we can define redecoration

redec : ∀A^{∗}∀B^{∗}. Tri A → (Tri A → B) → Tri B = Tri ⊆^{κ1} G

with G := λA^{∗}∀B^{∗}. (Tri A → B) → Tri B. The definition makes essential use of primitive recursion in that it also uses the variable i : X ⊆^{κ1} Tri in the body of argument to MRec^{κ1}:

redec := MRec^{κ1}(λiλredecλtλf. case (snd t,

u. sg (f (sg (fst t))),

r. cons (f (cons (fst t) (i r))) (redec r (lift f))))

Its reduction behavior is easy to calculate:

redec (sg a) f ⟶^{+} sg (f (sg a))
redec (cons a r) f ⟶^{+} cons (f (cons a r)) (redec r (lift f))

The reader is invited to compare this concise behaviour with the one obtained in [AMU04] within definitional extensions of system F^{ω} that therefore can only provide iteration schemes and no primitive recursion. Notice that the number of reduction steps does not depend on the terms a, r and f since these may just be variables. By a modification of the definition of redec above, it is easy to define a constant-time predecessor operation on triangles (a left inverse of in^{κ1} for Tri even with respect to reductions of open terms): The access to r in the cons case of the reduction will be type-correct by using (i r) instead of r, just as for redec.

5 Embedding of Mendler-Style Recursion into Fix^{ω}

In this section, we prove—via an embedding into Fix^{ω}—that Mendler recursion for higher ranks is strongly normalizing. The proof proceeds in two steps: First, we show that all constructions of MRec^{ω} can be defined in Fix^{ω} such that reduction is simulated. Then we map each welltyped term of MRec^{ω} onto a still welltyped term of Fix^{ω} of exactly the same shape (the translation is purely homomorphic). Thus, each infinite reduction sequence of MRec^{ω} would map onto an infinite sequence of Fix^{ω}, which is a contradiction to the result of Section 3.

Products and sums can be defined in Fix^{ω} via the standard impredicative encoding (see Example 1). The interesting part is the definition of least fixedpoints μ^{κ}F within Fix^{ω}. We give their definition only for kinds carrying no polarity information, i.e., kinds of the form κ = ∘κ → ∗. This suffices because their purpose is just to serve as images in the translation of the least fixed points in the polarity-free system MRec^{ω}. We define μ^{κ} := λF^{∘(∘κ→κ)}. fix Φ_{F} with

Φ_{F} := λY^{+κ}λX^{∘κ}∀G^{κ}. (∀X^{κ}. X ⊆^{κ} Y → X ⊆^{κ} G → F X ⊆^{κ} G) → G X.

It is not hard to see that F^{∘(∘κ→κ)} ⊢ Φ_{F} : +κ → ∘κ → ∗, since the variable Y occurs twice to the left of an arrow in the body of the definition of Φ_{F}. Thus, for any F : ∘κ → κ we have Φ_{F} : +κ → κ, and μ^{κ} : ∘(∘κ → κ) → κ as required.

Once we have found a suitable representation of μ^{κ} in Fix^{ω}, the definition of elimination and introduction falls into place:

MRec^{κ} := λsλr. r s
in^{κ} := λtλs. s id (MRec^{κ}s) t

Note that the right-hand sides do not depend on κ. These definitions yield simulation of primitive recursion within Fix^{ω}, as we can confirm by performing four β-reduction steps: MRec^{κ} s (in^{κ} t) ⟶^{+} s id (MRec^{κ} s) t.

Now, System MRec^{ω} can be translated into Fix^{ω} by replacing each arrow kind κ → κ′ by ∘κ → κ′, and each annotated abstraction λX^{κ} by λX^{∘κ}. All other syntactical constructions remain unchanged. Certainly, we can only map the constants in^{κ} and MRec^{κ} of MRec^{ω} onto their defined counterparts in Fix^{ω}, if the types of source and target match. This can been seen by type-checking, for which the following chart might be an aid.

Δ := F^{∘(∘κ→κ)}, G^{∘κ}, X^{∘κ},
s : ∀X^{κ}. X ⊆^{κ} μ^{κ}F → X ⊆^{κ} G → F X ⊆^{κ} G,
r : μ^{κ}F X = Φ_{F} (μ^{κ}F) X,
t : F (μ^{κ}F) X
Δ ⊢ r s : G X
Δ ⊢ λs. s id (MRec^{κ}s) t : Φ_{F} (μ^{κ}F) X = μ^{κ}F X

Theorem 2. In System MRec^{ω} of Mendler recursion for arbitrary kinds there exists no infinite reduction sequence t_{0} ⟶ t_{1} ⟶ … starting with a welltyped term t_{0}.

Proof. By Corollary 2, using the abovementioned translation into Fix^{ω}.

6 Conclusion and Future Work

We have presented two systems for total functions over higher-order and nested datatypes where the predecessor runs in constant time. The first system, Fix^{ω}, supports positive equi-recursive types of higher order. No primitive combinator for recursive functions is built in, but due to the strength of equi-recursive types in combination with impredicativity, customary recursion schemes can be defined. One instance is Mendler-style primitive recursion MRec, which for example can be used to define a redecoration algorithm for triangular matrices. We have shown that Mendler-style primitive recursion can be simulated in Fix^{ω}.

This simulation could have been extended to also account for coinductive type constructors, by defining Mendler-style corecursion for higher ranks in Fix^{ω}. A naturally corecursive program is substitution for the infinite version of de Bruijn terms coded as a nested datatype [AR99,BP99b]. Due to space restrictions we have to leave this direction to future work.

The systematic use of nested datatypes to represent datastructures with invariants is rather new [Hin98] (but also see [Oka96, Sections 10, 11] for earlier work). As an example, Hinze [Hin01] implemented Okasaki’s functional version of red-black trees [Oka99] by help of a nested datatype to actually ensure the balancing properties of red-black trees by the type system. Most algorithms for nested datatypes published so far require just iteration, hence can be implemented in the framework of generalized folds [BP99a] or efficient folds [MGB04] or Mendler iteration [AMU04]. As more classical algorithms will find functional implementations using nested datatypes, we imagine many more examples requiring primitive recursion for higher-rank datatypes, and thus may infer termination of the respective algorithms.

References

[AMU03] A. Abel, R. Matthes, and T. Uustalu. Generalized iteration and coiteration for higher-order nested datatypes. In A. Gordon, ed., Proc. of FoSSaCS 2003 , vol. 2620 of LNCS, pp. 54–69. 2003.

[AMU04] A. Abel, R. Matthes, and T. Uustalu. Iteration and coiteration schemes for higher-order and nested datatypes. Theoretical Computer Science, 2004. 79 pages, accepted for publication.

[AR99] T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In Proceedings of CSL ’99 , vol. 1683 of LNCS, pp. 453–468. 1999.

[BB85] C. Böhm and A. Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39:135–154, 1985.

[BP99a] R. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Aspects of Computing, 11(2):200–222, 1999.

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

[CP88] T. Coquand and C. Paulin. Inductively defined types—preliminary version. In P. Martin-Löf and G. Mints, eds., Proceedings of COLOG ’88 , vol. 417 of LNCS, pp. 50–66. 1988.

[DC98] D. Duggan and A. Compagnoni. Subtyping for object type constructors, 1998. Presented at FOOL 6.

[GHR93] P. Giannini, F. Honsell, and S. Ronchi Della Rocca. Type inference: some results, some problems. Fundamenta Informaticae, 19(1-2):87 – 125, 1993.

[Gog95] H. Goguen. Typed operational semantics. In M. Dezani-Ciancaglini and G. Plotkin, eds., Proc. of TLCA ’95 , vol. 902 of LNCS, pp. 186–200. 1995.

[Hin98] R. Hinze. Numerical representations as higher-order nested datatypes. Tech. Rep. IAI-TR-98-12, Institut für Informatik III, Universität Bonn, 1998.

[Hin01] R. Hinze. Manufacturing datatypes. Journal of Functional Programming, 11(5):493–524, 2001.

[Mat01] R. Matthes. Monotone inductive and coinductive constructors of rank 2. In L. Fribourg, ed., Proc. of CSL 2001 , vol. 2142 of LNCS, pp. 600–614. 2001.

[Men87] N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of LICS ’87 , pp. 30–36. 1987.

[MGB04] C. Martin, J. Gibbons, and I. Bayley. Disciplined, efficient, generalised folds for nested datatypes. Formal Aspects of Computing, 16(1):19–35, 2004.

[Oka96] C. Okasaki. Purely Functional Data Structures. Ph.D. thesis, Carnegie Mellon University, 1996.

[Oka99] C. Okasaki. Red-black trees in a functional setting. Journal of Functional Programming, 9(4):471–477, 1999.

[Ste98] M. Steffen. Polarized Higher-Order Subtyping. Ph.D. thesis, Technische Fakultät, Universität Erlangen, 1998.

[SU99] Z. Spławski and P. Urzyczyn. Type fixpoints: Iteration vs. recursion. In Proceedings of ICFP’99 , pp. 102–113. SIGPLAN Notices, 1999.

[Urz96] P. Urzyczyn. Positive recursive type assignment. Fundamenta Informaticae, 28(1–2):197–209, 1996.

[UV02] T. Uustalu and V. Vene. The dual of substitution is redecoration. In K. Hammond and S. Curtis, eds., Trends in Functional Programming 3 , pp. 99–110. Intellect, Bristol, Portland, OR, 2002.

[vBL^{+}97] S. van Bakel, L. Liquori, S. Ronchi Della Rocca, and P. Urzyczyn. Comparing cubes of typed and type assignment systems. Annals of Pure and Applied Logic, 86(3):267–303, 1997.

[vRS95] F. van Raamsdonk and P. Severi. On normalisation. Tech. Rep. CS-R9545, CWI, 1995.

[vRS^{+}99] F. van Raamsdonk, P. Severi, M. H. Sørensen, and H. Xi. Perpetual reductions in lambda calculus. Inf. and Comp., 149(2):173–225, 1999.