To appear in Canadian Mathematical Society Proceedings (Category Theory 1991, Montreal).

Strong Categorical Datatypes I

J. Robin B. Cockett Dwight Spencer

Dept. of Computer Science Dept. of Computer Science and Engineering

University of Calgary Oregon Graduate Institute Calgary, Alberta T2N 1N4, Canada Beaverton, Oregon 97006-1999

robin@cpsc.ucalgary.ca dwights@cse.ogi.edu

April 22, 1992

Abstract

An endofunctor of a cartesian closed category is often called strong if it is enriched over the exponential. Equivalently this strength can be provided as a natural transformation θ_{A,X} : F (A)×X ⟶ F (A×X) satisfying some elementary coherence conditions. This latter formulation does not require exponentials, relies only on the presence of an X–action over an X–strong category, and thereby provides a first–order viewpoint of strength.

The 2-category of X–strong categories is not finitely complete. It particularly lacks many standard constructions including the Eilenberg–Moore construction. Thankfully, the suggestion — attributed to Plotkin by Moggi — that strength can also be equivalently framed in terms of fibrations using projections to X–objects as display maps can be fully realized. The equivalence can be portrayed as an embedding of X–strong categories into the 2–category of X–indexed categories or split fibrations over X. This embedding can be used to give a coherent declarative implementation of parametrized datatypes-with-strength and their constructors/destructors in the style of Hagino.

The initiality and finality conditions associated with the strong datatype construction in the split fibration setting generate a strongly normalizing weak-head categorical combinator reduction system. The reduction rules permit both “eager” usage of initial datatypes and “lazy” usage of final datatypes to achieve reasonable computing strength. An X-action over a strong datatype can be computed in terms of programmed state transformations over its component datatypes. These reduction rules form the abstract engine for computation within the Charity categorical programming system.

1 Introduction

In many mathematical instances ordinary functors and natural transformations do not provide sufficient structure to successfully capture a particular phenomenon. A solution usually entails the enrichment of type-forming functors and natural transformations. When the phenomena are programs, we recognize a critical structure-capture requirement: the calculation of a functor should be doable at the same level as the calculation of maps. This has been reinforced by Moggi [12, 13, 14] by his demonstration of the direct relation of strong monads to the semantics of computation.

For cartesian closed categories, this causes us to focus on the obvious enrichment over the internal exponentiation. In this setting an endofunctor F : X ⟶ X is enriched if it is represented as a natural transformation

f_{A,B} : A ⇒ B ⟶ F (A) ⇒ F (B)

which behaves correctly with respect to the composition as internally given. This natural transformation provides the means for building a “strength” for the ordinary functor via the following equivalence:

\frac{X \overline{}^{curry(i_{A×X})} A ⇒ (A × X) \overline{}^{f_{A,A×X}} F (A) ⇒ F (A × X)}{F (A) × X \overline{}^{θ_{A,X}} F (A × X)}.

Conversely, one may formally define the notion of a functor with strength and show that the notion also implies enrichment by

\frac{F (A) × (A ⇒ B) \overline{}^{θ_{A,A⇒B}} F (A × (A ⇒ B)) \overline{}^{F (ev)} F (B)}{A ⇒ B  \overline{}^{f_{A,B}} F (A) ⇒ F (B)}.

These equivalences make redundant the requirement that exponentiation actually be present. We therefore simply consider functors with a given strength. This paper fully develops the consequences of following such a computational direction. Section 2 provides a definition of X–strong categories which serves, we believe, as the appropriate categorical foundation of strength. The definition departs from previous usage, i.e. as enrichment, by adopting the generality of a non-closed setting while concentrating on the product as the source and effect of a tensor action.

Datatypes are built with limits and colimits, yet the resulting 2-category of X–strong categories disappoints us by lacking arbitrary finite limits. In particular, the category of F -algebras of an endofunctor cannot be constructed. Thus there is no immediate guidance for obtaining the “correct” notion of a free monad or, more generally, a datatype. For example, the “correct” notion of a free monad on an endofunctor F is that it is the monad generated by the left adjoint to the underlying functor from the category of F –algebras.

Section 3 shows how our purview of strength can be moved to a complete setting. There we define and explain an embedding, attributed in [12, 13] to Gordon Plotkin, of the 2category of X-strong categories into the 2-category of split fibrations over X. This latter category, by virtue of its completeness, has the algebraic constructions and the guidance we seek.

Section 4 explains the limit constructions of the category of algebras for a strong initial datatype and the category of coalgebras for a strong final datatype within fibrations. The limits are unraveled into the universal initiality and finality diagrams from which all our combinators and computation rules for strong datatypes are derived, as detailed in Section 5. The fibration-based datatype notion we propose is correct in terms of its context parametrization of both constructors and destructors, a feature neglected in other approaches but vital to practical programming practices.

2 X–strength

This section’s purpose is to cast a foundational description of strength and then mold it into an elementary description that will be more widely recognized. The molding will be performed quite independently of cartesian closedness.

The starting point in generality is the notion of a V–tensored category Y. Here V is a category with an arbitrary tensor product, as described by Anders Kock [9], and Y is a category with a V–action on it given by a tensor preserving functor from V into Endo(Y). Our interest narrows to the special case of V’s tensor product being the (cartesian) product. We will hereafter designate such a category V as X. Furthermore, we demand that Y have its own tensor, viz. its product, and that the action, now an X–action, be representable by this tensor. The term X–strong will be used to describe such a category Y. It should be apparent that X–strong categories resemble K-algebras (for K a field) more closely than K-modules.

If X is a cartesian category (i.e. has a binary product and a terminal object) an X-strong category Y is a cartesian category Y with a bifunctor, called an X–action,

⊘ : Y × X ⟶ Y

that is compatible with the coherent natural isomorphisms

• ass : Y ⊘ (X_{1} × X_{2}) ⟶ (Y ⊘ X_{1}) ⊘ X_{2},

• rid : (Y ⊘ 1) ⟶ Y,

• rep : Y ⊘ X ⟶ Y × (1 ⊘ X).

The first two natural isomorphisms are the standard ones and must satisfy the coherence conditions expected for any monoidal action. The last allows the action to be represented by the product of the category Y on which X acts.

Because these categories are cartesian we can simplify the general commuting requirements to the following four equations:

• ass ; rid = id ⊘p_{0} : Y ⊘ (X × 1) ⟶ Y ⊘ X,

• rid = rep ; p_{0} : (Y ⊘ X) ⊘ 1 ⟶ Y ⊘ X,

• ass ; (rid ⊘ id) = id ⊘p_{1} : Y ⊘ (1 × X) ⟶ Y ⊘ X,

• rid ⊘ id = rep ; p_{1} : (1 ⊘ 1) ⊘ X ⟶ 1 ⊘ X.

Notice that they are aimed at ensuring that the map rid behaves correctly.

Proposition 2.1 A cartesian category Y with an X–action is X–strong if and only if there is a cartesian functor

J : X ⟶ Y

and a natural isomorphism r_{Y,X} : Y ⊘ X ⟶ Y × J(X).

Proof. If we are given J and the natural isomorphism r then by setting

rid = r_{Y,1} ; p_{0}
ass = r_{Y,X_{1}×X_{2}} ; ⟨⟨p_{0}, p_{1} ; J(p_{0})⟩, p_{1} ; J(p_{1})⟩; r_{Y ×J(X_{1}),X_{2}}^{−1} ; r_{Y,X_{1}}^{−1} ⊘ id
rep = r_{Y,X} ; id ×⟨!, id⟩; id ×r_{1,X}^{−1}

