Formal Aspects of Computing (1999) 3: 1–000

\begin{matrix}c \\ ◯ \end{matrix} 1999 BCS

Generalised folds for nested datatypes

Richard Bird^{1} and Ross Paterson^{2}

Abstract. Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transformations. Practical considerations therefore dictate the introduction of a generalised fold function in which this limitation can be overcome. In the paper we show how to construct generalised folds systematically for each nested datatype, and show that they possess a uniqueness property analogous to that of ordinary folds. As a consequence, generalised folds satisfy fusion properties similar to those developed for regular datatypes. Such properties form the core of an effective calculational theory of inductive datatypes.

Keywords: Functional programming, program construction.

1. Introduction

A nested datatype is a parametrised inductive datatype whose declaration involves a change to the accompanying type parameter(s). In other words, the recursion is “nested” within a change of parameter. A formal definition is given in Section 3. Such types have also been called non-regular or non-uniform.

A simple example is provided by the type Pow of power trees, declared in Haskell by:

data Pow a = Zero a | Succ (Pow (Pair a))
type Pair a = a × a

(We have varied the syntax slightly, writing a×a where Haskell would use (a, a).) Elements of Pow a consist of pairs of pairs of pairs … of values of type a, where the depth of nesting is given by reading the associated constructor expression as a Peano numeral. For example,

1 Programming Research Group, Oxford University, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK.

2 Department of Computer Science, City University, Northhampton Square, London EC1V 0HB, UK.

Succ (Succ (Zero ((1, 2), (3, 4))))

is a power tree of height 2. Each element therefore represents a perfectly balanced binary tree with labels in the leaves.

As this example suggests, nested datatypes can capture certain structural invariants in a way that regular datatypes cannot. Connelly and Lockwood Morris [CL95] use a nested type for modelling a generalisation of the trie data structure, and Okasaki [Oka98] puts nested datatypes to a variety of uses in the design of purely functional data structures. Bird and Paterson [BP99] use a nested datatype to describe de Bruijn notation for lambda expressions. Other examples of datatypes that have been shown very recently to be expressible by nested declarations include AVL trees, 2-3 trees, and square matrices.

The aim of this paper is to lay the groundwork for a useful calculational theory of nested datatypes; the work can be regarded as a successor to [BM98]. The categorical semantics is straightforward, but there is a complication. For a regular datatype, the fold function induced by initiality is a useful tool in the construction of practical programs. In nested datatypes, it isn’t. The basic reason is that the argument of the fold is required to be a natural transformation, and the result of the fold is also a natural transformation. Consequently, functions that inspect the elements of a nested datatype cannot be defined as folds. This phenomenon motivates the introduction of a generalised fold operator in which these limitations can be overcome. The first contribution of the paper is to show how to define a generalised fold operator for each nested type.

In the calculational theory of regular inductive datatypes, everything hinges on the uniqueness property of the fold function: the fold is the unique function of its type satisfying a certain functional equation. From this flow the fusion laws of fold; such laws are of fundamental importance in reasoning about programs and improving their efficiency (see, e.g. [Bir98, Mal90b]). The second contribution of the paper is to show that generalised folds also possess a uniqueness property.

Having established the uniqueness property, we can set up appropriate fusion laws for reasoning about nested datatypes. The third contribution in this paper is to present such laws, and to discuss some of their consequences.

The rest of the paper is organised as follows. In Sections 2 and 3 we briefly review the standard theory of regular datatypes, and show how the theory extends to nested datatypes. These sections also contain the formal definitions of regular and nested datatypes. In Section 4 we introduce the generalised folds, and in Section 5 we present the fusion laws. In Section 6 we will justify our proofs of the fusion laws by showing that generalised folds are uniquely determined by their defining equations. Familiarity with basic category theory is assumed.

2. Semantics of non-parametrised datatypes

In a categorical setting, non-parametrised inductive datatypes are introduced by taking categorical least fixed points of appropriate functors (see e.g. [Lam70, BdM97, Hag87, Mal90a, MA86]). Given a suitable category C, the least fixed point of a functor F :: C → C, if it exists, is an object T of C for which the arrow α :: F T → T is an initial algebra in the category of F -algebras. The objects of this category are arrows F A → A of C, and the arrows are homomorphisms between algebras. Thus, for objects f :: F A → A and g :: F B → B, an arrow h :: f → g is an arrow h :: A → B of C such that h · f = g · F h.

The initiality of α means that to each algebra f :: F A → A there is associated a unique homomorphism h :: α → f , that is a function h :: T → A satisfying the equation

h · α = f · F h.

The unique homomorphism h is denoted by fold f . It is a consequence of initiality that α is an isomorphism, whence T ≅ F T ; this explains the terminology ‘fixed point’.

One class of appropriate functors are the polynomial functors. In a category C with products and coproducts, the polynomial functors F :: C^{n} → C are defined by the following grammar:

F ::= \underline{A}^{n} | + | × | Π_{i}^{n} | F · ⟨F_{1}, …, F_{n}⟩

The functor \underline{A}^{n} is an n-ary constant functor, delivering the type A for all arguments. The functor Π_{i}^{n} is an n-ary projection, selecting its ith argument. A special case is Id = Π_{1}^{1}. The superscripts n will be omitted in the rest of the paper. The functor F · ⟨F_{1}, …, F_{n}⟩ denotes the composition of an n-ary functor F with n functors F_{i}, all of the same arity, so that

(F · ⟨F_{1}, …, F_{n}⟩) A_{1} … A_{m} = F (F_{1} A_{1} … A_{m}) … (F_{n} A_{1} … A_{m})

We omit the brackets when n = 1. We also write F + G for + · ⟨F , G⟩ and similarly F × G.

Provided the category C has colimits of all countable chains (the category Set of sets and total functions is an example), every unary polynomial functor possesses a least fixed point.

As examples, we can introduce the datatype Nat of natural numbers as the least fixed point of F = \underline{1} + Id, lists of natural numbers as the least fixed point of F = \underline{1} + \underline{Nat} × Id, and binary trees, with natural number labels, as the least fixed point of F = \underline{1} + \underline{Nat} × Id × Id.

