Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes

Andreas Abel^{a,∗}, Ralph Matthes^{b}, Tarmo Uustalu^{c}

aDepartment of Computer Science, Chalmers University of Technology Rännvägen 6, SWE-41296 Göteborg, Sweden

bInstitut für Informatik der Ludwig-Maximilians-Universität München Oettingenstraße 67, D-80538 München, Germany

cInstitute of Cybernetics, Tallinn Technical University Akadeemia tee 21, EE-12618 Tallinn, Estonia

Abstract

This article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration and coiteration constructions to support as primitive. We propose and compare several well-behaved extensions of System F^{ω} with some form of iteration and coiteration uniform in all kinds. In what we call Mendler-style systems, the iterator and coiterator have a computational behavior similar to the general recursor, but their types guarantee termination. In conventional-style systems, monotonicity witnesses are used for a notion of monotonicity defined uniformly for all kinds. Our most expressive systems GMIt^{ω} and GIt^{ω} of generalized Mendler resp. conventional (co)iteration encompass Martin, Gibbons and Bailey’s efficient folds for rank-2 inductive types. Strong normalization of all systems considered is proved by providing an embedding of the basic Mendler-style system MIt^{ω} into System F^{ω}.

Key words: Higher-Order Datatypes, Generalized Folds, Efficient Folds, Iteration, Coiteration, System F^{ω}, Higher-Order Polymorphism, Strong Normalization

∗ Corresponding author.

Email addresses: abel@cs.chalmers.se (Andreas Abel),

matthes@informatik.uni-muenchen.de (Ralph Matthes), tarmo@cs.ioc.ee

(Tarmo Uustalu).

Preprint submitted to Theoretical Computer Science 27 March 2004

1 Introduction and Overview

This article studies the implementation of higher-order inductive and coinductive constructors in the setting of typed rewriting. For introducing inductive and coinductive types to typed lambda calculi, there are several well-known non-controversial solutions. (Co)inductive types can be either added to firstorder simply typed lambda calculus together with (co)iteration or primitive (co)recursion, or alternatively, (co)inductive types with (co)iteration may be encoded in System F. The systems so obtained are all well-behaved. In particular, typed terms are strongly normalizable.

But besides inductive and coinductive types, in programming, one can also encounter inductive and coinductive constructors of higher kinds. In the mathematics of program construction community, there is a line of work devoted to programming with nested datatypes, or second-order inductive constructors, which are least fixed-points of type transformer transformers. Therefore, basically, a nested datatype is a datatype with a type parameter, hence a family of datatypes. But all of the family members are simultaneously defined by an inductive definition, parametrically uniformly in the argument type by which the family is indexed. Note that this does not include definitions of a family of types by iteration on the build-up of the argument type, but it does allow a reference in the definition of the type, indexed by A, to the family member, indexed by, say 1 + A, for all types A.

Therefore, the notion of nested datatype is more liberal than that of a family of inductive datatypes where each family member can be fully understood in isolation from the rest of the family. The typical example of this simpler situation is the regular datatype constructor List, where, for any type A, the type List A of finite lists of elements taken from A, is a separate inductive datatype. Clearly, List can also be viewed as a quite trivial nested datatype. What interests us, however, are nested datatypes whose family members are interwoven. Interesting examples of these nested datatypes, studied in the literature, include perfectly balanced trees, red-black trees, trie data structures and syntax with variable binding. As early as 1998, Hinze employs nested datatypes for efficient data structures. Hinze (2001) gives a more detailed explanation how these datatypes are constructed. This includes a nested datatype for red-black trees, where the invariants of red-black trees are ensured by the types—unlike the implementation of the operations for red-black trees of Okasaki (1999b). Kahrs (2001) shows that—with some refinement—one can even get back the efficiency of Okasaki’s implementation, despite this additional guarantee. Hence, nested datatypes provide more information on the stored data, while they need not slow down computation.

There already exist—see Section 9 for more bibliographical details—several

Sec. System Description  Page
2  F^{ω}  Higher-order polymorphic λ-calculus  7
3  MIt^{ω}  Mendler Iteration  15
4  GMIt^{ω} Generalized Mendler Iteration  28
5  \underline{It}^{ω}  Basic conventional Iteration  35
6  It_{=}^{ω}  Conventional Iteration along the identity (=)  44
MIt_{=}^{ω}  Mendler Iteration along the identity (=)
7  GIt^{ω}  Generalized conventional Iteration  49
8  Advanced examples  54
9  efold  efficient folds  60
10 Related and future work  69
11 Conclusion  74

Table 1 Contents

suggestions concerning useful and well-behaved combinators for programming with them, which are different versions of folds, or iteration—demonstrating that, in higher kinds, it is not at all obvious what iteration should mean. Unfortunately, however, these works do not provide or hint at answers to questions central in rewriting such as reduction behaviours and, in particular, termination. This is because, in functional programming, the main motivation to program in a disciplined fashion (e.g., to program with structured (co)recursion combinators rather than with unstructured general recursion) is to be able to construct programs or optimize (e.g., deforest) them “calculationally”, i.e., by means of equational reasoning.

In the typed lambda calculi and proof assistants communities, the motivation to rest on structured (co)recursion is more foundational—to ensure totality of definable functions or termination of typed programs, which, in systems of dependent types, is vital for type-checking purposes. This suggests the following research programme: take the solutions proposed within the functional programming community and see whether they solve the rewriting problems as well or, if they do not, admit elaborations which do. Another natural goal is to strive for solutions that scale up to higher-order (co)inductive constructors.

Contents. Table 1 displays the organization of the remainder of this article. In Section 2, we recapitulate System F^{ω} of higher-order polymorphism as a type assignment system for the λ-calculus with pairing (products), tagging (disjoint sums) and packing (existentials). In the following sections, we extend The Systems and their Interrelationship

\xymatrix{ & It_{=}^{ω} \ar@{=>}[d]^{7} \ar@{-->}[dddr]_{a} \ar[r]|{6} & MIt_{=}^{ω} \ar@{=>}[d]^{6} \\ efold \ar[r]^{9} & _{GIt_{ω}} \ar[r]^{7} & _{GMIt_{ω}} \ar[l]^{7} \ar[d]^{4} \ar@{-->}[dd]^{b} \\  & _{\underline{It}_{ω}} \ar[r]^{5} & _{MIt_{ω}} \ar@{.>}[l]^{5} \ar[d]^{3} \\  &  & F^{ω}}

Legend: [figure: n; special case of (see Section n); n; definable in (see Section n); 5; embeddable into (see Section 5); a; direct definition (Abel and Matthes, 2003); b; direct definition (Abel, Matthes, and Uustalu, 2003)]

Figure 1. Overview

F^{ω} by constants for inductive and coinductive constructors for arbitrary finite kinds together with iteration and coiteration schemes. Each scheme gives rise to a separate system which is named after its iterator. In the following, we will only talk about inductive constructors and iteration, although all systems support the dual concepts of coinductive constructors and coiteration as well. The superscript ^{ω} indicates that inductive constructors of all higher kinds are available, which holds for all of our own systems, defined in sections 3–7.

Section 3 starts with an introduction to iteration à la Mendler for the firstorder case, i.e., inductive types. The transfer of the central ideas to higher kinds by substituting natural transformations for functions results in the basic higher-order Mendler-style system MIt^{ω} which is embeddable into F^{ω} and generic enough to simulate all other systems. Figure 1 displays all embeddings carried out in the article. An arrow from A to B states that system A can be embedded into system B such that typing and reduction (i.e., computation) in system A are simulated in system B. The arrow styles indicate how direct the embedding is.

• A simple arrow from A to B, like from MIt^{ω} to F^{ω}, states that the new constants of system A, which form, introduce and eliminate inductive constructors, can be defined as terms of system B. Hence, system A simply provides new notation for existing constructs of system B. One also speaks of a shallow embedding.

• In contrast, a dotted arrow indicates a deep embedding. This means, all expressions of the source system have to be translated into appropriate expressions of the target system to simulate typing and reduction.

• Finally, the most direct embedding is displayed as a double arrow from A to B, meaning that system A is simply a restriction of system B. Consequently, the corresponding translation is the identity.

As Figure 1 illustrates, all other systems are definable in MIt^{ω}. But when it comes to practical usability, this system does not satisfy all wishes. As we will see in examples later, many programming tasks require a special pattern, namely Kan extensions, to be used in conjunction with Mendler iteration. Therefore, we have formulated the scheme of generalized Mendler iteration GIt^{ω} with hard-wired Kan extensions, presented in Section 4. The attribute generalized has been chosen in resemblance of Bird and Paterson’s (1999a) generalized folds. System GMIt^{ω} has been first described in a previous publication (Abel, Matthes, and Uustalu, 2003) where a direct embedding into F^{ω} is given.

By now, the question how to generalize Mendler iteration—which resembles programming with general recursion—to higher kinds seems to be answered sufficiently. But what about conventional iteration, which is motivated by the view of inductive types as initial algebras in category theory? Can conventional iteration be generalized to higher kinds in the same way as Mendler iteration? What is the precise relationship of Mendler iteration and conventional iteration for higher kinds? These questions are addressed in the sections 5–7.

Conventional iteration can be formulated for types which are obtained as the least fixed point of a monotone type transformer. A crucial task in finding conventional iterators for higher kinds will therefore be the formulation of higher-rank monotonicity. Section 5 investigates the most basic notion: A type constructor is monotone if it preserves natural transformations. The resulting system, \underline{It}^{ω}, is sufficiently strong to simulate Mendler iteration via a deep embedding, but the notion of monotonicity lacks important closure properties. Hence, a refined notion of monotonicity, which uses Kan extensions along the identity, is put forth in Section 6. The induced System It_{=}^{ω} has been treated before (Abel and Matthes, 2003). It is definable in F^{ω}, but also in terms of

Sec. No. Example  System(s)  Page
2  1 Booleans: true, false, if  F^{ω}  12
2 Maybe: bind  F^{ω} + patterns  14
3  3 Lists: map  Haskell  15
4 Lists: map  MIt^{ω}  17
5 Streams: head and tail  MIt^{ω}  18
6 Streams: upfrom  MIt^{ω}  18
7 Powerlists: get  MIt^{ω}  21
8 Powerlists: sum  MIt^{ω}  22
9 Infinite triangles: decomposition MIt^{ω}  24
10 Streams: redecoration  Haskell  25
11 Infinite triangles: redecoration MIt^{ω}  25
4 12 Powerlists: sum  GMIt^{ω}  31
13 Bushes: sum  GMIt^{ω}  31
14 Infinite Triangles: redecoration GMIt^{ω}  32
5 15 Powerlists: sum  \underline{It}^{ω}  37
6 16 De Bruijn terms: map  It_{=}^{ω}  47
17 Powerlists: reverse  It_{=}^{ω}  48
7 18 Powerlists: sum  GIt^{ω}  50
19 De Bruijn terms: substitution  GIt^{ω}  51
8 20 De Bruijn + expl. subst.: map It_{=}^{ω}  54
21 De Bruijn + expl. subst.: eval  It_{=}^{ω}  56
22 Finite triangles: redecoration  \underline{It}^{ω}, GMIt^{ω}, MIt^{ω}  56
9 23 Hofunctors  efold  61
24 Powerlists: efold (Typing)  GIt^{ω}  63
25 Powerlists: sum (Typing)  efold  64
26 Powerlists: efold (Reduction)  GIt^{ω}  64
27 Powerlists: sum (Reduction)  efold  65
28 De Bruijn terms: efold  GIt^{ω}  65
29 De Bruijn terms: substitution  efold  66

Table 2 Overview of examples

Mendler iteration via a cut-down version of GMIt^{ω}, called MIt_{=}^{ω}, which only uses Kan extensions along the identity. As shown in loc. cit., programming in It_{=}^{ω} often requires a second layer of Kan extensions. This flaw is remedied in System GIt^{ω}, the conventional counterpart of generalized Mendler iteration.

After completing the definition of our systems, some more examples demonstrate the applicability of the different iteration schemes for different purposes (Section 8). The remainder of the article is devoted to related work. Section 9 compares our work with iteration schemes for nested datatypes found in the literature. Special attention is given to the efficient folds of Martin, Gibbons, and Bayley (2003); a type-theoretic adaptation of their work is shown to be definable in System GIt^{ω}. Section 10 relates this work to generic and dependently typed programming, type classes and other trends in functional programming and type theory. Finally, the main contributions of this article are summarized in Section 11.

Examples form an important part of the article since they allow an intuitive comparison of the expressiveness of the systems. Therefore, the same programming tasks are dealt with several times. Table 2 contains a complete list of examples together with the system in which they have been implemented. Our running example is summation for powerlists which is has been defined in almost all of our systems. For the conventional iteration systems, most examples are centered around the representation of untyped de Bruijn-style lambda terms as a nested datatype.

Relation to our previous work. This article is an extended and reworked version of our conference paper (Abel, Matthes, and Uustalu, 2003) which mostly discussed system GMIt^{ω} (called MIt^{ω} in that article). New in this article are the basic systems MIt^{ω} and \underline{It}^{ω} as well as the discussion of GIt^{ω} and the definability of efficient folds within GIt^{ω}. The discussion of It_{=}^{ω} (a subsystem of GIt^{ω}) and some examples are taken from Abel and Matthes (2003). As in our previous work, the typing and reduction rules for iteration and coiteration are uniform in all kinds, in each of these systems.

2 System F^{ω}

Our development of higher-order datatypes takes place within the Curry-style version of system F^{ω}, extended with binary sums and products, unit type and existential quantification over type constructors. We employ the usual named-variables syntax, but identify α-equivalent expressions that is properly achieved in the nameless version à la de Bruijn. Capture-avoiding substitution of an expression e for a variable x in an expression f is denoted by f[x := e].

2.1 The Syntax

In System F^{ω}, there are three categories of expressions: kinds, type constructors and terms.

Kinds are generated from the kind ∗ for types by the binary function kind former →, and are denoted by the letter κ:

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

The rank of kind κ is denoted by rk(κ). We introduce abbreviations for some special kinds: k0 = ∗, types, k1 = ∗ → ∗, unary type transformers and k2 = (∗ → ∗) → (∗ → ∗) unary transformers of type transformers. Then, rk(ki) = i for i ∈ {0, 1, 2}.

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

Type constructors. (Denoted by uppercase latin letters.) Metavariable X ranges over an infinite set of type constructor variables.

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

Note that the type constructors are given in Curry style although quantification is written with kind annotation. This is because the semantics of the quantifiers needs the kind κ. The type ∀X^{κ}. A should be conceived as an abbreviation for ∀^{κ}λX.A where the lambda-abstracted variable is not kind annotated. Sometimes, “ ” will be used as name of a variable which never occurs free in a type constructor, hence we write λ .F for void abstraction.

Type constructor application associates to the left, i.e., F G H stands for (F G) H. For F⃗ = F_{1}, …, F_{n} a vector of constructors, we abbreviate F F_{1} … F_{n} as F F⃗. We write Id for λX.X and F ∘ G for λX. F (G X).

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_{1}, t_{2}⟩ | fst r | snd r | pack t | open (r, x. s)

Most term forms are standard; “pack” introduces and “open” eliminates existential quantification, see below. The term former fst, whenever it is used without argument, should be understood as the first projection function λx. fst x. This holds analogously for snd, inl, inr and pack. The identity λx.x will be denoted by id. We write f ∘g for the 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}.

Note that there is no distinguished form of recursion in the language of System F^{ω}. In the progression of this article, however, we will extend the system by different forms of iteration.

2.2 Kinding and Typing

In the following, we define judgments to identify the “good” expressions. All kinds are good by definition, but good type constructors need to be wellkinded and good terms need to be welltyped. As an auxiliary notion, we need to introduce contexts which record kinds resp. types of free variables.

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

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

Judgments. (The first two will be defined simultaneously, the third one based on these.)

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

Wellformed contexts. Γ cxt

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

Hence, contexts declare kinds for type variables and types (not arbitrary type constructors!) for object variables.

Wellkinded type constructors. Γ ⊢ F : κ

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

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

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

The rank of a type constructor is given by the rank of its kind. If no kinds are given and cannot be guessed from the context of discourse, we assume A, B, C, D : ∗, G, H, X, Y : k1 and F : k2. If the context is clear (by default, we take the empty context “·”), we write F : κ for Γ ⊢ F : κ. Sums and products can be extended to all kinds: For κ = κ⃗ → ∗ with |κ⃗| = |X⃗| = n, set

+^{κ} := λF λGλX⃗. F X⃗ + GX⃗ and ×^{κ} := λF λGλX⃗. F X⃗ × GX⃗.

Both these type constructors have kind κ → κ → κ. If no ambiguity arises, the superscript is omitted.

Equivalence on wellkinded type constructors. The notion of β-equivalence F = F′ for wellkinded type constructors F and F′ is given as the compatible closure (i.e. closure under all type constructor forming operations) of the following axiom.

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

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

As a consequence of this identification, wellkinded type constructor composition ∘ is associative.

Welltyped terms. Γ ⊢ t : A. The following chart recapitulates the typing rules for pure Curry-style F^{ω}.

\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 : A[X := F]}

More rules are needed for introduction and elimination of the System F^{ω} extensions: unit type, binary sum and product types, and existential types.

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

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

\frac{Γ ⊢ t_{1} : A Γ ⊢ t_{2} : B}{Γ ⊢ ⟨t_{1}, t_{2}⟩ : A × B}  \frac{Γ ⊢ r : A × B}{Γ ⊢ fst r : A}  \frac{Γ ⊢ r : A × B}{Γ ⊢ snd r : B}

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

As for wellkinded type constructors, we write t : A for Γ ⊢ t : A if the context is clear (by default, we again take the empty context “·”).

Logical equivalence. Let Γ ⊢ A : ∗ and Γ ⊢ B : ∗. We say A and B are logically equivalent in context Γ iff there are terms r, s such that Γ ⊢ r : A → B and Γ ⊢ s : B → A. If the context Γ is clear from the context of discourse, we just write A ↔ B for logical equivalence of A and B.

2.3 Operational Semantics

Terms of System F^{ω} denote functional programs whose operational meaning is given by the following reduction relation.

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 formers.^{1}

(λ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]
fst⟨t_{1}, t_{2}⟩  ⟶_{β} t_{1}
snd⟨t_{1}, t_{2}⟩  ⟶_{β} t_{2}
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.

Example 1 (Booleans) We can encode the datatype of booleans Bool : ∗ in System F^{ω} as Bool := 1 + 1, with data constructors true := inl⟨⟩ and false := inr⟨⟩. Elimination of booleans is done by if-then-else, which is encoded as if := λbλtλe. case (b, . t, . e). The reader is invited to check the typings true : Bool, false : Bool and if : Bool → ∀A. A → A → A as well as the operational behavior if true t e ⟶^{+} t and if false t e ⟶^{+} e.

2.4 Syntactic Sugar

The term language of System F^{ω} is concise and easy to reason about, but for programming, what we intend to do to a certain extent in this article, a little too spartan. To make programs more readable, we introduce let binding and pattern matching as a meta notation in this section. These new constructs should not be regarded as extensions to System F^{ω}; we formally describe a transformation relation ⇝ which eliminates all syntactic sugar.

Non-recursive let bindings. As implemented in some functional programming languages, e. g., Scheme or Ocaml, let x=r in s shall denote the β-redex (λx.s) r. This must not be confused with a recursive let; in our case, the variable x bound by let cannot be used in r. Formally, let-bindings can be removed

1 This means, we may apply one of the ⟶_{β}-rules to an arbitrary subterm of t in order to obtain one step of reduction. This especially includes the ξ-rule which says that t ⟶ t′ implies λx. t ⟶ λx. t′. Clearly, this rule is not implemented in the usual functional programming languages. Since we prove strong normalization, we are on the safe side.

from programs by performing the following transformation steps on any part of the program until no let-bindings remain.

let x=r in s ⇝ (λx.s) r

Pattern matching. Patterns are terms constructed from variables and introductions, except function type introduction (λ). Formally, they are given by the grammar

p ::= x | ⟨⟩ | ⟨p, p′⟩ | inl p | inr p | pack p.

We use shorthand notations for groups of similar patterns. For instance, inl p⃗ is an abbreviation for the list of patterns inl p_{1}, …, inl p_{n} where n = |p⃗|.

Pattern matching is introduced by the notation

match r with p_{1} ↦ s_{1} | … | p_{n} ↦ s_{n}.

The order of the clauses p_{i} ↦ s_{i} is irrelevant. For succinctness, we write match r with (p_{i} ↦ s_{i})_{i=1..n} or even match r with p⃗ ↦ s⃗, for short. The notation match r with p⃗ ↦ s⃗ | q⃗ ↦ t⃗ should also be easily understandable.

Pattern matching is expanded by the following new rules for the transformation relation ⇝. Patterns should only be used if they are well-typed, nonoverlapping, linear (no variable occurs twice) and exhaustive. We do not present a theory of patterns, but just have them as a meta-syntactic device. Therefore, we restrict the use of pattern matching to the situations where these transformation rules succeed in removing the syntactic sugar.

