Generalized Iteration and Coiteration for Higher-Order Nested Datatypes

Andreas Abel^{1}^{⋆}, Ralph Matthes^{2} and Tarmo Uustalu^{3}^{⋆⋆}

1 Department of Computer Science, University of Munich

               abel@informatik.uni-muenchen.de

2 Preuves, Programmes et Systèmes,

CNRS, Université Paris VII (on leave from University of Munich)

              matthes@informatik.uni-muenchen.de

3 Inst. of Cybernetics, Tallinn Technical University

                       tarmo@cs.ioc.ee

Abstract. We solve the problem of extending Bird and Paterson’s generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by appropriately generalizing Mendler-style (co)iteration. Characteristically to Mendler-style schemes of disciplined (co)recursion, the schemes we propose do not rest on notions like positivity or monotonicity of a constructor and facilitate programming in a natural and elegant style close to programming with the customary letrec construct, where the typings of the schemes, however, guarantee termination. For rank 2, a smoothened version of Bird and Paterson’s generalized folds and its dual are achieved; for rank 1, the schemes instantiate to Mendler’s original (re)formulation of iteration and coiteration. Several examples demonstrate the power of the approach. Strong normalization of our proposed extension of system F^{ω} of higherorder parametric polymorphism is proven by a reduction-preserving embedding into pure F^{ω}.

1 Introduction

Within the paradigm of generic programming, Bird and Paterson [8] with colleagues [11, 15] have studied the problem of identifying workable schemes for defining functions for nested, non-uniform or heterogeneous datatypes, i.e., inductive and coinductive constructors of rank 2 (type transformers), and put forth generalized folds as a scheme for defining functions like substitution for the de Bruijn notation of lambda terms in a natural fashion.

In [2], two of the authors of the present article showed that, making good use of right notions of containment and monotonicity of constructors, the schemes of

⋆ The first author gratefully acknowledges the support by the PhD Programme Logic

in Computer Science (GKLI) of the Deutsche Forschungs-Gemeinschaft. ⋆⋆ The third author is partially supported by the Estonian Science Foundation (ETF)

under grant No. 4155. He is also grateful to the GKLI for two invitations to Munich; the cooperation started during these visits.

iteration and coiteration are extensible to monotone (co)inductive constructors of any finite kind. In the present article, we similarly extend the more liberal generalized folds to all finite kinds. We accomplish this thanks to two ideas: a simple, but powerful generalization of the notion of constructor containment, and reformulation of the schemes in the style originated by Mendler [18]. The result is a concise extension of system F^{ω} of higher-order parametric polymorphism with (co)inductive constructors of any finite kind, equipped with Mendler-style generalized (co)iteration. Switching to Mendler style was not intentional, but in the end turned out rewarding. The reasons are the following.

Firstly, any syntactic positivity requirement can be avoided in the formation rules of (co)inductive types. This is beneficial as positivity and map terms associating to positive constructors would have to be defined by induction outside the system and parametrically polymorphic quantification over all positive constructors is impossible. Moreover, for higher kinds, there is no obvious canonical definition of positivity, although attempts of definition exist [14]. Replacing positivity with monotonicity [17, 2] gives an improvement, but formulations of the systems and especially programming remain clumsy.

Secondly, Mendler style facilitates a programming style very close to programming with general recursion (i.e., the letrec construct). The computation rules for Mendler-style disciplined (co)recursion schemes are nearly identical to the rule of letrec, the restrictive typings however ensure that all computations terminate.

Thirdly, Mendler-style disciplined (co)recursion schemes tend to be amenable for generalizations whereas conventional ones—making use of map terms or monotonicity witnesses—typically get complicated. Examples are: primitive (co-) recursion [18], course-of-value (co)iteration [21, 22], iteration over multiple inductive types at the same time [22] and—as the examples of this article testify— generalized iteration in the sense of generalized folds.

The article is organized as follows. In Sect. 2, we review our starting point system F^{ω} of higher-order parametric polymorphism. In Sect. 3, we present our system MIt^{ω} of (co)inductive constructors of finite ranks with generalized Mendler-style iteration and describe some programming examples. The embedding of MIt^{ω} into F^{ω} is presented in Sect. 4. We conclude with a summary and discussion of related work.

Acknowledgements: Many thanks to Peter Hancock for his suggestion in November 2000 of the unusual notion F ≤_{κ1} G. It started this whole research project.

2 System F^{ω}

Our development of higher-order datatypes takes place within a conservative extension of Curry-style system F^{ω} by binary sums and products, the unit type and existential quantification. It contains three syntactic categories:

Kinds. Kinds are given by the following grammar and denoted by the letter κ.

κ  ::= ∗ | κ → κ′
rk(∗)  := 0
rk(κ → κ′) := max(rk(κ) + 1, rk(κ′))

The rank of kind κ is computed by rk(κ). We introduce abbreviations for some special kinds: κ0 = ∗, types, κ1 = ∗ → ∗, unary type transformers and κ2 = (∗ → ∗) → ∗ → ∗ unary transformers of type transformers.