Such declarations can be translated into Haskell fairly directly. For example, the datatype of lists of natural numbers can be declared by

data NatListF a = Nil | Cons (Nat × a)
newtype NatList = In (NatListF NatList)

The data declaration introduces the polynomial functor NatListF , and the newtype declaration introduces NatList as isomorphic to NatListF NatList. In Haskell, both type variables and type constructor variables are denoted using lower-case letters.

In general, Haskell programs may fail to terminate, so these datatypes conceptually include an additional ‘value’ representing non-termination, and the language defines how non-termination propagates through an expression. However, we shall be using a subset of Haskell in which all programs terminate, so that this is not an issue, and our programs may be modelled in our category C. This means that we cannot use unrestricted recursion; we must show that any recursive definitions we use have unique solutions. An additional restriction in comparison with Haskell is that recursively defined types in this paper do not involve function types, so we are concerned solely with inductive types.

The constructor In corresponds to the initial algebra α. The converse function α^{−1} is given by the function out, defined in Haskell by

out  :: NatList → NatListF NatList
out (In x) = x

The type of lists of natural numbers can also be declared by

data NatList = Nil | Cons (Nat × NatList)

In this version, which is closer to the usual style of datatype declaration in functional programming, the polynomial functor NatListF does not appear explicitly.

The function fold may be defined in Haskell as follows:

fold :: (NatListF a → a) → NatList → a
fold f = f · natlistF (fold f ) · out

In Haskell, a free type variable, like a, is implicitly universally quantified, and may be instantiated to any type.

The function natlistF is the functorial action of NatListF :

natlistF  :: (a → b) → NatListF a → NatListF b
natlistF f Nil  = Nil
natlistF f (Cons (n, x)) = Cons (n, f x)

For example, sumNL = fold sumF sums a list, where

sumF  :: NatListF Nat → Nat
sumF Nil  = 0
sumF (Cons (m, n)) = m + n

3. Semantics of parametrised datatypes

Next, we consider the extension of this theory to parametrised datatypes, like the following Haskell definition for lists:

data List a = Nil | Cons (a × List a)

As before, this may be rewritten in the equivalent form

data Base a b = Nil | Cons (a × b)
newtype List a = In (Base a (List a))

To incorporate parametrised datatypes into the theory, one can proceed in essentially two different ways. The first method is standard, but the second extends to nested constructors. For simplicity, we will consider only datatypes parametrised by a single type variable; the extension to multiple parameters is straightforward.

3.1. First method: families of fixed points

The first method takes the fixed point of a binary functor B with respect to its second parameter. We begin with the observation that the partial application of a binary functor B to a type A yields a unary functor B A, whose least fixed point T A can be constructed in the usual way. Then for each A there is an associated initial algebra α_{A} of type

α_{A} :: B A (T A) → T A.

The associated fold function takes an algebra f :: B A Y → Y as argument, and is uniquely defined by the assertion that for any arrow h :: T A → Y , we have h = fold f if and only if

h · α_{A} = f · B id h.

The datatype constructor T can be made into a functor by defining T f :: T X → T Y for an arrow f :: X → Y by

T f = fold (α_{Y} · B f id).

Restated, this definition takes the form

T f · α_{X} = α_{Y} · B f (T f ).

Hence α is a natural transformation from B · ⟨Id, T ⟩ to T .

The class of regular functors is defined as the closure of the class of polynomial bifunctors under least fixed point operations. For example, List is the least fixed point of a bifunctor B = \underline{1} + Π_{1} × Π_{2}, and the general tree constructor Tree is the least fixed point of a bifunctor B = Π_{1} × (List · Π_{2}).

For the List datatype constructor, the fold function is implemented by

fold :: (Base a b → b) → List a → b
fold f = f · base id (fold f ) · out

where the function base implements the functorial action of Base:

base  :: (a → c) → (b → d) → Base a b → Base c d
base f g Nil  = Nil
base f g (Cons (x, y)) = Cons (f x, g y)

Though it is defined in a slightly different way than usual, the function fold is essentially the same as the standard function foldr in functional programming. The functorial action of List (corresponding to the standard function map) may be defined using fold:

list :: (a → b) → List a → List b
list f = fold (In · base f id)

3.2. Second method: higher-order fixed points

The second method yields a larger class of datatype constructors. Instead of constructing fixed points in the category C, we will work in the functor categories C^{n} → C. The objects of C^{n} → C are n-ary functors over C, and the arrows are natural transformations between functors. We shall write F → G for the set of natural transformations from F to G.

In this category, limits and colimits may be constructed pointwise from limits and colimits in C [Mac71, V.3]. For example, the shorthand notations F × G and F + G do in fact denote products and coproducts in this category^{3}.

Moreover, we can define a functor T :: C^{n} → C as a fixed point of a suitable higher-order functor F :: (C^{n} → C) → (C^{n} → C), via the same colimit construction used in C. We shall refer to such functors as hofunctors. As before, this means that α :: F T → T is an initial object in the category of F -algebras. Note that α is a natural transformation by construction. Hence, for f :: A → B, we have

3 Everything we do here generalises in a straightforward way to functor categories D → C, for an arbitrary category D.

T f · α_{A} = α_{B} · F T f .

The fold function induced by the initiality of α associates with each natural transformation f :: F N → N , for some given functor N , a natural transformation hfold f :: T → N defined as the unique function h satisfying

h · α = f · F h.

This is exactly the same definition as for fold on unparametrised datatypes, but installed at a higher level. One major difference though is that the functoriality of T is given by construction, not as an instance of the fold.

We define the class of polynomial hofunctors of the form F X = P, where P is a polynomial functor expression that may also include the functor variable X . The grammar for such functor expressions is

P ::= \underline{A}^{n} | + | × | Π_{i}^{n} | P · ⟨P_{1}, …, P_{n}⟩ | X

A fixed point of a polynomial hofunctor is called a nested functor^{4}. We consider three examples.