the (simplified) coherence requirements are straightforward to verify.

Conversely, given an X–action we may choose J(X) = 1 ⊘ X. Clearly J is a functor and r is definable as rep. It remains to show J is cartesian. Because rid : 1 ⊘ 1 ⟶ 1 is an isomorphism it follows that 1 ⊘ 1 is final. To show that products are preserved we consider

1 ⊘ A \overline{}^{1⊘p_{0}} 1 ⊘ (A × B) \overline{}^{1⊘p_{1}} 1 ⊘ B

and show that it is naturally isomorphic to

1 ⊘ A \overline{}^{p_{0}} 1 ⊘ A × 1 ⊘ B \overline{}^{p_{1}} 1 ⊘ B

This is accomplished with the following two diagrams:

[figure: 1 ⊘ (X × Y); id ⊘(id ×!); 1 ⊘ (X × 1); ass; ass; id ⊘p_{0}; (1 ⊘ X) ⊘ Y; (id ⊘ id)⊘!; (1 ⊘ X) ⊘ 1; rid; 1 ⊘ X; rep; rep; p_{0}; 1 ⊘ X × 1 ⊘ Y; id × id ⊘!; 1 ⊘ X × 1 ⊘ 1]

and in which the four identities are used in the triangles.

[figure: 1 ⊘ (X × Y); 1 ⊘ (! × id); 1 ⊘ (1 × Y); ass; ass; id ⊘p_{1}; (1 ⊘ X) ⊘ Y; (id ⊘!) ⊘ i; (1 ⊘ 1) ⊘ Y; rid ⊘i; 1 ⊘ Y; rep; rep; p_{1}; 1 ⊘ X × 1 ⊘ Y; id ⊘! × i; 1 ⊘ 1 × 1 ⊘ Y]

□

All the X–strong categories of interest can be regarded as having a cartesian embedding J of X into it. The X–action is, up to isomorphism, simply given by the product with the image of the objects of X under this embedding. This observation motivates our dropping the action notation A ⊘ X in favor of A × J(X) or just A × X.

X–strong functors, or simply strong functors, are functors between X–strong categories equipped with a natural transformation

θ_{Y,X}^{F} : F (Y) ⊘ X ⟶ F (Y ⊘ X),

called an X–strength, or simply a strength, such that

[figure: (F (A) ⊘ B) ⊘ C; ass; F (A) ⊘ (B × C); θ_{A,B}^{F} ⊘ id_{C}; F (A ⊘ B) ⊘ C; θ_{A,B×C}^{F}; θ_{A⊘B,C}^{F}; F ((A ⊘ B) ⊘ C); F (ass); F (A ⊘ (B × C))]

and

[figure: F (A) ⊘ 1; θ_{A,1}^{F}; F (A ⊘ 1); rid; F (rid); F (A)]

commute.

A strong functor, as used by Moggi for cartesian closed categories, is simply an X-strong endofunctor on X itself with the natural X–action given by product. It is quite reasonable to discuss “strong functors” for non-cartesian closed categories: the list datatype on a distributive category [2] is a strong functor even though its setting is not closed.

An X-strong natural transformation between strong functors F, G : Y_{1} ⟶ Y_{2} is a parameterized natural transformation

α_{A,X} : F (A) ⊘ X ⟶ G(A ⊘ X) : Y_{1} × X ⟶ Y_{2}

such that

[figure: (F (A) ⊘ X) ⊘ Y; θ_{A,X}^{F} ⊘ id_{Y}; F (A ⊘ X) ⊘ Y; α_{A,X} ⊘ id_{Y}; α_{A⊘X,Y}; G(A ⊘ X) ⊘ Y; θ_{A⊘X,Y}^{G}; G((A ⊘ X) ⊘ Y)]

commutes.

Let ν : X \overline{}^{≅} X_{1} ×X_{2} be any decomposition of X into a product. Then the composition of two strong transformations α_{A,X} and β_{A,X} is defined by the following sequence of maps:

[figure: F (A) ⊘ X; id ⊘ν; F (A) ⊘ (X_{1} × X_{2}); ass; (F (A) ⊘ X_{1}) ⊘ X_{2}); α_{A,X_{1}} ⊘ id; (α.β)_{A,X}; G(A ⊘ X_{1}) ⊘ X_{2}; β_{A⊘X_{1},X_{2}}; H(A ⊘ X); H(id ⊘ν^{−1}); H(A ⊘ (X_{1} × X_{2})); H(ass^{−1}); H((A ⊘ X_{1}) ⊘ X_{2})]

The composition does not depend on the particular decomposition of X. That is, all decompositions result in the same parameterized composition. Furthermore, this composition straightforwardly commutes with the strengths in the required manner.

By noting that (1) the definition of strength implies θ_{A,1}^{F} is an isomorphism and (2) the definition of strong natural transformation trivially implies θ^{F} is strong and commutative with all other strong transformations, we see θ^{F} is actually the identity strong transformation on F under this composition. This establishes that X–strong categories, X–strong functors and X–strong transformations form a 2-category Strong(X).

This formulation of an X–strong transformation reveals the structural effect of making transformations strong. However, it fails to promote easy manipulation of these transformations. Notice that an ordinary transformation α gives rise to a related strong transformation provided

[figure: F (A) ⊘ X; θ_{A,X}^{F}; F (A ⊘ X); α_{A} ⊘ id_{X}; α_{A⊘X}; G(A) ⊘ X; θ_{A,X}^{G}; G(A ⊘ X)]

commutes. The associated parameterized transformation is

α_{A,X} = α_{A} ⊘ id_{X} ; θ_{A,X}^{G} = θ_{A,X}^{F} ; α_{A⊘X},

which is clearly strong. Conversely, a strong transformation is related to an ordinary natural transformation by

F (A) rid^{−1} ; \overline{}F (A) ⊘ 1 \overline{}^{α_{A,1}} G(A ⊘ 1) \overline{}^{G(rid)} G(A)

and these associations are inverse. Thus we have reorganized our view of X–strong categories into a more accessible form:

Theorem 2.2 The 2-category Strong(X) is isomorphic to the 2-category having as

0-cells: cartesian functors J : X ⟶ Y,

1-cells: pairs (F, θ^{F}) where F is a functor F : Y ⟶ Y′ and θ^{F} is a strength:

θ_{Y,X}^{F} : F (Y) × J′(X) ⟶ F (Y × J(X)),

satisfying

[figure: (F (A) × J′(X_{1})) × J′(X_{2}); ass; F (A) × J′(X_{1} × X_{2}); θ_{A,X_{1}}^{F} × id; F (A × J(X_{1})) × J′(X_{2}); θ_{A,X_{1}×X_{2}}^{F}; θ_{A×J(X_{1}),X_{2}}^{F}; F ((A × J(X_{1})) × J(X_{2})); F (ass); F (A × J(X_{1} × X_{2}))]

and

[figure: F (A) × J′(X); θ_{A,X}^{F}; F (A × J(X)); p_{0}; F (p_{0}); F (A)]

2-cells: natural transformations α : F ⟶ G which satisfy :

[figure: F (A) × J′(X); θ_{A,X}^{F}; F (A × J(X)); α_{A} × id; α_{A×J(X)}; G(A) × J′(X); θ_{A,X}^{G}; G(A × J(X))]