Note that each kind κ′ can be uniquely written as κ → ∗, where we write κ for the sequence κ_{1}, …, κ_{n} and set κ → κ := κ_{1} → … → κ_{n} → κ. Provided another sequence κ′ = κ′_{1}, …, κ′_{n} of the same length, i.e., |κ′| = |κ|, set κ → κ′ := κ_{1} → κ′_{1}, …, κ_{n} → κ′_{n}. This last abbreviation does not conflict with the abbreviation κ → κ due to the required |κ′| = |κ|.

Constructors. Uppercase latin letters denote constructors, given by the following grammar. The metavariable X ranges over a denumerable set of constructor variables.

\begin{aligned}A, B, F, G & ::= & X | λX^{κ}.F | F G | ∀F^{κ}. A | ∃F^{κ}. A | A → B \\ & | & A + B | A × B | 1 \end{aligned}

We identify β-equivalent constructors. A constructor F has kind κ if there is a context Γ such that Γ ⊢ F : κ. The kinding rules for constructors appear in Appendix A.

The rank of a constructor is given by the rank of its kind. Preferably we will use letters A, B, C, D for constructors of rank 0 (types) and F, G, H for constructors of rank 1. If no kinds are given and cannot be guessed from the context, we assume A, B, C, D : ∗ and F, G, H : κ1. Write Id_{κ} := λX^{κ}.X for the identity constructor. If the kinding is clear from the context, we just write Id. Constructor application associates to the left, i. e., F G_{1} … G_{n} = (… (F G_{1}) …) G_{n}. Setting G := G_{1}, …, G_{n}, the constructor F G_{1} … G_{n} is also written as F G. Sums and products can inductively be extended to all kinds: For F, G : κ_{1} → κ_{2} set F + G := λX^{κ_{1}}.F X + GX and F × G := λX^{κ_{1}}.F X × GX.

Objects (Curry terms). Lower case letters denote terms. In the grammar below, the metavariable x ranges over a denumerable set of object variables.

r, s, t ::= x | λx.t | r s | inl t | inr t | case (r, x. s, y. t)
| ⟨⟩ | ⟨t_{0}, t_{1}⟩ | r.0 | r.1 | pack t | open (r, x. s)

Most term constructors are standard; “pack” introduces and “open” eliminates existential quantification. The polymorphic identity λx.x : ∀A. A → A will be denoted by id. We write f ∘ g for function composition λx. f (g x). Application r s associates to the left, hence rs = (… (r s_{1}) … s_{n}) for s = s_{1}, …, s_{n}.

A term t has type A if Γ ⊢ t : A for some context Γ. The relation ⟶ denotes the usual one-step β-reduction which is confluent, type preserving and strongly normalizing. The typing and reduction rules for terms are standard and can be found in Appendix A.

In the following we will refer to the here defined system simply as “F^{ω}”.

3 Generalized Mendler-Style Iteration and Coiteration

In this section, we recap and extend the notions of containment and monotonicity presented in [2]. On top of these notions, we define the system MIt^{ω} of generalized (co)iteration for inductive and coinductive constructors of arbitrary ranks, which we then specialize to rank 1 (types) and rank 2 (type transformers). To give a feel for our system, we spell out some examples involving nested or non-uniform datatypes [7].

3.1 Containment and Monotonicity of Constructors

Containment. The key to extending Mendler-style iteration and coiteration [19] to finite kinds consists in identifying an appropriate containment relation for constructors of the same kind κ. For types, the canonical choice is implication. For an arbitrary kind κ = κ → ∗, the easiest notion is “pointwise implication”: The constructor ⊆_{κ}: κ → κ → ∗ is defined by F ⊆_{κ} G := ∀X^{κ}. F X → GX, hence F ⊆_{κ} G is a type which, as a proposition, states that F is contained in G.

A more refined notion ≤_{κ} has been employed already in previous work [2] which studies (co)iteration for monotone (co)inductive constructors of higher kinds:

\begin{aligned}F & ≤_{∗} & G & := & F → G \\ F & ≤_{κ→κ′} & G & := & ∀X^{κ}∀Y^{κ}. X ≤_{κ} Y → F X ≤_{κ′} G Y \end{aligned}

Monotonicity. Using this notion of containment, we can define monotonicity mon_{κ} : κ → ∗ for kind κ directly by

mon_{κ} F := F ≤_{κ} F.

The type mon_{κ} F, seen as a proposition, asserts that F is monotone. The same type is used in polytypic programming for generic map functions [13, 3].

This notion does not enter the formulation of system MIt^{ω}, but many applications. We omit the subscripted kind κ when clear from the context, as in the definition of the following basic monotonicity witnesses. These are closed terms whose type is some mon F. They will pop up in examples later.

pair : mon(λAλB.A × B) := λfλgλp. ⟨f (p.0), g (p.1)⟩
fork : mon(λA.A × A) := λf. pair ff
either : mon(λAλB.A + B) := λfλgλx. case (x, a. inl (f a), b. inr (g b))
maybe : mon(λA.1 + A) := either id

Relativized refined containment. In order to be able to extend Mendler (co)iteration to higher kinds so that generalized folds [8] are covered, we have to relativize the notion ≤_{κ}, κ = κ → ∗, to a vector H of constructors of kinds κ → κ. For every kind κ = κ → ∗, we define a constructor ≤_{κ}^{(−)}: (κ → κ) → κ → κ → ∗ by structural recursion on κ as follows:

\begin{aligned}F & ≤_{∗} & G & := & F → G \\ F & ≤_{κ→κ′}^{H,H} & G & := & ∀X^{κ}∀Y^{κ}. X ≤_{κ} H Y → F X ≤_{κ′}^{H} G Y \end{aligned}

Note that, in the second line, H has kind κ → κ. For H a vector of identity constructors, the new notion ≤_{κ}^{H} coincides with ≤_{κ}. Similarly, we define another constructor ^{(−)}≤_{κ}: (κ → κ) → κ → κ → ∗, where the base case is the same as before, hence no ambiguity with the notation arises.

\begin{aligned}F & ≤_{∗} & G & := & F → G \\ F & ^{H,H}≤_{κ→κ′} & G & := & ∀X^{κ}∀Y^{κ}. H X ≤_{κ} Y → F X ^{H}≤_{κ′} G Y \end{aligned}

As an example, for F, G, H : κ1, one has

\begin{aligned}F & ≤_{κ1}^{H} & G & = & ∀A∀B. (A → HB) → F A → GB, \\ F & ^{H}≤_{κ1} & G & = & ∀A∀B. (HA → B) → F A → GB. \end{aligned}

3.2 System MIt^{ω}

Now we are ready to define generalized Mendler-style iteration and coiteration, which specialize to ordinary Mendler-style iteration and coiteration in the case of (co)inductive types, and to a scheme encompassing generalized folds [8, 11, 15] and the dual scheme for coinductive constructors of rank 2. This gives an extension of Mendler’s system [19] to finite kinds. The generalized scheme for coinductive constructors is a new principle of programming with non-wellfounded datatypes.

The system MIt^{ω} is given as an extension of F^{ω} by wellkinded constructor constants μ_{κ} and ν_{κ}, welltyped term constants in_{κ}, GIt_{κ}, out_{κ} and GCoit_{κ} for every kind κ, and new term reduction rules.

Inductive constructors. Let κ = κ → ∗ and κ′ = κ → κ.

Formation. μ_{κ} : (κ → κ) → κ
Introduction. in_{κ} : ∀F^{κ→κ}. F (μ_{κ}F) ⊆_{κ} μ_{κ}F
Elimination. GIt_{κ} : ∀F^{κ→κ}∀H^{κ′}∀G^{κ}. (∀X^{κ}. X ≤^{H} G → F X ≤^{H} G) → μ_{κ}F ≤^{H} G
Reduction. GIt_{κ} s f (in_{κ} t) ⟶_{β} s (GIt_{κ} s) f t

with |f| = |κ|.

Coinductive constructors. Let κ = κ → ∗ and κ′ = κ → κ.

Formation. ν_{κ}  : (κ → κ) → κ
Elimination. out_{κ} : ∀F^{κ→κ}. ν_{κ}F ⊆_{κ} F (ν_{κ}F)
Introduction. GCoit_{κ} : ∀F^{κ→κ}∀H^{κ′}∀G^{κ}. (∀X^{κ}. G ^{H}≤ X → G ^{H}≤ F X) → G ^{H}≤ ν_{κ}F
Reduction. out_{κ} (GCoit_{κ} s f t) ⟶_{β} s (GCoit_{κ} s) f t

with |f| = |κ|.

Notice that for every constructor F of kind κ → κ, μ_{κ}F is a constructor of kind κ. In Mendler’s original system [19] as well as its variant for the treatment of primitive (co-)recursion [18], always positivity of F is required which is a very natural concept in the case κ = ∗. However, for higher kinds, there does not exist such a canonical syntactic restriction. Anyway, in [21] it has been observed that, in order to prove strong normalization, there is no need for the restriction to positive inductive types—an observation which has been the cornerstone for the treatment of monotone inductive types in [16] and becomes even more useful for our higher-order nested datatypes.

As for F^{ω}, denote the term closure of the reduction rules by ⟶ and its transitive closure by ⟶^{+}.

3.3 Mendler-style (Co)Iteration for (Co)Inductive Types

In the case κ = ∗, the rules for μ_{κ} and ν_{κ} match with Mendler’s [19], except for our removal of the positivity condition and our choice of Curry-style typing:

Inductive types.

Formation. μ_{∗} : (∗ → ∗) → ∗
Introduction. in_{∗} : ∀F^{∗→∗}. F (μ_{∗}F) → μ_{∗}F
Elimination. GIt_{∗} : ∀F^{∗→∗}∀Y^{∗}. (∀X^{∗}. (X → Y) → F X → Y) → μ_{∗}F → Y
Reduction. GIt_{∗} s (in_{∗} t) ⟶_{β} s (GIt_{∗} s) t

Coinductive types.

Formation. ν_{∗}  : (∗ → ∗) → ∗
Elimination. out_{∗} : ∀F^{∗→∗}. ν_{∗}F → F (ν_{∗}F)
Introduction. GCoit_{∗} : ∀F^{∗→∗}∀Y^{∗}. (∀X^{∗}. (Y → X) → Y → F X) → Y → ν_{∗}F
Reduction. out_{∗} (GCoit_{∗} s t) ⟶_{β} s (GCoit_{∗} s) t