Example 3.1 The functor List is given as the least fixed point of the polynomial hofunctor ListF X = \underline{1} + Id × X . Thus List is a nested functor which is also a regular functor. In Haskell, the type constructor List may be introduced by the declarations

data Base a b = Nil | Cons (a × b)
type ListF x a = Base a (x a)
newtype List a = In (ListF List a)

The type declaration introduces ListF x a as a synonym for Base a (x a). The type constructor List is therefore exactly the same as before.

However, the fold function is different. This function may be expressed in Haskell as follows:

hfold :: (∀ a. ListF n a → n a) → List b → n b
hfold f = f · listF (hfold f ) · out

The function listF expresses part of the functorial action of ListF : for each natural transformation f :: X → Y , we have listF f :: ListF X → ListF Y . In Haskell, we have

listF :: (∀ a. x a → y a) → ListF x b → ListF y b
listF f = base id f

The first arguments of hfold and listF are polymorphic functions, described using a rank 2 type signature [McC84]. Such signatures are allowed in recent extensions to Haskell [Jon98, PL97]. Polymorphic functions correspond to natural transformations in a categorical setting.

The definition of hfold is equivalent to the earlier definition of the regular fold, but has a different type: the new version takes natural transformations to natural transformations. As a result, the new fold is less useful because individual list elements can never be inspected.

4 Though we deal only with single recursive definitions here, our results could be extended to systems of multiple simultaneous definitions.

For example, if a fold is to produce a natural number, we would have to take N = \underline{Nat}, the constant functor that returns Nat on every type, so that hfold f :: List → \underline{Nat}. This function will operate on lists of any type, and must satisfy the naturality property

hfold f = hfold f · list k

for any function k, and thus cannot depend on elements of the list. We can define the length function, but little more. In the following section we will see how to overcome this limitation.

We have noted above that a functor List is introduced automatically as part of the categorical semantics, but we have not yet defined its functorial action list in Haskell. An inductive argument establishes that list is uniquely determined by the naturality of In :: ListF List → List. To express this naturality condition, we could extend the definition of listF given above to the full functorial action of ListF , or simply expand ListF in the definition of List, yielding the definition

list :: (a → b) → List a → List b
list f = In · base f (list f ) · out

This is equivalent to the definition using fold at the end of the previous section. Note, however, that list cannot be defined using hfold.

Example 3.2 The type constructor Nest is defined as the least fixed point of

NestF X = \underline{1} + Id × (X · Pair).

In Haskell the corresponding declarations are:

data Base a b  = Nil | Cons (a × b)
type NestF x a = Base a (x (Pair a))
type Pair a  = a × a
newtype Nest a = In (NestF Nest a)

An equivalent datatype is introduced by the ‘flattened’ declaration

data Nest a = Nil | Cons (a × Nest (a × a))

Unlike List, the datatype constructor Nest is not a regular functor: occurrences of Nest in its defining expression are “nested” within a change of type parameter from a to Pair a. In effect, values of type Nest a correspond to lists in which the first element has type a, the second element has type (a × a), the third has type ((a × a) × (a × a)), and so on. A variant of Nest was used in [Oka98] as a basis for an implementation of lists with an efficient indexing operation.

The fold function for Nest may be implemented in Haskell by expanding NestF in terms of the bifunctor Base:

hfold :: (∀ a. Base a (n (Pair a)) → n a) → Nest b → n b
hfold f = f · base id (hfold f ) · out

Similarly, the mapping function nest may be defined by

nest  :: (a → b) → Nest a → Nest b
nest f  = In · base f (nest (pair f )) · out
pair  :: (a → b) → Pair a → Pair b
pair f (x, y) = (f x, f y)

Unlike the case of List, the naturality of the argument f in hfold f is crucial to the definition. The recursive occurrence of hfold f in its defining expression is applied to elements of type Nest (Pair a); consequently, f must have type

f :: Base (Pair^{k} b) (n (Pair^{k+1} b)) → n (Pair^{k} b)

for all k ≥ 0. The type signature of f in the definition of hfold generalises this requirement by making f fully polymorphic.

Note that in the definition of Nest, the parameters of the recursive use do not themselves contain a use of Nest. We call such nested datatypes linear; almost all of the known practical examples of nested datatypes belong to this class. For an exception, see Section 5 of [BP99]. Our final example is a non-linear variant of Nest.

Example 3.3 The type functor Host may be defined as the least fixed point of

HostF X = \underline{1} + Id × (X · (Id × X )),

The Haskell declaration is:

data Base a b  = Nil | Cons (a × b)
type HostF x a = Base a (x (a × x a))
newtype Host a = In (HostF Host a)

This datatype is equivalent to the flattened version

data Host a = Nil | Cons (a × Host (a × Host a))

In effect, values of type Host a correspond to lists in which the first element is of type a, the second element is of type a × Host a, the third element is of type

(a × Host a) × Host (a × Host a),

and so on. We know of no practical use for this datatype.

The fold and map functions may be implemented by

hfold  :: (∀ a. Base a (n (a × n a)) → n a) → Host b → n b
hfold f  = f · base id (hfold f · host (id × hfold f )) · out
host  :: (a → b) → Host a → Host b
host f  = In · base f (host (f × host f )) · out
×  :: (a → c) → (b → d) → a × b → c × d
(f × g) (x, y) = (f x, g y)

The functions host and × implement the functorial actions of Host and ×, respectively.

4. Generalised folds

A simple fold takes as argument a natural transformation f :: F N → N and returns a natural transformation of type T → N . Its definition has the form

hfold f · α = Ψ (hfold f )

where the form Ψ :: (T → N ) → F T → N is defined by Ψ h = f · F h.

Greater flexibility is achieved if we generalise the fold to return a natural transformation of type T · M → N . For example, both M and N could be taken to be the constant functor that returns the type of integers. Then we would have a way of reducing a T -structure of integers to a single integer. The generalised fold will take as arguments a series of natural transformations f , g_{1}, …, g_{m}, to be introduced below. A generalised fold