Therefore an X–strong category may be regarded without loss as a cartesian category with a cartesian functor from X, an X-strong functor as a functor with a strength, and an X–strong transformation as a transformation which commutes with the strengths as shown above. We shall henceforth identify ⊘ and × and avoid the use of the relatively unfamiliar coherence maps for ⊘ .

3 Strength to Fibrations

A strong functor may equivalently be regarded as a morphism of fibrations [5] in which X is viewed as a category of contexts. Technically this is given by an embedding of the 2– category Strong(X) into the 2–category of split fibrations over X, SplFib(X). The latter can, of course, be equivalently viewed as X–indexed categories. This section derives the embedding; the next section attaches the importance of this embedding to our fabrication methodology for datatypes.

Given an X–strong category Y we may form the category P_{X}(Y) to be be thought of as Y–maps with context ¿from X:

Objects: pairs of objects (Y, X) where Y ∈ Y and X ∈ X,

Maps: pairs of maps (f, x) : (Y, X) ⟶ (Y′, X′) where f : Y × X ⟶ Y′ in Y and x : X ⟶ X′ in X,

Identities: (p_{0}, id) : (Y, X) ⟶ (Y, X),

Composition: (f, h) ; (g, k) = (⟨f, p_{1}; h⟩; g, h; k).

A map (f, h) uses h to propagate the context in the second component and f to compute new data values from both data values in Y and the available context:

(f, h) : (Y, X) ⟶ (Y′, X′) ; (y, x) ↦ (f(y, x), h(x)).

Composing this map with (g, k) gives:

(f, h) ; (g, k) : (Y, X) ⟶ (Y′′, X′′) ; (y, x) ↦ (g(f(y, x), h(x)), k(h(x))).

Thus g receives a propagated context and the computed value. This can be viewed as the Kleisli composition for the comonad of the X–action (see Remark 3.4).

The objects of this category may be considered as second projections p_{1} : Y × X ⟶ X and the maps as naturality squares. The category, seen as arrows, can be viewed as a fibration sitting over X, i.e.

δ_{Y} : P_{X}(Y) ⟶ X

where (f, x) ↦ x. The second projections behave as display maps [21], i.e. context extractors. The map which carries Y to the fibration δ_{Y} is the object map of a 2–functor from strong categories to split fibrations over X, denoted P_{X}( ). We are now at the starting point for discussing the correspondence of strength to fibrations attributed to Plotkin by Moggi. The remainder of this section is dedicated to proving:

Theorem 3.1 The 2–functor P_{X}( ) : Strong(X) ⟶ SplFib(X) is a full and faithful embedding.

Let StrSplFib(X) denote the 2–category of split fibrations of the form δ_{Y}. The 1cells are morphisms of fibrations (functors F̃ : P_{X}(Y) ⟶ P_{X}(Z) that commute with the fibration legs and preserve the splitting on the nose). The 2-cells are natural transformations of morphisms of fibrations (α̃ : F̃_{1} ⟶ F̃_{2} such that δ_{Y} = δ_{Z} ∗ α̃ (horizontal composite)). We will show that P_{X}( ) factored through this full sub–2–category is an isomorphism.

First we assure ourselves that the functors δ are indeed fibrations that individually possess a splitting. The underlying cleavage is defined by

(x, (Y, X′)) ↦ (p_{0}, x) .

This is illustrated by the diagram

[figure: (Y, X); (p_{0}, x); (Y, X′); δ; δ; X; x; X′]

The fact that this cleavage yields cartesian arrows follows directly from the definitions and parallels the reasoning that

[figure: Y × X; i × x; Y × X′; p_{1}; pb; p_{1}; X; x; X′]

is a pullback. Because the X–action canonically provides the products used in defining the maps in P_{X}(Y), the cleavage is closed to composition, i.e. it is a splitting.

Suppose F̃ : P_{X}(Y) ⟶ P_{X}(Z) is a morphism of fibrations. On the objects it must take the simple form

F̃(A, X) = (F (A), X)

for some object function F due jointly to fixing the second coordinate and preserving splitting on the nose, thereby allowing the definition of F to be independent of X. On maps it must take the less precise form

F̃(f, x) = (F̃_{0}(f, x), x)

since the fibration morphism preserves fibers over morphisms as well.

In the fiber over 1 we may recapture an ordinary functor F : Y ⟶ Z by setting for x : Y ⟶ Y′

F (x) = ⟨id_{F (Y)},!_{F (Y)}⟩; F̃_{0}(p_{0} ; x , id_{1}) .

To see that this is a functor note first that

F (id) = ⟨id,!⟩; F̃_{0}(p_{0}, id_{1}) = ⟨id,!⟩; p_{0} = id

where F̃_{0}(p_{0}, id_{1}) = p_{0} since F̃ preserves identities. For composition we exploit the fact

F̃(p_{0} ; x; y , id_{1}) = F̃(p_{0} ; x , id_{1}) ; F̃(p_{0} ; y , id_{1})

so that

⟨id,!⟩; F̃_{0}(p_{0} ; x; y , id_{1}) = ⟨id,!⟩; ⟨F̃_{0}(p_{0} ; x , id_{1}) , p_{1} ; id_{1}⟩; F̃_{0}(p_{0} ; y , id_{1})
= ⟨id,!⟩; F̃_{0}(p_{0} ; x , id_{1}) ; ⟨id,!⟩; F̃_{0}(p_{0} ; y , id_{1})

follows, showing composition is preserved.

Next we shall show that this functor has a strength given by θ^{F} = F̃_{0}(id,!), the first component of

F̃(id,!) : (F (A), X) ⟶ (F (A × X), 1) .

θ^{F} ’s naturality in each argument derives easily from the commutativity of the following square:

Lemma 3.2 The diagram

[figure: (F (A), X); (θ^{F} ,!); (F (A × X), 1); (p_{0} ; F (a) , x); (p_{0} ; F (a × x) , id_{1}); (F (A′), X′); (θ^{F} ,!); (F (A′ × X′), 1)]

commutes.

Proof. The lemma’s diagram is the image in P_{X}(Z) of

[figure: (A, X); (id,!); (A × X, 1); (p_{0} ; a , x); (p_{0} ; (a × x) , id_{1}); (A′, X′); (id,!); (A′ × X′, 1)]

in P_{X}(Y) under F̃. To see this we observe that

F̃(p_{0} ; a , x) = F̃(p_{0}, x) ; F̃(p_{0} ; a , id) = (p_{0}, x) ; F̃(p_{0} ; a , id)

because the splitting over x, (p_{0}, x), must be taken by F̃ to the specified (i.e. same) splitting over x. Furthermore, any map F̃(p_{0} ; g , id) is determined as the unique map over the splitting of ! : X ⟶ 1 by applying F̃ to

[figure: (A, X); (p_{0},!); (A, 1); (p_{0} ; g , id_{X}); (p_{0} ; g , id_{1}); (A′, X); (p_{0},!); (A′, 1)]

and observing that (F̃_{0}(p_{0} ; g , id_{X}) , id_{X}) is the unique solution in the resultant image

[figure: (F (A), X); (p_{0},!); (F (A), 1); (F̃_{0}(p_{0} ; g , id_{1}), id_{1}); (F (A′), X); (p_{0},!); (F (A′), 1)]

Tracing the diagram’s first coordinate yields F̃_{0}(p_{0} ; g , id_{X}) = p_{0} ; F (g), giving the commutativity of the lemma’s diagram (and consequently the naturality of θ^{F}).

□