Relation to general recursion. Typed functional programming languages like ML and Haskell use recursive types instead of inductive and coinductive types and general recursion instead of strongly normalizing restrictions such as Mendler (co)iteration. General recursion can be introduced via a fixed-point combinator

\begin{matrix}fix : ∀A.(A → A) → A \\ fix s ⟶ s (fix s), \end{matrix}

from which the more common let rec f = r in t can be defined as let f = fix (λf. r) in t. A nice aspect of Mendler (co)iteration is that the reduction behaviour GIt_{∗} and GCoit_{∗} is almost identical to the one of fix. The only difference is that unfolding of GIt resp. GCoit is controlled by a guard “in” resp. “out”, which gets removed in the reduction step. Guarded unfolding of recursion is essential to strong normalization; similar setups can be found in other systems which facilitate type-based termination, e.g. [10, 1, 5].

In some sense GIt and GCoit are just restricted versions of fix, i. e., each rank-1 MIt^{ω} program translates (requiring minimal changes) into a Haskell program with the same meaning. For higher kinds κ, GIt_{κ} and GCoit_{κ} are not typable in the Hindley-Milner type systems of Haskell 98 and ML, but their reduction behaviour is still included in the one of fix. This suggests that one can code most naturally with GIt and GCoit, which we will demonstrate in the next subsection by some examples involving so-called nested or heterogeneous datatypes.

3.4 Programming with (Co)Inductive Constructors of Rank 2

Nested or non-uniform datatypes, i.e., inductive and coinductive constructors of rank 2 (more exactly, inductive and coinductive constructors induced by constructors of rank 2), arise in our system as applications of μ_{κ1} and ν_{κ1} (recall that κ1 = ∗ → ∗ and κ2 = κ1 → κ1). We obtain the following instances from the general definitions.

Inductive constructors of rank 2.

Formation. μ_{κ1} : κ2 → κ1
Introduction. in_{κ1} : ∀F^{κ2}∀A. F (μ_{κ1}F) A → μ_{κ1}F A
Elimination. GIt_{κ1} : ∀F^{κ2}∀H^{κ1}∀G^{κ1}. (∀X^{κ1}. X ≤^{H} G → F X ≤^{H} G) → μ_{κ1}F ≤^{H} G
Reduction. GIt_{κ1} s f (in_{κ1} t) ⟶_{β} s (GIt_{κ1} s) f t

Coinductive constructors of rank 2.

Formation. ν_{κ1} : κ2 → κ1
Elimination. out_{κ1} : ∀F^{κ2}∀A. ν_{κ1}F A → F (ν_{κ1}F)A
Introduction. GCoit_{κ} : ∀F^{κ2}∀H^{κ1}∀G^{κ1}. (∀X^{κ1}. G ^{H}≤ X → G ^{H}≤ F X) → G ^{H}≤ ν_{κ1}F
Reduction. out_{κ1} (GCoit_{κ1} s f t) ⟶_{β} s (GCoit_{κ1} s) f t

An example of a structure which can be modeled by a nested datatype is lists of length 2^{n}, which are called powerlists [6] or perfectly balanced, binary leaf trees [11]. In our system, they are represented by the type transformer PList := μ_{κ1} PListF where PListF : κ2 := λF λA. A + F (A × A). The data constructors are given by

zero : ∀A. A → PList A  := λa. in_{κ1}(inl a)
succ : ∀A. PList(A × A) → PList A := λl. in_{κ1}(inr l)

Assume a type Nat of natural numbers with addition “+” and multiplication “×”, both written infix. Suppose we want to define a function sum : PList Nat → Nat which sums up all elements of a powerlist by iteration over its structure. The case sum (succ t) imposes some challenge, since sum cannot be directly applied to t : PList(Nat × Nat). The solution is to define a more general function sum′ by polymorphic recursion, which has the following behaviour.

sum′ : ∀A. (A → Nat) → PList A → Nat
sum′ f (zero a) ⟶^{+} f a
sum′ f (succ l) ⟶^{+} sum′ (λp. f (p.0) + f (p.1)) l

Here, the iteration process builds up a continuation f which in the end sums up the contents packed into a. From sum′, the summation function is obtained by sum := sum′ id.

The system MIt^{ω} has been designed so that functions like sum′ can be defined directly via generalized iteration. In our case, use the instantiations F := PListF and G := H := λ . Nat and define:

sum′ : μ_{κ1}F ≤^{H} G
sum′ := GIt_{κ1} λsum′λfλx. case (x, a. f a,
l. sum′ (λp. f (p.0) + f (p.1)) l)

The postulated reduction behaviour is verified by a simple calculation.

For another example consider the non-wellfounded version of perfectly balanced, binary (node-labelled) trees. They are represented by the type transformer BTree := ν_{κ1} BTreeF where BTreeF : κ2 := λF λA. A × F (A × A). The data destructors are

root : ∀A. BTree A → A  := λt. (out_{κ1}t).0
subs : ∀A. BTree A → BTree(A × A) := λt. (out_{κ1}t).1

We want to define the tree nats : BTree Nat filled with natural numbers starting with 1 breadth-first left-first. A more general function nats′ : ∀A. (Nat → A) → (Nat → BTree A) with the reduction behaviour

root(nats′ f n) ⟶^{+} f n
subs(nats′ f n) ⟶^{+} nats′ (λm. ⟨f (2 × m), f (2 × m + 1)⟩) n