gfold f g_{1} ⋯ g_{m} :: T · M → N

will be defined by an equation of the form

gfold f g_{1} ⋯ g_{m} · α = Ψ (gfold f g_{1} ⋯ g_{m})

for some form Ψ :: (T · M → N ) → F T · M → N . To develop this operator Ψ, observe that every polynomial hofunctor F can be expressed in the form

F X = B · ⟨Id, X · F_{1} X , …, X · F_{n} X ⟩

for some n ≥ 0 (if n = 0, then F X = B · Id = B). The subsidiary hofunctors F_{i} may be decomposed similarly^{5}.

For example, in the case of List, Nest, or Host, the functor B is given by

B X Y = 1 + X × Y .

Now for h :: T · M → N , we require (expanding F T · M ):

Ψ h :: B · ⟨M , T · F_{1} T · M , …, T · F_{n} T · M ⟩ → N .

The component types T · F_{i} T · M are not suitable for arguments to h, so we introduce auxiliary forms Φ[F_{i}] h :: F_{i} T · M → M · F_{i} N , to be defined below. Then we have

h · T (Φ[F_{i}] h) :: T · F_{i} T · M → N · F_{i} N

and we can define

Ψ h = f · B id (h · T (Φ[F_{1}] h)) ⋯ (h · T (Φ[F_{n}] h))

for some natural transformation

f :: B · ⟨M , N · F_{1} N , …, N · F_{n} N ⟩ → N

which must be supplied as a parameter to gfold.

It remains to define Φ[F ]h, which we do inductively on the form of F . For F X = B · ⟨Id, X · F_{1} X , …, X · F_{n} X ⟩, we define

Φ[F ]h = g · B id (h · T (Φ[F_{1}]h)) ⋯ (h · T (Φ[F_{n}]h))

for some natural transformation

g :: B · ⟨M , N · F_{1} N , …, N · F_{n} N ⟩ → M · F N .

5 There may be several such decompositions, each giving rise to a different definition of gfold.

Each natural transformation g arising in this way is provided as an extra parameter to gfold.

Note that in the special case M = Id, we can set each g = id, obtaining the simple fold as a special case:

hfold f = gfold f id ⋯ id.

Another special case arises when both M and N are constant functors; the associated instance of gfold is called a reduction.

Let us now consider the detailed instantiations for each of our three example datatypes.

Example 4.1 For List we have List = F List, where

F X = Base · ⟨Id, X · F_{1} X ⟩
F_{1} X = Id.

The generalised fold therefore takes the following form in Haskell:

gfold  :: (∀ a. Base (m a) (n a) → n a) →

(∀ a. m a → m a) → List (m b) → n b

gfold f g = f · base id (gfold f g · list g) · out

Of the two additional ingredients, M and g, it is the presence of the functor M that is the crucial one; the second argument g is useful but its effect can be achieved by other means. The point about M is that it provides greater freedom of manoeuvre.

As noted above, we can take both M and N to be constant functors, delivering, say, the types x and y respectively. Then the associated instance of gfold is a reduction of type

reduce :: (Base x y → y) → (x → x) → List x → y.

Viewing f :: Base x y → y as a pair e :: y and ⊕ :: x × y → y, the effect of reduce f g on a list [a_{0}, …, a_{n}] is to produce the value

a_{0} ⊕ (g a_{1} ⊕ (g^{2} a_{2} ⊕ ⋯ (g^{n} a_{n} ⊕ e) ⋯)).

The regular fold is the special case of a list reduction in which g = id. List reductions are an important component of the circuit design language Ruby [JS93]; see also [BdM97].

This analysis of reductions suggests that a generalised fold over lists can be decomposed into a simple fold after a triangle. The triangle with respect to a function g takes [a_{0}, a_{1}, …, a_{n}] to [a_{0}, g a_{1}, …, g^{n} a_{n}]. This function can be expressed as a fold:

triangle :: (a → a) → List a → List a
triangle g = fold (In · base id (list g)).

The claim is that

gfold f g = fold f · triangle g.

This result will be proved in the following section. In fact, for regular datatypes, we can always decompose a generalised fold into the composition of two regular folds in this way.

Example 4.2 For Nest we have Nest = F Nest, where

F X = Base · ⟨Id, X · F_{1} X ⟩
F_{1} X = Pair.

The generalised fold therefore has the following form in Haskell:

gfold  :: (∀ a. Base (m a) (n (Pair a)) → n a) →

(∀ a. Pair (m a) → m (Pair a)) → Nest (m b) → n b

gfold f g = f · base id (gfold f g · nest g) · out

If we take M and N to be constant functors, delivering types x and y respectively, then we obtain an instance of gfold, again called a reduction, with type:

reduce :: (Base x y → y) → (Pair x → x) → Nest x → y

In particular, we can sum a nest of integers by sumN = reduce sumB plus, where plus (m, n) = m + n and

sumB  :: Base Int Int → Int
sumB Nil  = 0
sumB (Cons (m, n)) = m + n

A nest of integers cannot be summed using a fold over nests (at least, not simply) because sumB is not a natural transformation of the right type. The summation function can be defined using a generalised fold because every function between two given types lifts to a natural transformation between constant functors.

Example 4.3 For Host we have Host = F Host, where

F X = Base · ⟨Id, X · F_{1} X ⟩
F_{1} X = × · ⟨Id, X · F_{2} X ⟩
F_{2} X = Id.

The generalised fold therefore has the following form in Haskell:

gfold  :: (∀ a. Base (m a) (n (a × n a)) → n a) →

(∀ a. m a × n a → m (a × n a)) → (∀ a. m a → m a) → Host (m b) → n b

gfold f g_{1} g_{2} = f · base id (\begin{matrix}gfold f g_{1} g_{2} · \\ host (g_{1} · id × (gfold f g_{1} g_{2} · host g_{2}))) · out \end{matrix}

Taking M and N to be constant functors, delivering types x and y respectively, we can define a reduction over Host as an instance of gfold with type

reduce :: (Base x y → y) → (x × y → x) → (x → x) → Host x → y