A more precise form for the F̃–image of an arbitrary map (a, x) : (A, X) ⟶ (A′, X′) . can now be derived:

Lemma 3.3

F̃(a, x) = (θ^{F} ; F (a) , x).

Proof. A splitting can be factored out by (a, x) = (a, id) ; (p_{0}, x), leaving the problem of finding F̃(a, id). But we note that

[figure: (A, X); (id,!); (A × X, 1); (a, id); (p_{0} ; a , id_{1}); (A′, X); (p_{0},!); (A′, 1)]

commutes so F̃(a, id) is the unique solution (by the familiar splitting argument) in the diagram’s F̃-image (created via the proof of Lemma 3.2)

[figure: (F (A), X); (θ^{F} ,!); (F (A × X), 1); (p_{0} ; F (a) , id_{1}); (F (A′), X); (p_{0},!); (F (A′), 1)]

which is clearly given by (θ^{F} ; F (a) , id_{X}).

□

This observation is useful in showing how to reconstruct the functor F̃ from (F, θ^{F}). More immediately we see it provides

[figure: F (A) × 1; θ^{F}; F (A × 1); p_{0}; F (p_{0}); F (A)]

the first requirement for strength by examining the first coordinate of the image of

[figure: (A, 1); (id_{A},!); (A × 1, 1); (p_{0}, id); (p_{0} ; p_{0} , id_{1}); (A, 1)]

under F̃. For verifying associativity of the strength we can now track the first coordinate in the F̃–image of

[figure: (A, X × Y); (ass ; p_{0} , p_{1}); (A × X, Y); (id,!); ((A × X) × Y, 1); (p_{0}, id); (p_{0} ; ass , id_{1}); (A, X × Y); (id,!); (A × (X × Y), 1)]

This boils down to distilling from the fibration morphism a strong functor. In similar fashion we can extract from a natural transformation α̃ : F̃_{1} ⟶ F̃_{2} of fibration morphisms a strong transformation α between the respective extracted functors. The (A, X)-component of α̃ has the general form

α̃^{A,X} = (α̃_{0}^{A,X}, id_{X})

due to the horizontal composition requirement. In the fiber over 1 the A-component of α is defined as

α_{A} = ⟨id,!⟩; α̃_{0}^{A,1}

It is straightforward to verify the required transformational properties of α and to derive the relationship

α̃^{A,X} = (p_{0} ; α_{A} , id_{X})

directly as the unique comparison over a splitting arrow in the following diagram:

[figure: F̃(A, X); F̃(p_{0},!); F̃(A, 1); (α̃_{0}^{A,1}, id_{1}); G̃(A, X); G̃(p_{0},!); G̃(A, 1)]

This extraction process preserves composition of ordinary functors and transformations as it clearly does so in the fiber over 1. We must also check that it preserves the strong compositions. For functors this fact is given by breaking the defining map for the strength of F into a composition

(θ^{F} ,!) = (id,!) ; (p_{0} ; θ_{F} , id_{1})

Under G̃ this yields in the first coordinate the Kock equation

θ^{G∘F} = θ^{G}; G(θ^{F})

as desired. For natural transformations of morphisms of fibrations the strengthening of the extracted natural transformations is found in the first coordinate of

[figure: F̃(A, X); F̃(id,!); F̃(A × X, 1); α̃^{A,X}; α̃^{A×X,1}; G̃(A, X); G̃(id,!); G̃(A × X, 1)]

This establishes a 2–functor

StrSplFib(X) ⟶ Strong(X)

To show it is an isomorphism it suffices to show bijectivity on objects, functors, and transformations. By construction, bijectivity immediately holds for objects.

Given a strong functor (F, θ^{F}) we define an opposing lifting map that sends F to F̃ defined by:

[(A, X) \overline{}^{(a,x)} (A′, X′)] ↦ [(F (A), X) \overline{}^{(θ^{F}; F (a) , x)} (F (A′), X′)].

Note that if F̃ is a morphism of fibrations the strong functor recaptured from the fiber over 1 will be F since

⟨id,!⟩; F̃_{0}(p_{0} ; a , id_{1}) = ⟨id,!⟩; θ^{F} ; F (p_{0} ; a)
= ⟨id,!⟩; p_{0} ; F (a)
= F (a).

So F ⟶ F̃ ⟶ F will be the identity. Conversely, Lemma 3.3 will tell us that the transition F̃ ⟶ F ⟶ F̃ is also the identity. This means the 2–functor will be an isomorphism on functors.

F̃ is indeed a morphism of fibrations as it is a functor P_{X}(Y) ⟶ P_{X}(Z) by

⟨θ^{F} ; F (g) , x⟩; θ^{F} ; F (g′) = ⟨θ^{F} , p_{1}⟩; (F (g) × x) ; θ^{F} ; F (g′)
= ⟨θ^{F} , p_{1}⟩; θ^{F} ; F (g × x) ; F (g′)
= ⟨id, p_{1}⟩; (θ^{F} × id) ; F (g × x) ; F (g′)
= (id ×Δ) ; ass; (θ^{F} × id) ; F (g × x) ; F (g′)
= (id ×Δ) ; θ^{F} ; F (ass) ; F (g × x) ; F (g′)
= θ^{F} ; F (id ×Δ) ; F (ass) ; F (g × x) ; F (g′)
= θ^{F} ; F (⟨g , p_{1} ; x⟩; g′)

and it preserves the splitting because θ^{F} ; F (p_{0}) = p_{0}.

Finally, we must show that strong transformations can be lifted back to transformations of fibrations. We now know that a strong transformation is determined by its underlying ordinary transformation. From this fact the process of extracting the strong transformation from a lifted strong transformation is clearly seen to behave as the identity.

If the lifting of the strong transformation extracted from a transformation of fibrations can also be proved to be the identity then we will have established an isomorphism of transformations. To confirm this, we first remark that a strong transformation α may be lifted by using the following diagram as a “naturality square”:

[figure: (F (A), X); (θ^{F} ; F (a) , x); (F (A′), X′); (p_{0} ; α_{A} , id_{X}); (p_{0} ; α_{A′} , id_{X′}); (G(A), X); (θ^{G}; G(a) , x); (G(A′), X′)]

Furthermore, we discovered above that transformations of fibrations also have this form. So the lifting of an extracted transformation is truly the identity. This completes the proof of Theorem 3.1.

We shall hereafter refer to the full and faithful embedding of Strong(X) into SplFib(X) that follows from this development as the strong–fibration embedding.

Remark 3.4 A very compact perspective of strength leverages the equivalence between the categories of split fibrations and of indexed categories. Because we can view the X–action ⊘ of the X–strong category Y as an ordinary product in Y, each functor ⊘ X for X ∈ X is a comonad of Y. The unit and multiplier are:

η : ⊘ X \overline{}^{p_{0}}

μ : ⊘ X \overline{}^{⟨id,p_{1}⟩} ( ⊘ X) ⊘ X

The Kleisli category of this comonad is also Lambek’s polynomial category obtained by adjoining an element [10].

To each X ∈ X we may associate the Kleisli category Y_{X}. Since any morphism f : X_{1} → X_{2} in X clearly induces a morphism of the respective comonads, then it also induces a functor f^{∗} : Y_{X_{2}} → Y_{X_{1}}. Our association is consequently an indexed category F : X^{op} → Cat. The morphisms of fibrations in StrSplFib(X) restricted to the fiber over 1, i.e. the strong functors, can now be seen to be exactly the morphisms of the Grothendieck construction of the corresponding split fibration for F.