is definable as a generalized coiteration by

nats′ := GCoit_{κ1} λnats′λfλn. ⟨f n, nats′ (λm. ⟨f (2 × m), f (2 × m + 1)⟩) n⟩

choosing F := BTreeF, G := H := λ . Nat. To obtain nats, one sets nats := nats′ id 1.

Higher-order representation of de Bruijn terms. Bird & Paterson [9] and Altenkirch & Reus [4] have shown that nameless untyped λ-terms can be represented by a heterogeneous datatype. As in the system GMIC of [2], this type is obtained in MIt^{ω} as the least fixed point of the monotone rank-2 constructor LamF.

LamF : κ2  := λF λA. A + (F A × F A + F (1 + A))
lamf : mon LamF := λsλf. either f (either (fork (s f)) (s (maybe f)))

The type Lam A again represents all de Bruijn terms with free variables in A, the constructors var, app and abs are simplified w. r. t. [2]. Again, we provide an auxiliary function weak which lifts each variable in a term to provide space for a fresh variable.

Lam : κ1  := μ_{κ1} LamF
lam : mon Lam  := GIt_{κ1} λmapλfλx. in_{κ1} (lamf map f x)
var : ∀A. A → Lam A  := λa. in_{κ1} (inl a)
app : ∀A. Lam A → Lam A → Lam A := λt_{1}λt_{2}. in_{κ1} (inr (inl ⟨t_{1}, t_{2}⟩))
abs : ∀A. Lam(1 + A) → Lam A  := λr. in_{κ1} (inr (inr r))
weak : ∀A. Lam A → Lam(1 + A)  := lam (λa. inr a)

The most natural question on this representation of untyped λ-calculus is the representability of substitution. With generalized iteration, it is possible to give a direct definition of substitution (the bind or extension operation of the lambda terms monad):

subst : ∀A∀B. (A → Lam B) → Lam A → Lam B ≡ Lam ≤^{Lam} Lam
subst := GIt_{κ1} λsubstλfλt. case (t,
a. f a, t′. case (t′,
p. app (subst f (p.0)) (subst f (p.1)),
r. abs (subst (lift f) r)),
lift : ∀A∀B. (A → Lam B) → (1 + A) → Lam (1 + B)
lift := λfλx. case (x, u. var (inl u), a. weak (f a))

Note that the formulation of generalized folds in [8] would yield the flattening function (the join or multiplication operation of the monad)

flatten : ∀A. Lam(Lam A) → Lam A.

We obtain flattening as special case of substitution by flatten := subst id.

Triangles. The dual of substitution for variables in a term or non-wellfounded term is redecoration of a non-wellfounded or wellfounded decorated tree, cf. [23]. An interesting and intuitive example of decorated tree types arising from a rank-2 coinductive constructor are triangles. Define

TriF := λEλF^{κ1}λA. A × F (E × A) : ⋆ → κ2
Tri := λE. ν_{κ1}(TriF E)  : ⋆ → κ1

Then Tri EA is the type of triangular tables of the sort

A E E E E …
A E E E …
A E E …
A E …
A …

decomposing into a scalar (an element of A) and a trapezium (an element of Tri E(E × A)). The destructors and the monotonicity witness are

top := λt. (out_{κ1} t).0 : ∀E∀A. Tri EA → A
rest := λt. (out_{κ1} t).1 : ∀E∀A. Tri EA → Tri E(E × A)
tri := GCoit_{κ1} λmapλfλx. ⟨f (top x), map (pair id f) (rest x)⟩ : ∀E. mon_{κ1}(Tri E)

Redecoration is an operation dual to substitution that takes a redecoration rule f (an assignment of B-decorations to A-decorated trees) and an A-decorated tree t, and returns a B-decorated tree t′. The return tree t′ is obtained from t by Bredecorating every node based on the A-decorated subtree it roots, as instructed by the redecoration rule. For streams, for instance redec : ∀A∀B. (Str A → B) → Str A → Str B) takes f : Str A → B and t : Str A and returns redec f t, which is a B-stream obtained from t by replacing each of its elements by what f assigns to the substream this element heads. Triangles are a generalization of streams much in the same way as de Bruijn notations for lambda terms differ from terms in the universal algebra style signature with one binary and one unary operator. For triangles, redecoration works as follows: In the triangle

A E E E E …
A E E E …
\underline{A} E E …
A E …
A …

the underlined A (as an example) gets replaced by the B assigned by the redecoration rule to the subtriangle cut out by the horizontal line; similarly, every other A is replaced by a B. This is straightforward to define using GCoit:

lift : ∀E∀A∀B. (Tri EA → B) → Tri E(E × A) → E × B
lift := λfλy. ⟨(top y).0, f (tri (λp. p.1) y)⟩
redec : ∀E∀A∀B. (Tri EA → B) → Tri EA → Tri EB
redec := GCoit_{κ1} λredecλfλx. ⟨f x, redec (lift f) (rest x)⟩

4 Embedding into System F^{ω}

In this section, we show how to embed MIt^{ω} into F^{ω}. The embedding establishes strong normalization for MIt^{ω}.

4.1 Kan extensions