match r with x ↦ s  ⇝ let x=r in s
match r with ⟨⟩ ↦ s  ⇝ s

match r with (⟨p_{i}, p′_{j}⟩ ↦ s_{ij})_{i∈I,j∈J} ⇝ let x=r in

match (fst x) with

(p_{i} ↦ match (snd x) with

(p′_{j} ↦ s_{ij})_{j∈J})_{i∈I}

match r with inl p⃗ ↦ s⃗
| inr q⃗ ↦ t⃗

⇝

case (r, x. match x with p⃗ ↦ s⃗,
y. match y with q⃗ ↦ t⃗)
match r with pack p⃗ ↦ s⃗  ⇝ open (r, x. match x with p⃗ ↦ s⃗)

In the case of matching against pairs, I and J denote finite index sets. Note that a let expression has been inserted on the right hand side to avoid duplication of term r.

Patterns in lets and abstractions. For a single-pattern matching, which has the form match r with p ↦ s we introduce a more concise notation let p = r in s, which is common in functional programming. Furthermore, an abstraction of a variable x plus a matching over this variable, λx. let p=x in s, can from now be shortened to λp.s. In both cases, in order to avoid clashes with the existing syntax we need to exclude patterns p which consist just of a single variable. Formally, we add two transformation rules:

let p=r in s ⇝ match r with p ↦ s  if p is not a variable
λp. s  ⇝ λx. match x with p ↦ s if p is not a variable

Sugar for term abbreviations. In the course of this article, we will often define term abbreviations c of the form c := λx_{1} … λx_{n}. s with n ≥ 0. For such c, we allow the expression c^{∘}t⃗ to mean s[x⃗ := t⃗] where |t⃗| = n. In the special case that s is a pattern p, the sugared expression c^{∘}x⃗ is just p, and we can use it in a matching construct to increase readability of code.

In the next section, we will introduce a new term constant in^{κ} and data constructors of the shape c := λx⃗. in^{κ}p. The notation c^{−}t⃗ shall denote p[x⃗ := t⃗], i.e., instantiation after removal of “in^{κ}”. Summarizing, we have two additional transformations:

\begin{matrix}c^{∘}t⃗ & ⇝ & s[x⃗ := t⃗] & if c := λx⃗. s \\ c^{−}t⃗ & ⇝ & p[x⃗ := t⃗] & if c := λx⃗. in^{κ}p \end{matrix}

Example 2 (“Maybe” Type Transformer) To see the meta syntax in action, consider the option datatype with two data constructors:

Maybe := λA. 1 + A : k1
nothing := inl⟨⟩  : ∀A. Maybe A
just  := λa. inr a : ∀A. A → Maybe A

The type transformer Maybe is a monad with unit just and the following multiplication operation:

bind : ∀A∀B. Maybe A → (A → Maybe B) → Maybe B
bind := λmλk. match m with nothing^{∘} ↦ nothing | just^{∘} a ↦ k a

We could have dropped the annotation “^{∘}” in matching against “nothing^{∘}”— since “nothing” is a data constructor without arguments and the annotation “^{∘}” is changing nothing in this case—, but we included it for reasons of symmetry.

3 System MIt^{ω} of Basic Mendler Iteration and Coiteration

In this section, we will introduce System MIt^{ω}, a conservative extension of F^{ω}, which provides schemes of iteration and coiteration for higher-order datatypes, also called heterogeneous, nested or rank-n datatypes (n ≥ 2). But first we will recall Mendler iteration for first-order (resp. homogeneous or rank-1) types which we then generalize to higher ranks.

3.1 Mendler Iteration for Rank-1 Inductive Types

Recall a standard example for homogeneous inductive types: the type of lists List(A) : ∗ over some element type A, which has two data constructors nil : List(A) and cons : A → List(A) → List(A). Types like this one are called homogeneous because the argument to the type constructor List is invariant in the type of the data constructors. In our case the argument is always the fixed type A. We will later see examples of heterogeneous types where the argument A to the type constructor, call it T, varies in the different occurrences of T in the type of a data constructor. The argument A can even contain T itself; in this case we speak of truly nested datatypes.

We favor a view on inductive types that is motivated from category theory and goes back to Hagino (1987). List(A) is defined as the least fixed-point of an operator ListF(A) := λX. 1 + A × X and we write List(A) := μ(ListF(A)). There is just a single constructor in : ListF(A)(List(A)) → List(A) for lists. The functions nil and cons can be defined in terms of in:

nil := in (inl ⟨⟩)  : List(A)
cons := λaλas. in (inr ⟨a, as⟩) : A → List(A) → List(A)

To define operations on lists we need a means of recursion. In our theory all functions should be total, hence we restrict to a scheme which we call Mendler iteration for reasons that become apparent later. One function which falls into this scheme is the general-purpose function map.

Example 3 (Map Function for Lists) It is part of the Haskell standard library and could be defined like this:

    map :: (a -> b) -> [a] -> [b]
    map f = map'
        where map' []       = []
              map' (a : as) = (f a) : (map' as)

The recursive part of this definition is the interior function map' which arises as the fixed-point of a functional s = λmap′. <body of map'> such that the equation map' = s map' holds. (The name “s” stands for “step term”.) In general it is undecidable whether such fixed-point equations are uniquely solvable in total functions. But unique solvability can be guaranteed if the term s has a special shape. In our case, a recursive call of map' occurs only with argument “as” which is a direct subterm of the input (a : as). This already ensures termination of map'. Furthermore, the sublist “as” is only used as an argument to map', hence the function is even iterative.

Mendler (1991) first observed that by a certain polymorphic typing of the term s, one can determine the fixed-point of s to be an iterative function. The trick is to assign a fresh type X to the direct subcomponent “as” and restrict applications of the recursive function map' to arguments of this type. This has a twofold effect: Since X is a type we know nothing of, necessarily it holds that

(1) the component “as” can neither be further analyzed nor used in any way besides as an argument to map', and

(2) the function map' cannot be called recursively unless applied to “as”.

Mendler’s trick is implemented by requiring s to be of type (X → B) → ListF(A)X → B for a fresh type variable X. The first parameter of s is the name map′ for the recursive function whose application is now restricted to input of type X; the second parameter will later be bound to the term t of the input “in t” of map', but is now by its type ListF(A)X restricted to be either the canonical inhabitant ⟨⟩ of type 1—for the case of the empty list nil as input to map'—, or a pair of a head element of type A and a tail of type X—for the cons case. In the nil case, s somehow has to produce a result of type B, in the cons case, s can—among other possibilities—apply map′ to the tail in order to arrive at a result of type B.

We call the respective fixed-point combinator which produces iterative functions Mendler iterator—written MIt(s) for a step term s. It has the following reduction behavior:

MIt(s) (in t) ⟶_{β} s MIt(s) t

During reduction, the type variable X is substituted by the inductive type μF, in our example List(A). The fixed-point type μF is unrolled into F (μF), hence, the data constructor in is dropped. On the level of terms, this is exactly what distinguishes Mendler iteration from general recursion. The reduction can only take place when the data constructor “in” is present. This—and the fact that it is removed by reduction—makes “in” act as a guard for unrolling recursion and ensures strong normalization, as we will prove later.

Summing up, we can augment the higher-order polymorphic lambda-calculus with rank-1 iteration by adding the following constants, typing and reduction rules:

Formation.  μ : (∗ → ∗) → ∗
Introduction. in : ∀F^{∗→∗}. F (μF) → μF
Elimination.  \begin{matrix}Γ ⊢ F : ∗ → ∗ \\ Γ ⊢ B : ∗ \\ Γ ⊢ s : ∀X^{∗}. (X → B) → F X → B \\ Γ ⊢ MIt(s) : μF → B \end{matrix}

Reduction.  MIt(s) (in t) ⟶_{β} s MIt(s) t

Example 4 (Map Function for Lists) Using the syntax of F^{ω} with the meta-notation for pattern matching described in Section 2, we can encode the Haskell function map with Mendler iteration as follows:

map : ∀A∀B. (A → B) → List(A) → List(B)

map

:= λf. MIt (λmap′λt. match t with
nil^{−}  ↦ nil
| cons^{−}a as ↦ cons (f a) (map′ as))

In the following we give an assignment of bound variables to types from which one can infer that map is well-typed.

f  : A → B
map′ : X → List(B)
t  : ListF(A) X
a  : A
as  : X

Here, X : ∗ is a fresh type variable introduced by the Mendler iterator. Also note that, according to the conventions introduced in Section 2, nil^{−} = inl⟨⟩ and cons^{−}a as = inr⟨a, as⟩. The ^{−}-notation discards the general constructor in for inductive types, which is necessary since the Mendler iterator takes an argument t of the unfolded inductive type.

3.2 Mendler Coiteration for Rank-1 Coinductive Types

In the previous section, we considered least fixed points of recursive type equations. If we consider greatest fixed points instead, we obtain coinductive types νF which are dual to inductive types in the category-theoretic sense. Hence, obtaining rules for Mendler-style coinductive types is a matter of reversing some arrows.

Formation.  ν : (∗ → ∗) → ∗
Elimination.  out : ∀F^{∗→∗}. νF → F (νF)

Introduction.

Γ ⊢ F : ∗ → ∗
Γ ⊢ A : ∗
Γ ⊢ s : ∀X^{∗}. (A → X) → A → F X
Γ ⊢ MCoit(s) : A → νF
Reduction.  out (MCoit(s) t) ⟶_{β} s MCoit(s) t

Dually to the general constructor in for inductive types, coinductive types possess a general destructor out which triggers unrolling of the coiterator MCoit in the reduction rule. Since elements of coinductive types can be infinite objects, they need to be constructed by a recursive process—this gives some intuition why coinductive types are introduced by the coiterator.

Example 5 (Streams) The most popular coinductive type is the type of infinite streams over some element type. In the system of Mendler coiteration, it can be defined as follows:

Stream := λA. ν(λX. A × X) : ∗ → ∗
head := λr. fst (out r)  : ∀A. Stream A → A
tail := λr. snd (out r)  : ∀A. Stream A → Stream A

Example 6 (Sequence of Natural Numbers) Assume a type Nat of natural numbers with addition “+” and numerals 0, 1, 2, . . .. We can define the sequence of all natural numbers starting at a number n as a stream using Mendler coiteration:

upfrom := MCoit(λupfromλn. ⟨n, upfrom (n + 1)⟩)
: Nat → Stream Nat

3.3 Heterogeneous Datatypes

In contrast to the polymorphic types given in the previous sections, there are recursive type constructors whose arguments vary in different occurrences in their defining equation. For instance, consider the following Haskell types:

    data PList a = Zero a | Succ (PList (a, a))
    data Bush  a = Nil    | Cons a (Bush (Bush a))

    data Lam   a = Var a  | App (Lam a) (Lam a)
                         | Abs (Lam (Maybe a))

The first definition, PList, is the type of powerlists (Bird et al., 2000) resp. perfectly balanced, binary leaf trees (Hinze, 2000a). Notice that the argument to the type transformer PList on the right hand side is not simply the type variable “a”, but (a, a) which is the Haskell notation for the Cartesian product a × a. This is why PList is called a heterogeneous or nested type in contrast to homogeneous or non-nested types like List where in the definition the argument is always the same type variable.

The second line defines “bushes” (Bird and Meertens, 1998) which are like lists except that the element type gets bigger as we are traversing the list from head to tail. On the right hand side of the defining equation the type transformer Bush occurs as part of the argument to itself. We will speak of a type with this property as a truly nested type, in contrast to the term nested type which in the literature denotes just any heterogeneous type.

Finally, the third type Lam a is inhabited by de Bruijn representations of untyped lambda terms over a set of free variables “a”. This type has been studied by Altenkirch and Reus (1999) and Bird and Paterson (1999b); a precursor of this type has been considered already by Pfenning and Lee (1989) and Pierce et al. (1989). The constructor for lambda-abstraction Abs expects a term over the extended set of free variables Maybe a, which is the Haskell representation of the sum type 1 + a. The disjoint sum reflects the choice for a bound variable under the abstraction: either it is the variable freshly bound (left injection into the unit set “1”) or it is one of the variables that have been available already (right injection into “a”).

We notice that all of the datatypes PList, Bush, Lam are first-order as type constructors: they are of kind ∗ → ∗. It is possible, of course, also to combine nestedness and higher-orderness, but this combination does not happen in these three examples. Moreover, we do not find this combination very important conceptually, as the challenges are not in the kinds of the parameters of a datatype, but in the kind of the μ-operator employed.

We will encounter all these three datatypes in examples later. For now we are interested in encoding these types in a suitable extension of F^{ω}. The encoding is possible if a combinator μ^{k1} : (k1 → k1) → k1 for least fixed-point types of rank 1 is present. (Recall that k1 = ∗ → ∗.) In the following we give representations of these three types as least fixed points μF of type transformer transformers F : k2.

PListF := λXλA. A + X (A × A)  : k2
PList := μ^{k1} PListF  : k1
BushF := λXλA. 1 + A × X (X A)  : k2
Bush := μ^{k1} BushF  : k1
LamF := λXλA. A + (X A × X A + X (1 + A)) : k2
Lam := μ^{k1} LamF  : k1

Similarly to the rank-1 case we just have one general datatype constructor in^{k1} which rolls an inhabitant of F (μ^{k1}F) into the fixed point μ^{k1}F. Note, however, that μ^{k1}F is not a type but a type constructor, hence, we need a polymorphic data constructor in^{k1} : ∀A. F (μ^{k1}F) A → μ^{k1}F A. Now, we are ready to define the usual data constructors for the heterogeneous datatypes we are encoding:

zero := λa. in^{k1} (inl a)  : ∀A. A → PList A
succ := λl. in^{k1} (inr l)  : ∀A. PList(A × A) → PList A
bnil := in^{k1} (inl ⟨⟩)  : ∀A. Bush A
bcons := λaλb. in^{k1} (inr ⟨a, b⟩)  : ∀A. A → Bush (Bush A) → Bush A
var := λa. in^{k1} (inl a)  : ∀A. A → Lam A
app := λt_{1}λt_{2}. in^{k1} (inr (inl ⟨t_{1}, t_{2}⟩)) : ∀A. Lam A → Lam A → Lam A
abs := λr. in^{k1} (inr (inr r))  : ∀A. Lam (1 + A) → Lam A

Our aim is to define iteration for nested datatypes, a quest which recently has attracted some interest in the functional programming community (Bird and Paterson, 1999a; Hinze, 2000a; Martin, Gibbons, and Bayley, 2003). In the remainder of this section we will show how to generalize Mendler iteration to higher ranks and point out some difficulties with this approach. In the remainder of this article we will present refined iteration schemes which overcome the shortcomings of plain Mendler iteration.

3.4 Mendler Iteration for Higher Ranks

To generalize Mendler iteration from types to type constructors, we introduce a syntactic notion of natural transformations F ⊆^{κ} G from type constructor F : κ to G : κ. Since every kind κ can be written in the form κ⃗ → ∗, natural transformations for kind κ can simply be defined as follows:

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

(Here, we have made use of the vector notation ∀X⃗κ⃗ as an abbreviation for ∀X_{1}^{κ_{1}} … ∀X_{n}^{κ_{n}} where n = |X⃗|.)

For types F, G : ∗, the type F ⊆^{∗} G of natural transformations from F to G is just the ordinary function type F → G. As an example, we observe that the general constructor in^{k1} from the last subsection is a natural transformation of type F (μ^{k1}F) ⊆^{k1} μ^{k1}F. The superscript κ in “⊆^{κ}” will sometimes be omitted for better readability.

Generalizing Mendler iteration to higher kinds κ is now just a matter of replacing some arrows by natural transformations. We obtain the following family of constants, typing and reduction rules, indexed by κ.

Formation.  μ^{κ} : (κ → κ) → κ
Introduction. in^{κ} : ∀F^{κ→κ}. F (μ^{κ}F) ⊆^{κ} μ^{κ}F
Elimination.  \begin{matrix}Γ ⊢ F : κ → κ, \\ Γ ⊢ G : κ \\ Γ ⊢ s : ∀X^{κ}. X ⊆^{κ} G → F X ⊆^{κ} G \\ Γ ⊢ MIt^{κ}(s) : μ^{κ}F ⊆^{κ} G \end{matrix}

Reduction.  MIt^{κ}(s) (in^{κ} t) ⟶_{β} s MIt^{κ}(s) t

Notice that for every type constructor F of kind κ → κ, μ^{κ}F is a type constructor of kind κ. In Mendler’s original system (Mendler, 1991) as well as its variant for the treatment of primitive (co-)recursion (Mendler, 1987), positivity of F is always required, which is a very natural concept in the case κ = ∗. (A first-order type constructor F : ∗ → ∗ is said to be positive iff every occurence of X in F X is positive in the sense of being enclosed in an even number of left-hand sides of →.) For higher kinds, however, there is no such canonical syntactic restriction. Anyway, in Uustalu and Vene (1997) 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 Matthes (1998) and becomes even more useful for higher-order datatypes.

It remains to show that we have obtained a sensible system. Subject reduction is easy to check for the new reduction rule; confluence is not jeopardized since there are no critical pairs; and strong normalization will be shown later by an embedding into F^{ω}. In the following we will try to evaluate whether with MIt^{κ} we have obtained a sensible and usable device for programming.

Example 7 (Retrieving a Leaf of a Perfectly Balanced Tree) Let t : PList A be a binary leaf-labelled tree and p : Stream Bool a bit stream which acts as a path to one of the leaves a of t. Using MIt^{k1} we can implement a function get such that get t p retrieves element a.

get :=

MIt^{k1}(λget λt λp. match t with
zero^{−} a ↦ a
| succ^{−} l ↦ let ⟨a_{1}, a_{2}⟩ = get l (tail p) in
if (head p) a_{1} a_{2})
: ∀A. PList A → Stream Bool → A
= PList ⊆^{k1} (λA. Stream Bool → A)

Here we reused the type of streams defined in Example 5 and the booleans defined in Section 2. To verify welltypedness, observe that the bound variables have the following types:

X  : k1 (not visible due to Curry-style)
get  : ∀A. X A → Stream Bool → A
A  : ∗ (not visible due to Curry-style)
t  : PListF X A = A + X (A × A)
p  : Stream Bool
a, a_{1}, a_{2} : A
l  : X (A × A)

In the recursive calls, the polymorphic type of get is instantiated with the product A × A which entails the typing get l (tail p) : A × A. It is now easy to check welltypedness of the whole function body. Note that MIt^{k1} facilitates a kind of polymorphic recursion.

Example 8 (Summing up a Powerlist) Next, we want to define a function sum : PList Nat → Nat which sums up all elements of a powerlist by iteration over its structure. In the case sum (zero n) we can simply return n. The case sum (succ t), however, 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 behavior.

sum′ : ∀A. PList A → (A → Nat) → Nat
sum′ (zero a) f ⟶^{+} f a
sum′ (succ l) f ⟶^{+} sum′ l (λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2})

Here, the iteration process builds up a “continuation” f which in the end sums up the contents packed into a. Having found out the desired behavior of sum′, its implementation using MIt^{k1} is a mechanical process which results in the following definition:

sum′ := MIt^{k1}(λsum′λtλf. match t with
zero^{−} a ↦ f a
| succ^{−} l ↦ sum′ l (λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2}))
: PList ⊆^{k1} (λA. (A → Nat) → Nat)

The postulated reduction behavior is verified by a simple calculation. From sum′, the summation function is obtained by sum := λt. sum′ t id.

Let us remark here that the result type constructor G′ = λA. (A → Nat) → Nat is an instance of a general scheme which is extremely useful for defining functions over heterogeneous datatypes. For the constant type constructors G = H = λB. Nat, the result type constructor G′ is equivalent to λA∀B. (A → H B) → G B which is a syntactic form of the right Kan extension of G along H. Kan extensions are so commonly used with nested datatypes that we will present an elimination scheme in Section 4 with hardwired Kan extensions.

Having completed these two examples we are confident that MIt^{κ} is a useful iterator for higher-rank inductive types. In the following, we will again dualize our definition to handle also greatest fixed points of rank-n type constructors (n ≥ 2).

3.5 Mendler Coiteration for Higher Ranks

Adding the following constructs, we obtain our System MIt^{ω}, which is an extension of Mendler’s system (1991) to finite kinds.

Formation.  ν^{κ} : (κ → κ) → κ
Elimination.  out^{κ} : ∀F^{κ→κ}. ν^{κ}F ⊆^{κ} F (ν^{κ}F)

Introduction.

Γ ⊢ F : κ → κ,
Γ ⊢ G : κ
Γ ⊢ s : ∀X^{κ}. G ⊆^{κ} X → G ⊆^{κ} F X
Γ ⊢ MCoit^{κ}(s) : G ⊆^{κ} ν^{κ}F
Reduction.  out^{κ} (MCoit^{κ}(s) t) ⟶_{β} s MCoit^{κ}(s) t