4 Datatypes and Strength

Tatsuya Hagino’s thesis [6] proposed a categorical programming language that introduced two sorts of datatype declarations: initial datatypes and final datatypes. Gavin Wraith [25] somewhat simplified the original system and declarations by assuming explicitly that the underlying setting was a bicartesian closed category. In our treatment we take another direction: assume that the underlying category is a cartesian category and replace the closed requirement by the assumption that the datatypes are strong. Because the strong functors of Section 3 are always covariant, we avoid the well-known nuisance of moving contravariant functors — such as exponentials and hom-functors — to a new venue, e.g. O-categories [19], where they can also act covariantly — the limit-colimit coincidence [17]

— and thereby become eligible for computing ω-colimits as solutions of recursive domain equations for datatypes.

Factorizer versions of the Hagino “right” and “left” forms of datatype declaration done in a style similar to that suggested by Wraith are:

data C ⟶ R(A) =  data L(A) ⟶ C =
d_{1} : C ⟶ E_{1}(A, C)  c_{1} : E_{1}(A, C) ⟶ C
| … | …
| d_{n} : C ⟶ E_{n}(A, C).  | c_{n} : E_{n}(A, C) ⟶ C.

The first declaration asserts that any map to the new type R(A) from a state type C is to be determined by a set of programmer-chosen maps from C to the types E_{1}(A, C), ..., E_{n}(A, C). The second definition forms exactly the dual. The labels d_{i} and c_{i} name the collection of canonical operations (not to be confused with the programmer-chosen maps) that are universally associated with their respective datatypes and in one-to-one correspondence with the programmer-chosen maps in a particular declaration. Clearly the first definition declares a final datatype, the second an initial datatype.

The chosen parameter type variable A usually ranges over a power of the given category. However, we shall take the interpretation that it simply ranges over some category and assume the typing E_{i} : A × C ⟶ C. The object R(A) comes equipped with canonical maps

d_{i} : R(A) ⟶ E_{i}(A, R(A))

which Wraith called destructors as they play the dual role to the canonical maps associated with L(A)

c_{i} : E_{i}(A, L(A)) ⟶ L(A)

which are traditionally called constructors. With respect to these maps the initial and final datatypes satisfy the following universal properties:

[figure: C; g_{i}; E_{i}(A, C); E_{i}(A, L(A)); c_{i}; L(A); f_{R}(g); E_{i}(A, f_{R}(g)); E_{i}(A, f_{L}(h)); f_{L}(h); R(A); d_{i}; E_{i}(A, R(A)); E_{i}(A, C); h_{i}; C]

Here g and h respectively represent the n-tuples of the g_{i} and h_{i} morphisms.

We shall denote the datatypes as (R, d) and (L, c), respectively, to emphasize the definitional consolidation of destructors and constructors with their respective datatypes. Additionally, these finality and initiality diagrams often constitute recursive definitions; they shall be referred to as the “recursion” diagrams for their datatypes.

Potentially the category of coalgebras for the final datatypes may be constructed as an inserter (see Kelly [8]), a 2–categorical limit, if it exists. The inserter resembles the comma category except that the functors giving the domain and codomain originate on the same object. In fact it is a lax equalizer: for general functors G, H : A → B, the inserter is the universal pair (U, β) where U : Insert(G, H) → A is a functor and β : G ∘ U → H ∘ U is a natural transformation.

For example, in the 2-category Cat the objects of the inserter category Insert(G, H) are the pairs (A, b) where A is in A and b : G(A) → H(A). A morphism (A_{1}, b_{1}) → (A_{2}, b_{2}) corresponds to the existence of a commuting “naturality square” generated by a A-morphism f : A_{1} → A_{2}:

[figure: G(A_{1}); G(f); G(A_{2}); b_{1}; b_{2}; H(A_{1}); H(f); H(A_{2})]

The inserter functor U is realized as the underlying (forgetful) functor from Insert(G, H). The required natural transformation β consequently arises with the components β_{(A,b)} = b.

In our final datatype situation this means that we seek an underlying functor to the category of origin

U_{R} : Insert(Δ_{n} ∘ Pr_{1}, ⟨E_{1}, ..., E_{n}⟩) ⟶ A × C

and a natural transformation α, regarded as the universal destructor of the final datatype, where

Insert(Δ_{n} ∘ Pr_{1}, ⟨E_{1}, ..., E_{n}⟩) [figure: ⇓; α] C^{n}

in which α : Δ_{n} ∘ Pr_{1} ∘U_{R} ⟶ ⟨E_{1}, ..., E_{n}⟩ ∘ U_{R}. Similarly the opposite construction

(Insert(⟨E_{1}, ..., E_{n}⟩, Δ_{n} ∘ Pr_{1}), U_{L}, α′)

constructs the algebras for the initial datatype and its universal constructor.

To find what the universal properties expressed by the destructor squares translate to in this construction, we must take heed that these datatypes are parametrized by objects of A. To naively demand that the underlying functor followed by the first projection, i.e. Pr_{0} ∘U_{R}, have a right adjoint for extracting the final coalgebra and the associated destructor squares is inadequate: such an adjunction would permit the parameter to vary within it!

Parametrization is more precisely viewed in fibrational terms: it is elementary to show that P = Pr_{0} ∘U_{R} : Insert(Δ_{n} ∘ Pr_{1}, ⟨E_{1}, ..., E_{n}⟩) ⟶ A is a cofibration where the cocartesian arrows in the inserter category of the cofibration) are the naturality squares of the form ((A, C), α) → ((A′, C), α′) generated by A×C-morphisms (h_{A}, h_{C}) : (A, C) → (A′, C) where h_{C} = id_{C}.

The final coalgebra for each A-object can now be viewed as picking out final objects in each fiber of P. This is formalized by asserting the existence of a fibered right adjoint R of Pr_{0} ∘U_{R}(= P) between the identity cofibration I : A → A and P:

[figure: A; A; Insert(…); R; ⊥; P; I; P]

The unit and counit of this adjunction are required by definition to be vertical arrows, thereby allowing the restrictions of the functors P and R to the respective fibers over any object A to form an adjunction where the parameter is constant. Each fiber-restricted right adjoint of P does the selection of the final coalgebra for the corresponding base in A exactly according to the universal destructor square. Furthermore, this definition is slightly redundant: it is easy to show that the unit is vertical if and only if the counit is vertical. Since I-verticals can only be identities, the fundamental requirement becomes having a right adjoint to P that possesses an identity counit.

Moreover, with R being a fibration morphism, this view of parametrization converts back to the general 2-categorical setting where we essentially insist A to be a reflective subcategory of Insert(…) via an inclusion that is the right adjoint to P. Under the expanded requirement, we can now let P act as a (fiber-wise) underlying functor in order to follow the “correct” notion for building final datatypes.

Likewise, the initial datatype algebra for each A-object can be “correctly” specified by noting that Q = Pr_{0} ∘U_{L} : Insert(⟨E_{1}, ..., E_{n}⟩, Δ_{n} ∘ Pr_{1}) ⟶ A is a fibration and providing a fibered left adjoint L that has an identity unit as follows:

[figure: A; Insert(…); A; Q; ⊥; L; Q; I]

Analogously, here A can also be seen as a coreflective subcategory of Insert(…) under the inclusion L.