For the sake of the embedding of MIt^{ω} into its subsystem F^{ω}, we use a syntactic version of Kan extensions, see [20, chapter 10]. Compared with [2], Kan extensions “along” are now defined for all kinds, not just for rank 1.

Right Kan extension along H. Let κ = κ → ∗ and κ′ = κ → κ and define for G : κ, H : κ′ and X : κ the type (Ran_{H} G) X by iteration on |κ|:

Ran G := G
(Ran_{H,H} G) XX := ∀Y^{κ_{1}}. X ≤ HY → (Ran_{H} (G Y)) X

Left Kan Extension along H. Let again κ = κ → ∗ and κ′ = κ → κ and define for F : κ, H : κ′ and Y : κ the type (Lan_{H} F)Y by iteration on |κ|:

Lan F := F
(Lan_{H,H} F) Y Y := ∃X^{κ_{1}}. HX ≤ Y × (Lan_{H} (F X)) Y

Proposition 1. Let F, G : κ → ∗ and H : κ → κ. The following pairs of types are logically equivalent:

1. F ≤^{H} G and ∀X^{κ}. F X → (Ran_{H} G)X.

2. F ^{H}≤ G and ∀Y^{κ}. (Lan_{H} F)Y → G Y .

Proof. Part 1 requires just a close look at the definition of ≤^{H}. Part 2 is only slightly more complicated. ⊓ ⊔

4.2 Embedding

We can simply define the new constants of MIt^{ω} in F^{ω}. Let κ = κ → ∗ and n := |κ|.

μ_{κ}  : (κ → κ) → κ → ∗
μ_{κ}  := λF^{κ→κ}λX^{κ}∀H^{κ→κ}∀G^{κ}. (∀X^{κ}. X ≤^{H} G → F X ≤^{H} G) → (Ran_{H} G)X
GIt_{κ} : ∀F^{κ→κ}∀H^{κ→κ}∀G^{κ}. (∀X^{κ}. X ≤^{H} G → F X ≤^{H} G) → μ_{κ}F ≤^{H} G
GIt_{κ} := λsλfλr. r s f
in_{κ} : ∀F^{κ→κ}∀X^{κ}. F (μ_{κ}F) X → μ_{κ}F X
in_{κ} := λtλsλf. s (GIt_{κ} s) f t
ν_{κ}  : (κ → κ) → κ → ∗
ν_{κ}  := λF^{κ→κ}λY^{κ}∃H^{κ→κ}∃G^{κ}. (∀X^{κ}. G ^{H}≤ X → G ^{H}≤ F X) × (Lan_{H} G)Y
GCoit_{κ} : ∀F^{κ→κ}∀H^{κ→κ}∀G^{κ}. (∀X^{κ}. G ^{H}≤ X → G ^{H}≤ F X) → G ^{H}≤ ν_{κ}F
GCoit_{κ} := λsλfλt. pack^{n+1} ⟨s, pack⟨f_{1}, …, pack⟨f_{n}, t⟩ …⟩⟩
out_{κ} : ∀F^{κ→κ}∀Y^{κ}. ν_{κ}F Y → F (ν_{κ}F) Y
out_{κ} := λr. open (r, r_{1}. open (r_{1}, r_{2}…. open (r_{n−1}, r_{n}. open (r_{n}, ft_{0}.
open (ft_{0}.1, ft_{1}. open (ft_{1}.1, ft_{2}…. open (ft_{n−1}.1, ft_{n}.
ft_{0}.0 (GCoit_{κ} ft_{0}.0) ft_{1}.0 … ft_{n}.0 ft_{n}.1) …)))) …))

Theorem 1 (Simulation). With the definitions above, the following reductions take place in F^{ω}:

GIt_{κ} s f (in_{κ} t)  ⟶^{+} s (GIt_{κ} s) f t
out_{κ} (GCoit_{κ} s f t) ⟶^{+} s (GCoit_{κ} s) f t

Proof. By easy computation.

Corollary 1 (Strong Normalization). System MIt^{ω} is strongly normalizing, i. e., there is no infinite reduction sequence r_{0} ⟶ r_{1} ⟶ r_{2} ⟶ … for any typable term r_{0}.

Proof. Use strong normalization of F^{ω} and simulation.

Since there are no critical pairs in MIt^{ω}, reduction is locally confluent; by strong normalization and Newman’s Lemma, it is confluent on well-typed terms.

5 Conclusion and Related Work

We have proposed MIt^{ω}, a system of generalized (co)iteration for arbitrary ranks, which turned out to be a definitional extension of Girard’s system F^{ω} and hence enjoys its good meta-theoretic properties, most notably strong normalization. It combines the ideas of Mendler for (co)inductive types with the notion of generalized folds for inductive constructors of rank 2 invented by Bird and Paterson.

MIt^{ω} has been carefully set up to come with a perspicuous computational behavior, which is very close to general recursion à la letrec—a distinctive feature of Mendler-style recursion schemes. For higher ranks, i.e., for the treatment of fixed-points which are themselves type transformers, we described a modified containment relation (via the index H) in order to encompass generalized folds, proposed by Bird and Paterson as a means of more elegant definitions of functions operating on nested datatypes.

Therefore, MIt^{ω} might serve as a basis of a total programming language for nested datatypes. Alternatively, it can be seen as a discipline of programming in existing languages like Haskell which gives termination guarantees for free.