The reader is invited to check that no problems for subject reduction and confluence arise from these definitions. To demonstrate the usefulness of MCoit^{k1} as a coiteration scheme, in the following we will develop a redecoration algorithm for infinite triangular matrices, which can be defined as a heterogeneous coinductive type. To this end, we fix a type E : ∗ of matrix elements. The type Tri A of triangular matrices with diagonal elements in A and ordinary elements E can be obtained as follows:

TriF := λXλA. A × X(E × A) : k2
Tri := ν^{k1} TriF  : k1

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′. This explains the definition of TriF. We can visualize triangles like this:

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

The vertical lines hint at the decomposition scheme.

Example 9 (Triangle Decomposition) Using the destructor for coinductive types on a triangle Tri A, we can obtain the top element of type A and the remainder of type Tri (E ×A) which looks like an infinite trapezium in our visualization.

top := λt. fst (out^{k1} t) : ∀A. Tri A → A
rest := λt. snd (out^{k1} t) : ∀A. Tri A → Tri (E × A)

Cutting off the top row of a trapezium Tri (E × A) to obtain a triangle Tri A can be implemented using Mendler coiteration for rank 2:

cut := MCoit^{k1}(λcutλt. ⟨snd (top t), cut (rest t)⟩)
: (λA. Tri (E × A)) ⊆^{k1} Tri

Remark 1 (Corrigendum) In Abel, Matthes, and Uustalu (2003) we used tri snd instead of cut, where tri is the mapping function for Tri and snd the second projection. This does type-check yet not yield the right operational behavior, since it cuts off the side diagonal rather than the top row.

Redecoration is an operation 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′. (By an A-decorated tree we mean a tree with A-labelled branching nodes.) 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 f. For streams, for instance

redec : ∀A∀B. (Stream A → B) → Stream A → Stream B

takes f : Stream A → B and t : Stream 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 sub stream this element heads.

Example 10 (Stream Redecoration) Markus Schnell posted an implementation of stream redecoration to the Haskell Mailing List (2002).

    slide :: ([a] -> b) -> [a] -> [b]
    slide f [] = []
    slide f xs = f xs : slide f (tail xs)

He showed how to encode a lowpass digital filter using slide. Here is the implementation of a smoothening filter which replaces each stream element by the average of n adjacent elements.

    smooth :: Int -> [Float] -> [Float]
    smooth n = slide (\ xs -> sum (take n xs) / fromInt n)

Theoretically, redecoration is an operation dual to substitution in trees T A over some label type A. Viewing T as a monad, substitution (A → T B) → T A → T B of B-labelled trees for A-labels is the monad multiplication operation. Viewing T as a comonad, redecoration (T A → B) → T A → T B becomes the comultiplication (Uustalu and Vene, 2002).

Example 11 (Triangle Redecoration) 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 sub triangle cut out by the horizontal line; similarly, every other A is replaced by a B. Redecoration redec has type ∀A∀B. (Tri A → B) → Tri A → Tri B. Therefore, it cannot be implemented directly using Mendler coiteration, but via an auxiliary function redec′ with an isomorphic type in the proper format.

redec := λfλt. redec′ (pack ⟨f, t⟩)
: ∀A∀B. (Tri A → B) → Tri A → Tri B
redec′

:=

MCoit^{k1} (λredec′λ(pack⟨f, t⟩).
⟨f t, redec′ (pack ⟨lift f, rest t⟩)⟩)
: (λB∃A. (Tri A → B) × Tri A) ⊆^{k1} Tri

Here we make use of a function lift : ∀A∀B. (Tri A → B) → Tri(E × A) → (E × B) which lifts the redecoration rule to trapeziums such that it can be used with the trapezium rest t.

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

Hence, if f is a redecoration rule, the new redecoration rule lift f for trapeziums takes a trapezium t of type Tri(E × A) and yields a diagonal element of a trapezium in Tri(E × B), which means a pair ⟨e, b⟩ of type E × B. Since the elements outside the diagonal do not have to be transformed, the left component e stays fixed. The right component b comes from applying f to the triangle which results from cutting off the top row from t.

For the typing of redec′ let G′ := λB∃A. (Tri A → B) × Tri A. If the variable redec′ receives the type G′ ⊆^{k1} X and pack ⟨f, t⟩ is matched, then f gets type Tri A → B and t gets type Tri A. Hence f t : B, and the term starting with redec′ gets type X(E × B) because the argument to redec′ gets type G′(E × B): The existential quantifier for A is instantiated with E × A, the universal quantifiers for A and B in the type of lift are just instantiated by A and B themselves. It is clear that one gets the following reduction behavior.

out^{k1}(redec′ (pack ⟨f, t⟩)) ⟶^{+} ⟨f t, redec′ (pack ⟨lift f, rest t⟩)⟩
top (redec f t)  ⟶^{+} f t
rest (redec f t)  ⟶^{+} redec^{∘} (lift f) (rest t)

On the last line we have used the^{∘}-notation because simply redec (lift f) (rest t) is no β-reduct of the left hand side. Without the^{∘}-notation we could only state that left and right hand side are β-equal, i. e., have a common reduct.

The source type constructor G′ of function redec′ is a left Kan extension of Tri along Tri, since it is an instance of the general scheme λB∃A. (H A → B)×G A with G = H = Tri. In Section 4 we will introduce a generalized coiteration scheme with hardwired Kan extensions. This will allow us to define redec directly and not via an uncurried auxiliary function redec′.

3.6 Embedding into F^{ω}

In this subsection, we will show strong normalization for System MIt^{ω} by embedding it into F^{ω}. Since this shows that MIt^{ω} is just a conservative extension of F^{ω}, we can conclude that higher-order datatypes and Mendler iteration schemes are already present in F^{ω}. The quest for a precise formulation of this fact led to the definition of MIt^{ω} in which these concepts are isolated and named.

Embeddings of (co)inductive type constructors into F^{ω} can be obtained via the following recipe:

(1) Read off the encoding of (co)inductive type constructors from the type of the (co)iterator.

(2) Find the encoding of the (co)iterator, which usually just consists of some lambda-abstractions and some shuffling resp. packing of the abstracted variables.

(3) Take the right-hand side of the reduction rule for (co)iteration as the encoding of the general data constructor resp. destructor.

To implement this scheme, we start by performing some simple equivalence conversions on the type of λs. MIt^{κ}(s). For the remainder of this section, let kind κ = κ⃗ → ∗.

∀F^{κ→κ}∀G^{κ}. (∀X^{κ}. X ⊆ G → F X ⊆ G) → μ^{κ}F ⊆ G
≡ ∀F^{κ→κ}∀G^{κ}. (∀X^{κ}. X ⊆ G → F X ⊆ G) → ∀Y⃗ κ⃗. μ^{κ}F Y⃗ → G Y⃗
↔ ∀F^{κ→κ}∀Y⃗ κ⃗. μ^{κ}F Y⃗ → ∀G^{κ}. (∀X^{κ}. X ⊆ G → F X ⊆ G) → G Y⃗

This equivalent type for λs. MIt^{κ}(s) states that there is a mapping of μ^{κ}F Y⃗ into some other type. Now we simply define μ^{κ}F Y⃗ to be that other type. The definitions of MIt^{κ}(s) and in^{κ} then simply fall into place:

μ^{κ}  : (κ → κ) → κ⃗ → ∗
μ^{κ}  := λF λY⃗ ∀G^{κ}. (∀X^{κ}. X ⊆ G → F X ⊆ G) → G Y⃗
MIt^{κ}(s) : μ^{κ}F ⊆ G  for s : ∀X^{κ}. X ⊆ G → F X ⊆ G
MIt^{κ}(s) := λr. r s
in^{κ}  : ∀F^{κ→κ}. F (μ^{κ}F) ⊆ μ^{κ}F
in^{κ}  := λtλs. s MIt^{κ}(s) t

Lemma 1 With the definitions above, MIt^{κ}(s) (in^{κ} t) ⟶^{+} s MIt^{κ}(s) t in System F^{ω}.

Proof. By simple calculation. □

To find an encoding of (co)inductive type constructors, we consider the type of the (universal) coiterator λs. MCoit^{κ}(s):

∀F^{κ→κ}∀G^{κ}. (∀X^{κ}. G ⊆ X → G ⊆ F X) → G ⊆ ν^{κ}F
≡ ∀F^{κ→κ}∀G^{κ}. (∀X^{κ}. G ⊆ X → G ⊆ F X) → ∀Y⃗ κ⃗. G Y⃗ → ν^{κ}F Y⃗
↔ ∀F^{κ→κ}∀Y⃗ κ⃗. (∃G^{κ}. (∀X^{κ}. G ⊆ X → G ⊆ F X) × G Y⃗) → ν^{κ}F Y⃗

These considerations lead to the following definitions:

ν^{κ}  : (κ → κ) → κ⃗ → ∗
ν^{κ}  := λF λY⃗ ∃G^{κ}. (∀X^{κ}. G ⊆ X → G ⊆ F X) × G Y⃗
MCoit^{κ}(s) : G ⊆ ν^{κ}F  for s : ∀X^{κ}. G ⊆ X → G ⊆ F X
MCoit^{κ}(s) := λt. pack ⟨s, t⟩
out^{κ}  : ∀F^{κ→κ}. ν^{κ}F ⊆ F (ν^{κ}F)
out^{κ}  := λ(pack⟨s, t⟩). s MCoit^{κ}(s) t

Lemma 2 With the definitions above, out^{κ} (MCoit^{κ}(s) t) ⟶^{+} s MCoit^{κ}(s) t in System F^{ω}.

Proof. By simple calculation. □

Theorem 1 (Strong normalization) System MIt^{ω} is strongly normalizing, i.e., for each welltyped term t_{0} there is no infinite reduction sequence t_{0} ⟶ t_{1} ⟶ t_{2} ⟶ …

Proof. By lemmata 1 and 2, such a reduction sequence would translate into the infinite sequence t_{0} ⟶^{+} t_{1} ⟶^{+} t_{2} ⟶^{+} … of well-typed terms of System F^{ω} (here, the above definitions are meant to be unfolded), a contradiction to the strong normalization property of F^{ω}. □

4 System GMIt^{ω}: Refined and Generalized Mendler (Co)Iteration

The system GMIt^{ω} of this section is a minor variant of the system MIt^{ω} in Abel, Matthes, and Uustalu (2003). Its intension is to ease programming with Mendler iteration in case Kan extensions have to be used (cf. examples 8 and 11 in Section 3). In a sense, we are just hard-wiring the Kan extensions into the (co)iteration scheme of MIt^{ω}.

4.1 Containment of Type Constructors

The key idea consists in identifying an appropriate containment relation for type constructors of the same kind κ. For types, the canonical choice is implication. For an arbitrary kind κ, the easiest notion is “pointwise implication” ⊆^{κ}, used in the previous section for the definition of MIt^{ω}.

Refined containment. A more refined notion is ≤^{κ}, which first appeared in Hinze’s work (1999) as the polykinded type Map of generic mapping functions. We learned it first from Peter Hancock in 2000 and employed it already in earlier work (Abel and Matthes, 2003) which studied iteration for monotone inductive type constructors of higher kinds:

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

Hence, for F, G : k1, F ≤^{k1} G = ∀A∀B.(A → B) → F A → GB. Here, one does not only have to pass from F to G, but this has to be stable under changing the argument type from A to B.

This notion will give rise to a notion of monotonicity on the basis of which traditional-style iteration and coiteration can be extended to arbitrary ranks— see Section 6.

Relativized refined containment. In order to extend Mendler (co)iteration to higher kinds such that generalized and efficient folds (Hinze, 2000a; Martin, Gibbons, and Bayley, 2003) are directly covered, we have to relativize the notion ≤^{κ}, for κ = κ⃗ → ∗, to a vector H⃗ of type constructors of kinds κ⃗ → κ⃗, i. e., H_{1} : κ_{1} → κ_{1}, H_{2} : κ_{2} → κ_{2}, … In addition to a variation of the argument type constructor as in the definition of ≤^{κ→κ′}, moreover, H_{i} is applied to the i-th “target argument” (below, another definition similarly modifies the “source argument”).

For every kind κ = κ⃗ → ∗, define a type 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 type constructors I⃗d, the new notion ≤κ ; H⃗ coincides with ≤^{κ}. Similarly, we define another type 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 : k1, one has

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

Even more concretely, we have the following types which will be used in the examples 12 and 14:

PList ≤_{λB.Nat}^{k1} λB.Nat = ∀A∀B.(A → Nat) → PList A → Nat
Tri _{Tri}≤^{k1} Tri  = ∀A∀B.(Tri A → B) → Tri A → Tri B

4.2 Definition of GMIt^{ω}

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 rank-1 (co)inductive types, and to a scheme encompassing generalized folds (Bird and Paterson, 1999a; Hinze, 2000a; Martin, Gibbons, and Bayley, 2003) and the dual scheme for coinductive type constructors of rank 2. The generalized scheme for coinductive type constructors is a new principle of programming with non-wellfounded datatypes.

The system GMIt^{ω} is given as an extension of F^{ω} by wellkinded type constructor constants μ^{κ} and ν^{κ}, and welltyped term constants in^{κ}, out^{κ} as for MIt^{ω}, and the elimination rule GMIt^{κ}(s) and the introduction rule GMCoit^{κ}(s) for every kind κ, and new term reduction rules.

Inductive type constructors. Let κ = κ⃗ → ∗.

Formation.  μ^{κ} : (κ → κ) → κ
Introduction. in^{κ} : ∀F^{κ→κ}. F (μ^{κ}F) ⊆^{κ} μ^{κ}F

Elimination.

Γ ⊢ F : κ → κ Γ ⊢ G : κ Γ ⊢ H⃗ : κ⃗ → κ⃗

Γ ⊢ s : ∀X^{κ}. X ≤κ ; H⃗ G → F X ≤κ ; H⃗ G

Γ ⊢ GMIt^{κ}(s) : μ^{κ}F ≤κ ; H⃗ G

Reduction.  GMIt^{κ}(s) f⃗ (in^{κ} t) ⟶_{β} s GMIt^{κ}(s) f⃗ t

where |f⃗| = |κ⃗|.

Example 12 (Summing up a Powerlist, Revisited) The function sum′ for powerlists (see Example 8) can be naturally implemented with GMIt^{k1}. The difference to the original implementation confines itself to swapping the arguments t (powerlist) and f (continuation). The swapping is necessary since for this example GMIt^{k1} yields a recursive function of type PList ≤_{λB.Nat}^{k1} λB.Nat, which can be simplified to ∀A. (A → Nat) → PList A → Nat by removing the void quantification over B.

Example 13 (Summing up a Bush) Recall the nested datatype of “bushy lists” given in Section 3.3 and first considered in Bird and Meertens (1998) within Haskell.

BushF = λXλA. 1 + A × X (X A) : k2
Bush = μ^{k1} BushF  : k1
bnil = in^{k1} (inl ⟨⟩)  : ∀A. Bush A
bcons = λaλb. in^{k1} (inr ⟨a, b⟩)  : ∀A. A → Bush (Bush A) → Bush A

Similarly to powerlists, we can define a summation function sum′ for bushes:

bsum′

:=

GMIt^{k1}( λbsum′λfλt. match t with
bnil^{−}  ↦ 0
| bcons^{−} a b ↦ f a + bsum′ (bsum′ f) b)
: ∀A. (A → Nat) → Bush A → Nat

The 0 in the first case is the supposed zero in Nat. The types would be assigned as follows:

bsum′  : X ≤_{λB.Nat}^{k1} λB.Nat
f  : A → Nat
t  : 1 + A × X(XA)
a  : A
b  : X(XA)
bsum′f  : XA → Nat
bsum′ (bsum′f) : X(XA) → Nat

While termination of sum′ for powerlists is already observable from the reduction behavior, this cannot be said for bsum′ where the nesting in the datatype is reflected in the nesting of the recursive calls:

bsum′ f bnil  ⟶^{+} 0
bsum′ f (bcons a b) ⟶^{+} f a + bsum′ (bsum′f) b

Note that in the outer recursive call the second argument decreases structurally: on the left-hand side, one has bcons a b, one the right-hand side only b. But, the inner call bsum′f does not specify a second argument. One could force the second argument by η-expanding it to λx. bsum′ f x, which does not help much because the fresh variable x does not stand in any visible relation to the input bcons a b. Consequently, proving termination of bsum′ using a term ordering seems to be problematic, whereas in our system it is just a byproduct of type checking (see Theorem 1).

Coinductive type constructors. Let κ = κ⃗ → ∗.

Formation.  ν^{κ} : (κ → κ) → κ
Elimination.  out^{κ} : ∀F^{κ→κ}. ν^{κ}F ⊆^{κ} F (ν^{κ}F)

Introduction.

Γ ⊢ F : κ → κ
Γ ⊢ G : κ
Γ ⊢ H⃗ : κ⃗ → κ⃗
Γ ⊢ s : ∀X^{κ}. G H⃗≤^{κ} X → G H⃗≤^{κ} F X
Γ ⊢ GMCoit^{κ}(s) : G H⃗≤^{κ} ν^{κ}F
Reduction.  out^{κ}(GMCoit^{κ}(s) f⃗ t) ⟶_{β} s GMCoit^{κ}(s) f⃗ t
where |f⃗| = |κ⃗|.

Example 14 (Triangle Redecoration, Revisited) Using GMCoit^{k1}, triangle redecoration can be implemented much more concisely. In the context of Example 11 we obtain the function redec directly as follows.

redec := GMCoit^{k1} (λredec λfλt. ⟨f t, redec (lift f) (rest t)⟩)
: ∀A∀B. (Tri A → B) → Tri A → Tri B = Tri _{Tri}≤^{k1} Tri

Thus, one can enforce the desired reduction behavior without any detours. In MIt^{ω}, where we implemented triangle redecoration in Example 11, we were required to implement an auxiliary function redec′ first which used a tagged argument pair pack⟨f, t⟩. In contrast, the curried version redec above can handle f and t as two separate arguments directly. This leads to a very natural reduction behavior:

top (redec f t) ⟶^{+} f t
rest (redec f t) ⟶^{+} redec (lift f) (rest t)

In Example 11, we had the small spot ^{∘} in the picture in that only redec^{∘} for the function redec we defined there appeared on the right-hand side.

4.3 Embedding GMIt^{ω} into MIt^{ω}

The embedding of GMIt^{ω} into MIt^{ω} shown in this section preserves reductions. Hence, GMIt^{ω} inherits strong normalization from MIt^{ω}. The embedding can even be read as a definition of GMIt^{κ}(s) and GMCoit^{κ}(s) within MIt^{ω}. Therefore, we will later freely use these constructions within the system MIt^{ω}.

For the sake of the embedding, we use a syntactic version of Kan extensions (see Mac Lane, 1998, Chapter 10). In conjunction with nested datatypes, Kan extensions appear already in Bird and Paterson (1999a, Section 6.2), but not as a tool of programming with nested types, but a means to categorically justify the uniqueness of generalized folds as elimination principles for nested datatypes. In this article, for the examples 8 and 11 within MIt^{ω}, special Kan extensions have been used already. The same programming tasks have been accomplished directly within GMIt^{ω} in the examples 12 and 14. In the sequel, this will be clarified: Just by choosing the target type constructor of iteration to be an appropriate Kan extension, one gets the behavior of GMIt^{κ}(s) within MIt^{ω}, and similarly for the source type constructor in the coinductive case.

Compared to Abel and Matthes (2003), 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⃗}^{κ_{1}→κ̃} G) XX⃗ := ∀Y^{κ_{1}}. X ≤^{κ_{1}} HY → (Ranκ̃ ; H⃗ (G Y)) X⃗

Here, κ_{1} → κ̃ is the general format for a composed kind κ. Clearly, κ̃ = κ_{2}, …, κ_{|κ⃗|} → ∗.

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⃗}^{κ_{1}→κ̃} F) Y Y⃗ := ∃X^{κ_{1}}. HX ≤^{κ_{1}} Y × (Lanκ̃ ; H⃗ (F X)) Y⃗

The kind κ̃ is to be understood as in the previous definition.

We omit the index H⃗ if it is just a vector of identities Id.

Lemma 3 Let κ = κ⃗ → ∗, F, G : κ and H⃗ : κ⃗ → κ⃗. The following pairs of types are logically equivalent:

(1) F ≤κ ; H⃗ G and F ⊆^{κ} Ranκ ; H⃗ G.

(2) F H⃗≤^{κ} G and Lanκ ; H⃗ F ⊆^{κ} G.

Proof. For κ = ∗, all these types are just F → G. Otherwise, let κ′ := κ⃗ → κ⃗, n := |κ⃗| and define