The motivation for laying out such abstract formalization is that once datatype building can be understood in this way we may ship it into any 2–category with finite limits in order to install the correct notion in that setting. The most natural candidate for receiving shipment is, of course, the 2–category Strong(X). Alas, Strong(X) is not finitely complete and even fails to have inserters. This situation is rescued by the strong–fibration embedding. With it we can make datatypes using Strong(X) inside of SplFib(X) which, by its equivalence to the 2–category of X–indexed categories, is finitely complete.

The abstract construction of a strong initial or strong final datatype using the strong– fibration embedding, i.e. respectively the initial object or the final object of an inserter, can be unwound and the computationally unimportant components of morphism pairs then removed. The resulting elementary recursion diagrams expressing the two relevant universal properties are displayed below. We express the collection of functions, g_{1}, …, g_{n} as “gs”. For a strong final datatype the diagram is

[figure: C × X; ⟨g_{i}, p_{1}⟩; E_{i}(A, C) × X; θ_{2}^{E_{i}}; unfold{gs}; E_{i}(A, C × X); E_{i}(A, unfold{gs}); R(A); d_{i}; E_{i}(A, R(A))]

in which θ_{2}^{E_{i}}, as θ^{E_{i}} ; E_{i}(p_{0}, id_{C×X}) via the naturality of θ^{E_{i}}, is the strength applied in the second argument only. Similarly, the diagram for a strong initial datatype is

[figure: E_{i}(A, L(A)) × X; c_{i} × id_{X}; L(A) × X; ⟨θ_{2}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; fold{hs}; E_{i}(A, fold{hs}) × id_{X}; E_{i}(A, C) × X; h_{i}; C]

These diagrams are explored further in the next section, but we should note here the serendipitous inclusion of the context parameter X in the domain of each h_{i} and g_{i}, the components of actions — fold and unfold, respectively — that are in turn determined by these components.

It makes moral intuitional sense to allow the context to be processed with the state by the components of an action using that same context. This feature contrasts with other often-used examples, e.g. concerning lists and natural number objects, where this morality has not been kept.

An immediate corollary of the strong-fibration embedding is :

Lemma 4.1 In the datatypes (R, d) and (L, c), R and L are strong functors.

It is well-known that if a category has coproducts and admits the construct of final datatypes then the destructors form a product cone. Dually, if the category has products then the constructors of initial datatypes form coproduct cocones. For strong initial datatypes we have the even stronger result:

Lemma 4.2 If (L, c) is an initial X–strong datatype then c forms an X–sum.

Here we use the term X–sum to indicate that the X–action distributes over the coproduct, i.e. the c_{i} × id_{X} morphisms are embeddings.

Proof. Suppose h_{i} : E_{i}(A, L(A)) × X ⟶ C then any comparison map

h : L(A) × X ⟶ C

with (c_{i} × id_{X}) ; h = h_{i} satisfies the following recursion diagram

[figure: E_{i}(A, L(A)) × X; c_{i} × id_{X}; L(A) × X; ⟨θ_{2}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; ⟨p_{0}, h⟩; E_{i}(A, ⟨p_{0}, h⟩) × id_{X}; E_{i}(A, L(A) × C) × X; ν_{i}; L(A) × C]

where ν_{i} = ⟨p_{0} ; E_{i}(id_{A}, p_{0}) ; c_{i} , (E_{i}(id_{A}, p_{0}) × id_{X}) ; h_{i}⟩. Therefore it exists and is unique. □

Many initial datatypes have been studied in first-order settings. For example, Leopoldo Román proposed various recursion schemes for the natural numbers in [18] including the one suggested by the above analysis. The first author studied the list datatype in [2] by using a slight variant of the list recursion diagram. For initial datatypes based on functors whose strengths are isomorphisms (these we call linear functors) the exact form of the recursion diagrams is not critical. As an example, the recursion suggested in [2] is correct — but morally “wrong” — and is shown by

A × (list(A) × X)

ass ; cons × id_{X}

\overline{}

list(A) × X

nil × id_{X} ; \overline{}
1 × X

id_{A} ×a a

[figure: f]

A × C \overline{} ; g C

It is quickly seen to be equivalent to the morally correct version

[figure: (A × list(A)) × X; cons × id_{X}; list(A) × X; nil × id_{X}; 1 × X; ⟨ass^{−1} ; id_{A} ×a , p_{2}⟩; a; f; (A × C) × X; g′; C]

that combines the context X with the state C for processing by the programmer-chosen maps f and g′.

For more complex datatypes based on functors whose strengths are not isomorphisms the equivalence between the datatypes implied by the diagrams above fails.

Choosing the correct diagram in these cases becomes critical, but the proper choice is made evident by our general construction.

A common asserted justification for stronger recursion diagrams are their validity in a cartesian closed category. This justification’s weakness is revealed by its not confirming whether we have obtained all the strength it is natural to have.

Yet, admittedly, knowing that our strength-based diagrams are valid in a cartesian closed category certainly provides assurance:

Proposition 4.3 In a cartesian closed category ordinary datatypes are necessarily strong datatypes.

Proof. We shall demonstrate this for the initial datatypes. Suppose (L, c) is an ordinary initial datatype, i.e. it satisfies the simple algebra initiality property firstly-mentioned in this section.

Let h_{i} : E_{i}(A, C) × X ⟶ C be a collection of programmer-chosen maps. Define h_{i}^{∗} as a particular transpose via

\frac{E_{i}(A, X ⇒ C) × X \overline{}^{⟨θ_{2}^{E_{i}},p_{1}⟩} E_{i}(A, (X ⇒ C) × X) × X \overline{}^{E_{i}(id_{A},eval)×id_{X} ; h_{i}} C}{E_{i}(A, X ⇒ C) \overline{}^{h_{i}^{∗}} X ⇒ C}

Using the h_{i}^{∗} as programmer-chosen maps for the ordinary initial datatype L, we construct the diagram below to obtain a unique arrow a : L(A) ⟶ X ⇒ C which gives commutativity in its top square. The bottom pentagon commutes by adjointness.

By rearranging the left vertical composite, the outermost polygon becomes the strong recursion diagram for fold{hs} = (a×id_{X}) ; eval. Since any fold map can be factored in the presence of cartesian closure into the form of the right vertical composite, the comparison map is unique. Thus (L, c) is strong as well.

[figure: E_{i}(A, L(A)) × X; c_{i} × id_{X}; L(A) × X; E_{i}(id_{A}, a) × id_{X}; a × id_{X}; E_{i}(A, X ⇒ C) × X; h_{i}^{∗} × id_{X}; (X ⇒ C) × X; ⟨θ_{2}^{E_{i}}, p_{1}⟩; E_{i}(A, (X ⇒ C) × X) × X; eval; E_{i}(id_{A}, eval) × id_{X}; E_{i}(A, C) × X; h_{i}; C]

□

5 Datatypes to Combinator Reduction

We now transition from specifying strong datatypes to establishing a categorical combinator reduction system that is directly derivable from our brand of Hagino-Wraith style declarations. The strong initiality and strong finality diagrams of the previous section provide immediately the re-write rules for the fold{h_{1}, …, h_{n}} and unfold{g_{1}, …, g_{n}} actions by pasting the diagrams in the direction of decreasing data structure complexity, i.e. towards earlier declaration. These respective actions are uniquely built ¿from a programmer’s specification of context-parameterized state transformers h_{i} coming from components of a datatype and of context-parametrized state de-transformers g_{i} going to components of a datatype. If components of a datatype are intuitively regarded both as its generalized “subterms” and as “instances” of the domains (codomains) of the transformers (detransformers), the rewriting rules can be seen to correspond closely to folding and unfolding program transformations as first cataloged by Burstall and Darlington [1].