Some related work. The generalized iteration scheme of the present article is a reformulation working in all finite ranks of generalized folds in the liberal sense of Sec. 4.1 and 6 of [8]. More exactly, it extends the “efficient” [11, 15] version of that scheme. The efficient generalized folds differ from the original generalized folds in the target type which is constructed with ≤^{H} rather than ⊆^{H}. Here, ⊆^{H} is the appropriate relativized version of ⊆, defined by

F ⊆^{H} G := ∀X^{κ}.F (HX) → GX.

Future work. The realm of higher-rank datatypes seems hardly explored. We certainly wish to try out our schemes on the examples of inductive constructors of rank 3 from [12]. Further, we seek to extend MIt^{ω} to cover other recursion schemes on nested datatypes like a form of “generalized primitive recursion”. This scheme, and others, would no longer have an operationally faithful embedding into System F^{ω}.

References

1. A. Abel. Termination checking with types. Technical Report 0201, Inst. für Informatik, Ludwigs-Maximilians-Univ. München, 2002.

2. A. Abel and R. Matthes. (Co-)iteration for higher-order nested datatypes. To appear in H. Geuvers, F. Wiedijk, eds., Post-Conf. Proc. of IST WG TYPES 2nd Ann. Meeting, TYPES’02, Lect. Notes in Comput. Sci., Springer-Verlag.

3. T. Altenkirch and C. McBride. Generic programming within dependently typed programming. To appear in J. Gibbons and J. Jeuring, Proc. of IFIP TC2 WC on Generic Programming, WCGP 2002, Kluwer Acad. Publishers.

4. T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In J. Flum and M. Rodríguez-Artalejo, eds., Proc. of 13th Int. Wksh. on Computer Science Logic, CSL’99, vol. 1683 of Lect. Notes in Comput. Sci., pp.53–468. Springer-Verlag, 1999.

5. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Math. Struct. in Comput. Sci., to appear.

6. R. Bird, J. Gibbons, and G. Jones. Program optimisation, naturally. In J. Davies, B. Roscoe, J. Woodcock, eds., Millenial Perspectives in Computer Science. Palgrave, 2000.

7. R. Bird and L. Meertens. Nested datatypes. In J. Jeuring, ed., Proc. of 4th Int. Conf. on Mathematics of Program Construction, MPC’98, vol. 1422 of Lect. Notes in Comput. Sci., pp. 52–67. Springer-Verlag, 1998.

8. R. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Aspects of Comput., 11(2):200–222, 1999.

9. R. Bird and R. Paterson. De Bruijn notation as a nested datatype. J. of Funct. Program., 9(1):77–91, 1999.

10. E. Giménez. Structural recursive definitions in type theory. In Proc. of 25th Int. Coll. on Automata, Languages and Programming, ICALP’98, vol. 1443 of Lect. Notes in Comput. Sci., pp. 397–408. Springer-Verlag, 1998.

11. R. Hinze. Efficient generalized folds. In J. Jeuring, ed., Proc. of 2nd Wksh. on Generic Programming, WGP 2000, Tech. Report UU-CS-2000-19, Dept. of Comput. Sci., Utrecht Univ., pp. 1–16. 2000.

12. R. Hinze. Manufacturing datatypes. J. of Funct. Program., 11(5): 493–524, 2001.

13. R. Hinze. Polytypic values possess polykinded types. Sci. of Comput. Program., 43(2–3):129–159, 2002.

14. C. B. Jay. Distinguishing data structures and functions: The constructor calculus and functorial types. In S. Abramsky, ed., Proc. of 5th Int. Conf. on Typed Lambda Calculi and Appl., TLCA’01, vol. 2044 of Lect. Notes in Comput. Sci., pp. 217–239. Berlin, 2001.

15. C. Martin, J. Gibbons and I. Bayley. Disciplined, efficient, generalised folds for nested datatypes. Submitted.

16. R. Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilians-Univ. München, 1998.

17. R. Matthes. Monotone inductive and coinductive constructors of rank 2. In L. Fribourg, ed., Proc. of 15th Int. Wksh. on Computer Science Logic, CSL 2001, vol. 2142 of Lect. Notes in Comput. Sci., pp. 600–614. Springer-Verlag, 2001.

18. N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proc. of 2nd Ann. IEEE Symp. on Logic in Computer Science, LICS’87, pp. 30–36. IEEE CS Press, 1987.

19. N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Ann. of Pure and Appl. Logic, 51(1–2):159–172, 1991.

20. S. Mac Lane. Categories for the Working Mathematician, vol. 5 of Graduate Texts in Mathematics, 2nd ed. Springer-Verlag, 1998.

21. T. Uustalu and V. Vene. A cube of proof systems for the intuitionistic predicate μ-, ν-logic. In M. Haveraaen and O. Owe, eds., Selected Papers from the 8th Nordic Wksh. on Programming Theory, NWPT ’96, Res. Rep. 248, Dept. of Informatics, Univ. of Oslo, pp. 237–246, 1997.

22. T. Uustalu and V. Vene. Coding recursion à la Mendler (extended abstract). In J. Jeuring, ed., Proc. of 2nd Wksh. on Generic Programming, WGP 2000, Tech. Rep. UU-CS-2000-19, Dept. of Comput. Sci., Utrecht Univ., pp. 69–85. 2000.