leqRan^{κ} := λgλtλf⃗. g f⃗ t
: ∀F^{κ}∀G^{κ}∀H⃗^{κ′}. F ≤κ ; H⃗ G → F ⊆^{κ} Ranκ ; H⃗ G
ranLeq^{κ} := λhλf⃗λr. h rf⃗
: ∀F^{κ}∀G^{κ}∀H⃗^{κ′}. F ⊆^{κ} Ranκ ; H⃗ G → F ≤κ ; H⃗ G
leqLan^{κ} := λgλ(pack⟨f_{1}, pack⟨f_{2}, … pack⟨f_{n}, t⟩ …⟩⟩). g f⃗ t
: ∀F^{κ}∀G^{κ}∀H⃗^{κ′}. F H⃗≤^{κ} G → Lanκ ; H⃗ F ⊆^{κ} G
lanLeq^{κ} := λhλf⃗λt. h pack⟨f_{1}, pack⟨f_{2}, … pack⟨f_{n}, t⟩ …⟩⟩
: ∀F^{κ}∀G^{κ}∀H⃗^{κ′}. Lanκ ; H⃗ F ⊆^{κ} G → F H⃗≤^{κ} G

(The definition for right Kan extension would even work for κ = ∗, the one for left Kan extension would be incorrect in that case.) □

We can now simply define the new function symbols of GMIt^{ω} in MIt^{ω} in case κ ≠ ∗ (otherwise, the typing and reduction rules are just the same for both systems):

GMIt^{κ}(s) := ranLeq^{κ} (MIt^{κ} (leqRan^{κ} ∘ s ∘ ranLeq^{κ}))
GMCoit^{κ}(s) := lanLeq^{κ} (MCoit^{κ} (leqLan^{κ} ∘ s ∘ lanLeq^{κ}))

Then GMIt^{κ}(s) and GMCoit^{κ}(s) have precisely the typing behavior as required for GMIt^{ω}. We only treat the inductive case, the coinductive one is analogous. Assume the step term s for GMIt^{κ}(s) of type ∀X^{κ}. X ≤κ ; H⃗ G → F X ≤κ ; H⃗ G. Then,

ŝ:= leqRan^{κ} ∘ s ∘ ranLeq^{κ} : ∀X^{κ}. X ⊆^{κ} Ranκ ; H⃗ G → F X ⊆^{κ} Ranκ ; H⃗ G.

Therefore, MIt^{κ}(ŝ) : μ^{κ}F ⊆^{κ} Ranκ ; H⃗ G, finally GMIt^{κ}(s) : μ^{κ}F ≤κ ; H⃗ G.

We calculate, using the above abbreviation ŝ,

GMIt^{κ}(s) f⃗ (in^{κ} t) ⟶^{+} MIt^{κ}(ŝ) (in^{κ} t) f⃗
⟶ ŝ MIt^{κ}(ŝ) t f⃗
⟶^{+} s (ranLeq^{κ}(MIt^{κ}(ŝ))) f⃗ t

With a similar, but notationally more tedious calculation for the coinductive case, we get, with these definitions, in MIt^{ω}:

GMIt^{κ}(s) f⃗ (in^{κ} t) ⟶^{+} s GMIt^{κ}(s) f⃗ t
out^{κ}(GMCoit^{κ}(s) f⃗ t) ⟶^{+} s GMCoit^{κ}(s) f⃗ t

Since one step of reduction in GMIt^{ω} is replaced by at least one reduction step of the encoding in MIt^{ω}, GMIt^{ω} inherits strong normalization of MIt^{ω}. Since the number of steps is fixed for every kind κ, in the examples we will just treat GMIt^{ω} as a subsystem of MIt^{ω} in the sense that we assume that both iteration and both coiteration schemes are present in MIt^{ω} together with their reduction rules.

5 Basic Conventional Iteration

We are looking for a system of conventional iteration into which we can embed MIt^{ω} in a way which sends Mendler iteration into conventional iteration.

Systems of conventional iteration, unlike Mendler-style systems, directly follow the idea of initial algebras in category theory. In that model, F : κ → κ would have to be an endofunctor on a category associated with κ. The fixed-point μ^{κ}F would be the carrier of an initial F -algebra, and in^{κ} : F (μ^{κ}F) ⟶ μ^{κ}F be its structure map. In the Mendler-style systems of this article, we have chosen to represent those morphisms by terms of type F (μ^{κ}F) ⊆^{κ} μ^{κ}F. This decision for the type of the data constructor in^{κ} will remain fixed throughout the article. The main open question is the choice of the syntactic representation of being a functor. Certainly, we cannot require the equational functor laws in our framework of F^{ω}, but have to concentrate on the types: If a functor F is applied to a morphism s : A ⟶ B, then the result is a morphism F s : F A ⟶ F B. If F is a type constructor, i. e., of kind k1, then this can be represented by the existence of a term m of type

mon^{k1} F := ∀A∀B. (A → B) → F A → F B,

which is nothing but monotonicity of F. Then, s : A → B implies m s : F A → F B.

The notion mon^{k1} F is the most logically-minded definition of rank-1-functors: It is free from the analysis of the shape of F (polynomial, strictly positive, non-strictly positive). Moreover, it is the only possible definition that is based on the existence of a witness of monotonicity, i. e., a term inhabiting the type expressing functoriality. This is no longer so for higher kinds. We will stick to the logical approach, but face several possible definitions of monotonicity expressing functoriality. In this section, we will start with basic monotonicity, and in Section 6, a more refined definition will be studied.

Basic Monotonicity Define

\underline{mon}^{κ→κ′} := λF. ∀X^{κ}∀Y^{κ}. X ⊆^{κ} Y → F X ⊆^{κ′} F Y : (κ → κ′) → ∗

This will be our notion of monotonicity of type constructors F : κ → κ′, and hence our representation of functoriality. Consequently, we only use our inductive constructor μ^{κ}F in the presence of some term m of type \underline{mon}^{κ→κ} F. As has been observed in Matthes (1998), there is no need to require a fixed term m beforehand. It is sufficient to give it as an argument to either the data constructor or the iterator. Moreover, it does not need to be closed, hence giving rise to conditional monotonicity or (in the case m is just a variable) to hypothetical monotonicity. Anyhow, in loc. cit., it has been shown that strong normalization holds for inductive types. There, only mon^{k1} enters the definitions. Clearly, \underline{mon}^{k1} F = mon^{k1} F.

In the next subsection, we will see that a canonical formulation of (co)iteration, based on basic monotonicity \underline{mon}^{κ→κ} for all kinds κ, is a subsystem of MIt^{ω}.

5.1 Defining Basic Conventional Iteration in Terms of Mendler Iteration

Define the basic conventional iterators and coiterators by

\underline{It}^{κ}(m, s) := MIt^{κ}(λitλt. s (m it t))
\underline{Coit}^{κ}(m, s) := MCoit^{κ}(λcoit λt. m coit (s t))

Then, one immediately gets the following derived typing rules

\frac{Γ ⊢ F : κ → κ Γ ⊢ m : \underline{mon}^{κ→κ} F Γ ⊢ G : κ Γ ⊢ s : F G ⊆^{κ} G}{Γ ⊢ \underline{It}^{κ}(m, s) : μ^{κ}F ⊆^{κ} G}

\frac{Γ ⊢ F : κ → κ Γ ⊢ m : \underline{mon}^{κ→κ} F Γ ⊢ G : κ Γ ⊢ s : G ⊆^{κ} F G}{Γ ⊢ \underline{Coit}^{κ}(m, s) : G ⊆^{κ} ν^{κ}F}

and reduction behavior as follows

\underline{It}^{κ}(m, s) (in^{κ} t)  ⟶^{+} s (m \underline{It}^{κ}(m, s) t)
out^{κ} (\underline{Coit}^{κ}(m, s) t) ⟶^{+} m \underline{Coit}^{κ}(m, s) (s t)

The interpretation of the typing rule for \underline{It}^{κ}(m, s) is as follows: Given a monotonicity witness m for F and an F -algebra s, i. e., a type constructor G and a term s of type F G ⊆^{κ} G, “initiality” of μ^{κ}F yields a “morphism” from μ^{κ}F to G. This “morphism” is witnessed by \underline{It}^{κ}(m, s) of type μ^{κ}F ⊆^{κ} G.

Also the reduction behavior is as expected (see Matthes, 1999): If \underline{It}^{κ}(m, s) is given the constructor term in^{κ} t, this reduces to the step term (the F -algebra) s, applied to the recursive call, where m organizes how the whole function \underline{It}^{κ}(m, s) is applied to the term t which was the argument to in^{κ}.

The rules for ν^{κ}F are just found by dualization.

Example 15 (Summing up a Powerlist, Conventional Style) We redo Example 8 with \underline{It}^{k1}. Again, we define a more general function

sum′ : ∀A. PList A → (A → Nat) → Nat = PList ⊆^{k1} G′

with G′ := λA. (A → Nat) → Nat : k1. This is done as follows:

PListF := λXλA. A + X (A × A)
: k2

plistfb

:= λsλt. match t with
zero^{−} a ↦ zero^{−} a
| succ^{−} l ↦ succ^{−} (s l)
: \underline{mon}^{k2} PListF

s := λtλf. match t with

zero^{−} a ↦ f a
| succ^{−} res ↦ res (λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2})
: PListF G′ ⊆^{k1} G′
sum′ := \underline{It}^{k1}(plistfb, s)
: PList ⊆^{k1} G′

An easy calculation shows that, as in Example 8, we get the reduction behavior

sum′ : ∀A. PList A → (A → Nat) → Nat
sum′ (zero a) f ⟶^{+} f a
sum′ (succ l) f ⟶^{+} sum′ l (λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2})

We want to isolate these means of basic conventional iteration and coiteration in the form of a system \underline{It}^{ω} in order to make it the target of an embedding.

5.2 Definition of \underline{It}^{ω}: Basic Conventional Iteration and Coiteration

Let the system \underline{It}^{ω} be given by the extension of system F^{ω} by the following constants, function symbols, typing and reduction rules for iteration and coiteration, starting with those for iteration:

Formation.  \underline{μ}^{κ} : (κ → κ) → κ
Introduction. \underline{in}^{κ} : ∀F^{κ→κ}. F (\underline{μ}^{κ}F) ⊆^{κ} \underline{μ}^{κ}F

Elimination.

Γ ⊢ F : κ → κ,
Γ ⊢ m : \underline{mon}^{κ→κ} F
Γ ⊢ G : κ
Γ ⊢ s : F G ⊆^{κ} G
Γ ⊢ \underline{It}^{κ}(m, s) : \underline{μ}^{κ}F ⊆^{κ} G
Reduction.  \underline{It}^{κ}(m, s) (\underline{in}^{κ} t) ⟶_{β} s (m \underline{It}^{κ}(m, s) t)

As has been promised, this is nothing more than a system version of the definitions in the previous subsection. Since the embedding of MIt^{ω} into \underline{It}^{ω} in the next subsection will even change the type constructors (not only the terms), also the name of the fixed-point former μ^{κ} has been changed into \underline{μ}^{κ}, as well as the name of the general data constructor in^{κ}, which has been changed to \underline{in}^{κ}. Similar remarks apply to coiteration, given as follows:

Formation.  \underline{ν}^{κ} : (κ → κ) → κ
Elimination.  \underline{out}^{κ} : ∀F^{κ→κ}. \underline{ν}^{κ}F ⊆^{κ} F (\underline{ν}^{κ}F)

Introduction.

Γ ⊢ F : κ → κ,
Γ ⊢ m : \underline{mon}^{κ→κ} F
Γ ⊢ G : κ
Γ ⊢ s : G ⊆^{κ} F G
Γ ⊢ \underline{Coit}^{κ}(m, s) : G ⊆^{κ} \underline{ν}^{κ}F
Reduction.  \underline{out}^{κ} (\underline{Coit}^{κ}(m, s) t) ⟶_{β} m \underline{Coit}^{κ}(m, s) (s t)

Using the definitions in the previous subsection, \underline{It}^{ω} embeds into MIt^{ω}. The interesting result, however, is the embedding in the converse direction: MIt^{ω} even embeds into \underline{It}^{ω}.

5.3 Embedding Mendler Iteration into Conventional Iteration

Here, we present a somewhat surprising embedding of MIt^{ω} into \underline{It}^{ω}. Certainly, there is the embedding through F^{ω} that polymorphically encodes the (co)inductive constructors (see section 3.6) and ignores the additional capabilities of \underline{It}^{ω}. An interesting embedding has to send the Mendler (co)iterators of MIt^{ω} to the conventional (co)iterators of \underline{It}^{ω}. Unlike the embedding of GMIt^{ω} into MIt^{ω}, our embedding will not just be a “notational definition”, but also transforms the (co)inductive constructors. As before, Kan extensions play a central role.

Naive Kan extensions along the identity. In the following, we define a naive form of Kan extensions (unlike in previous papers and above). Let κ := κ_{0} → κ⃗ → ∗, F : κ, G : κ_{0} and G_{i} : κ_{i} for 1 ≤ |κ⃗|. The types (\underline{Ran}^{κ} F) G G⃗ and (\underline{Lan}^{κ} F) G G⃗ are defined as follows:

\begin{aligned}(\underline{Ran}^{κ} F) G G⃗ & := & ∀Y^{κ_{0}}. G ⊆^{κ_{0}} Y → F Y G⃗ \\ (\underline{Lan}^{κ} F) G G⃗ & := & ∃X^{κ_{0}}. X ⊆^{κ_{0}} G × F X G⃗ \end{aligned}

Alternatively, \underline{Ran}^{κ} and \underline{Lan}^{κ} can be seen as type constructors of kind κ → κ.

Notice that, trivially, always \underline{Ran} F ⊆ F and F ⊆ \underline{Lan} F. More precisely, we can define for κ ≠ ∗

ranId : \underline{Ran}^{κ} ⊆^{κ} Id by ranId := λx.x id
lanId : Id ⊆^{κ} \underline{Lan}^{κ}  by lanId := λx. pack⟨id, x⟩

Lemma 4 For any F, F′ : κ → κ and G : κ, we have the following logical equivalences (already in F^{ω}):

(∀X^{κ}. G ⊆ X → G ⊆ F X) ↔ G ⊆ (\underline{Ran}^{κ→κ} F) G  (1)
(∀X^{κ}∀Y^{κ}. X ⊆ Y → F X ⊆ F′ Y) ↔ F ⊆ \underline{Ran}^{κ→κ′} F′  (2)
\underline{mon}^{κ→κ′} F ↔ F ⊆ \underline{Ran}^{κ→κ′} F  (3)
(∀X^{κ}. X ⊆ G → F X ⊆ G) ↔ (\underline{Lan}^{κ→κ} F) G ⊆ G  (4)
(∀X^{κ}∀Y^{κ}. X ⊆ Y → F X ⊆ F′ Y) ↔ \underline{Lan}^{κ→κ′} F ⊆ F′  (5)
\underline{mon}^{κ→κ′} F ↔ \underline{Lan}^{κ→κ′} F ⊆ F  (6)

Proof. The first two equivalences are proven by Schönfinkel’s transposition operator T := λsλtλf. s f t—in either direction. For the fourth and fifth equivalence from left to right, the proof is U := λsλ(pack⟨f, t⟩). s f t, a kind of uncurrying operator, and λsλfλt. s (pack⟨f, t⟩) for the reverse direction, a currying procedure. Obviously, (3) is an instance of (2), and (6) is an instance of (5). □

The terms T := λsλtλf. s f t and U := λsλ(pack⟨f, t⟩). s f t in the previous proof will be used in the embedding below.

The following is a crucial property of \underline{It}^{ω}: There is a uniform proof of monotonicity for all Kan extensions. (Recall that κ ≠ ∗.)

\underline{M}_{Lan}^{κ} := λgλ(pack⟨f, t⟩). pack⟨g ∘ f, t⟩ : ∀G^{κ}. \underline{mon}^{κ} (\underline{Lan}^{κ} G)
\underline{M}_{Ran}^{κ} := λgλtλf. t (f ∘ g)  : ∀G^{κ}. \underline{mon}^{κ} (\underline{Ran}^{κ} G)

The embedding ⌜·⌝ of System MIt^{ω} of Mendler iteration and coiteration into \underline{It}^{ω} is now straightforward. Kinds are left fixed; the translation of most typeconstructor and term formers is homomorphic, e.g., a type application ⌜F G⌝ is encoded as a type application ⌜F ⌝ ⌜G⌝. Only syntax related to least and greatest fixed-points has to be translated non-homomorphically:

Formation. ⌜μ^{κ}⌝  : (κ → κ) → κ
⌜μ^{κ}⌝  := \underline{μ}^{κ} ∘ \underline{Lan}^{κ→κ}
Introduction. ⌜in^{κ}⌝  : ∀F^{κ→κ}. F ⌜μ^{κ}F ⌝ ⊆ \underline{μ}^{κ}(\underline{Lan}^{κ→κ} F)
⌜in^{κ}⌝  := λt. \underline{in}^{κ} (lanId t)
Elimination. \frac{F : κ → κ G : κ s : ∀X^{κ}. X ⊆ G → F X ⊆ G}{⌜MIt^{κ}(s)⌝ : ⌜μ^{κ}F ⌝ ⊆ ⌜G⌝}

⌜MIt^{κ}(s)⌝  := λx. \underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) x  where
U ⌜s⌝  : \underline{Lan}^{κ→κ} ⌜F ⌝ ⌜G⌝ ⊆ ⌜G⌝
Reduction. MIt^{κ}(s) (in^{κ} t) ⟶ s MIt^{κ}(s) t

This behavior is simulated by finitely many steps inside \underline{It}^{ω}:

⌜MIt^{κ}(s) (in^{κ} t)⌝ ⟶^{+} \underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) (\underline{in}^{κ} (lanId ⌜t⌝))
⟶ U ⌜s⌝ (\underline{M}_{Lan}^{κ} \underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) (lanId ⌜t⌝))
⟶ U ⌜s⌝ (\underline{M}_{Lan}^{κ} \underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) pack⟨id, ⌜t⌝⟩)
⟶^{+} U ⌜s⌝ pack⟨\underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) ∘ id, ⌜t⌝⟩
⟶^{+} ⌜s⌝ (\underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) ∘ id) ⌜t⌝
⟶ ⌜s⌝ (λx. \underline{It}^{κ}(\underline{M}_{Lan}^{κ}, U ⌜s⌝) x) ⌜t⌝
= ⌜s MIt^{κ}(s) t⌝

Notice that the embedding employs a left Kan extension for the inductive case while the embedding of GMIt^{ω} into MIt^{ω} uses a right Kan extension for that purpose. Hence, there is a real need for the existential quantifier also for inductive constructors alone. We come to the coinductive case.

Formation. ⌜ν^{κ}⌝  : (κ → κ) → κ
⌜ν^{κ}⌝  := \underline{ν}^{κ} ∘ \underline{Ran}^{κ→κ}
Elimination. ⌜out^{κ}⌝  : ∀F^{κ→κ}. \underline{ν}^{κ}(\underline{Ran}^{κ→κ} F) ⊆ F ⌜ν^{κ}F ⌝
⌜out^{κ}⌝  := λr. ranId (\underline{out}^{κ} r)
Introduction. \frac{F : κ → κ G : κ s : ∀X^{κ}. G ⊆ X → G ⊆ F X}{⌜MCoit^{κ}(s)⌝ : ⌜G⌝ ⊆ ⌜ν^{κ}F ⌝}

⌜MCoit^{κ}(s)⌝  := λx. \underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝) x  where
T ⌜s⌝  : ⌜G⌝ ⊆ \underline{Ran}^{κ→κ} ⌜F ⌝ ⌜G⌝
Reduction. out^{κ} (MCoit^{κ}(s) t) ⟶ s MCoit^{κ}(s) t

⌜out^{κ} (MCoit^{κ}(s) t)⌝ ⟶^{+} ranId (\underline{out}^{κ} (\underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝) ⌜t⌝))
⟶ ranId (\underline{M}_{Ran}^{κ} \underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝) (T ⌜s⌝ ⌜t⌝))
⟶^{+} ranId (λf. T ⌜s⌝ ⌜t⌝ (f ∘ \underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝)))
⟶^{+} T ⌜s⌝ ⌜t⌝ (id ∘ \underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝))
⟶^{+} ⌜s⌝ (λx. \underline{Coit}^{κ}(\underline{M}_{Ran}^{κ}, T ⌜s⌝) x) ⌜t⌝
= ⌜s MCoit^{κ}(s) t⌝

5.4 Remarks on Monotonicity

Although sufficient to cover all of MIt^{ω}, our basic notion of monotonicity has several defects which will be overcome in the next section.

Lemma 5 There is no closed term of type \underline{mon}^{k2}(λX. X ∘ X) in F^{ω}.

Proof. Assume, to the contrary,

m : ∀X∀Y. (∀A. XA → Y A) → ∀A. X(XA) → Y (Y A).

Assume a type variable Z and consider X := λA. A → ⊥ with ⊥ := ∀Z.Z, and Y := λA. A → Z. Then, s := λtλa. t a : ∀A. XA → Y A. Therefore, m s : X(XZ) → Y (Y Z) = ¬¬Z → (Z → Z) → Z, with ¬A := A → ⊥.