Thus the fold rewrite rules for the initial datatype L are easily seen to be:

c_{i} × id_{X} ; fold^{L}{h_{1}, …, h_{n}} ⟹ ⟨θ^{E_{i}}{p_{0}, fold^{L}{h_{1}, …, h_{n}}}, p_{1}⟩; h_{i}

and similarly the unfold rewrite rules for the final datatype R are:

unfold^{R}{g_{1}, …, g_{n}}; d_{i} ⟹ ⟨g_{i}, p_{1}⟩; θ^{E_{i}}{p_{0}, unfold^{R}{g_{1}, …, g_{n}}}

where θ^{F} {f_{1}, …, f_{m}} will hereafter abbreviate θ^{F} ; F (f_{1}, …, f_{m}) for any strong datatype F. We call fold^{L} the L fold factorizer or informally the fold from L. Likewise we term unfold^{R} the R unfold factorizer or informally the unfold to R. These two factorizers can form a minimal utilizable set of categorical programming primitives within this setting, but such a severe constraint in expressiveness leads expectedly to over-complicated codes.

This problem is alleviated by defining two specializations, respectively, of both folding and unfolding that correspond to familiar and vital programming tools. The definitions leverage the fact that, although we are working in a cartesian setting, this setting is closed over all declarations of strong initial and final datatypes.

First, the respective analogies of case analysis and higher-order transformation for initial datatypes can be specified with the use of the available binary products, which can be considered as the strong final datatype Prod of parametric arity 2 where the component functors E_{1} and E_{2} are respectively Pr_{0} ∘ Pr_{0} and Pr_{1} ∘ Pr_{0}:

(i) L case factorizer :

case^{L}{h_{1}, …, h_{n}} ≡
fold^{L}{…, ⟨p_{0} ; E_{i}(id_{A}, p_{0}) ; c_{i} , (E_{i}(id_{A}, p_{0}) × id_{X}) ; h_{i}⟩, …}; p_{1}

(ii) L map factorizer :

map^{L}{h_{1}, …, h_{n}} ≡ fold^{L}{…, θ^{E_{i}}{(h_{1}, …, h_{n}), p_{0}}; c_{i}, …}

Second, the analogies of record formation and higher-order transformation for final datatypes are definable by using the available binary sums, which can be treated as the strong initial datatype Sum of arity 2 with the same component functors as Prod:

(i) R record factorizer :

record^{R}{g_{1}, …, g_{n}} ≡
b_{1} × id_{X} ; unfold^{R}{…, ⟨caseSum{p_{0} ; d_{i} , g_{i}}; E_{i}{id_{A}, b_{0}} , p_{1}⟩, …}

(ii) R map factorizer :

map^{R}{g_{1}, …, g_{n}} ≡
unfold^{R}{…, d_{i} × id_{X} ; ⟨θ^{E_{i}}{(g_{1}, …, g_{n}), p_{0}}, p_{1}⟩, …}

Each of the four specializations and their associated rewriting rules are justified below.

The L case factorizer is precisely the comparison map h of the diagram in the proof of Lemma 4.2. The rewrite rule derives directly from the X–sum factoring property:

c_{i} × id_{X}; case^{L}{h_{1}, …, h_{n}} ⟹ h_{i}

The L map factorizer is defined by the diagram below in which the the collection of passed functions, h_{1}, …, h_{n} is abbreviated as “hs”:

[figure: E_{i}(A, L(A)) × X; c_{i} × id_{X}; L(A) × X; ⟨θ_{2}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; θ^{L}; E_{i}(id, θ^{L}) × id_{X}; E_{i}(A, L(A × X)) × X; θ_{1}^{E_{i}}; E_{i}(A × X, L(A × X)); c_{i}; L(A × X); E_{i}(id, L(hs)) × id_{X}; E_{i}(hs, L(hs)); L(hs); E_{i}(A, L(B)) × X; θ^{E_{i}}{hs, p_{0}}; E_{i}(B, L(B)); c_{i}; L(B)]

The top hexagon defines L strength as a fold operator and the outermost polygon defines the L map factorizer as a fold operator. That is, map^{L}{hs} = θ^{L}{hs}. The diagram’s polygons are essentially pasted from upper-right-to-lower-left to derive the following rewrite rule:

c_{i} × id_{X} ; map^{L}{h_{1}, …, h_{n}} ⟹ θ^{E_{i}}{(h_{1}, …, h_{n}), map^{L}{h_{1}, …, h_{n}}}; c_{i}

The R record factorizer can be defined in a manner dual to the definition of the L case factorizer:

(R(A) + C) × X ν_{i} ; \overline{} E_{i}(A, R(A) + C) × X

θ_{2}^{E_{i}}

[figure: caseSum{p_{0}, g}] E_{i}(A, (R(A) + C) × X)

[figure]

E_{i}(id_{A}, caseSum{p_{0}, g})

R(A) \overline{} ; d_{i} E_{i}(A, R(A))

where

ν_{i} = ⟨caseSum{p_{0} ; d_{i} , g_{i}} , p_{1}⟩; E_{i}(id_{A}, b_{0}) × id_{X}

and g : C × X → R(A) is any comparison map such that g; d_{i} = g_{i}. Here record^{R}{g_{1}, …, g_{n}} is defined to be exactly g which is, in turn, defined by the unique definition of caseSum{p_{0}, g} as an unfold operator. By Lemma 4.2 g is uniquely specified. From the definition’s factorization condition we have the rewrite rule:

record^{R}{g_{1}, …, g_{n}}; d_{i} ⟹ g_{i}

The duality is seen clearly by noting that the L case factorizer definition can now be expressed in terms of record factorizers, viz. by using the relation recordProd{f_{1}, f_{2}} = ⟨f_{1}, f_{2}⟩ for f_{1} and f_{2} having a common domain.

Finally, the R map factorizer is defined by the following diagram in which the collection of passed functions g_{1}, …, g_{n} is abbreviated as “gs”:

[figure: R(A) × X; d_{i} × id_{X}; E_{i}(A, R(A)) × X; ⟨θ_{1}^{E_{i}}, p_{1}⟩; E_{i}(A × X, R(A)) × X; E_{i}(gs, id) × id_{X}; E_{i}(B, R(A)) × X; θ^{R}; θ_{2}^{E_{i}}; θ_{2}^{E_{i}}; E_{i}(A × X, R(A) × X); E_{i}(gs, id); E_{i}(B, R(A) × X); E_{i}(id, θ^{R}); R(A × X); d_{i}; E_{i}(A × X, R(A × X)); E_{i}(id, θ^{R}{gs}); R(gs); E_{i}(gs, R(gs)); R(B); d_{i}; E_{i}(B, R(B))]

The top left hexagon defines R strength as an unfold operator and the outermost polygon defines the R map factorizer as an unfold operator. Again, this means map^{R}{gs} = θ^{R}{gs}. The polygons of the diagram are pasted lower-left-to-upper-right to obtain the rewrite rule:

map^{R}{g_{1}, …, g_{n}}; d_{i} ⟹ d_{i} × id_{X} ; θ^{E_{i}}{(g_{1}, …, g_{n}), map^{R}{g_{1}, …, g_{n}}}