In particular, we can sum a host of integers by sumH = reduce sumB plus id, using the functions sumB and plus defined above.

4.1. Remarks

As we have defined them, generalised folds can be criticised from two opposing points of view. One can argue that our folds are too general in that arguments of type M → M could be dropped, since it is not clear what they contribute. On the other hand, one can also argue that our folds are too specific. For example, it is quite possible to assign the following type signature to the above definition of gfold for Host:

gfold :: (∀ a. Base (m a) (n (p a)) → n a) →

(∀ a. m a × n (q a) → m (p a)) → (∀ a. m a → m (q a)) → Host (m b) → n b

The idea is that gfold f g h :: Host (m b) → n b is a natural transformation, and different instances may be instantiated at different types, reflected by the type constructors q and p. The previous type of gfold is then the instance in which q a = a and p a = a × n a.

Even more generally, we can recall that the generalised fold is defined as the unique solution of an equation

x · α = Ψ x.

We can use any form Ψ :: (T ·M → N ) → (F T ·M → N ) for which this equation has a unique solution. As we shall see in Section 6, it suffices that Ψ is defined in such a way that any functor may be used in place of T . In particular, Ψ may not use α or α^{−1} to build or dismantle values of type T . We write

Ψ :: ∀ X . (X · M → N ) → (F X · M → N ).

Thus Ψ is a natural transformation between two contravariant functors.

As always, the more general forms have more degrees of freedom, but consequently offer less guidance to the program designer. We have found the version described in this section, with associated fusion laws presented below, to be a reasonable compromise in practice [BP99]. However, more experience is needed to determine which of the formulations turn out to be the most useful in practical program construction.

5. Fusion laws

The fusion laws for a nested datatype T come in two flavours: fold-fusion and map-fusion. The former provides conditions under which

k · gfold f g_{1} ⋯ g_{m} = gfold f′ g′_{1} ⋯ g′_{m}.

The map-fusion law is similar, providing conditions under which

gfold f g_{1} ⋯ g_{m} · T k = gfold f′ g′_{1} ⋯ g′_{m}.

In the standard theory of regular datatypes, map-fusion is a special case of foldfusion because the functorial action of regular datatypes can be defined as a fold. This is not the case with the higher-order semantics of Section 3.

In deriving the fusion laws, we shall assume that gfold f′ g′_{1} ⋯ g′_{m} is the unique function h′ satisfying its defining equation. This assumption will be justified in Section 6.

As in the previous section, we suppose α :: F T → T , where

F X = B · ⟨Id, X · F_{1} X , …, X · F_{n} X ⟩.

To reduce clutter, we show the calculations only for the case n = 1; the generalisation is straightforward.

The map-fusion law is dealt with first.

5.1. Map-fusion laws

Abbreviating gfold f g_{1} ⋯ g_{m} to h, and gfold f′ g′_{1} ⋯ g′_{m} to h′, our aim is to give conditions under which h · T k = h′, where k :: M′ → M . As noted above, we assume that h′ is the unique function of type T · M′ → N satisfying

h′ · α = Ψ′ h′,

where Ψ′ is obtained by replacing each f and g_{i} in Ψ with the corresponding f′ or g′_{i}. Hence it is sufficient to give conditions under which

h · T k · α = Ψ′ (h · T k).

The general scheme is given by the following calculation:

h · T k · α
=  {naturality of α}
h · α · B k (T (F_{1} T k))
=  {definition of h}
f · B id (h · T (Φ[F_{1}]h)) · B k (T (F_{1} T k))
=  {functoriality of B}
f · B k (h · T (Φ[F_{1}]h) · T (F_{1} T k))
=  {functoriality of T }
f · B k (h · T (Φ[F_{1}]h · F_{1} T k))
=  {assume Φ[F_{1}]h · F_{1} T k = k · Φ′[F_{1}](h · T k)}
f · B k (h · T (k · Φ′[F_{1}](h · T k)))
=  {functoriality of T }
f · B k (h · T k · T (Φ′[F_{1}](h · T k)))
=  {functoriality of B}
f · B k id · B id (h · T k · T (Φ′[F_{1}](h · T k)))
=  {assume f′ = f · B k id}
f′ · B id (h · T k · T (Φ′[F_{1}](h · T k)))
=  {definition}
Ψ′ (h · T k).

The first assumption in this calculation is the condition

Φ[F_{1}]h · F_{1} T k = k · Φ′[F_{1}](h · T k),

which can be simplified using the inductive definitions of Φ and Φ′ with a similar calculation. Eventually we will arrive at subforms that are independent of h, having generated a series of side-conditions. We will spell out the details for our three example datatypes.

Example 5.1 For List, we have Φ[F_{1}]h = g :: M → M and F_{1} List = Id. Since Φ′[F_{1}](h · list k) = g′ :: M′ → M′, we obtain

Map-fusion law for List.

gfold f g · list k = gfold (f · base k id) g′ ⇐ g · k = k · g′.

Taking the special case g = id and g′ = id, we have

fold f · list k = fold (f · base k id).

Example 5.2 For Nest, we have Φ[F_{1}]h = g :: Pair · M → M · Pair and F_{1} Nest = Pair. Since Φ′[F_{1}](h · nest k) = g′ :: Pair · M′ → M′ · Pair, we obtain

Map-fusion law for Nest.

gfold f g · nest k = gfold (f · base k id) g′ ⇐ g · pair k = k · g′.

Example 5.3 For Host, we have

Φ[F_{1}]h = g_{1} · id × (h · host g_{2})
Φ′[F_{1}](h · host k) = g′_{1} · id × (h · host k · host g′_{2}),

where g_{1} :: M × N → M · (Id × N ) and g_{2} :: M → M . The types of g′_{1} and g′_{2} are similar, except that M is replaced by M′. Since F_{1} Host k = k × host k, the condition for map-fusion takes the form

g_{1} · id × (h · host g_{2}) · k × host k = k · g′_{1} · id × (h · host k · host g′_{2})

or equivalently