Hence, λu. m s u id : ∀Z. ¬¬Z → Z. This is impossible, since F^{ω} is not classical (to be proven using normalization). □

The lemma hinges on our definition of monotonicity: The notion of monotonicity studied in the next section will cover λXλA. X(XA).

A motivation why the lemma holds can be given as follows: How would we go from X(XA) to Y (Y A)? Two possibilities seem to exist: either through X(Y A) or through Y (XA). However, in the first case, we would badly need monotonicity (in the only possible sense) of X to exhibit X(XA) → X(Y A), in the second case, we would need monotonicity of Y to pass from Y (XA) to Y (Y A). If neither X nor Y are monotone, we cannot expect at all to succeed. The above lemma even gives an appropriate example.

The definition of monotonicity is naive in the sense that the following properties do not hold in general:

\underline{mon}^{κ→κ′} F, \underline{mon}^{κ} X imply \underline{mon}^{κ′}(F X),
\underline{mon}^{κ→κ} F  implies \underline{mon}^{κ}(\underline{μ}^{κ}F).

This means monotonicity of a least fixed-point \underline{μ}^{κ}F : κ is not inherited from monotonicity of F : κ → κ. Still, this notion of monotonicity has been shown to be suitable to define iteration and coiteration in the sense of \underline{It}^{ω}.

Both non-implications are exemplified with the single example F := λ λA. ¬A. Trivially, \underline{mon}^{k2} F is inhabited by m_{F} := λx. id. Certainly, F X = λA. ¬A is not monotone: If m : mon^{k1}(λA. ¬A), then m : (⊥ → A) → (⊥ → ⊥) → ¬A, hence m id id : ∀A.¬A, hence logical inconsistency of F^{ω} ensues. Also \underline{μ}^{k1}F is not monotone because this type constructor is logically equivalent with λA. ¬A: The data constructor \underline{in}^{k1} yields one direction, the other comes from

\underline{It}^{k1}(m_{F} , id) : (\underline{μ}^{k1}F) ⊆ F (\underline{μ}^{k1}F)
= ∀A. (\underline{μ}^{k1}F) A → ¬A

Remark 2 (Another notion of monotonicity) Consider a modified notion of monotonicity which excludes some more type constructors.

\underline{vmon}^{κ⃗→∗} F := ∀X⃗κ⃗∀Y⃗ κ⃗. X⃗ ⊆κ⃗ Y⃗ → F X⃗ → F Y⃗

This notion is monotonicity preserving in a very strong sense: \underline{vmon}^{κ→κ′} F alone implies \underline{vmon}^{κ′}(F X), but it fails to give a good target system for MIt^{ω}. This is because for the appropriate modification of left Kan extension \underline{Lan}^{κ}, (although a term \underline{M}_{Lan} exists here as well,) the step term of MIt^{κ} does not have a type isomorphic to \underline{Lan}^{κ→κ} F G ⊆^{κ} G.

Although we have shown that monotonicity of F : κ → κ fails to entail monotonicity of \underline{μ}^{κ}F in general, it does work if F additionally preserves monotonicity of its first argument. More precisely, if there is a term p which transforms every monotonicity witness n : \underline{mon}^{κ} X into a monotonicity witness p n : \underline{mon}^{κ}(F X), then \underline{μ}^{κ}F : κ is monotone, canonically. To see this, define

\underline{M}_{μ}^{κ}(p, m) := λfλt. \underline{It}(m, λt′λf′. \underline{in}^{κ} (m ranId (p \underline{M}_{Ran}^{κ} f′ t′))) t f.

Then F : κ → κ, p : ∀X^{κ}. \underline{mon}^{κ} X → \underline{mon}^{κ}(F X) and m : \underline{mon}^{κ→κ} F imply that the step term s has type F (\underline{Ran}^{κ}(\underline{μ}^{κ}F)) ⊆^{κ} \underline{Ran}^{κ}(\underline{μ}^{κ}F) and

\underline{M}_{μ}^{κ}(p, m) : \underline{mon}^{κ}(\underline{μ}^{κ}F)
\underline{M}_{μ}^{κ}(p, m) f (\underline{in}^{κ} t) ⟶^{+} \underline{in}^{κ} (m ranId^{κ} (p \underline{M}_{Ran}^{κ} f (m \underline{It}^{κ}(m, s) t)))

For well-behaved F, p and m (such as the regular rank-2 constructors and their canonical monotonicity-preservation and monotonicity witnesses described in Section 9), the right-hand side is reducible further, and we get a common ⟶^{+}- reduct for the terms \underline{M}_{μ}^{κ}(p, m) f (\underline{in}^{κ} t) and \underline{in}^{κ} (p \underline{M}_{μ}^{κ}(p, m) f t). For general F and m, however, such further simplification is obviously impossible (take F to be a constructor variable and m an object variable assumed to inhabit \underline{mon}^{κ→κ} F).

It is also true that if a monotone F : κ → κ preserves monotonicity, then \underline{ν}^{κ}F : κ is canonically monotone.

6 Refined Conventional Iteration

Let MIt_{=}^{ω} be the restriction of GMIt^{ω} where the vector H⃗ : κ′ of H’s in the typing of GMIt^{κ} and GMCoit^{κ} only consists of identities Id. Consequently, one changes the name of GMIt^{κ} to MIt_{=}^{κ} and GMCoit^{κ} to MCoit_{=}^{κ}. The reduction rules do not change (except for the names just introduced).

We shall now proceed to the presentation of a system of conventional iteration corresponding to the system MIt_{=}^{ω}. The system will be called It_{=}^{ω} and is the system discussed in Abel and Matthes (2003). In Section 7, arbitrary vectors H⃗ will be reintroduced and a system GIt^{ω}, corresponding to the full system GMIt^{ω}, will be studied.

As a first step, we have to employ a notion of monotonicity different from \underline{mon}, with the basic containment notion ⊆ replaced with the refined notion of containment ≤.

Refined monotonicity We define mon^{κ} := λF. F ≤^{κ} F, hence

\begin{aligned}mon^{κ→κ′} & = & λF. F ≤^{κ→κ′} F \\ & = & λF. ∀X^{κ}∀Y^{κ}. X ≤^{κ} Y → F X ≤^{κ′} F Y & : & (κ → κ′) → ∗ \end{aligned}

The type mon^{κ} F, seen as a proposition, asserts essentially that F is monotone in all argument positions, for monotone argument values. The same type is used in polytypic programming for generic map functions in Hinze (2002) as well as in Altenkirch and McBride (2003). Contrast this with \underline{mon}^{κ} F which asserts that F is monotone in its first argument position, for all argument values.

Notice that for k1 = ∗ → ∗, the new definition of monotonicity, mon, coincides with the old one, \underline{mon}. For higher ranks, however, the notions differ considerably. For instance, the type constructor λX. X ∘X : (κ → κ) → κ → κ, which for κ = ∗ we disproved to be monotonic w. r. t. the old notion in Lemma 5, is monotonic w. r. t. the new notion:

λeλf. e (e f) : mon^{(κ→κ)→κ→κ}(λXλY. X (X Y))

Also, the new definition is compatible with application: If F : κ → κ′ and X : κ are monotone, then F X : κ′ is monotone as well:

m : mon^{κ→κ′} F and n : mon^{κ} X imply m n : mon^{κ′}(F X)

The following are the canonical monotonicity witnesses for some closed F which we will need in examples later.

pair := λfλgλ⟨a, b⟩. ⟨f a, g b⟩  : mon^{∗→∗→∗} (λAλB. A × B)
fork := λf. pair^{∘} f f  : mon^{∗→∗} (λA. A × A)
either := λfλgλx. case (x, a. inl (f a), b. inr (g b)) : mon^{∗→∗→∗} (λAλB. A + B)
maybe := either id  : mon^{∗→∗} (λA. C + A)

In the definition of maybe, we assume that A does not occur free in C.

6.1 Definition of It_{=}^{ω}

The system It_{=}^{ω} is an extension of F^{ω} specified by the following typing and reduction rules.

Inductive constructors. Let κ = κ⃗ → ∗.

Formation.  μ^{κ} : (κ → κ) → κ
Introduction. in^{κ} : ∀F^{κ→κ}. F (μ^{κ}F) ⊆^{κ} μ^{κ}F

Elimination.

Γ ⊢ F : κ → κ,
Γ ⊢ m : mon^{κ→κ} F
Γ ⊢ G : κ
Γ ⊢ s : F G ⊆^{κ} G
Γ ⊢ It_{=}^{κ}(m, s) : μ^{κ}F ≤^{κ} G
Reduction.  It_{=}^{κ}(m, s) f⃗ (in^{κ} t) ⟶_{β} s (m It_{=}^{κ}(m, s) f⃗ t)
where |f⃗| = |κ⃗|.

This system is “conventional” in the sense \underline{It}^{ω} is conventional: Iteration is only possible in the presence of a monotonicity witness m, being our representation of functoriality. And the argument s to It_{=}^{κ} (the “step term”) has the type F G ⊆^{κ} G, making (G, s) the syntactic representation of an F -algebra. Somewhat surprisingly, the type of It_{=}^{κ}(m, s) is not μ^{κ}F ⊆^{κ} G, hence there seems to be a mismatch: The type of in^{κ} and the step term are based on the view of functors inhabiting types of the form F_{1} ⊆^{κ} F_{2} but the result type of iteration is of the stronger form F_{1} ≤^{κ} F_{2}. But this strengthening is needed to ensure subject reduction since the monotonicity witness m is applied to the iterator. It is also crucial for the following fact:

Lemma 6 (Monotonicity of Least Fixed-Points) If type constructor F : κ → κ is monotone, witnessed by m : mon^{κ→κ} F, then μ^{κ}F is again monotone, witnessed by

M_{μ}^{κ}(m) := It_{=}^{κ}(m, in^{κ}) : mon^{κ}(μ^{κ}F), where
M_{μ}^{κ}(m) f⃗ (in^{κ} t) ⟶ in^{κ} (m M_{μ}^{κ}(m) f⃗ t).

Proof. Directly by instantiation of the typing and reduction rules for It_{=}^{κ}. □

Remark 3 (Alternative Introduction Rule) To overcome the mismatch between step term and iterator mentioned above, one might accept the type of the iterator term It_{=}^{κ}(m, s) as it stands, but would use ≤^{κ} instead of ⊆^{κ} for the types of data constructor in^{κ} and step term s. In fact, this was the typing rule underlying the original submission of Abel and Matthes (2003) and a similar typing rule was suggested to us also by Peter Aczel in May 2003. However, a data constructor of type in^{κ} : F (μ^{κ}F) ≤^{κ} μ^{κ}F would have the drawback that the canonical inhabitants of higher-order inductive types would be of the form in^{κ} g⃗ t, where the g_{i} are functions. As a consequence, a single data object could have several, even infinitely many distinct normal forms. For instance, in^{k1} (λn. n + 5) (inl 10) and in^{k1} id (inl 15) would both denote the powerlist containing solely the number 15. For ground types, i. e., inductive types without embedded function spaces like powerlists, this seems unsatisfactory.

Coinductive constructors. Let κ = κ⃗ → ∗.

Formation.  ν^{κ} : (κ → κ) → κ
Elimination.  out^{κ} : ∀F^{κ→κ}. ν^{κ}F ⊆^{κ} F (ν^{κ}F)

Introduction.

Γ ⊢ F : κ → κ,
Γ ⊢ m : mon^{κ→κ} F
Γ ⊢ G : κ
Γ ⊢ s : G ⊆^{κ} F G
Γ ⊢ Coit_{=}^{κ}(m, s) : G ≤^{κ} ν^{κ}F
Reduction.  out^{κ} (Coit_{=}^{κ}(m, s) f⃗ t) ⟶_{β} m Coit_{=}^{κ}(m, s) f⃗ (s t)
where |f⃗| = |κ⃗|.

As for least fixed-points, monotonicity of greatest fixed-points can be defined canonically.

Lemma 7 (Monotonicity of Greatest Fixed-Points) If type constructor F : κ → κ is monotone, witnessed by m : mon^{κ→κ} F, then ν^{κ}F is again monotone, witnessed by

M_{ν}^{κ}(m) := Coit_{=}^{κ}(m, out^{κ}) : mon^{κ}(ν^{κ}F), where
out^{κ} (M_{ν}^{κ}(m) f⃗ t) ⟶ m M_{ν}^{κ}(m) f⃗ (out^{κ} t).

6.2 Examples

The following two developments exemplify the use of M_{μ}^{k1}, i. e., the preservation of monotonicity under formation of least fixed-points. More examples for programming in It_{=}^{ω}, also with Coit_{=}^{k1}, can be found in Abel and Matthes (2003).

Example 16 (Free Variable Renaming for de Bruijn Terms) The free variables of a de Bruijn term may be renamed by the canonical monotonicity witness of Lam, called lam below.

lamf := λeλf. either f (either (fork (e f)) (e (maybe f))) : mon^{k2} LamF
lam := M_{μ}^{k1}(lamf)  : mon^{k1} Lam

The reduction behavior shows that we have indeed obtained the mapping function for de Bruijn terms:

lam f (var a) ⟶^{+} var^{∘} (f a)
lam f (app t_{1} t_{2}) ⟶^{+} app^{∘} (lam f t_{1}) (lam f t_{2})
lam f (abs r) ⟶^{+} abs^{∘} (lam (maybe f) r)

A special case of free variable renaming extends the free variable supply (the context) of a given term with a new variable (0) and renames the original free variable supply accordingly (n ↦ n + 1). We call the corresponding program weak, as it corresponds to the weakening rule of natural deduction.

weak := lam inr : ∀A. Lam A → Lam (1 + A)

Example 17 (Reversing a Powerlist) A reversal program for powerlists is obtainable from the monotonicity witness of PList canonically generated from a noncanonical monotonicity witness of PListF.

The canonical monotonicity witnesses of PListF and PList are

plistf := λeλf. either f (e (fork f)) : mon^{k2} PListF
plist := M_{μ}^{k1}(plistf)  : mon^{k1} PList

The reversal program, however, does not make use of the canonical monotonicity witnesses. It is manufactured as follows:

swap := λfλ⟨a_{1}, a_{2}⟩. ⟨f a_{2}, f a_{1}⟩  : mon^{k1} (λA.A × A)
revf′ := λeλf. either f (e (swap f)) : mon^{k2} PListF
rev′ := M_{μ}^{k1}(revf′)  : mon^{k1} PList
rev := rev′ id  : PList ⊆^{k1} PList
rev′ f (zero a) ⟶^{+} zero^{∘} (f a)
rev′ f (succ l) ⟶^{+} succ^{∘} (rev′ (swap f) l)

Specializing f to id in the reduction rules, it becomes traceable that rev reverses a powerlist.

6.3 Embedding It_{=}^{ω} into MIt_{=}^{ω}

The iterator and coiterator of It_{=}^{ω} are definable within MIt_{=}^{ω} (see the beginning of this section) so that the typing rules are obeyed and reduction is simulated. We define:

It_{=}^{κ}(m, s) := MIt_{=}^{κ}(λitλf⃗λt. s (m it f⃗ t))
Coit_{=}^{κ}(m, s) := MCoit_{=}^{κ}(λcoitλf⃗λt. m coit f⃗ (s t))

Embedding MIt_{=}^{ω} into It_{=}^{ω} in a typing- and reduction-preserving way seems to be impossible, except for the uninformative embedding through F^{ω}.

7 Generalized Refined Conventional Iteration

Similar to MIt_{=}^{ω}, it is also possible to define a conventional-style counterpart to GMIt^{ω}. We will now present a system GIt^{ω} that accomplishes this. One important aspect is that the efficient folds of Martin, Gibbons, and Bayley (2003) are directly definable in this system. This will be shown later on in Section 9.

7.1 Definition of System GIt^{ω}

System GIt^{ω} recasts the generality of System GMIt^{ω} following the design of System It_{=}^{ω}. It generalizes It_{=}^{ω} in two directions: ≤ is generalized to ≤H⃗, and an additional type constructor parameter F′ : κ → κ appearing in the type of m adds further flexibility. Compared to It_{=}^{ω}, only the typing rules are changed; the reduction rules are the same. Significantly, the term m in GIt^{κ}(m, s) is no longer a monotonicity witness in general, because of the changed type. Still, we consider it to be a form of conventional iteration as the division of work between the step term s and the pseudo monotonicity witness m is exactly the same as in the case of iteration of system It_{=}^{ω}: The term s handles assembling the result of a call of the iterative function from the results of the recursive calls while m organizes the recursive calls.

GIt^{ω} is specified by the following constants and typing and reduction rules.

Inductive constructors. Let κ = κ⃗ → ∗.

Formation.  μ^{κ} : (κ → κ) → κ
Introduction. in^{κ} : ∀F^{κ→κ}. F (μ^{κ}F) ⊆^{κ} μ^{κ}F

Elimination.

Γ ⊢ F, F′ : κ → κ Γ ⊢ H⃗ : κ⃗ → κ⃗

Γ ⊢ m : ∀X^{κ}∀Y^{κ}. X ≤κ ; H⃗ Y → F X ≤κ ; H⃗ F′ Y

Γ ⊢ G : κ

Γ ⊢ s : F′ G ⊆^{κ} G

Γ ⊢ GIt^{κ}(m, s) : μ^{κ}F ≤κ ; H⃗ G

Reduction.  GIt^{κ}(m, s) f⃗ (in^{κ} t) ⟶_{β} s (m GIt^{κ}(m, s) f⃗ t)

where |f⃗| = |κ⃗|.

Coinductive constructors. Let κ = κ⃗ → ∗.

Formation.  ν^{κ} : (κ → κ) → κ
Elimination.  out^{κ} : ∀F^{κ→κ}. ν^{κ}F ⊆^{κ} F (ν^{κ}F)

Introduction.

Γ ⊢ F′, F : κ → κ
Γ ⊢ H⃗ : κ⃗ → κ⃗
Γ ⊢ m : ∀X^{κ}∀Y^{κ}. X H⃗≤^{κ} Y → F′ X H⃗≤^{κ} F Y
Γ ⊢ G : κ
Γ ⊢ s : G ⊆^{κ} F′ G
Γ ⊢ GCoit^{κ}(m, s) : G H⃗≤^{κ} ν^{κ}F
Reduction.  out^{κ} (GCoit^{κ}(m, s) f⃗ t) ⟶_{β} m GCoit^{κ}(m, s) f⃗ (s t)
where |f⃗| = |κ⃗|.

Evidently, It_{=}^{ω} is (apart from different names for iterators and coiterators) just the special case with F′ = F and H⃗ = I⃗d.

7.2 Examples

We demonstrate programming in GIt^{ω} on two examples.

Example 18 (Summing up a Powerlist, Revisited) In GIt^{ω}, the implementation of the summation of a powerlist in system GMIt^{ω} (Example 12) can be closely mimicked. We can define

sum′ := GIt^{k1}(m, s)
: PList ≤_{H}^{k1} G = ∀A∀ . (A → Nat) → PList A → Nat

where

G := λ . Nat : k1
H := λ . Nat : k1
Q := anything : k1
F′ := λXλA. Nat + X (Q A) : k2
m := λeλf. either f (e (λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2}))
: ∀X∀Y. X ≤_{λ . Nat}^{k1} Y → PListF X ≤_{λ . Nat}^{k1} F′ Y
= ∀X∀Y. (∀A′∀B. (A′ → Nat) → X A′ → Y B)
→ ∀A∀B′. (A → Nat) → A + X (A × A) → Nat + Y (Q B′)
s := λt. match t with inl n ↦ n | inr n ↦ n
: F′ (λ . Nat) ⊆^{k1} λ . Nat = ∀ . Nat + Nat → Nat

The reduction behavior is precisely that of sum′ in Example 12, but the work accomplished by s in that example is now divided between m and s. Crucially, the addition (the non-polymorphic operation of the recursive definition) takes place in m. The reason why any type constructor of kind k1 can be used as Q is that the type constructors G and H used by the iterator are constant, which is a degenerate situation. (In Example 25, Q will be chosen in a canonical way.)

We see that one should not at all think of real monotonicity witnesses in GIt^{ω}. The pseudo monotonicity witnesses are meant to do work specific to the programming task at hand. Example 17 of powerlist reversal by means of a noncanonical monotonicity witness demonstrated this idea as well.

The next example shows that the iterator of GIt^{ω} turns out to be very handy when one wants to move on from variable renaming in de Bruijn terms to substitution.

Example 19 (Substitution for de Bruijn Terms) In GIt^{ω}, the following smooth definition of substitution for de Bruijn terms as an iteration is possible, where we first define lifting as in the structurally inductive approach in Altenkirch and Reus (1999).

lift := λfλx. case (x, u. var (inl u), a. weak (f a))
: ∀A∀B. (A → Lam B) → 1 + A → Lam (1 + B)
subst := GIt^{k1}(m, s)
: Lam ≤_{Lam}^{k1} Lam = ∀A∀B. (A → Lam B) → (Lam A → Lam B)