Conjoining these six rewriting rules with the well-known basic rewriting rules for cartesian categories forms a strongly-normalizing polymorphic combinatory reduction system in which an expansive variety of eager initial and lazy final datatypes can be declared in a cartesian setting and their terms computed. This system forms the abstract machine backbone of the Charity categorical programming language implemented by Cockett and Fukushima [4].

To balance our discussions of the more familiar initial datatypes, we close this section with two concrete strong final datatype examples: infinite lists and colists, two forms of “lazy lists”. Their utility often lies in reducing complexity in list manipulation. Final datatypes are often infinitary and correspond to greatest fixpoints of colimit-preserving functors (e.g. see Manes and Arbib [11]). Our first example, infinite lists, are declared with the component functors Pr_{0} and Pr_{1} and with the destructors that extract respectively the head and the (infinite) tail of an infinite list. Essentially we are solving the domain equation Inflist(A) = A × Inflist(A) maximally, i.e. finding all truly infinite lists of the parameter type A. The strong infinite list recursion diagram is presented below:

[figure: A × X; ⟨f, p_{1}⟩; C × X; ⟨g, p_{1}⟩; C × X; p_{0}; unfoldInflist{f, g}; unfoldInflist{f, g}; A; head; Inflist(A); tail; Inflist(A)]

The colist datatype includes the non-empty finite lists as well as the infinite lists. Here Pr_{0} and Sum{1, C} are the declaration functors and consequently we envision the equation Colist(A) = A + (A × Colist(A)) = A × (1 + Colist(A)). Recall that the second equality follows ¿from Lemma 4.2. Using like-named destructors, the strong colist recursion diagram reduces to

[figure: A × X; ⟨f, p_{1}⟩; C × X; ⟨g, p_{1}⟩; (1 + C) × X; p_{0}; unfoldColist{f, g}; θSum{p_{0}, unfoldColist{f, g}}; A; head; Colist(A); tail; 1 + Colist(A)]

The partiality of the colist tail, revealed by the appearance of an error type (1) in its codomain, contrasts with the totality of head.

6 Conclusions and Future Work

A forthcoming paper will describe a term logic with support for strong datatypes which serves as a categorical programming language. The translation of this term logic into the above datatype combinators will be explained and proven to be consistent and functionally complete.

Such a categorical programming language has been implemented: Charity is currently an operational testbed for categorical programming and uses a mixture of eager initial and lazy final datatypes (Cockett and Fukushima [4]). As a programming language it is remarkably useable (considering its formal nature and the fact that all programs strongly normalize). The arithmetic strength of the setting is weaker than most comparable systems (as there is no exponentiation) but does allow, for example, the definition of Ackermann’s function.

Categorical computation remains relatively inefficient compared even to conventional functional languages, so techniques such as optimizing the translation of the term logic to combinators in order to speed up execution will be important. Recent intriguing results by Barry Jay [7] on the efficiency of iteration within categorical computation may help illuminate such optimizations. The discovery of additional specializations of the fold and unfold factorizers to outfit a categorical programmer’s “toolkit” in the sense hinted by David Turner [22] would further this goal. Also, optimizing via program transformations similar to those developed by Malcolm [15, 16] for general Hagino datatypes may be feasible. Finally, the current research surge in functional programming analysis ¿from the perspectives of control, continuations, and partial evaluation might well be worthwhile in this setting.

Cockett’s recent investigations [3] indicate that attractive abstract data structure specifications, such as those espoused by Walters [23], are highly applicable to this programming setting. Also, preliminary investigations have begun towards incorporating dependent types into the system which would yield further improvements in abstract data structure expressiveness.

7 Acknowledgements

Robin Cockett would like to acknowledge the support — financial and intellectual — that the Australian Research Council and the Sydney category seminar provided during the preparation of this work. He is grateful to Richard Wood for explaining his V–indexed categories [24] amid the Kangaroos and to Barry Jay for his burgeoning interest in this topic. And above all, he would like to acknowledge the constant contributions and support provided by Ross Street throughout his stay in Sydney.

Dwight Spencer wishes to thank the Formal Methods Group of the University of Calgary Computer Science Department for giving warm support and open collaboration to this author’s pursuits in categorical computation. He gives particular thanks to Tom Fukushima for his sharp-eyed error-checking of this paper.

References

[1] R.M. Burstall and J. Darlington A transformation system for developing recursive programs. Journal of the Association for Computing Machinery, 24, No. 1 (1977), 44-67.

[2] J.R.B. Cockett, List-arithmetic distributive categories: locoi. Journal of Pure and Applied Algebra 66 (1990) 1-29.

[3] J.R.B. Cockett, Conditional control is not quite categorical control, IV Higher Order Workshop, Banff 1990, Graham Birtwistle (Ed.) Springer–Verlag, Workshops in Computing (1991) 190-217.

[4] J.R.B. Cockett and T. Fukushima, About Charity, University of Calgary (1991). Unpublished manuscript.

[5] J. W. Gray, Fibred and cofibred categories. Proceedings of the Conference on Categorical Algebra, La Jolla, 1965 (Springer, Berlin) 21-84.

[6] T. Hagino, A categorical programming language. Ph.D. Thesis, University of Edinburgh (1987).

[7] C.B. Jay, Tail recursion via universal invariants, University of Edinburgh Research Report Preprint (1991).

[8] G.M. Kelly, Elementary observations on 2-categorical limits. Bulletin of the Australian Mathematical Society 39 (1989) 301-317.

[9] A. Kock, Strong functors and monoidal monads. Archiv der Mathematik, 23 (1972) 113-120.

[10] J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic. Cambridge University Press (1986).

[11] E. G. Manes and M. A. Arbib, Parametrized datatypes do not need highly constrained parameters. Information and Control 52 (1982) 139-158.

[12] E. Moggi, Computational lambda-calculus and monads. Proceedings of the 4^{th} Annual Symposium on Logic in Computer Science (1989) 14-23.

[13] E. Moggi, An Abstract View of Programming Languages. Lecture Notes, University of Edinburgh (June 1989).

[14] E. Moggi, Notions of computation and monads. Information and Control 93 (1991) 55-92.

[15] G. Malcolm, Data Structures and Program Transformation. Science of Computer Programming 14 (1990) 255-279.

[16] G. Malcolm, Algebraic Data Types and Program Transformation. Ph.D. Thesis, University of Groningen (1990).

[17] P. Panangaden, P. Mendler and M. Schwartzbach, Recursively defined types in constructive type theory in Resolution of Equations in Algebraic Structures. Academic Press (1989).

[18] L. Román, On recursive principles in cartesian categories. Preprint.

[19] M. Smyth and G. Plotkin, The category theoretic solution of recursive domain equations. SIAM Journal of Computing 11 (1982) 761-783.

[20] D. Spencer, A survey of categorical computation: fixed points, partiality, combinators, ... control? Bulletin of the European Association of Theoretical Computer Science 43 (February, 1991) 285-312.

[21] P. Taylor, Recursive domains, indexed category theory and polymorphism, Ph.D. Thesis, University of Cambridge (1986).

[22] D. Turner, Duality and De Morgan Principles for Lists, Computer Laboratory Research Report Preprint, University of Kent (1991).

[23] R.F.C. Walters, Data types in distributive categories. Bulletin of the Australian Mathematical Society 40 (1989) 79-82.

[24] R.J. Wood, V–indexed categories. in Springer Lecture Notes in Mathematics 661 (1978) 126-140.

[25] G.C. Wraith, A note on categorical datatypes in Springer Lecture Notes in Computer Science 389 (1989) 118-127.