g_{1} · k × id · id × (h · host (g_{2} · k)) = k · g′_{1} · id × (h · host (k · g′_{2})).

This equation follows from g_{1} · k × id = k · g′_{1} and g_{2} · k = k · g′_{2}. Hence

Map-fusion law for Host.

gfold f g_{1} g_{2} · host k = gfold (f · base k id) g′_{1} g′_{2}

⇐ g_{1} · k × id = k · g′_{1} ∧ g_{2} · k = k · g′_{2}.

5.2. Fold-fusion laws

Again abbreviating gfold f g_{1} ⋯ g_{m} to h and gfold f′ g′_{1} ⋯ g′_{m} to h′, our aim is to give conditions under which k · h_{M′} = h′, where k :: N · M′ → N′. As before, it is sufficient to give conditions under which

k · h · α = Ψ′ (k · h).

The general scheme is given by the following calculation:

k · h · α
=  {definition of h}
k · f · B id (h · T (Φ[F_{1}] h))
=  {assume k · f = f′ · B id (k · N p_{1}) for some p_{1}}

f′ · B id (k · N p_{1}) · B id (h · T (Φ[F_{1}] h))
=  {functoriality of B}
f′ · B id (k · N p_{1} · h · T (Φ[F_{1}] h))
=  {naturality of h :: T · M → N , and functoriality of T }
f′ · B id (k · h · T (M p_{1} · Φ[F_{1}] h))
=  {assume M p_{1} · Φ[F_{1}]h = Φ′[F_{1}](k · h)}
f′ · B id (k · h · T (Φ′[F_{1}](k · h)))
=  {definition}
Ψ′ (k · h).

The second assumption in this calculation, namely,

M p_{1} · Φ[F_{1}]h = Φ′[F_{1}](k · h),

where p_{1} :: F_{1} N · M′ → M′ · F_{1} N′, is elaborated to simpler assumptions, using the inductive definitions of Φ and Φ′. We will spell out the details for our three examples.

Example 5.4 For List we have Φ[F_{1}]h = g :: M → M . Hence

Fold-fusion law for List. Given the typings f :: Base · ⟨M , N · Pair⟩ → N , g :: M → M and p :: M′ → M′, we have

k · gfold f g = gfold f′ (M p · g) ⇐ k · f = f′ · base id (k · N p).

For example, consider the composition

gfold f id · gfold α g,

where f :: Base · ⟨M , N · Pair⟩ → N and g :: M → M . The function gfold f id :: List · M → N is a fold, while the function gfold α g :: List · M → List · M is called the triangle with respect to g. We have

gfold f id · α = f · base id (gfold f id · list id).

Hence an appeal to fold-fusion gives

gfold f id · gfold α g = gfold f g.

Thus every generalised fold on lists (and indeed any regular type) can be factored as a regular fold after a triangle. In fact, every triangle can be expressed as a regular fold:

gfold α g · α

=  {definition}

α · base id (gfold α g · list g)

=  {map-fusion}

α · base id (gfold (α · base g id) g)

=  {fold-fusion (backwards)}

α · base id (g · gfold α g)

=  {functoriality of base}

α · base id g · base id (gfold α g).

Hence gfold α g = fold (α · base g id), and gfold f g is a composition of regular folds. Note that we have not used any property of base except functoriality, so this factorisation may be applied to the generalised fold on any regular type.

Example 5.5 For Nest, we have Φ[F_{1}]h = g :: Pair · M → M · Pair. Hence

Fold-fusion law for Nest. Given the typings

f :: Base · ⟨M , N · Pair⟩ → N
g :: Pair · M → M · Pair
p :: Pair · M′ → M′ · Pair

we have

k · gfold f g = gfold f′ (M p · g) ⇐ k · f = f′ · base id (k · N p).

The fold-fusion law for Nest takes the same form as for List, Though the types of g and p are different. Here is a simple example. The function listify :: Nest → List can be defined by

listify = gfold (α · base id (concat · list duo)) id

where α :: Base · ⟨Id, List⟩ → List is the initial list algebra, duo :: Pair → List converts a pair of values into a list of two values, and concat :: List · List → List concatenates a list of lists into one list. Here M = Id and N = List.

Furthermore, the function sumL :: List · \underline{Int} → \underline{Int}, which sums a list of integers, is given by

sumL = fold sumB,

where fold is the fold function for lists.

Now consider the combination sumL · listify. We can fuse the two functions provided

sumL · α · base id (concat · list duo) = f′ · base id (sumL · list p),

for some p :: Pair · \underline{Int} → \underline{Int} and f′ :: Base · ⟨\underline{Int}, \underline{Int}⟩ → \underline{Int}. For the proviso we can calculate:

sumL · α · base id (concat · list duo)

=  {definition of sumL}

sumB · base id sumL · base id (concat · list duo)

=  {functoriality of base}

sumB · base id (sumL · concat · list duo)

=  {property of sumL and functoriality of list}

sumB · base id (sumL · list (sumL · duo))

=  {since sumL · duo = plus}

sumB · base id (sumL · list plus).

Hence sumL · listify = gfold sumB plus. The expression on the right is just the function sumN , given in the previous section, for summing a nest of integers directly.

Example 5.6 For T = Host, we have Φ[F_{1}]h = g_{1} · id × (h · T g_{2}), where g_{1} :: M × N → M · (Id × N ) and g_{2} :: M → M . For fold-fusion we require k · f = f′ · base id (k · N p), where p :: M′ × (N · M′) → M′ · (Id × N′) is required to satisfy the equation

M p · Φ[F_{1}]h = Φ′[F_{1}](k · h).

This condition expands to

M p · g_{1} · id × (h · T g_{2}) = g′_{1} · id × (k · h · T g′_{2}).

To eliminate the dependence on h, suppose

M p · g_{1} = g′_{1} · id × (k · N q)

for some q :: M′ → M′. Then we can argue:

M p · g_{1} · id × (h · T g_{2})
=  {assumption, and functoriality of ×}
g′_{1} · id × (k · N q · h · T g_{2})
=  {naturality of h :: T · M → N and functoriality of T }
g′_{1} · id × (k · h · T (M q · g_{2}))

Hence the fold-fusion law can be put in the form

Fold-fusion law for Host. Given the typings

f :: Base · ⟨M , N · (Id × N )⟩ → N
g_{1} :: M × N → M · (Id × N )
g_{2} :: M → M
q :: M′ → M′,

we have

k · gfold f g_{1} g_{2} = gfold f′ g′_{1} (M q · g_{2})

provided that, for some p :: M′ × (N · M′) → M′ · (Id × N′),

k · f = f′ · base id (k · N p) and M p · g_{1} = g′_{1} · id × (k · N q).

6. Uniqueness of generalised folds

Our aim in this section is to show that generalised folds are the unique solutions of their defining equations, which have the form

gfold f g_{1} ⋯ g_{m} · α_{M} = Ψ (gfold f g_{1} ⋯ g_{m})

for some form Ψ :: ∀ X . (X · M → N ) → (F X · M → N ). It turns out that it is easier to solve a more general problem. Suppose we are given functors F :: C → C and L :: C → D for categories C and D, for which F has least fixed point α :: F T → T , and a natural transformation Ψ :: ∀ A. (L A → B) → (L (F A) → B). We seek conditions on F and L to ensure there is a unique x :: L T → B such that

x · L α = Ψ x.  (1)

Note that the naturality of Ψ implies that

Ψ (f · L x) = Ψ f · L (F x).  (2)

Some instances of this general scheme are:

• The gfold over nested types is the special case where F and L are higher order functors, with L = (·M ). The action of this functor on natural transformations, like α, yields instances α_{M} .

• In the special case L = Id, equation (2) implies

Ψ x = Ψ id · F x

so that Ψ is determined by Ψ id :: F B → B and the generalised fold reduces to an ordinary fold.

• Further instances are defining equations of the form

x · L α = f · G x · g

for functions f :: G B → B and g :: L · F → G · L. For example, ziplike functions [FSZ94] are of this form, with L = × (a binary functor) and g :: F_{1} × F_{2} → G · ×.

Furthermore, this uniqueness property leads to a general fusion law, stating that for any natural transformation Φ :: ∀ A. (L A → B) → (L′ A → B),

Φ (gfold Ψ) = gfold Ψ′ ⇐ Φ · Ψ = Ψ′ · Φ.

All the previous fusion laws are instances of this scheme.

We present two solutions to this problem. The first depends on the details of the colimit construction of the fixed point, but works for a larger class of functors L than the second, more abstract, approach. For example, the first approach works for L = ×, while the second does not.

6.1. First method: colimits

Theorem 1. Suppose the functors F and L preserve colimits of chains (all those we can define in Haskell do), and L preserves initiality. Then equation (1) has a unique solution.

Proof. Suppose the colimit used to construct the fixed point T of F consists of functions e_{n} :: F^{n} 0 → T . By construction, the isomorphism α :: F T ≅ T satisfies

α · F e_{n} = e_{n+1}  (3)

for each n. Since L preserves initiality, there is a unique arrow z :: L 0 → B. We shall show that

x · L α = Ψ x ≡ ∀ n. x · L e_{n} = Ψ^{n} z.

Since the arrows L e_{n} comprise a colimit, this establishes the existence and uniqueness of x.

First, we prove

∀ n. x · L e_{n} = Ψ^{n} z ⇐ x · L α = Ψ x

Generalised folds for nested datatypes 19

by induction on n. The base case is immediate from the initiality of L 0. The induction step is

x · L e_{n+1}

=  {equation (3)}

x · L (α · F e_{n})

=  {functor}

x · L α · L (F e_{n})

=  {hypothesis}

Ψ x · L (F e_{n})

=  {equation (2)}

Ψ (x · L e_{n})

=  {induction hypothesis}

Ψ (Ψ^{n} z)

To establish the reverse implication, we reason

x · L α = Ψ x

≡  {isomorphism}

x = Ψ x · L α^{−1}

⇐  {colimit}

∀ n. Ψ x · L α^{−1} · L e_{n} = Ψ^{n} z

⇐  {by cases of n (see below)}

∀ n. x · L e_{n} = Ψ^{n} z

The case n = 0 is immediate from the initiality of L 0. The case n = m + 1 is

Ψ x · L α^{−1} · L e_{m+1}

=  {equation (3)}

Ψ x · L α^{−1} · L α · L (F e_{m})

=  {functor, isomorphism}

Ψ x · L (F e_{m})

=  {equation (2)}

Ψ (x · L e_{m})

=  {hypothesis}

Ψ (Ψ^{m} z)

completing the proof.

6.2. Second method: adjoints

Another approach is to note that we seek a function of type L T → B, whereas a fold can supply a function of type T → B′. Recall that an adjunction between L and a functor R defines an isomorphism

φ :: ∀ A, B. (L A → B) ≅ (A → R B).  (4)

Setting A = T , this yields a correspondence between generalised folds and ordinary folds.

Theorem 2. If L has a right adjoint, then equation (1) has a unique solution.

Proof. Let φ denote the isomorphism defined by the adjunction, as above. We will be applying it to both sides of equation (1). We calculate

φ (Ψ x)
=  {isomorphism}
φ (Ψ (φ^{−1} (φ x)))
=  {naturality of φ^{−1}, introducing the counit ε = φ^{−1} id}
φ (Ψ (ε · L (φ x)))
=  {naturality of Ψ}
φ (Ψ ε · L (F (φ x)))
=  {naturality of φ}
φ (Ψ ε) · F (φ x)

Thus we have

x · L α = Ψ x
≡  {isomorphism}
φ (x · L α) = φ (Ψ x)
≡  {naturality of φ}
φ x · α = φ (Ψ x)
≡  {above calculation}
φ x · α = φ (Ψ ε) · F (φ x)
≡  {fold uniqueness}
φ x = fold (φ (Ψ ε))
≡  {isomorphism}
x = φ^{−1} (fold (φ (Ψ ε)))