where

F′ := λXλA. Lam A + (X A × X A + X (1 + A)) : k2
m := λeλf. either f (either (fork (e f)) (e (lift f)))
: ∀X∀Y. X ≤_{Lam}^{k1} Y → LamF X ≤_{Lam}^{k1} F′ Y
= ∀X∀Y. (∀A∀B. (A → Lam B) → X A → Y B)
→ ∀A∀B. (A → Lam B)
→ A + (X A × X A + X (1 + A))
→ Lam B + (Y B × Y B + Y (1 + B))
s := λt. match t with inl u ↦ u | inr t′ ↦ in^{k1}(inr t′)
: F′ Lam ⊆^{k1} Lam
= ∀A. Lam A + (Lam A × Lam A + Lam (1 + A)) → Lam A

Notice that we use weakening weak of Example 16 in the definition of the lifting function lift, implicitly embedding It_{=}^{ω} into GIt^{ω}. The program subst has exactly the expected reduction behavior in the sense that, if f : A → Lam B is a substitution rule, then subst f : Lam A → Lam B behaves as the corresponding substitution function replacing the variables of its de Bruijn term argument according to the rule f:

subst f (var a) ⟶^{+} f a
subst f (app t_{1} t_{2}) ⟶^{+} app^{∘} (subst f t_{1}) (subst f t_{2})
subst f (abs r) ⟶^{+} abs^{∘} (subst (lift f) r)

Alternatively, one might program substitution within It_{=}^{ω}, but this would necessitate an explicit use of a right Kan extension—a fact swept under the carpet in Altenkirch and Reus (1999). In GIt^{ω}, this more liberal format is part of the design.

7.3 Embeddings between GIt^{ω} and GMIt^{ω}

GIt^{ω} embeds into GMIt^{ω} much the same way as It_{=}^{ω} embeds into MIt_{=}^{ω}:

GIt^{κ}(m, s) := GMIt^{κ}(λitλf⃗λt. s (m it f⃗ t))
GCoit^{κ}(m, s) := GMCoit^{κ}(λcoitλf⃗λt. m coit f⃗ (s t))

The embedding of GMIt^{ω} into GIt^{ω} is much more interesting and again just a definitional embedding.

GMIt^{κ}(s) := GIt^{κ}(lanLeq^{κ→κ} id, leqLan^{κ→κ} s)
GMCoit^{κ}(s) := GCoit^{κ}(ranLeq^{κ→κ} id, leqRan^{κ→κ} s)

Here, we used the definitions in the proof of Lemma 3. It is easy to check that, with these definitions,

GMIt^{κ}(s) f⃗ (in^{κ} t) ⟶^{+} s GMIt^{κ}(s) f⃗ t
out^{κ}(GMCoit^{κ}(s) f⃗ t) ⟶^{+} s GMCoit^{κ}(s) f⃗ t

Hence, the reductions are simulated. Type-preservation has not yet been addressed; however, it is a consequence of the following lemma.

Lemma 8 Assume κ = κ⃗ → ∗, n = |κ⃗|, κ′ = κ⃗ → κ⃗, F : κ → κ and H⃗ : κ′. Define the constructor

F′ := λY λY⃗ ∃X^{κ}. X ≤κ ; H⃗ Y → Lan^{κ}(F X)(H⃗ Y⃗) : κ → κ.

Here, (H⃗ Y⃗) means (H_{1} Y_{1}) … (H_{n} Y_{n}). Then, we have the following typings:

lanLeq^{κ→κ} : ∀X^{κ}∀Y^{κ}. F′Y ⊆^{κ} F′Y → X ≤κ ; H⃗ Y → F X ≤κ ; H⃗ F′ Y
leqLan^{κ→κ} : ∀G^{κ}. (∀X^{κ}. X ≤κ ; H⃗ G → F X ≤κ ; H⃗ G) → F′ G ⊆^{κ} G

Redefine the constructor F′ to be

F′ := λXλX⃗∀Y^{κ}. X H⃗≤^{κ} Y → Ran^{κ}(F Y)(H⃗ X⃗).

Then, types can be assigned as follows:

ranLeq^{κ→κ} : ∀X^{κ}∀Y^{κ}. F′X ⊆^{κ} F′X → X H⃗≤^{κ} Y → F′ X H⃗≤^{κ} F Y
leqRan^{κ→κ} : ∀G^{κ}. (∀X^{κ}. G H⃗≤^{κ} X → G H⃗≤^{κ} F X) → G ⊆^{κ} F′ G

Proof. By simple unfolding of the definitions of Lan^{κ} and Ran^{κ}. Observe that the vector H⃗ enters only the arguments; the Kan extensions are not formed along H⃗. The premisses F′Y ⊆^{κ} F′Y and F′X ⊆^{κ} F′X are there just for perfect fit with the definitions of lanLeq and ranLeq. They will later always be instantiated by id. □

With the lemma at hand, the above-defined embedding is easily seen to be type-preserving. Certainly, the name F′ has been chosen to name the additional constructor which can freely be chosen in GIt^{ω}. For the inductive case, it is the definition involving Lan^{κ}, for the coinductive case, F′ needs Ran^{κ}.

While all of GMIt^{ω} can be embedded into GIt^{ω}—using canonical definitions of F′ and canonical terms m which do not have an interesting operational meaning—we have seen in the Example 18 that the term m can really be problem-specific and even do the essential part of the computation. Many more such terms will be shown in Section 9. They will be found in a systematic way by induction on the build-up of regular rank-2 constructors. Hence, they are still generic but much less uniform than those constructed in the embedding shown above.

8 Advanced Examples

Since all of the systems considered in this article definitionally embed into MIt^{ω}, we do the following examples in MIt^{ω} and freely use the iteration schemes from everywhere (since, for ⟶^{+}, there is no difference between the original systems and the embeddings). Therefore, we can also use every definition from the previous examples.

Example 20 (Explicit Substitutions) Examples 16 and 19 have shown that de Bruijn terms constitute a Kleisli triple (Lam, var, subst) with unit var : ∀A. A → Lam A and bind operation

subst : ∀A∀B. (A → Lam B) → (Lam A → Lam B).

From the “Kleisli triple” formulation of Lam we mechanically get the “monad” formulation (Lam, var, flatten) with flatten the join or multiplication operation of the monad, since flatten : ∀A. Lam (Lam A) → Lam A can be obtained from subst as flatten := subst id.

Consider now an extension of de Bruijn terms with explicit flattening which is a special form of explicit substitution. This truly nested datatype is definable as follows:^{2}

L̂amF := λXλA. LamF X A + X (X A) : k2
L̂am := μ^{k1} L̂amF  : k1
v̂ar := λb. in^{k1} (inl (inl b))  : ∀A. A → L̂am A
âpp := λt_{1}λt_{2}. in^{k1} (inl (inr (inl ⟨t_{1}, t_{2}⟩))) : ∀A. L̂am A → L̂am A → L̂am A
âbs := λr. in^{k1} (inl (inr (inr r)))  : ∀A. L̂am (1 + A) → L̂am A
ˆflat := λe. in^{k1} (inr e)  : ∀A. L̂am (L̂am A) → L̂am A

Renaming of free variables in a term is implemented by the canonical monotonicity witness of L̂am, derived from the following generic monotonicity witness l̂amf for the datatype functor L̂amF, using lamf from example 16:

l̂amf := λgλf. either (lamf g f) (g (g f)) : mon^{k2} L̂amF
l̂am := M_{μ}^{k1}(l̂amf) = It_{=}^{k1}(l̂amf, in^{k1}) : mon^{k1} L̂am

Note that the treatment of explicit flattening in the definition of l̂amf would be impossible with basic monotonicity \underline{mon}^{k1}, see Lemma 5. The following reduction behavior immediately follows:

l̂am f (v̂ar^{∘} a) ⟶^{+} v̂ar^{∘} (f a)
l̂am f (âpp^{∘} t_{1} t_{2}) ⟶^{+} âpp^{∘} (l̂am f t_{1}) (l̂am f t_{2})
l̂am f (âbs^{∘} r) ⟶^{+} âbs^{∘} (l̂am (maybe f) r)
l̂am f (ˆflat^{∘} e) ⟶^{+} ˆflat^{∘} (l̂am (l̂am f) e)

As was the case with the summation for the truly nested datatype Bush in Example 13, the termination of l̂am is not obvious at all: In the recursive call in the last line, the parameter f is changed to l̂am f, hence using the whole iteratively defined function l̂am f. Nevertheless, termination holds by strong normalization of MIt^{ω}.

Using l̂am, we can represent full explicit substitution

esubst : ∀A∀B. (A → L̂am B) → (L̂am A → L̂am B)
esubst := λfλt. ˆflat (l̂am f t)

2 This presentation should be compared with the slightly unmotivated extension of de Bruijn’s notation in Bird and Paterson (1999b, Sect. 5), where âbs and ˆflat are replaced by just one constructor of type ∀A. L̂am (1 + L̂am A) → L̂am A, which again gives rise to true nesting. However, that constructor could easily be defined as ˆflat ∘ âbs in the present system.

esubst is explicit substitution in the sense that a term of the form ˆflat (r) is returned for esubst f t, hence only renaming but no substitution is carried out.

Alternatively, one can represent full explicit substitution by way of a data constructor like ˆflat. If we redefine L̂am to be

L̂am := μ^{k1}(λXλA. LamF X A + ∃B. (B → X A) × X B),

we may set êxs := λfλt. in^{k1} (inr (pack⟨f, t⟩)), which (after exchanging the bound variables A and B) receives the type we have above for esubst. Notice that ∃B. (B → X A)×X B = (\underline{Lan}^{k1} X) (X A), with the naive Kan extension defined in Section 5.3. From Lemma 4, it follows that (\underline{Lan}^{k1} X) (X A) and X (X A) are logically equivalent if X is monotone. Since the fixed point L̂am is monotone, the variant just discussed is logically equivalent with our example above. The formulation with explicit flattening has the advantage of not using quantifiers in the datatype definition. Instead of that, it needs true nesting.

Example 21 (Resolution of Explicit Substitutions) The set of de Bruijn terms Lam can be embedded into the set of de Bruijn terms L̂am with explicit flattening. The embedding function emb : ∀A. Lam A → L̂am A can be defined by iteration in a straightforward manner. The other direction is handled by a function eval : ∀A. L̂am A → Lam A which has to resolve the explicit flattenings. With the help of It_{=}^{k1}, this is defined by

eval′ := It_{=}^{k1}(l̂amf, s) : L̂am ≤^{k1} Lam
eval := eval′ id  : L̂am ⊆^{k1} Lam

where s := λt. case (t, t′. in^{k1} t′, e. flatten e) : L̂amF Lam ⊆^{k1} Lam, with flatten taken from the previous example. The most interesting case of the reduction behavior is

eval′ f (ˆflat e) ⟶^{+} flatten (eval′ (eval′ f) e).

As in the last example, the nesting in the definition of datatype L̂am is reflected in the nested recursion in eval′.

Example 22 (Redecoration of Finite Triangles) In the following, we reimplement the redecoration algorithms for finite triangles, as opposed to infinite ones. Passing from coinductive to inductive types, we need to apply rather different programming methodologies.

Again, fix a type E : ∗ of matrix elements. The type FTri A of finite triangular matrices with diagonal elements in A and ordinary elements E can be obtained as follows:

FTriF := λXλA. A × (1 + X (E × A)) : k2
FTri := μ^{k1} FTriF  : k1

The columnwise decomposition and visualization of elements of type FTri A is done as for the infinite triangles of type Tri A. Finiteness arises from taking the least fixed-point. By taking the left injection into the sum 1 + …, one can construct elements without further recurrence, hence the type FTri A is not empty unless A is. More generally, elements of type FTri A are constructed by means of

sg := λa. in^{k1} ⟨a, inl ⟨⟩⟩ : ∀A. A → FTri A, and
cons := λaλr. in^{k1} ⟨a, inr r⟩ : ∀A. A → FTri (E × A) → FTri A.

There are two monotonicity witnesses for FTriF, for \underline{mon}^{k2} and for mon^{k2}:

\underline{ftrif} := λg. pair id (maybe g)  : \underline{mon}^{k2}
ftrif := λgλf. pair f (maybe (g (pair id f))) : mon^{k2}
ftri := M_{μ}^{k1}(ftrif)  : mon^{k1} FTri

Note that the last definition uses means of It_{=}^{ω}. For the definition of redecoration we need methods to decompose triangles. The following function ftop returns the first column of a triangle, which happens to be just the topmost diagonal element. Later we will define another function fcut which takes the remaining trapezium and removes its top row.

ftop : ∀A. FTri A → A
ftop := \underline{It}^{k1}(\underline{ftrif}, fst)

This function uses the iterator from \underline{It}^{ω}. It could be also be implemented in It_{=}^{ω} as It_{=}^{k1}(ftrif, fst) id. Either way, reduction is as expected:

ftop (sg a) ⟶^{+} a
ftop (cons a r) ⟶^{+} a

As announced above, we need to define a function fcut that cuts off the top row of a trapezium FTri (E × A) to obtain a triangle FTri A. Since in the domain type of this function, the argument to FTri is not a type variable, it does not fit directly into any of our iteration schemes. Aiming at using GMIt^{ω}, we need to define a more general function fcut′ : FTri ≤_{H}^{k1} FTri with H := λA. E × A. Note that this is a rare instance of the scheme μF ≤_{H}^{κ_{1}} G with G ≠ H ≠ Id.

fcut′ : ∀A∀B. (A → E × B) → FTri A → FTri B
fcut′ := GMIt^{k1}(λfcut′λf. pair (snd ∘f) (maybe (fcut′ (pair id f))))
fcut′ f (sg a) ⟶^{+} sg^{∘} (snd (f a))
fcut′ f (cons a r) ⟶^{+} cons^{∘} (snd (f a)) (fcut′ (pair id f) r)

The cut function is obtained by specializing f to the identity.

fcut : ∀A. FTri (E × A) → FTri A
fcut := fcut′ id

Unfortunately, in the β-theory alone we do not get the desired reduction behavior. It holds that

fcut (sg ⟨e, a⟩)  ⟶^{+} a, and
fcut (cons ⟨e, a⟩ r) ⟶^{+} cons a (fcut′ (pair id id) r), but
fcut (cons ⟨e, a⟩ r) ⟶ / ^{+} cons a (fcut r).

However, if one added a tiny bit of extensionality, one would have extensional equality of pair id id and id, which would imply extensional equality of left and right hand side of the last relation.

For the definition of redecoration, we will again need a means of lifting a redecoration rule on triangles to one on trapeziums. It is defined precisely as in Example 11, but with the new auxiliary functions.

flift : ∀A∀B. (FTri A → B) → FTri (E × A) → E × B
flift := λfλt. ⟨fst (ftop t), f (fcut t)⟩

Finally, we can define redecoration fredec. Its description is the same as that for redec that works on infinite triangles in Example 11. The only difference is that we swapped its arguments such that its type now is

∀A. FTri A → ∀B. (FTri A → B) → FTri B = FTri ⊆^{k1} G,
where  ∀B. (FTri A → B) → FTri B =: G.

Unfortunately, G is not a right Kan extension (which might have allowed a direct definition of fredec inside GMIt^{ω}), but G = (Ran_{Id}^{k1} FTri) ∘ FTri. Moreover, fredec essentially will need primitive recursion, not just iteration. Since the present article confines itself to iteration, the standard trick with products is adopted to represent primitive recursion: We will define a more general function fredec′ : FTri ⊆^{k1} FTri ×^{k1}G. It seems that any hardwired Kan extensions in the system would only complicate the following definition which is done in plain MIt^{ω}.