23. T. Uustalu and V. Vene. The dual of substitution is redecoration. In K. Hammond and S. Curtis, eds., Trends in Funct. Programming 3, pp. 99–110. Intellect, 2002.

A System F^{ω}

In the following we present Curry-style system F^{ω} enriched with binary sums and products, unit type and existential quantification over constructors. Although we choose a human-friendly notation of variables, we actually mean the nameless version à la de Bruijn which identifies α-equivalent terms. (Capture-avoiding) Substitution of an expression e for a variable x in expression f is denoted by f[x := e].

Kinds are generated from the kind ∗ for types by the binary function kind constructor →:

κ ::= ∗ | κ → κ′

Constructors. (Denoted by uppercase letters.) Metavariable X ranges over an infinite set of constructor variables.

\begin{aligned}A, B, C, F, G & ::= & X | λX^{κ}.F | F G | ∀F^{κ}. A | ∃F^{κ}. A | A → B \\ & | & A + B | A × B | 1 \end{aligned}

Equivalence on constructors. Equivalence F = F′ for constructors F and F′ is given as the compatible closure of the following axiom.

(λX.F) G =_{β} F [X := G]

We identify constructors up to equivalence, which is a decidable relation due to normalization and confluence of simply-typed λ-calculus (where our constructors are the terms and our kinds are the types of that calculus).

Objects (Terms). (Denoted by lowercase letters) The metavariable x ranges over an infinite set of object variables.

r, s, t ::= x | λx.t | r s | inl t | inr t | case (r, x. s, y. t)
| ⟨⟩ | ⟨t_{0}, t_{1}⟩ | r.0 | r.1 | pack t | open (r, x. s)

Contexts. Variables in a context Γ are assumed to be distinct.

Γ ::= · | Γ, X^{κ} | Γ, x:A

Judgments. (Simultaneously defined)

Γ cxt  Γ is a wellformed context
Γ ⊢ F : κ F is a wellformed constructor of kind κ in context Γ
Γ ⊢ t : A t is a wellformed term of type A in context Γ

Wellformed contexts. Γ cxt

· cxt  {Γ cxt \atop Γ, X^{κ} cxt}  {Γ ⊢ A : ∗ \atop Γ, x:A cxt}

Wellkinded constructors. Γ ⊢ F : κ

{X^{κ} ∈ Γ  Γ cxt \atop Γ ⊢ X : κ}  {Γ, X^{κ} ⊢ F : κ′ \atop Γ ⊢ λX^{κ}.F : κ → κ′}  {Γ ⊢ F : κ → κ′  Γ ⊢ G : κ \atop Γ ⊢ F G : κ′}

{Γ, X^{κ} ⊢ A : ∗ \atop Γ ⊢ ∀X^{κ}. A : ∗}  {Γ, X^{κ} ⊢ A : ∗ \atop Γ ⊢ ∃X^{κ}. A : ∗}  {Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A → B : ∗}

{Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A + B : ∗}  {Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A × B : ∗}  {Γ cxt \atop Γ ⊢ 1 : ∗}

Welltyped terms. Γ ⊢ t : A

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

{Γ, X^{κ} ⊢ t : A \atop Γ ⊢ t : ∀X^{κ}.A}  {Γ ⊢ t : ∀X^{κ}.A  Γ ⊢ F : κ \atop Γ ⊢ t : A[X := F]}

{Γ ⊢ t : A[X := F]  Γ ⊢ F : κ \atop Γ ⊢ pack t : ∃X^{κ}.A}  {Γ ⊢ r : ∃X^{κ}.A  Γ, X^{κ}, x:A ⊢ s : C \atop Γ ⊢ open (r, x. s) : C}

{Γ cxt \atop Γ ⊢ ⟨⟩ : 1}  {Γ ⊢ t : A  Γ ⊢ B : ∗ \atop Γ ⊢ inl t : A + B}  {Γ ⊢ t : B  Γ ⊢ A : ∗ \atop Γ ⊢ inr t : A + B}

{Γ ⊢ r : A + B  Γ, x:A ⊢ s : C  Γ, y:B ⊢ t : C \atop Γ ⊢ case (r, x. s, y. t) : C}

{Γ ⊢ t_{0} : A_{0}  Γ ⊢ t_{1} : A_{1} \atop Γ ⊢ ⟨t_{0}, t_{1}⟩ : A_{0} × A_{1}}  {Γ ⊢ r : A_{0} × A_{1} i ∈ \{0, 1\} \atop Γ ⊢ r.i : A_{i}}

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

(λx.t) s  ⟶_{β} t[x := s]
case (inl r, x. s, y. t) ⟶_{β} s[x := r]
case (inr r, x. s, y. t) ⟶_{β} t[y := r]
⟨t_{0}, t_{1}⟩.i ⟶_{β} t_{i} if i ∈ {0, 1}
open (pack t, x. s) ⟶_{β} s[x := t]

We denote the transitive closure of ⟶ by ⟶^{+} and the reflexive-transitive closure by ⟶^{∗}.

The defined system is a conservative extension of system F^{ω}. Reduction is type-preserving, confluent and strongly normalizing.