Note that this version is strictly weaker than the lower-level approach using colimits: any functor with a right adjoint necessarily preserves all colimits, while × is an example of a functor that preserves initiality and colimits of chains, but not coproducts.

To apply this theorem to generalised folds over nested datatypes, it remains to construct a right adjoint to (·M ). This is a well-studied problem in category theory, where it is known as the right Kan extension [Mac71, X.3], and is known to exist if M is defined on a small complete category. It is also possible to eliminate the size condition by restricting the class of functors M , say to nested functors.

We can define this adjunction in Haskell by introducing a continuation type Cont M N , and constructing an isomorphism pair between T · M → N and T → Cont M N . The functor Cont is declared as

newtype Cont m n a = MkCont (∀ b. (a → m b) → n b)

Thus, Cont wraps a higher-order polymorphic function. For fixed M and N , the functorial action of Cont is defined by

cont  :: (a → b) → Cont m n a → Cont m n b
cont f (MkCont g) = MkCont (λ k. g(k · f ))

One half of the isomorphism is the function

toCont  :: Functor t ⇒ (∀ a. t (m a) → n a) → t b → Cont m n b
toCont f x = MkCont (λ k. f (map_{t} k x))

The function map_{t} is the functorial action of t. The subscript is added for clarity; it is not used in Haskell.

The other half of the isomorphism pair is

fromCont :: Functor t ⇒ (∀ a. t a → Cont m n a) → t (m b) → n b
fromCont f = applyto id · f

where the function applyto k applies a continuation to k:

applyto  :: (a → m b) → Cont m n a → n b
applyto k f  = unCont f k
unCont  :: Cont m n a → (a → m b) → n b
unCont (MkCont x) = x

Then toCont and fromCont is an isomorphism pair, meaning that

toCont · fromCont = id
fromCont · toCont = id.

The first identity is verified by the following calculation:

toCont (fromCont f ) x

=  {definitions of toCont and fromCont}

MkCont (λ k. applyto id (f (map_{t} k x)))

=  {definition of applyto}

MkCont (λ k. unCont (f (map_{t} k x)) id)

=  {naturality of f }

MkCont (λ k. unCont (cont k (f x)) id)

=  {definition of cont}

MkCont (λ k. (λ k′. unCont (f x) (k′ · k)) id)

=  {beta reduction; identity}

MkCont (λ k. unCont (f x) k)

=  {eta reduction; definition of unCont}

f x.

For the second identity, we calculate:

fromCont (toCont f ) x

=  {definitions of fromCont, applyto}

unCont (toCont f x) id

=  {definitions of toCont and unCont}

(λ k. f (map_{t} k x)) id

=  {beta reduction}

f (map_{t} id x)

=  {functoriality of map_{t}}

f x.

7. Final remarks

The subject of nested datatypes and what they might provide for the practical programmer is still in its infancy. Most of the published work so far (in particular, [Oka98]) uses nested types only as a conceptual tool; the results are translated into programming terms by embedding nested types in regular ones in a systematic way. One reason that nested types have not been used directly is that, until recently, there has been no language support for defining functions over such types. Recent versions of Haskell permit rank-2 type signatures and, as we have seen, such a move is necessary to implement functions over nested types.

Defining functions over nested datatypes by explicit recursion is complicated, and even more error prone than using a similar style with regular types. The real purpose of concentrating on the fold function for a datatype is that it provides a structured approach to inductive functional programming. Such a concentration has added force when the datatype is nested.

Acknowledgements

Peter Freyd, Andy Pitts, James Worrell and Dominic Hughes directed us to the appropriate category theory for the adjunction in Section 6.2. Anonymous referees made several helpful suggestions.

References

[BdM97] R. Bird and O. de Moor. Algebra of Programming. Prentice Hall, 1997.

[Bir98] Richard Bird. Introduction to Functional Programming using Haskell. Prentice Hall, second edition, 1998.

[BM98] Richard S. Bird and Lambert Meertens. Nested datatypes. In Mathematics of Program Construction, volume 1422 of Lecture Notes in Computer Science, pages 52–67. Springer, 1998.

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

[CL95] R.H. Connelly and F. Lockwood Morris. A generalisation of the trie data structure. Mathematical Structures in Computer Science, 5(3):381–418, 1995.

[FSZ94] Leonidas Fegaras, Tim Sheard, and Tong Zhou. Improving programs which recurse over multiple inductive structures. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, June 1994.

[Hag87] T. Hagino. Category Theoretic Approach to Data Types. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, UK, 1987. Technical Report ECS-LFCS-87-38.

[Hoo97] Paul Hoogendijk. A Generic Theory of Data Types. PhD thesis, Eindhoven University of Technology, 1997.

[Jon98] Mark Jones. A technical summary of the new features in Hugs 1.3c, 1998. unpublished.

[JS93] Geraint Jones and Mary Sheeran. Designing arithmetic circuits by refinement in Ruby. In R. Bird, C. Morgan, and J. Woodcock, editors, Mathematics of Program Construction, volume 669 of Lecture Notes in Computer Science, pages 208–232. Springer, 1993.

[Lam70] J. Lambek. Subequalizers. Canadian Mathematical Bulletin, 13:337–349, 1970.

[MA86] E.G. Manes and M.A. Arbib. Algebraic Approaches to Program Semantics. Texts and Monographs in Computing Science. Springer, 1986.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer, New York, 1971.

[Mal90a] Grant R. Malcolm. Algebraic Data Types and Program Transformation. PhD thesis, Rijksuniversiteit Groningen, 1990.

[Mal90b] Grant R. Malcolm. Data structures and program transformation. Science of Computer Programming, 14(2-3):255–279, 1990.

[McC84] N. J. McCracken. The typechecking of programs with implicit type structure. In Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 301–315. Springer, 1984.

[Oka98] Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

[PL97] S. Peyton Jones and J. Launchbury. Explicit quantification in Haskell, 1997. See:

http://www.dcs.gla.ac.uk/people/personal/simonpj/.