fredec′ : ∀A. FTri A → (FTri A × (∀B. (FTri A → B) → FTri B))
fredec′ := MIt^{k1}(λfredec′λt.
let fid = fst ∘ fredec′ in
let fredec = snd ∘ fredec′ in
let r  = in^{k1}(\underline{ftrif} fid t) in
⟨r, λf. match t with
sg^{−}  ↦ sg (f r)
cons^{−} x ↦ cons (f r) (fredec x (flift f))⟩

The function fredec′ actually defines two functions simultaneously: fid := fst ∘ fredec′ : FTri ⊆^{k1} FTri, an iterative identity on finite triangles, and fredec := snd ∘ fredec′ : FTri ⊆^{k1} G, the actual redecoration function. The iterative identity is needed to reconstruct the current function argument r from its unfolded version t. Why a simple “r = in^{k1}t” does not do the job can be seen from the types of the bound variables:

fredec′ : X ⊆^{k1} FTri ×^{k1}G
t  : FTriF X A = A × (1 + X (E × A))
fid  : X ⊆^{k1} FTri
r  : FTri A
f  : FTri A → B
x  : X (E × A)
fredec : X (E × A) → (FTri (E × A) → (E × B)) → FTri (E × B)

Since in the Mendler discipline t is not of type FTriF FTri A, we cannot apply in^{k1} to t directly, but need a conversion function of type X ⊆^{k1} FTri. The functionality of fredec′ can be understood through its reduction behavior:

fredec′ (sg a) ⟶^{+} ⟨sg^{∘} a, λf. sg (f (sg^{∘} a))⟩
fredec′ (cons a x) ⟶^{+} ⟨cons^{∘} a (fid x),

λf. cons (f (cons^{∘} a (fid x))) (fredec x (flift f))⟩

Untangling the two intertwined functions within fredec′, we get the following reduction relations from which correctness of the implementation becomes apparent.

fid (sg a)  ⟶^{+} sg^{∘} a
fid (cons a x)  ⟶^{+} cons^{∘} a (fid x)
fredec (sg a) f  ⟶^{+} sg (f (sg^{∘} a))
fredec (cons a x) f ⟶^{+} cons (f (cons^{∘} a (fid x))) (fredec x (flift f))

Since fid is an iteratively defined identity, fid x with x a variable does not reduce to x. Apart from this deficiency, which could be overcome if a scheme of primitive recursion was available, fredec behaves as specified.

9 Efficient Folds

In this section, we relate our iteration schemes to other approaches found in the literature. Bird and Meertens (1998) were the first to publish iteration schemes for nested datatypes, called simple folds, which correspond to our System \underline{It}^{ω}. To overcome their limited usability, Bird and Paterson (1999a) formulated generalized folds. Their proposal inspired our work on System GMIt^{ω}, but our attempts to establish a clear relationship between their and our approach failed, for reasons we can explain better at the end of this section.

The generalized folds of Bird and Paterson exhibit an inefficiency in their computational behavior. To mend this flaw, Hinze (2000a) proposed an alternative system of folds for nested datatypes. Inspired from that, Martin, Gibbons and Bayley (2003) presented their efficient folds, or efolds for short, which are closest to Bird and Paterson’s generalized folds.

All of the abovementioned approaches only deal with least fixed points μ^{k1}F of special type constructors F : k2 of rank 2, which are called hofunctors (short for higher-order functors). Since our systems have no such restrictions, it may well be possible that the other approaches can be simulated in our systems. In the following, we will demonstrate this for the proposal of Martin, Gibbons, and Bayley (2003). Their efolds can be expressed in System GIt^{ω}.

Hofunctors. Following Martin, Gibbons, and Bayley (2003), hofunctors are type constructors F : k2 of one of the following shapes:

(a) λ .Q  with m_{Q} : mon^{k1} (note Q : k1)  constant
(b) λX.X  identity
(c) F_{0} +^{k2} F_{1}  with F_{0}, F_{1} hofunctors  disjoint sum
(d) F_{0} ×^{k2} F_{1}  with F_{0}, F_{1} hofunctors  product
(e) λX. Q ∘ (F_{0} X) with m_{Q} : mon^{k1} and F_{0} hofunctor composition
(f) λX. X ∘ (F_{0} X) with F_{0} hofunctor  nesting

Note that this inductive characterization is not deterministic, e. g., one can always apply rule (e) with Q = Id without modifying the hofunctor extensionally. Even more, case (b) is a special case of (f) with F_{0} = λ . Id. Probably, case (b) is present in Martin, Gibbons, and Bayley (2003) in order to characterize non-nested hofunctors by rules (a) – (e).

Example 23 (Hofunctors) All of the type constructors F : k2 whose fixedpoints we considered in the previous examples are hofunctors. For instance,

PListF := λXλA. A + X (A × A)
= (λ . Id) +^{k2} λX. X ∘ (((λ . Id) ×^{k2} (λ . Id)) X)
BushF := λXλA. 1 + X (X A)
= (λ λ .1) +^{k2} λX. X ∘ ((λX. X) X)
LamF := λXλA. A + ((X A × X A) + X (1 + A))
= (λ . Id) +^{k2} ((Id ×^{k2} Id) +^{k2} λX. X ∘ ((λ λA. 1 + A) X))

Efficient folds are another means to construct functions of type μ^{k1}F ≤_{H}^{k1} G which eliminate inhabitants of the nested datatype μ^{k1}F. As in the previous sections, F : k2 and G, H : k1, but now F additionally needs to be a hofunctor. By induction on the generation of hofunctor F we define a type constructor F_{H}^{F} : k2 which is parametric in H, a sequence of types D⃗_{H}^{F} all of which are parametric in H, and a term

M^{F} (d⃗) : ∀X∀Y. X ≤_{H}^{k1} Y → F X ≤_{H}^{k1} F_{H}^{F} Y

which is dependent on a sequence of terms d⃗: D⃗_{H}^{F}. How exactly we obtain F_{H}^{F}, D⃗_{H}^{F} and M^{F} (·) will be explained later. With these definition, we can introduce typing and reduction for efolds.

Elimination.

Γ ⊢ F : k2 hofunctor
Γ ⊢ H : k1
Γ ⊢ d⃗ : D⃗_{H}^{F}
Γ ⊢ G : k1
Γ ⊢ s : F_{H}^{F} G ⊆^{k1} G
Γ ⊢ efold^{F} (d⃗, s) : μ^{k1}F ≤_{H}^{k1} G
Reduction.  efold^{F} (d⃗, s) f (in^{k1} t) ⟶_{β} s (M^{F} (d⃗) efold^{F} (d⃗, s) f t)

Embedding into GIt^{ω}. Efficient folds are simply an instance of generalized conventional iteration for kind k1.

efold^{F} (d⃗, s) := GIt^{k1}(M^{F} (d⃗), s)

To see that this definition preserves typing and reduction, recall the k1 elimination and computation rule for generalized conventional iteration:

Elimination. Γ ⊢ m : ∀X∀Y. X ≤_{H}^{k1} Y → F X ≤_{H}^{k1} F′ Y

Γ ⊢ s : F′ G ⊆^{k1} G
Γ ⊢ GIt^{k1}(m, s) : μ^{k1}F ≤_{H}^{k1} G
Reduction.  GIt^{k1}(m, s) f (in^{k1} t) ⟶_{β} s (m GIt^{k1}(m, s) f t)

The free parameter F′ : k2 in the elimination rule is instantiated by the type constructer F_{H}^{F} generated from F, and m is replaced by M^{F} (d⃗), which assembles the simpler terms d⃗ into a pseudo monotonicity witness. Hence, efficient folds can be viewed as a user interface for GIt^{k1}, which takes on the difficult task of choosing an appropriate F′.

Definition of efficient folds. To complete the description of efolds, the hofunctor F_{H}^{F}, the types D⃗_{H}^{F} and the term M^{F} are defined inductively by the hofunctoriality of F. In principle, any consistent definition gives rise to a class of efficient folds, the question is only how useful they will be, i. e., which functions can be programmed as instances of these efolds. Figure 2 lists Martin, Gibbon and Bayley’s (2003) choices of F_{H}^{F}, D⃗_{H}^{F} and M^{F} for each rule (a – f) how to generate a hofunctor. Especially interesting are cases (b), (e) and (f) where a new term d is assumed. We will comment on the role of these terms later. Also observe, that in the last two cases F_{H}^{F} is defined via F_{0}, not recursively via F_{H}^{F_{0}}. This is due to the emission of a new term d.

F  F_{H}^{F}  d⃗ : D⃗_{H}^{F}

M^{F} (d⃗) e f

(a) λ .Q  λ . Q ∘ H

m_{Q} f

(b) λX.X  λX.X  d : H ⊆^{k1} H

e (d ∘ f)

(c) F_{0} +^{k2} F_{1}  F_{H}^{F_{0}} +^{k2} F_{H}^{F_{1}}  d⃗_{0} : D⃗_{H}^{F_{0}},
d⃗_{1} : D⃗_{H}^{F_{1}}

either (M^{F_{0}}(d⃗_{0}) e f) (M^{F_{1}}(d⃗_{1}) e f)

(d) F_{0} ×^{k2} F_{1}  F_{H}^{F_{0}} ×^{k2} F_{H}^{F_{1}}  d⃗_{0} : D⃗_{H}^{F_{0}},
d⃗_{1} : D⃗_{H}^{F_{1}}

pair (M^{F_{0}}(d⃗_{0}) e f) (M^{F_{1}}(d⃗_{1}) e f)

(e) λX. Q ∘ (F_{0} X) λX. Q ∘ H ∘ (F_{0} X) d : ∀X. F_{H}^{F_{0}} X ⊆^{k1} H ∘ (F_{0} X),
d⃗_{0} : D⃗_{H}^{F_{0}}

m_{Q} (d ∘ (M^{F_{0}}(d⃗_{0}) e f))

(f) λX. X ∘ (F_{0} X) λX. X ∘ (F_{0} X)  d : ∀X. F_{H}^{F_{0}} X ⊆^{k1} H ∘ (F_{0} X),
d⃗_{0} : D⃗_{H}^{F_{0}}

e (d ∘ (M^{F_{0}}(d⃗_{0}) e f))

Figure 2. Definition of efficient folds

Example 24 (Efolds for Powerlists, Typing) Recall that the general typing rule for efold was

Γ ⊢ d⃗ : D⃗_{H}^{F}
Γ ⊢ s : F_{H}^{F} G ⊆^{k1} G

Γ ⊢ efold^{F} (d⃗, s) : μ^{k1}F ≤_{H}^{k1} G

where we took the freedom to omit the kinding judgements of F, G and H for conciseness. The typing of an efficient fold for a concrete hofunctor F requires only the recursively computed F_{H}^{F} and D⃗_{H}^{F}. For powerlists, we obtain the following instances.

PListF = λXλA. A + X (A × A)
F_{H}^{PListF} = λXλA. H A + X (A × A)
D⃗_{H}^{PListF} = (∀X∀A. H A × H A → H (A × A))

Instantiating the general rule for efficient folds and expanding the definitions of ⊆^{k1} and ≤_{H}^{k1}, we obtain efficient folds for powerlists.

Γ ⊢ d : ∀A. H A × H A → H (A × A)
Γ ⊢ s : ∀A. H A + G (A × A) → G A
Γ ⊢ efold^{PListF}(d, s) : ∀A∀B. (A → H B) → PList A → G B

We will refer to d as distributivity term for reasons its type makes apparent: d witnesses that the product constructor × distributes over constructor H.

Example 25 (Summing up a Powerlist, Typing) We can define function sum′ of Example 18 using efficient folds for powerlists. We set G := H := λ .Nat, as in the previous implementations of sum′, and

sum′ := efold^{PListF}(d, s)  : ∀A. (A → Nat) → PList A → Nat, where
d := λ⟨n, m⟩. n + m  : Nat × Nat → Nat, and
s := λx. case (x, n. n, n. n) : Nat + Nat → Nat.

The given implementation is type-correct, we will verify the reduction behavior later.

As in the implementation using GIt^{k1} in Example 18, the task of the step term s is trivial whereas the addition happens in the other term. Back then, we could use F′ := λXλA. Nat + X (Q A) with Q any constructor in k1. With the special choice F′ := F_{λ .Nat}^{PListF}, which the given definition of efficient folds takes, Q is fixed to λA. A × A.

Example 26 (Efolds for Powerlists, Reduction) Setting m_{Id} := λfλx. f x for the canonical monotonicity witness of Id : k1, we can compute the pseudo monotonicity witness for efficient powerlist folds according to Figure 2.

d  : ∀A. H A × H A → H (A × A)
M^{PListF}(d)  : ∀X∀Y. X ≤_{H}^{k1} Y → PListF X ≤_{H}^{k1} F_{H}^{PListF} Y
= ∀X∀Y. X ≤_{H}^{k1} Y → ∀A∀B. (A → H B) →
A + X (A × A) → H B + Y (B × B)
M^{PListF}(d) e f := either (m_{Id} f) (e (d ∘ (pair (m_{Id} f) (m_{Id} f))))
⟶^{+} either (λx. f x) (e (d ∘ (fork^{∘} f)))

Note that fork is defined in terms of pair^{∘} on page 45. Using this pseudo monotonicity witness in the general reduction rule for efolds, which was

efold^{F} (d⃗, s) f (in^{k1} t) ⟶_{β} s (M^{F} (d⃗) efold^{F} (d⃗, s) f t),

we get the following reduction behavior for powerlist efolds:

efold^{PListF}(d, s) f (zero a) ⟶^{+} s (inl (f a))
= s (zero^{−} (f a))
efold^{PListF}(d, s) f (succ l) ⟶^{+} s (inr (efold^{PListF}(d, s) (d ∘ (fork^{∘} f)) l))
= s (succ^{−} (efold^{PListF}(d, s) (d ∘ (fork^{∘} f)) l))

Example 27 (Summing up a Powerlist, Reduction) Instantiating the above scheme for

sum′ := efold^{PListF}(d, s),  where
d := λ⟨n, m⟩. n + m,  and
s := λx. case (x, n. n, n. n),

we obtain the precise reduction behavior of Example 18.

Example 28 (Efolds for de Bruijn Terms) As shown in Example 23, the generating type constructor LamF for de Bruijn terms is a hofunctor. Hence, we can calculate F_{H}^{LamF} and D⃗_{H}^{LamF} according to Figure 2.

LamF = λXλA. A + (X A × X A + X (1 + A))
F_{H}^{LamF} = λXλA. H A + (X A × X A + X (1 + A))
D⃗_{H}^{LamF} = (∀A. H A → H A,
∀A. H A → H A,
∀X∀A. 1 + H A → H (1 + A))

The first two components of D⃗_{H}^{LamF} arise from the two homogeneous applications X A in LamF, the third from the heterogeneous application X (1 + A).

The efficient fold for de Bruijn terms is typed as follows:

Γ ⊢ d_{1} : ∀A. H A → H A
Γ ⊢ d_{2} : ∀A. H A → H A
Γ ⊢ d_{3} : ∀A. 1 + H A → H (1 + A)
Γ ⊢ s : ∀A. H A + (G A × G A + G (1 + A)) → G A
Γ ⊢ efold^{LamF}(d_{1}, d_{2}, d_{3}, s) : ∀A∀B. (A → H B) → Lam A → G B

Recall that maybe is the canonical monotonicity witness for λA. 1 + A. The pseudo monotonicity witness M^{LamF} is computed as

M^{LamF}(d_{1}, d_{2}, d_{3}) e f = either (m_{Id} f)
(either (pair (e (d_{1} ∘ f)) (e (d_{2} ∘ f)))
(e (d_{3} ∘ (maybe f)))).

Setting e := efold^{LamF}(d_{1}, d_{2}, d_{3}, s) this yields the following reduction behavior for this special efficient fold.

e f (var a) ⟶^{+} s (inl (f a))
= s (var^{−} (f a))
e f (app t_{1} t_{2}) ⟶^{+} s (inr (inl ⟨e (d_{1} ∘ f) t_{1}, e (d_{2} ∘ f) t_{2}⟩))
= s (app^{−} (e (d_{1} ∘ f) t_{1}) (e (d_{2} ∘ f) t_{2}))
e f (abs r) ⟶^{+} s (inr (inr (e (d_{3} ∘ (maybe f)) r)))
= s (abs^{−} (e (d_{3} ∘ (maybe f)) r))

Example 29 (Renaming and Substitution for de Bruijn Terms) The functions lam of Example 16 and subst of Example 19 can be expressed with efficient folds as

lam := efold^{LamF}(id, id, id, in^{k1}) : Lam ≤_{Id}^{k1} Lam
subst := efold^{LamF}(id, id, lift id, s) : Lam ≤_{Lam}^{k1} Lam,

where we use lift and s from Example 19.

Since composition with the identity η-expands terms, the reduction behavior of lam is not exactly as in Example 16. This problem is even more visible for subst:

subst f (var a) ⟶^{+} f a
subst f (app t_{1} t_{2}) ⟶^{+} app (subst (λx. f x) t_{1}) (subst (λx. f x) t_{2})
subst f (abs r) ⟶^{+} abs (subst (λx. lift id (maybe f x)) r)

We would have liked to see lift f instead of λx. lift id (maybe f x). Extensionally, they are equal: Both ⟶^{+}-reduce to var (inl u) for argument inl u, and both ⟶^{+}-reduce to weak (f a) for argument inr a. Certainly, also λx. f x and f are extensionally equal.

A second look at efficient folds. As we pointed out before, Figure 2 describes just one possible definition of efficient folds. One might wonder whether it could not be simplified at bit. The first case worth a discussion is (b) identity: Is it really necessary to emit a distributivity witness d : H ⊆^{k1} H here? This question has been raised already by Bird and Paterson (1999a, Sec. 4.1) for their version of generalized folds. In the last example, these terms are just instantiated with the identity id. So supposedly, they could be dropped, leading to the simpler definition

M^{λX.X}() e f := e f .

Another questionable clause is (e) composition. As mentioned in the beginning of this section, clause (e) can be iterated with Q := Id in the proof of hofunctoriality for a type constructor F. This means that one can also obtain an arbitrary number of different definitions of an efficient fold for such an F. Each iteration of the rule would emit another distributivity term d. We therefore suggest different definition clauses for case (e):

\begin{aligned}F & = & λX. Q ∘ (F_{0} X) \\ F_{H}^{F} & := & λX. Q ∘ (F_{H}^{F_{0}} X) \\ D⃗_{H}^{F} & := & D⃗_{H}^{F_{0}} \\ M^{F} (d⃗) e f & := & m_{Q} (M^{F_{0}}(d⃗) e f) \end{aligned}

In contrast to the original definition, this variant defines F_{H}^{F} recursively through F_{H}^{F_{0}}. Iteration of these clauses with Q = Id do now neither change the typing rule for the efficient fold nor the reduction behavior of the pseudo monotonicity witness M^{F}. Now, the only case where the need of a distributivity term d arises is (f) nesting. This means that for a homogeneous hofunctor F and H = Id, it holds that F_{H}^{F} = F, D⃗_{H}^{F} is empty, M^{F} is the canonical monotonicity witness of F and the eliminator efold^{F} is identical to It_{=}^{k1}.

Comparison with Bird and Paterson (1999a). Whilst for a fixed hofunctor F : k2, the efficient fold “e” is of type μ^{k1}F ≤_{H}^{k1} G, Bird and Paterson define a generalized fold “g” of type (μ^{k1}F)∘H ⊆^{k1} G. As observed by Martin, Gibbons, and Bayley (2003), both kinds of folds are interdefinable, extensionally:

\begin{aligned}g & = & e id \\ e & = & λf. g ∘ (m_{μF} f) \end{aligned}

where m_{μF} is the canonical monotonicity witness of μ^{k1}F. These equations explain why e is called “efficient”: it combines two traversals of a datastructure, a fold and a map, into a single traversal.

One might wonder whether generalized folds can also be expressed in System GMIt^{ω}. Recall the reduction rule for efficient folds:

e f (in^{k1} t) ⟶_{β} s (M^{F} (d⃗) e f t)

If we could alter the definition of M^{F} in such a way that in the resulting term M^{F} (d⃗) e f t the variable e occurred only in the form e id, then by setting f = id we would obtain a reduction rule for g which is simulated in System GMIt^{ω}. The necessary changes affect certainly clause (f) with F = F_{H}^{F} = λX. X ∘(F_{0} X) of the definition of M^{F}, which we recall in a somewhat sketchy form as follows:

Provided e : ∀A∀B. (A → H B) → X A → Y B
and  f : A → H B,
M^{F} (…) e f : F X A → F_{H}^{F} Y B
= X (F_{0} X A) → Y (F_{0} Y B)
M^{F} (…) e f := e f′,
where f′ : F_{0} X A → H (F_{0} Y B)
f′ := …

In order to obtain the reduction behavior of Bird and Paterson (1999a) we need to change the definition of M^{F} (…) e f to e id ∘ (m_{μF} f′). But this is not well-typed. Typing requires monotonicity m_{X} for the abstract type constructor X instead of m_{μF}.

To summarize this discussion, we might say that Bird and Paterson’s generalized folds are not an instance of GMIt^{ω} due to their inefficient reduction behavior. Whether they can be simulated in System F^{ω} in a different way, remains an open question.

10 Related and Future Work

A discussion of related work on iteration schemes for higher-order datatypes can be found in the previous section. This section tries to develop a broader perspective—especially with respect to possible applications in the field of generic programming.

Generic Programming (also called polytypic programming) aims at programming functions operating “canonically” on all the datatypes associated with a class of admissible F ’s, which are typically the regular datatypes. For an extensive overview of generic programming, see Backhouse, Jansson, Jeuring, and Meertens (1999). The tutorial also includes a description of the generic programming language PolyP (Jansson and Jeuring, 1997). Typically for generic programming, as well as for Jay’s Constructor Calculus (Jay, 2001), admissible F ’s are built in a combinatorial, i. e., λ-free calculus.^{3} Polytypic functions are then constructed by recursion on the generation of their type parameter F. In contrast, our constructions of fixed points and the associated schemes of iteration and coiteration just assume some arbitrary type constructor F : κ → κ. In this respect, we follow the approach in category theory where an arbitrary endofunctor on some category would be given (for the definition of initial algebras and final coalgebras—not for existence theorems). There is no analysis of the form of F, and thus, our constructions have to work uniformly in F. Unlike the category-theoretic situation, we do not even impose any equational laws on F. In the conventional-style systems, the usage—as opposed to the existence—of the schemes rests on terms inhabiting one of our notions of monotonicity. In It_{=}^{ω}, there would be a canonical choice of a witness of monotonicity for a wide range of type constructors F, including, for instance, the hofunctors of Section 9. The canonical monotonicity witness could be computed by recursion on the structure of all these admissible F ’s. Note, however, that “ungeneric” powerlist reversal (Example 17) uses some monotonicity witness that cannot be found generically.

Type Classes. Norell and Jansson (2003) describe an implementation of the polytypic programming language PolyP within the Haskell programming language, using the type-class mechanism (Wadler and Blott, 1989). The latter is a form of ad-hoc polymorphism where a class name is associated with a number of functions, called the dictionary, whose types may involve the type parameter of the class. A type becomes a member of the class by providing

3 This even holds for the related work on nested datatypes we mentioned in Section 9.

implementations of the dictionary functions. Most importantly, the type system allows to provide an implementation for type H A under the assumption that already A belongs to the class, and hence by using the assumed implementations of the dictionary functions for A.

Summing Up with Type Classes. Our running example of powerlist summation may be recast in the framework of type classes by defining a type class Summable so that type A belongs to it iff there is an implementation of the function sum : A → Nat. (For a Haskell implementation, see below.) Trivially, Nat is summable, and if A is summable then so is A × A. The crucial step is to show that summability of A entails that of PList A. The argument f : A → Nat to sum′ in Example 8 is no longer needed because one can just take sum for type A. On the other hand, the freedom to manipulate f is also lost, and no function λ⟨a_{1}, a_{2}⟩. f a_{1} + f a_{2} can be given as an additional argument. Fortunately, λ⟨a_{1}, a_{2}⟩. sum a_{1} + sum a_{2} is precisely the function sum for type A × A. Finally, sum at type PList Nat is the function we were after in the first place. Certainly, its termination is not guaranteed by this construction, but intuitively holds, anyway. This is more delicate with summation for bushes (Example 13). In terms of type class Summable it just requires that for summable A, also Bush A is summable. The crucial definition clause is then sum (bcons a b) := sum a + sum b. The first summand uses the assumed function sum for type A (which used to be f in that example), the second one uses polymorphic recursion: the term b is of type Bush (Bush A), hence the same definition of sum is invoked with Bush A in place of A. Its hidden argument f is therefore sum f, in accordance with the reduction behavior shown in Example 13. Again, no termination guarantee is provided by this implementation. Moreover, bsum′ in the example works for arbitrary types A as soon as a function f : A → Nat is provided. This includes different functions for the very same type A, not just the one derived by the type class instantiation mechanism. For instance, the first argument—bsum′f—in the recursive call may be modified to, e. g., bsum′ (λx. f x + 1), keeping typability and thus termination. Using type class Summable, there is just no room for such an “ungeneric” modification, as is clear from the explanation above.

The following Haskell code corresponds to the above discussion and can be executed with current extensions to the Haskell 98 standard. These extensions are only needed because we instantiate Summable(a,a) with two occurrences of a.

    data PList a = Zero a | Succ (PList(a, a))
    data Bush  a = Nil    | Cons a (Bush (Bush a))
    class Summable a where
      sum:: a -> Integer

    instance Summable Integer where
      sum = id
    instance Summable a => Summable (a,a) where
      sum (a1,a2) = sum a1 + sum a2
    instance Summable a => Summable (PList a) where
      sum (Zero a) = sum a
      sum (Succ l) = sum l
    instance Summable a => Summable (Bush a) where
      sum Nil = 0
      sum (Cons a b) = sum a + sum b

Generic Haskell (Clarke, Jeuring, and Löh, 2002) is a system of generic programming in all kinds: A family of functions may be programmed where the indices range over all type constructors F of all kinds. The type τ(F) of the function indexed by F is calculated from the kind of F, hence has a polykinded type (Hinze, 2002). The idea of this calculation roughly follows the idea of the type-class mechanism, e. g., the function associated with PList : ∗ → ∗ takes any function for any type A and yields a function for the type PList A, i. e., τ(PList) = ∀A. τ(A) → τ(PList A). Therefore, only the types τ(A) for A a veritable type (type constructor of kind ∗, also called a manifest type) can be freely chosen.

Clearly, the iteration schemes of this article do not follow that discipline: By no means is an iterator for μ^{κ_{1}→κ_{2}}F explained in terms of an iterator for μ^{κ_{2}}(F G) for some or any G : κ_{1}. However, programming iterators inside Generic Haskell would counteract its philosophy. In fact, Generic Haskell leaves the programmer from the burden to consider the fixed points that come from the definitions of datatypes. The associated instances are automatically generated by the compiler—without any clause in the generic program referring to them. Likewise, type abstraction and type instantiation are dealt with automatically (Hinze, Jeuring, and Löh, 2003), using a model of the kinded type constructor system based on applicative structures.^{4} The most recent

4 Intensional type analysis (Harper and Morrisett, 1995) is a compilation technology which uses an intermediate language with “intensional polymorphism”, i. e., with structural recursion over types. In the extension to all kinds that has been motivated by Generic Haskell, Weirich (2002) directly encodes the notion of set-theoretic model for the lambda calculus, including environments, in order to describe the instantiation mechanism. This might also help in understanding the output of the Generic Haskell compiler.

presentation of Generic Haskell is given by Hinze and Jeuring (2003b); there is also a collection containing the three most interesting examples (Hinze and Jeuring, 2003a), among which the generalization of the trie data structure to datatypes of all kinds (Hinze, 2000b). The tries over a regular datatype are often already truly nested datatypes, hence the latter ones arise naturally also in this context. Since the merging functions for tries are recursive in two arguments (Hinze and Jeuring, 2003a, Sect. 2.7), we would need to extend our iteration schemes in order to cover them, too.

As becomes clear from all the examples cited above, there is usually no need to have any kind of recursive calls inside the programs in Generic Haskell. Therefore, a useful version of Generic Haskell could well be imagined that only uses program clauses taken from System F^{ω}. We would hope to extend our Mendler-style iteration schemes in order to be able to provide a syntactic analysis of those restricted Generic Haskell programs that allows to conclude that any instantiated function (as being generated by the Generic Haskell compiler) terminates as well, as long as only fixed points of monotone type constructors are formed. Here, we would use Mendler-style systems since they directly allow to express the algorithms. The step term s of the iterator would be provided by a modification of the compiler for generic programs. In the other direction, we might get help from generic programming in building libraries of pseudo monotonicity witnesses for System GIt^{ω}, hence with a generic definition for every specific task at hand; recall that real work is also delegated to the witnesses in that system. In general, our conventional schemes would typically be used with some generically found monotonicity witness.

Dependent Types. Let us comment on systems with dependent types (i. e., with types that depend on terms) and universes. These are very rich systems in which higher-order datatypes can easily be expressed. Impredicative dependent type theories, like the Calculus of Constructions, encompass System F^{ω}, hence our schemes. Interestingly, the native fixed-point constructions of all of these theories, especially the systems Coq and LEGO, exclude non-strictly positive type constructors. But non-strictly positive dependencies immediately arise with Kan extensions. For our intended extensions to systems with primitive recursion, one would have to require non-strictly positive “native” fixed points in the system. On the other hand, there is plenty of work on predicative systems of dependent types. One would use small universes as the system of admissible type indices of the families in question. Hence, one gives up the uniform treatment of all possible indices, see Altenkirch and McBride (2003). The operational behavior of the datatypes thus obtained has to be studied further. Interestingly, a nontrivial part of programming with dependent types can be simulated within Haskell (McBride, 2002; Chen et al., 2003).

Type Checking and Type Inference. This article deliberately neglects the important practical problem of finding the types which are given to the example programs throughout the article. It is well-known that already typechecking for Curry-style System F is undecidable (Wells, 1999). Nevertheless, we have chosen the unannotated Curry-style due to its succintness. The type annotations are only given on the informal level of presentation. With these, the terms in Church-style formulation, hence with explicit type abstraction, type instantiation and type annotations for every bound variable have successfully been reconstructed with a prototype implementation^{5} , at least for the examples that have been tried, and these were the majority of the programming examples in the article. Note that, in systems of dependent types, termination of well-typed programs would be a necessity for type checking, since the types may depend on the terms. Our systems are layered, hence these problems are not intertwined.

The problem of type inference is deeper than that of type checking—already polymorphic recursion, i. e., recursion where different instances of a universally quantified target type have to be inferred, makes type inference undecidable (Henglein, 1993; Kfoury, Tiuryn, and Urzyczyn, 1993a,b). Type abstraction in Haskell is only partly solved in Neubauer and Thiemann (2002) by providing a restricted amount of lambda expressions. The problem is also known for the programming language family ML as the “quest for type inference with firstclass polymorphic types” (Le Botlan and Rémy, 2003). A practical system would certainly allow the user to communicate her typing intuitions. In this respect, Haskell is half way: help with types is accepted, but not with kinds.

On “higher-order nested”. In this article, “higher-order nested” means that fixed-points of higher ranks are formed and that recursive calls are heterogeneous. “True nesting” means nested calls to the datatype, as in Example 20, where the least fixed-point of λXλA. … + X (X A) is considered. This datatype would be called “doubly nested” in Bird and Paterson (1999b), and in general, true nesting is called “non-linear nests” in Hinze (2001). Okasaki (1999a) considers the fixed-point (called square ) of

λF λV λW. V (V A) + F V (W ×^{k1} W) + F (V ×^{k1} W) (W ×^{k1} W),

with V, W : k1. The type constructor V is even nested, but it is just a parameter which is used heterogeneously. Nevertheless, this would be called a higher-order nest by Hinze (1998), regardless of the component V (V A), but because the higher-order parameters V and W (which are not types but type transformers) are given as arguments to the variable F, representing the fixed point. Hinze (2001) contains plenty of examples where higher-order parameters are varied in the recursive calls to the datatype being defined, but nowhere

5 Fomega 0.10 alpha, by the first author, available on his homepage

“true nesting”. Truly nested datatypes may seem to be esoteric, but they occur naturally in the representation of explicit substitution (see Example 20), a fact which might explain why termination questions in connection with explicit substitutions are notoriously difficult. Certainly, we would like to see more natural examples of true nesting. As indicated above, trie data structures (Hinze, 2000b) serve this purpose.

Extensional Equality. Finally, an important subject for future research would be the study of the equational laws for our proposed iteration and coiteration schemes in order to use the mathematics of program calculation for the verification of programs expressed by them. After all, this is seen as the major benefit of a programming discipline with iterators in a setting of partial functions, e. g., the “algebra of programming” (Bird and de Moor, 1997). Note that these calculations would always be carried out within an extensional framework, such as parametric equality theory. The goal would be to demonstrate that a given program denotes some specified element in some semantics which, e. g., could be total functions. This article views a program as an algorithm which is explored in its behavior, e.g., whether it is strongly normalizing as a term rewrite system. Parametricity would, e. g., be used for establishing that our syntactic natural transformations would also be natural in the category-theoretic sense. For an introduction to these ideas, see Wadler (1989), more details are to be found in Wadler (2003), and interleaved positive (co)inductive types are treated in Altenkirch (1999). An interesting new field is the connection between parametric equality and generic programming: Backhouse and Hoogendijk (2003) show that, under reasonable naturality and functoriality assumptions on the family of zip functions, exactly one such zip exists for all “regular relators”.

11 Conclusion

We have put forth and compared the expressive power of several possible formulations of iteration and coiteration for (co)inductive constructors of higher kinds. All of them have a clear logical underpinning (exploiting the well-known Curry-Howard isomorphism) and uniformly extend from rank-2 type constructors to rank-n type constructors, for arbitrary n.

The main technical problem we faced with the formulation of (co)iteration schemes, is the absence of a canonical definition of admissible constructor for forming the least/greatest fixed-points. In our approach, every constructor is allowed for the formation of the fixed-points. For conventional-style schemes (inspired from initial algebras in category theory), the search for an optimal type-based approach led to several plausible notions of monotonicity, which is required when applying the (co)iteration scheme in the systems \underline{It}^{ω}, It_{=}^{ω} and GIt^{ω}, respectively. In the even more radical line of thought (inspired by Mendler’s work, but not derived from it), every constructor is allowed for the (co)iteration, but the typing requirements for its step term nevertheless guarantee termination for our Mendler-style systems MIt^{ω}, MIt_{=}^{ω} and GMIt^{ω}.

Of the systems considered here, GMIt^{ω} and GIt^{ω} are clearly the most advanced in terms of direct expressive power. In particular, this is witnessed by the fact that the efolds of Martin, Gibbons, and Bayley (2003) are very straightforwardly defined in GIt^{ω}. But for many applications, the more basic \underline{It}^{ω} and MIt^{ω} are perfectly sufficient and invoking GMIt^{ω} or GIt^{ω} is simply not necessary. There are many interesting cases where the more basic systems \underline{It}^{ω} and MIt^{ω} do not suffice to express the algorithmic idea appropriately, but where the freedom in choosing the additional parameters H⃗ in both GMIt^{ω} and GIt^{ω}, and parameter F′ in GIt^{ω}, is not needed. These more rigid typings are embodied in the intermediary systems MIt_{=}^{ω} and It_{=}^{ω}, which have exactly the reduction behavior of their “generalized” versions GMIt^{ω} and GIt^{ω} but are easier to typecheck in practice.

In GMIt^{ω} and MIt^{ω}, where the iterator and coiterator are Mendler-style, their computational behavior is very close to letrec, except that termination of computations is guaranteed. Thus, through type checking, these systems provide termination checking for given algorithmic ideas. The conventional-style systems aid more in finding algorithms: According to the type of the function to be programmed, one chooses the generic (pseudo) monotonicity witness m and tries to find a term s of the right type. Certainly, this “type-directed programming” might fail, see Remark 1, but has proven its usefulness in many cases.

As demonstrated with the advanced examples, in practice, an eclectic view is most helpful: in principle, we would program in MIt^{ω}, but constantly use the expressive capabilities of the other systems, viewed as macro definitions on top of MIt^{ω}.

Acknowledgments Peter Hancock deserves thanks for suggesting to us the definition mon F := F ≤ F. We also highly appreciate the feedback we got from Peter Aczel at TYPES’03 in Turin, April/May 2003. One quarter of this article can be traced back to the stimulating advice by our anonymous referees whom we warmly thank.

The first author acknowledges the support by both the PhD Programme Logic in Computer Science (GKLI) of the Deutsche Forschungs-Gemeinschaft and the project CoVer of the Swedish Foundation of Strategic Research. The third author was partially supported by the Estonian Science Foundation under grants no. 4155 and 5677.

All three authors received support also from the FP5 thematic network project TYPES (IST-1999-29001).

References

Abel, A., Matthes, R., 2003. (Co-)iteration for higher-order nested datatypes. In: Geuvers, H., Wiedijk, F. (Eds.), Types for Proofs and Programs, International Workshop, TYPES 2002. Vol. 2646 of Lecture Notes in Computer Science. Springer, Berg en Dal, The Netherlands, pp. 1–20.

Abel, A., Matthes, R., Uustalu, T., April 2003. Generalized iteration and coiteration for higher-order nested datatypes. In: Gordon, A. (Ed.), Foundations of Software Science and Computation Structures (FoSSaCS 2003). Vol. 2620 of Lecture Notes in Computer Science. Springer, Warsaw, Poland, pp. 54–69.

Altenkirch, T., 1999. Logical relations and inductive/coinductive types. In: Gottlob, G., Grandjean, E., Seyr, K. (Eds.), Computer Science Logic, 12th International Workshop, Brno, Czech Republic, August 24–28, 1998, Proceedings. Vol. 1584 of Lecture Notes in Computer Science. pp. 343–354.

Altenkirch, T., McBride, C., 2003. Generic programming within dependently typed programming. In: Gibbons, J., Jeuring, J. (Eds.), Proceedings of the IFIP TC2 Working Conference on Generic Programming, Dagstuhl, Germany, July 2002. Kluwer Academic Publishers, pp. 1–20.

Altenkirch, T., Reus, B., 1999. Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodríguez-Artalejo, M. (Eds.), Computer Science Logic, 13th International Workshop, CSL ’99, Proceedings. Vol. 1683 of Lecture Notes in Computer Science. Springer, pp. 453–468.

Backhouse, R., Hoogendijk, P., 2003. Generic properties of datatypes. In: Backhouse, R., Gibbons, J. (Eds.), Generic Programming. Vol. 2793 of Lecture Notes in Computer Science. pp. 97–132.

Backhouse, R., Jansson, P., Jeuring, J., Meertens, L., 1999. Generic programming—an introduction. In: Swierstra, S. D., Henriques, P. R., Oliveira, J. N. (Eds.), Advanced Functional Programming. Vol. 1608 of Lecture Notes in Computer Science. pp. 28–115.

Bird, R., de Moor, O., 1997. Algebra of Programming. Vol. 100 of International

Series in Computer Science. Prentice Hall. Bird, R., Gibbons, J., Jones, G., 2000. Program optimisation, naturally. In:

Millenial Perspectives in Computer Science. Palgrave. Bird, R., Meertens, L., 1998. Nested datatypes. In: Jeuring, J. (Ed.), Mathe-

matics of Program Construction, MPC’98, Proceedings. Vol. 1422 of Lecture Notes in Computer Science. Springer, pp. 52–67.

Bird, R., Paterson, R., 1999a. Generalised folds for nested datatypes. Formal

Aspects of Computing 11 (2), 200–222. Bird, R. S., Paterson, R., 1999b. De Bruijn notation as a nested datatype.

Journal of Functional Programming 9 (1), 77–91. Chen, C., Zhu, D., Xi, H., 2003. Implementing cut elimination: A case study

of simulating dependent types in Haskell, submitted. Clarke, D., Jeuring, J., Löh, A., 2002. The Generic Haskell user’s guide—

version 1.23. Technical Report UU-CS-2002-047, Institute of Information and Computing Sciences, Utrecht University.

Hagino, T., 1987. A typed lambda calculus with categorical type constructors. In: Pitt, D. H., Poigné, A., Rydeheard, D. E. (Eds.), Category Theory and Computer Science. Vol. 283 of Lecture Notes in Computer Science. Springer, pp. 140–157.

Harper, R., Morrisett, G., January 1995. Compiling polymorphism using intensional type analysis. In: Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California. ACM Press, pp. 130–141.

Haskell Mailing List, July 25 2002. Markus Schnell’s message slide: useful

function?
URL http://www.mail-archive.com/haskell@haskell.org/

Henglein, F., 1993. Type inference with polymorphic recursion. ACM Transac-

tions on Programming Languages and Systems (TOPLAS) 15 (2), 253–289. Hinze, R., December 1998. Numerical representations as higher-order nested

datatypes. Technical Report IAI-TR-98-12, Institut für Informatik III, Universität Bonn.

Hinze, R., December 1999. Polytypic values possess polykinded types. Tech-

nical Report IAI-TR-99-15, Institut für Informatik III, Universität Bonn. Hinze, R., July 2000a. Efficient generalized folds. In: Jeuring, J. (Ed.), Pro-

ceedings of the Second Workshop on Generic Programming, WGP 2000. Ponte de Lima, Portugal.

Hinze, R., July 2000b. Generalizing generalized tries. Journal of Functional

Programming 10 (4), 327–351. Hinze, R., September 2001. Manufacturing datatypes. Journal of Functional

Programming 11 (5), 493–524. Hinze, R., 2002. Polytypic values possess polykinded types. Science of Com-

puter Programming, MPC Special Issue 43, 129–159. Hinze, R., Jeuring, J., 2003a. Generic Haskell: applications. In: Backhouse,

R., Gibbons, J. (Eds.), Generic Programming. Vol. 2793 of Lecture Notes in Computer Science. Springer, pp. 57–97.

Hinze, R., Jeuring, J., 2003b. Generic Haskell: practice and theory. In: Backhouse, R., Gibbons, J. (Eds.), Generic Programming. Vol. 2793 of Lecture Notes in Computer Science. pp. 1–56.

Hinze, R., Jeuring, J., Löh, A., 2003. Type-indexed data types. To appear in

Science of Computer Programming . Jansson, P., Jeuring, J., 1997. PolyP—a polytypic programming language ex-

tension. In: Conference Record of POPL’97. ACM Press, pp. 470–482. Jay, C. B., 2001. Distinguishing data structures and functions: The con-

structor calculus and functorial types. In: Abramsky, S. (Ed.), Typed Lambda-Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings. Vol. 2044 of Lecture Notes in Computer Science. Springer, pp. 217–239.

Kahrs, S., July 2001. Red-black trees with types. Journal of Functional Pro-

gramming 11 (4), 425–432. Kfoury, A., Tiuryn, J., Urzyczyn, P., 1993a. Type reconstruction in the pres-

ence of polymorphic recursion. ACM Transactions on Programming Languages and Systems (TOPLAS) 15 (2), 290–311.

Kfoury, A., Tiuryn, J., Urzyczyn, P., 1993b. The undecidability of the semi-

unification problem. Information and Computation 102 (1), 83–101. Le Botlan, D., Rémy, D., 2003. MLF: raising ML to the power of system

F. In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden: 25-29 August 2003. ACM Press, pp. 27–38.

Mac Lane, S., 1998. Categories for the Working Mathematician, 2nd Edition.

Vol. 5 of Graduate Texts in Mathematics. Martin, C., Gibbons, J., Bayley, I., 2003. Disciplined, efficient, generalised

folds for nested datatypes. Accepted for publication in Formal Aspects of Computing .

Matthes, R., 1998. Extensions of system F by iteration and primitive recursion on monotone inductive types. Doktorarbeit (PhD thesis), University of Munich, available via the homepage

http://www.tcs.informatik.uni-muenchen.de/˜ matthes/.

Matthes, R., 1999. Monotone (co)inductive types and positive fixed-point

types. Theoretical Informatics and Applications 33 (4/5), 309–328. McBride, C., 2002. Faking it (simulating dependent types in Haskell). Journal

of Functional Programming 12 (4+5), 375–392. Mendler, N. P., 1987. 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. pp. 30–36.

Mendler, N. P., 1991. Inductive types and type constraints in the second-order

lambda calculus. Annals of Pure and Applied Logic 51 (1–2), 159–172. Neubauer, M., Thiemann, P., 2002. Type classes with more higher-order poly-

morphism. In: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming. ACM Press, pp. 179–190.

Norell, U., Jansson, P., 2003. Polytypic programming in Haskell. In: Proceedings of the 15th International Workshop on the Implementation of Functional Languages, Edinburgh, Scotland September 8th - 10th, 2003. Lecture Notes in Computer Science. Accepted for publication.

Okasaki, C., 1999a. 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, September

27-29, 1999. Vol. 34 of SIGPLAN Notices. ACM, pp. 28–35. Okasaki, C., 1999b. Red-black trees in a functional setting. Journal of Func-

tional Programming 9 (4), 471–477. Pfenning, F., Lee, P., 1989. LEAP: A language with eval and polymorphism.

In: TAPSOFT, Vol.2. Vol. 352 of Lecture Notes in Computer Science. Springer, pp. 345–359.

Pierce, B., Dietzen, S., Michaylov, S., 1989. Programming in higher-order

typed lambda-calculi. Tech. rep., Carnegie Mellon University. Uustalu, T., Vene, V., 1997. A cube of proof systems for the intuitionistic

predicate μ-, ν-logic. In: Haveraaen, M., Owe, O. (Eds.), Selected Papers from the 8th Nordic Workshop on Programming Theory (NWPT ’96), Oslo, Norway, December 1996. Vol. 248 of Research Reports, Department of Informatics, University of Oslo. pp. 237–246.

Uustalu, T., Vene, V., 2002. The dual of substitution is redecoration. In: Hammond, K., Curtis, S. (Eds.), Trends in Functional Programming 3. Intellect, Bristol / Portland, OR, pp. 99–110.

Wadler, P., 1989. Theorems for free! In: Proceedings of the fourth international conference on functional programming languages and computer architecture, Imperial College, London, England, September 1989. ACM Press, pp. 347–359.

Wadler, P., 2003. The Girard-Reynolds isomorphism. Information and Com-

putation 186 (2), 260–284. Wadler, P., Blott, S., January 1989. How to make ad-hoc polymorphism less

ad hoc. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas. ACM Press, pp. 60–76.

Weirich, S., 2002. Higher-order intensional type analysis. In: Métayer, D. L. (Ed.), Proceedings of 11th European Symposium on Programming, ESOP 2002. Vol. 2305 of Lecture Notes in Computer Science. pp. 98–114.

Wells, J. B., 1999. Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic 98 (1–3), 111–156.