About Charity

Robin Cockett Department of Computer Science University of Calgary Calgary, Alberta CANADA robin@cpsc.ucalgary.ca

Tom Fukushima Department of Computer Science University of Calgary Calgary, Alberta CANADA fukushim@cpsc.ucalgary.ca

May 27, 1992

Abstract

Charity is a categorical programming language based on distributive categories (in the sense of Schanuel and Lawvere) with strong datatypes (in the sense of Hagino). Distributive categories come with a term logic which can express most standard programs; and they are fundamental to computer science because they permit proof by case analysis and, when strong datatypes are introduced, proof by structural induction.

Charity is functional and polymorphic in style, and is strongly normalizing. As a categorical programming language it provides a unique marriage of computer science and mathematical thought. The above aspects are particularly important for the production of verified programs as the naturality of morphisms gives us “theorems for free”, termination proofs are not required, and mathemathical specifications can be used.

1 Introduction

Functional and logic programming languages have reduced the gap between theory and implementation by reducing the notational movement from mathematics to program, but some significant gaps persist. In particular, the use of general recursion, which produces “fixed points” in the semantics of these languages implies that they represent a peculiar version of mathematics.

The language charity starts from the basis that one can and should actually implement standard mathematics without trickery. Thus, we eliminate the uncomfortable transition

discrete mathematics [figure: ?]^{?} Program

by basing the discrete mathematics in distributive categories and making the programming language charity which makes them the same pursuit.

Bob Walters, Steve Schanuel, Bill Lawvere, and Robin Cockett had all observed that of all the various sorts of categories available distributive categories seem to have exactly the right properties for doing computer science. Indeed, Robin Cockett had observed that the subject of discrete structures was really^{1} about the properties of (the initial) distributive category with list arithmetic[Coc90].

Currently one of the most unsatisfactory aspects of software development is the movement from specification to program. There are various factors which exacerbate the achievement of a smooth transition. A fundamental problem is that, while one wants the specification to be in a language which is generally understandable, this is often in conflict with the requirement that it be rigorous and implementable.

The solution which seems to be emerging has been to link up formal mathematical methods more closely with programming. The idea being that if a specification is essentially a piece of mathematics it will be rigorous and, on the other hand, readable as we have been taught to read mathematics! Whatever one thinks of such a solution, it is clear that there is considerable value to the idea. There is, after all, a wealth of mathematical understanding out there which could be useful in developing specifications.

The point of charity is that it is an uncompromising implementation of constructive discrete mathematics. While it is certainly possible to implement constructive discrete mathematics in a functional language, it is not the case that the semantics of these languages embody constructive discrete mathematics. Certainly, there is a logic underlying functional (and imperative) programming, but it is not the logic which underpins or indeed is even compatible with the vast majority of our mathematical training. In fact, mathematically speaking it is decidedly peculiar!

In mathematics, functions are total, however, when programming over an imperative or functional language, one does have to be careful to avoid the production of non-terminating programs. As charity has a semantics which is compatible with this mathematical intuition one cannot write a non-terminating program. This is not to say that everything is automatically correct but rather that a subtle and all pervading source of incorrectness has been eliminated. For the program verifier this means that the hard proof of termination is no longer required.

The adoption of categorical or type theoretic languages like charity requires a change of the programming paradigm. In particular, general recursion, which is an absolutely fundamental tool in modern computer science thought, is not explicitly allowed in these paradigms. While charity is still under development, we already know that not using general recursion is possible theoretically, pragmatically, and practically. However, much work remains to bring this paradigm incisively to bear on practical applications.

2 Preliminaries

A recent trend in computer science is to see a category as being the proof theory of some known logic. Thus, cartesian closed categories are the proof theory of intuitionistic propositional logic, ∗–autonomous categories of the multiplicative fragment of linear logic. As computer scientists have often seen the usefulness of logic (implying that a similar statement concerning category theory is more tendentious) this provides a convenient justification of the use of categories. We may start therefore by asking rather cynically “for what logic are distributive categories the proof theory?” Fortunately, there is such a logic and it is the (∧, ∨)–fragment of propositional logic – or at least morally so!

1A computer scientist was asked what struck him most about category theorists. He replied that they always told him what subjects, which he had been studying for some time, were really about and this really annoyed him.

We shall start by explaining what a distributive category is. This is somewhat complicated by the fact that there are several different shades of distributive categories with embedding theorems allowing one to slip relatively smoothly between them. We start with predistributive categories: a distributive category is a completion of this basic concept (in the same sort of sense that the complex numbers are a completion of the real numbers). We shall assume that everyone knows what a category is and what a product and coproduct are.

2.1 Notation

Roman font, lower-case italics and upper-case italics will be used to indicate items with predefined meanings, variables for maps and type variables respectively. If f : X ⟶ Y and g : Y ⟶ Z then the composition of the maps will be written, using the algebraic order, f; g.

The notation used for maps associated with the product and coproduct will be:

identity  1 : X ⟶ X
terminal map  ! : Z ⟶ 1
product factorizer  ⟨x, y⟩ : W ⟶ X × Y
first projection  p_{0} : X × Y ⟶ X
second projection  p_{1} : X × Y ⟶ Y
product symmetry c = ⟨p_{1}, p_{0}⟩ : X × Y ⟶ Y × X
product diagonal map Δ = ⟨1, 1⟩ : X ⟶ X × X
coproduct factorizer  ⟨v | w⟩ : X + Y ⟶ W
first coprojection  b_{0} : X ⟶ X + Y
second coprojection  b_{1} : Y ⟶ X + Y

where

x : W ⟶ X, y : W ⟶ Y, v : X ⟶ W, and w : Y ⟶ W

and these satisfy the standard equations

z; ! = !
⟨x, y⟩; p_{0} = x
⟨x, y⟩; p_{1} = y
⟨x; p_{0}, x; p_{1}⟩ = x
b_{0}; ⟨v | w⟩ = v
b_{1}; ⟨v | w⟩ = w
⟨b_{0}; x | b_{1}; x⟩ = x.

2.2 Predistributive categories

A predistributive category is a category with finite products and binary coproducts such that the map

⟨b_{0} ×1 | b_{1} ×1⟩ : (A × X) + (B × X) ⟶ (A + B) × X

is invertible. When coproducts satisfy this we shall call them sums. In particular, given any maps:

f : A × X ⟶ C and g : B × X ⟶ C

there is a unique map

case{f, g} : (A + B) × X ⟶ C

defined by case{f, g} = ⟨b_{0} ×1 | b_{1} ×1⟩^{−1}; ⟨f | g⟩. This can be thought of as the if...then...else program control construct: “if the value is in the first case do f else do g.” It is precisely the ability of distributive categories to express control which makes them so applicable to computer science.

2.3 Proof theory

The way in which predistributive categories arise as the proof theory of the (∧, ∨)–fragment of propositional logic is as follows:

Axiom

A ⊢ A identity A \overline{}^{1} A

Logical Rules

A⊢true  truth  A \overline{}^{!} 1
\frac{\underline{Γ⊢B Γ⊢C}}{Γ⊢B∧C}  ∧–intro. and elim. \frac{\underline{Γ \overline{}^{f} B Γ \overline{}^{g} C}}{Γ \overline{}^{⟨f,g⟩} B×C}
\frac{\underline{A,Γ⊢C B,Γ⊢C}}{A∨B,Γ⊢C}  ∨–intro. and elim. \frac{\underline{A×Γ \overline{}^{f} C B×Γ \overline{}^{g} C}}{case\{f,g\}:(A+B)×Γ⟶C}

Structural rules

\frac{Γ,A,B,Λ⊢C}{Γ,B,A,Λ⊢C}  exchange  \frac{Γ×A×B×Λ \overline{}^{h} C}{1×c ×1;h:Γ×B×A×Λ⟶C}
\frac{Γ,A,A⊢C}{Γ,A⊢C}  contraction  \frac{Γ×A×A \overline{}^{h} C}{1×Δ;h:Γ×A⟶C}
\frac{Γ⊢B}{Γ,A⊢B}  weakening  \frac{Γ \overline{}^{h} B}{p_{0};h:Γ×A⟶B}

Cut Rule

\frac{Γ⊢A A,Λ⊢B}{Γ,Λ⊢B}  cut  \frac{Γ \overline{}^{f} A A×Λ \overline{}^{g} B}{f×1;g:Γ×Λ⟶B}

2.4 A remark on abstract data structures

Bob Walters particularly has exploited the presence of control in describing how the specification of data structures can be accomplished using the language of distributive categories. The specification of a stack in a distributive category may be expressed as follows:

Sorts:
      A,stack(A)
Operations:
      empty: 1 --> stack(A),
      push: A * stack(A) --> stack(A),
      pop: stack(A) --> 1 + A * stack(A)
Equations:
      (empty | push) ; pop = 1,
      pop ; (empty | push) = 1

This is a short sweet specification compared to others in the literature: it says that a stack on A is any object with elements which are either empty or of the form push(A,X). The specification done for a general type A does not introduce any extraneous types, and all its models are what we intuitively expect stacks to be!

2.5 Distributive categories

A category is distributive (in the sense of Schanuel and Lawvere) in case it is finitely complete and has binary coproducts satisfying the following diagrammatic condition:

[figure: A′; f′; B′; g′; C′; a; (1); b; (2); c; A; f; B; g; C]

whenever the lower row is a coproduct, squares (1) and (2) are pullbacks if and only if the top row is a coproduct.

A distributive category is certainly predistributive. There are many examples of distributive categories: the category of sets, Set, and any topos, topological spaces, the dual of the category of commutative rings, finitely complete bicartesian closed categories (with inhabited non-empty types) and formal categories of datatypes. The last example being the motivation behind this work.

Observe that the coproduct embeddings in a distributive category must be monic by considering:

[figure: A; b_{0}; A + B; b_{1}; B; !; pb; !+!; pb; !; 1; true; 1 + 1; false; 1]

and using the fact that any map from the final object is monic so that its pullback along !+! must be monic.

Considering, the pullback of the two embeddings into a coproduct we have an object 0 given by the left-hand pullback below:

[figure: 0; 0; 1; 1; 1; !; pb; false; pb; 1; 1; true; 1 + 1; false; 1]

This is an initial object. From the fact that the top row is a coproduct it follows that 0 + 1 ≡ 1. However, this gives

[figure: 0; b_{0}; 0 + B; b_{1}; B; 1; pb; 1+!; pb; !; 0; b_{0}; 0 + 1; b_{1}; 1]

in which the embeddings b_{1} are isomorphisms.

Any two different maps P ⟶ B will provide two different maps P + B to B, whose second component is the identity. If b_{1} : B ⟶ P + B is an isomorphism it follows that no two such maps can exist. If b_{1} : B ⟶ P + B is an isomorphism for every B then there can be at most one map from P to B. In other words P is a preinitial object (at most one map to any other object).

The object 0 is therefore preinitial. However, there always is a map b_{0}; b_{1}^{−1} : 0 ⟶ 0 + B ⟶ B and so it is an initial object. Furthermore, it is a strict initial object (in the sense that any map with codomain 0 is an isomorphism) as any object P with a map to it is preinitial because b_{1} : B ⟶ P + B is necessarily an isomorphism by pulling back over 0 + 1.

This means that the coproduct in a distributive category is disjoint and universal. In fact, having disjoint universal coproducts implies the category is distributive.

As the defining diagrammatic condition of a distributive category is connected it will hold in any slice category. This means that if X is a distributive category then X/A is a distributive category.

We shall assume for the rest of this report that we are working in a distributive category.

3 Datatypes and term logic

The initial distributive category is the category of finite sets. While this is a very interesting category it is not sufficiently rich to model the data structures commonly used in computer science. Thus, we need to show how we may add datatypes in the sense of Hagino.

The purpose of this section is not only to introduce these datatypes but also to introduce the term logic which is used for their manipulation.

3.1 Number and list arithmetic

A distributive category has number arithmetic if it has a strong natural number object. A strong natural number object (N , 0, s) has an element 0 : 1 ⟶ N and a successor map s : N ⟶ N. Such that given any f : X ⟶ C and endomorphism g : C ⟶ C there is a unique map fold^{N} {f, g} such that

[figure: X; ⟨!; 0, 1⟩; N × X; s × 1; N × X; f; fold^{N} {f, g}; fold^{N} {f, g}; C; g; C]

Morally speaking this is the wrong diagram it should really be

[figure: 1 × X; 0 × 1; N × X; s × 1; N × X; f; fold^{N} {f, g}; ⟨fold^{N} {f, g}, p_{1}⟩; C; g; C × X]

However, by having X as a component of C in the first diagram we can obtain the effect of the second diagram.

It is well-known that a natural number object present in this strong form allows the representation of all the primitive recursive functions. Indeed the initial cartesian category with a strong natural number object is the formal theory of primitive recursive functions.

It is simple to see that a strong natural number object is preserved by slicing. In X/A the new natural number object is [N × A \overline{}^{p_{1}} A]. Furthermore, this is a strong natural number for X/A.

A distributive category with list arithmetic, a locos, is the categorical setting for discrete structures. A distributive category has list arithmetic in case it has a strong list object for every A. A strong list object for A, (list(A), nil, cons), has an element nil : 1 ⟶ list(A) and an action cons : A×list(A) ⟶ list(A) such that given any f : 1×X ⟶ C and action g : (A×C)×X ⟶ C there is a unique map fold^{list}{f, g} making the following diagram commute:

1 × X

nil ×1 ; \overline{}

list(A) × X

cons ×1 ; \overline{}
(A × list(A)) × X

[figure] f [figure] fold^{list}{f, g} [figure] ⟨θ_{R}^{×}; 1 × fold^{list}{f, g}, p_{1}⟩

C \overline{} ; g (A × C) × X

where θ_{R}^{×} : (A × list(A)) × X ⟶ A × (list(A) × X); ((x, y), z) ↦ (x, (y, z)) is the associative isomorphism. The notation θ_{R}^{×} will be described in more detail later. A strong list object is an algebraically free monoid in the sense of Max Kelly and has associated with it a multiplication (given by append = fold^{list}{p_{1}, p_{0}; cons}). The list object on the final object is a strong natural number object, thus, list arithmetic certainly implies number arithmetic. We would not expect the reverse to be true, so it is a little surprising to discover how nearly it is true. It suffices to have enough “A–infinite objects” to obtain the list arithmetic from number arithmetic[Coc91a].

If a distributive category has list arithmetic then all its slice categories will have list arithmetic. This is a non-trivial observation.

3.2 Datatypes

Both the strong natural number object and the list datatype are examples of the general notion of an initial datatype which was introduced by Tatsuya Hagino in his thesis[Hag87]. Gavin Wraith somewhat simplified the original system and declarations by assuming explicitly that the underlying setting was a bicartesian closed category[Wra89]. In this treatment we take another direction and assume that the underlying category is distributive and replace the closed requirement by the assumption that the datatypes are strong. We also include final datatypes, which are the dual of initial datatypes.

Initial datatypes are given by definitions of the form:

data L(A) ⟶ S =
c_{1} : E_{1}(A, S) ⟶ S
⋮
| c_{n} : E_{n}(A, S) ⟶ S.

This says that the maps from the new type L(A) to a type S are determined by maps to S from the types E_{1}(A, S), ..., E_{n}(A, S). The type variable A is usually taken to range over a power (a finite product) of the given category. The object L(A) comes equipped with canonical maps

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

whose type is obtained by setting S = L(A) in the declaration. These are called constructors. The functor L is called the type construction of the datatype. The datatype is given by the pair (L, c) of construction and constructors.

With respect to these maps the datatype satisfies the following universal property: given g_{i} : E_{i}(A, Y) × X ⟶ Y there is a unique map fold^{L}{g_{1}, ..., g_{n}}, such that the following diagram commutes:

[figure: E_{i}(A, L(A)) × X; c_{i} × 1; L(A) × X; ⟨θ_{R}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; fold^{L}; E_{i}{1, fold^{L}} × 1; E_{i}(A, Y) × X; g_{i}; Y]

where θ_{R}^{E_{i}} = θ^{E_{i}}; E_{i}{p_{0}, 1} and the subscripted R means to use the strength in the recursive argument only, that is, where L(A) occurs. In the datatype (L, c), the construction L is necessarily a strong functor. It is well-known that if a category has products (or sums) and has initial datatypes then the constructors form a coproduct cone. For strong initial datatypes we have the stronger result: if (L, c) is an initial strong datatype then the constructors form a sum (where we use the term sum, as before, to indicate that the product distributes over this coproduct).

The strength of the type constructor L is defined uniquely by the following diagram:

[figure: E_{i}(A, L(A)) × X; c_{i} × 1; L(A) × X; ⟨θ_{R}^{E_{i}}, p_{1}⟩; E_{i}(A, L(A) × X) × X; θ^{L}; E_{i}{1, θ^{L}} × 1; E_{i}(A, L(A × X)) × X; θ_{¬R}^{E_{i}}; E_{i}(A × X, L(A × X)); c_{i}; L(A × X)]

The subscripted ¬R on the strength means to use the strength in the non-recursive arguments only. Notice that

c_{i} × 1; map^{L}{f} = c_{i} × 1; θ^{L}; L{f}
= ⟨θ_{R}^{E_{i}}, p_{1}⟩; E_{i}{1, θ^{L}} × 1; θ_{¬R}^{E_{i}}; c_{i}; L{f} by definition
= ⟨θ_{R}^{E_{i}}, p_{1}⟩; θ_{¬R}^{E_{i}}; E_{i}{1, θ^{L}}; c_{i}; L{f}  naturality of θ_{¬R}^{E_{i}}
= θ^{E_{i}}; E_{i}{1, θ^{L}}; c_{i}; L{f}  corollary 3.4 below
= θ^{E_{i}}; E_{i}{1, θ^{L}}; E_{i}{f, L{f}}; c_{i}  naturality of c_{i}
= θ^{E_{i}}; E_{i}{f, θ^{L}; L{f}}; c_{i}  functorality of E_{i}
= map^{E_{i}}{f, map^{L}{f}}; c_{i}

where θ^{E_{i}}; E_{i}{x, y} and θ^{L}; L{x} are combined to give the map combinators map^{E_{i}}{x, y} and map^{L}{x} for the map operation which will be discussed again later. The equation also gives an optimized rewrite rule for the map combinator which will be used in the formulation of the abstract machine.

Final datatypes are given by definitions of the form:

data S ⟶ R(A) =
d_{1} : S ⟶ F_{1}(A, S)
⋮
| d_{n} : S ⟶ F_{n}(A, S).

Dual to the initial datatypes, this says that the maps from S to the new type R(A) are determined by maps from S to the types F_{1}(A, S), ..., F_{n}(A, S). Again, the type variable A is taken to range over a power (a finite product) of the given category. The object R(A) comes equipped with canonical maps

d_{j} : R(A) ⟶ F_{j}(A, R(A))

whose type is obtained by setting S = R(A) in the declaration. These are called destructors. The functor R is called the type constructor of the datatype.

The datatype satisfies the following universal property: given g_{i} : S × X ⟶ F_{i}(A, S) there is a unique map unfold^{R}{g_{1}, ..., g_{n}}, such that the following diagram commutes:

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

The strength of the type constructor R is defined uniquely by the following diagram:

[figure: R(A) × X; d_{i} × 1; F_{i}(A, R(A)) × X; ⟨θ_{¬R}^{F_{i}}, p_{1}⟩; F_{i}(A × X, R(A)) × X; θ_{R}^{F_{i}}; θ^{R}; F_{i}(A × X, R(A) × X); F_{i}{1, θ^{R}}; R(A × X); d_{i}; F_{i}(A × X, R(A × X))]

Notice that

map^{R}{h}; d_{i} = θ^{R}; R{h}; d_{i}
= d_{i} × 1; ⟨θ_{¬R}^{F_{i}}, p_{1}⟩; θ_{R}^{F_{i}}; F_{i}{1, θ^{R}}; F_{i}{h, R{h}} by definition
= d_{i} × 1; θ^{F_{i}}; F_{i}{1, θ^{R}}; F_{i}{h, R{h}}  corollary 3.4 below
= d_{i} × 1; θ^{F_{i}}; F_{i}{h, θ^{R}; R{h}}  functorality of F_{i}
= d_{i} × 1; map^{F_{i}}{h, map^{R}{h}}.

As with the initial datatypes, this identity will be used to give an efficient rewriting rule for the abstract machine.

The achieve the above equalities we need the following results.

Definition 3.1 A bifunctor F : A×B ⟶ C is strong if there is a natural transformation θ_{A,B,X}^{F} : F (A, B) × X ⟶ F (A × X, B × X).

Definition 3.2 A bifunctor F : A × B ⟶ C is bistrong if F ( , B) and F (A, ) are strong.

Proposition 3.3 A bifunctor is strong if and only if it is bistrong and

[figure: (F (A, B) × X) × Y; s; (F (A, B) × Y) × X; θ_{B,X}^{F (A, )} × 1; θ_{A,Y}^{F (_{,}B)} × 1; F (A, B × X) × Y; F (A × Y, B) × X; θ_{A,Y}^{F ( ,B×X)}; θ_{B,X}^{F (A×Y, )}; F (A × Y, B × X)]

commutes, where s = ⟨⟨p_{0}; p_{0}, p_{1}⟩; p_{0}; p_{1}⟩.

Corollary 3.4 ⟨θ_{R}^{E_{i}}, p_{1}⟩; θ_{¬R}^{E_{i}} = θ^{E_{i}} and ⟨θ_{¬R}^{E_{i}}, p_{1}⟩; θ_{R}^{E_{i}} = θ^{E_{i}}.

Proof. θ_{¬R}^{E_{i}} and θ_{R}^{E_{i}} strengthen the first and second components of the bifunctor E_{i} : A × C ⟶ C and so are θ^{E_{i}( ,C)} and θ^{E_{i}(A, )} respectively. Thus,

⟨θ_{R}^{E_{i}}, p_{1}⟩; θ_{¬R}^{E_{i}}
= ⟨θ_{C,X}^{E_{i}(A, )}, p_{1}⟩; θ_{A,X}^{E_{i}( ,C×X)}
= 1 × Δ; a; θ_{B,X}^{E_{i},(A, )} × 1; θ_{A,X}^{E_{i}( ,C×X)}
= θ^{E_{i}}.

Similarly, we can prove that ⟨θ_{¬R}^{E_{i}}, p_{1}⟩; θ_{R}^{E_{i}} = θ^{E_{i}}.

□

3.3 Term logic

It is sometimes convenient to describe the maps of a distributive category using a term logic. This removes the necessity to specify projections and can provide more natural looking proofs and programs. The term logic used here is the term logic of cartesian categories augmented with an appropriate notation for the sum and any other datatypes which have been declared. The notation used for maps from the sum is:

case\{f, g\} : X × (A + B) ⟶ C; (x, z) ↦ \{ \begin{matrix}b_{0}(z_{0}) & ↦ & f(x, z_{0}) \\ b_{1}(z_{1}) & ↦ & g(x, z_{1}) \end{matrix} \} (z).

In the combinator (or categorical notation) and term logic we shall use braces (which we shall often omit together with their contents when they can be inferred from the context) to enclose the arguments of a map whose definition is dependent on other maps (such as the arguments {f, g} in case{f, g} above).

For the number arithmetic of the setting we shall sometimes use the special term notation

n{f, g} : N × X ⟶ X; (n, x) ↦ g^{n}(f(x)).

This notation suggests that the following equations should hold and they do:

f^{0}(x) = x
f^{n}(f(x)) = f^{n+1}(x)
f^{n}(f^{m}(x)) = f^{n+m}(x)
(f^{n})^{m}(x) = f^{n·m}(x).

For the initial datatype declared above there is a sum which is determined by its constructors. We may determine a map by its definition on each constructor. This gives the case expression of the charity programming language:

case^{L}{f_{1}, ..., f_{n}} : L(A) × X ⟶ Y; (z, x) ↦ { c_{1}(z_{1}) ↦ f_{1}(z_{1}, x) ; ⋮ ; c_{n}(z_{n}) ↦ f_{n}(z_{n}, x) } (z)

where f_{i} : E_{i}(A, L(A)) ⟶ Y.

The fold operation is written as

fold^{L}{g_{1}, ..., g_{n}} : L(A) × X ⟶ C; (z, x) ↦ { ; | c_{1} : z_{1} ↦ g_{1}(z_{1}, x) ; ⋮ ; c_{n} : z_{n} ↦ g_{n}(z_{n}, x) | ; } (z)

where g_{i} : E_{i}(A, C) × X ⟶ C.

The map expression will be written as

map^{G}{h_{1}, ..., h_{m}} : G(A_{1}, ..., A_{m}) × X ⟶ G(B_{1}, ..., B_{m}); (z, x) ⟶ G { y_{1} ↦ h_{1}(y_{1}, x) ; ⋮ ; y_{m} ↦ h_{m}(y_{m}, x) } (z)

where h_{i} : A_{i} × X ⟶ B_{i}.

For the final datatype declared above there is a product which is determined by its destructors. We may determine a map by its definition on each constructor. The record expression is written as:

record^{R}{f_{1}, ..., f_{n}} : X ⟶ R(A); (x) ↦ ( d_{1} : f_{1}(x) ; ⋮ ; d_{m} : f_{n}(x) )

where f_{i} : X ⟶ F_{i}(A, R(A)).

The unfold expression is written as

unfold^{R}{g_{1}, ..., g_{n}} : C × X ⟶ R(A); (z, x) ↦ (|z ↦ d_{1} : g_{1}(z, x) ; ⋮ ; d_{n} : g_{n}(z, x) |) (z)

where g_{i} : C × X ⟶ F_{i}(A, C).

The map expression is the same as for the initial datatypes.

Note that although our notation for the term logic resembles the notation used by the squiggol community somewhat, they have different meanings. In [EMP91] the fold and unfold expressions are given by the banana and lens while our notation uses bananas for the unfold expression and “macaroons” for the fold expression. The reason for this is that right datatypes are product types and since we enclose pairs in parentheses, other operations on right data should also use the same syntax. The braces denote operations which operate mainly on left data. The map expression which operates on both left and right data uses braces.

4 The term logic in use

Rather than formally developing the term logic we shall concentrate on illustrating how it may be used. To this end we shall develop some simple charity programs using the term logic.

4.1 Boolean datatype

The simplest and most basic datatype is an object consisting of two copies of the final object 1. This is the “recognizable subobject classifier” and introduces a simple propositional logic into the setting.

data Bool ⟶ X =
true : 1 ⟶ X
| false : 1 ⟶ X

The expressions corresponding to “and,” “or,” and “not” are:

∧ : Bool × Bool ⟶ Bool; (x_{0}, x_{1}) ↦ \{ \begin{matrix}true & ↦ & x_{1} \\ false & ↦ & false \end{matrix} \} (x_{0})

∨ : Bool × Bool ⟶ Bool; (x_{0}, x_{1}) ↦ \{ \begin{matrix}true & ↦ & true \\ false & ↦ & x_{1} \end{matrix} \} (x_{0})

¬ : Bool ⟶ Bool; x ↦ \{ \begin{matrix}true & ↦ & false \\ false & ↦ & true \end{matrix} \} (x)

Notice that all of these maps are given by the case expression. For this simple declaration this is the only expression of any significance. In fact, the fold operation and case expression coincide and the map expression has no arguments and so is the projection. It is easy although tedious to show that ∧, ∨, and ¬ give Boolean algebra operations on Bool. The maps from any type to Bool are then the propositions of that type and induce a simple logic for the setting.

From the point of view of programming the most recognizable construct which may be produced when the Boolean datatype is present is the conditional:

If\{p, f, g\} : Y × (X_{0} × X_{1}) ⟶ Z; (y, (x_{0}, x_{1})) ↦ \{ \begin{matrix}true & ↦ & f(x_{0}) \\ false & ↦ & g(x_{1}) \end{matrix} \} (p(y))

This says “if p then f else g.” It takes as parameters a proposition p : Y ⟶ Bool and two functions f : X_{0} ⟶ Z and g : X_{1} ⟶ Z.

4.2 Number Arithmetic

Probably the next most basic datatype is the natural numbers:

data N ⟶ X =
zero : 1 ⟶ X
| succ : X ⟶ X

4.2.1 The case expression

Suppose we wish to express the map from N to N which is zero at zero and one elsewhere we would write:

δ : N ⟶ N; n ↦ \{ \begin{matrix}zero & ↦ & zero \\ succ( ) & ↦ & succ(zero) \end{matrix} \} (n).

The meaning of this expression is literally “if n is zero the answer is zero else if n is the successor of some ‘don’t care’ value set the answer to the successor of zero.” Thus, the case expression does pattern matching on the structure of the term.

Here is another example of the use of the case expression in which we compute the predecessor of a number:

pred : N ⟶ N; n ↦ \{ \begin{matrix}zero & ↦ & zero \\ succ(n′) & ↦ & n′ \end{matrix} \} (n).

In this case again we output zero if n is zero, but this time on matching n and succ(n′) we output n′ the value obtained through the matching.

Here is a slightly more complex example which illustrates how one can use variables available from outside the case factorization. We shall assume that we have defined x . − y (monus). Then note that one way of discovering whether x > y is by determining whether y . − x is zero or not. Thus, to determine the maximum of two numbers we have the following expression:

max(n, m) : N × N ⟶ N; (n, m) ↦ \{ \begin{matrix}zero & ↦ & n \\ succ( ) & ↦ & m \end{matrix} \} (m . − n).

Similarly, the expression for the minimum of two numbers is:

min(n, m) : N × N ⟶ N; (n, m) ↦ \{ \begin{matrix}zero & ↦ & m \\ succ( ) & ↦ & n \end{matrix} \} (m . − n).

However, this begs the question of how one expresses . −; for this we need the fold operation.

4.2.2 The fold operation

The fold operation of a datatype is the fundamental map associated with the datatype. Both the case expression and the map expression can be obtained from it. However, this does not mean that it is not worth having these last two present independently. They both have computational and expressive value. We have already seen that the case expression is quite useful expressively; to see why the map expression is useful we will have to wait until we discuss the list arithmetic. In the meantime let us consider the fold itself.

To express the function which adds two numbers we have two alternatives:

+ : N × N ⟶ N; (n, m) ↦ succ^{n}(m)

or using the fold operation notation above:

+ : N × N ⟶ N; (n, m) ↦ \{| \begin{matrix}zero : () & ↦ & m \\ succ : n′ & ↦ & succ(n′) \end{matrix} |\} (n).

where we regard the second (succ) phrase of the operation to be a map which is iterated n times with starting conditions given by the first (zero) phrase. Clearly the first notation is much more suggestive, however, it does not generalize to arbitrary datatypes which the second notation, of course, does. For this reason we shall stress the latter syntax as this will lead into its use for more general datatypes later.

There is another way of viewing the meaning of the latter expression which is very suggestive. A natural number may be regarded as being a code in the sense that 2 means “take zero, apply succ, apply succ” the expression in the curly brackets indicates how this code is to be modified. Thus, on the instruction “take zero” one instead takes m and on the instruction “apply succ” one instead performs the second phrase, in this case (confusingly) to apply succ. The point being as the starting point is different the expression so interpreted computes n + m.

The expression for n . − m is as follows

. −: N × N ⟶ N; (n, m) ↦ \{| \begin{matrix}zero : () & ↦ & n \\ succ : n′ & ↦ & pred(n′) \end{matrix} |\} (m).

In this case, regarding m as the code on the instruction “take zero” one instead takes n and on the instruction “apply succ” one instead applies pred.

The expression for multiplication is of interest as it uses strength in the recursive (succ) phrase; this would not be possible if we had used the first diagram in section 3.1 to give the fold operation:

· : N × N ⟶ N; (n, m) ↦ \{| \begin{matrix}zero : () & ↦ & zero \\ succ : n′ & ↦ & n′ + n \end{matrix} |\} (m).

This may be regarded as saying add n m times to zero. It is interesting to express multiplication in the other syntax:

x · y = p_{1}({(n, m) ↦ (n, m + n)}^{y}(x, zero))

which is not so nice!

Suppose we wish to create the proposition which tests whether a number is even. The way to do this is to use ¬:

even : N ⟶ Bool; n ↦ \{| \begin{matrix}zero : () & ↦ & true \\ succ : x & ↦ & ¬(x) \end{matrix} |\} (n),

which demonstrates how “regular” propositions on the natural numbers can arise. It is worth noting that eventually every map on a finite number of states either becomes fixed or cycles. This makes the regular propositions on the natural numbers eventually equivalent to a proposition of the form “p divides n.”

The reader should try to write down the expression of other common arithmetic expressions in this syntax: for example the exponential and truncated halving (harder). As a last example consider the problem of writing factorial n:

fac : N ⟶ N; n ↦ p_{0}(\{| \begin{matrix}zero : () & ↦ & (succ(zero), succ(zero)) \\ succ : (n′, m) & ↦ & (n′ · m, succ(m)) \end{matrix} |\} (n)).

Notice that here we have had to resort to a state which is a pair of values in order to express the factorial. This is needed as we need to have both the number we should multiply by and the factorial so far and both are changing.

Burstall gives an alternative syntax for the fold expression in [Bur87] which exploits the use of a cartesian closed setting.

4.3 List arithmetic

The list datatype has the following definition:

data list(A) ⟶ X =
nil : 1 ⟶ X
| cons : A × X ⟶ X

in which nil is the empty list and cons is the operation which adds a new element to the front of the list.

4.3.1 The case expression

A map of classical interest is the following:

tail : list(A) ⟶ list(A); z ↦ \{ \begin{matrix}nil & ↦ & nil \\ cons( , z′) & ↦ & z′ \end{matrix} \} (z).

What this does is to throw away the head of the list should there be one. Compare this to the map pred. Bearing in mind that list(1) is a natural number object we see that tail is the “generalization” of pred. Notice also that tail is not the pop of a stack although a simple way of implementing a stack is as a list.

A more complex use of the case expression is as follows: given a list of numbers return the sum of the first two numbers in the list. If the list does not contain two numbers return zero. This map is given by the following expression:

f : list(N) ⟶ N; z ↦ \{ \begin{matrix}nil & ↦ & zero \\ cons(n_{0}, z′) & ↦ & \{ \begin{matrix}nil & ↦ & zero \\ cons(n_{1}, ) & ↦ & n_{0} + n_{1} \end{matrix} \} (z′) \end{matrix} \} (z)

which shows how the case expressions can be nested.

The simple pattern matching available for the case expression required that the case statements be nested in the above example. The ability to do more complex pattern matching is possible, but is not available yet.

4.3.2 The fold operation

The operation of appending two lists is given by the following fold operation:

append : list(A) × list(A) ⟶ list(A); (z_{1}, z_{2}) ↦ \{| \begin{matrix}nil : () & ↦ & z_{2} \\ cons : (x, y) & ↦ & cons(x, y) \end{matrix} |\} (z_{1}).

In the same way that tail generalizes pred, the operation of appending two lists generalizes addition. Appending is confusing in exactly the same way as addition is confusing, as the second phrase in the fold operation uses the map cons. A useful way to regard this expression is to think of the list z_{1} as being the code “take the empty list, push a_{n} onto the list, push a_{n−1} onto the list, ... , push a_{1} onto the list.” The two phrases of the fold operation then modify this code so that instead of starting with the empty list one starts with the list z_{2} and then replacing each of the “push a_{i} onto the list”s with (the same) “push a_{i} onto the list.”

A common thing one wants to do with lists is to reverse them. We shall show how to do this two different ways. First we shall do the naive reverse:

reverse : list(A) ⟶ list(A); z ↦ \{| \begin{matrix}nil : () & ↦ & nil \\ cons : (a, y) & ↦ & append(y, cons(a, nil)) \end{matrix} |\} (z).

It is well-known that this is inefficient as one repeatedly calls an append inside the second phrase of the fold operation acting on z (order n^{2}). Much more efficient is the following formulation of reverse (order n):

reverse′ : list(A) ⟶ list(A);

z ↦ p_{0}(\{ | \begin{matrix}nil : () & ↦ & (nil, z) \\ cons : ( , (y_{0}, y_{1})) & ↦ & \{ \begin{matrix}nil & ↦ & (y_{0}, y_{1}) \\ cons(a, y′_{1}) & ↦ & (cons(a, y_{0}), y′_{1}) \end{matrix} \} (y_{1}) \end{matrix} | \} (z)).

Now we are claiming that they are the same maps, however we should really be able to prove this! We shall return to this in the next section.

Suppose that one has a list of lists, often one wants to flatten the list by appending all the inner lists together. This operation can be defined by:

flatten : list(list(A)) ⟶ list(A); z ↦ \{| \begin{matrix}nil : () & ↦ & nil \\ cons : (z_{0}, z_{1}) & ↦ & append(z_{0}, z_{1}) \end{matrix} |\} (z).

For example this has the effect of taking

[[a_{1}, a_{2}], [], [b_{1}, b_{2}]] ↦ [a_{1}, a_{2}, b_{1}, b_{2}].

This is the generalization of the map which sums the entries of a list of natural numbers. It is also the “multiplication” of the list monad.

Perhaps the most common thing one wants to do with a list is to order the contents in some manner; this can be done with the following naive insertion sort. We will suppose that we are given a predicate p : X × X ⟶ Bool which determines the order (true if x > y): this will be used as a parameter in the map. To create the map which orders a list of X’s it is first necessary to have a map which inserts an element into its proper place in an ordered list:

insert{p} : X × list(X) ⟶ list(X);
(x, z) ↦ cons(\{ | \begin{matrix}nil : () & ↦ & (x, nil) \\ cons : (x_{0}, (x_{1}, z_{1})) & ↦ & \{ \begin{matrix}true & ↦ & (x_{1}, cons(x_{0}, z_{1})) \\ false & ↦ & (x_{0}, cons(x_{1}, z_{1})) \end{matrix} \} (p(x_{0}, x_{1})) \end{matrix} | \} (z)).

Notice that the map insert has the parameter p which allows this map to be general for all types with an order (in fact any proposition p will do). Also note that pushdown is not as efficient as it might be as it continues to do unnecessary comparisons after the inserted element has been placed in the list; this can be remedied by using a flag in the state to signal when the element has been inserted. The elements of the input list are then inserted, an element at a time, into the initially empty ordered list:

insort\{p\} : list(X) ⟶ list(X); z ↦ \{| \begin{matrix}nil : () & ↦ & nil \\ cons : (x, z_{1}) & ↦ & insert\{p\}(x, z_{1}) \end{matrix} |\} (z).

4.3.3 The map expression

Suppose we have a list of numbers to which we want to add some other number. We could certainly do this using the fold operation, however, there is a much more succinct expression for this using the map expression:

list(N) × N ⟶ list(N); (z, n) ↦ list{y ↦ n + y}(z).

Now this may seem to be a somewhat trivial thing to want to do but it is surprising how often one wishes to do something uniformly to every item of a list (or data structure).

For example suppose that one has two lists and one wants to form the list of all possible pairs in which the first record is an item from the first list and the second record is an item from the second list. This may be done as follows. First, form the list with each item a pair whose first record is an item of the first list and second record a copy of the second list, next for each of these pairs form the list of pairs whose records are respectively the item from the first list and an item from the second list. This will give a list of lists which must be flattened to obtain the list of pairs. The expression for this is:

pairs : list(X) × list(Y) ⟶ list(X × Y); (z_{0}, z_{1}) ↦ flatten(list{x_{0} ↦ list{x_{1} ↦ (x_{0}, x_{1})}(z_{1})}(z_{0})).

Now suppose p : X × Y ⟶ Bool is some proposition then we might have asked for a list of pairs for which p(x, y) = true. One way to obtain this list is as follows: first form all pairs then for each pair in the list apply the map which gives the empty list if the pair is outside p and the singleton list if it is inside p. Applying this uniformly to the list and then flattening will yield the desired result. Set

filter\{p\} : list(X) ⟶ list(X); z ↦ flatten(list\{x ↦ \{ \begin{matrix}true & ↦ & cons(x, nil) \\ false & ↦ & nil \end{matrix} \} (p(x))\}(z))

then the map we want is pairs; filter{p}. These, of course, are the maps underlying list comprehension[Wad90]. This leads us to believe that it is suitable to add monads to charity because of the categorical basis of the system.

A further little example of the use of the map expression is given by the following: suppose we want to know how many times an item occurs in a list. We could form the list of pairs whose first record is the item and whose second record is an element of the list (map expression), then filter with respect to the equality test and determine the length of the resulting list.

4.4 Trees and Quicksort

Given a list of data and a predicate we have seen how we can order the data using an insertion sort. Here we show how charity can be used to sort a list of data using a method similar to Quicksort. The algorithm takes a list of unsorted data; removes the first element as a pivot piv; and divides the rest of the list l into two lists l_{1} and l_{2}. Using a predicate p, each element x of l is put in l_{1} if p(x, piv) and l_{2} otherwise. Using natural numbers and the relation ≤, the effect would be:

[figure: [3, 1, 5, 3] ⇒; 3; ≤; ≤ /; [1, 3]; [5]]

The process is then applied to the sublists. When all that remains are the pivots and empty sublists, the structure is a sorted binary tree with elements as the nodes and empty lists as the leaves. The nodes can then be gathered to produce the sorted list.

[figure: 3; 1; [ ]; 3; [ ]; [ ]; 5; [ ]; [ ]; ⇒ [1, 3, 3, 5]]

To implement this in charity we need to declare a datatype to hold the intermediate trees from above. This datatype is a binary tree where, if the input list is type list(A) then the nodes contain elements of type A, and the leaves contain elements of type list(A).

data btree′(A) ⟶ X =

leaf : list(A) ⟶ X

| node : (X × (A × X)) ⟶ X

This datatype definition suffices to implement the algorithm, but in order to present a map expression which has two phrases, the more general definition

data btree(A, B) ⟶ X =
leaf : A ⟶ X
| node : (X × (B × X)) ⟶ X

will be used. The difference between the definitions is that in btree the leaf may contain data not necessarily related to the type of data in the nodes. In fact, btree′ is an instantiation of btree (ie. btree′(A) ≡ btree(list(A), A)).

Solving the problem from the bottom up, a map is needed which splits a list using the pivot and a predicate p : A × A ⟶ Bool (as in the insertion sort of section 4.3.2):

split list{p} : list(B) × A ⟶ list(B) × (A × list(B));

(l, piv) ↦ \{ | \begin{matrix}nil : () & ↦ & (nil, (piv, nil)) \\ cons : (a, (l_{1}, (piv, l_{2}))) & ↦ & \{ \begin{matrix}true & ↦ & (l_{1}, (piv, cons(a, l_{2}))) \\ false & ↦ & (cons(a, l_{1}), (piv, l_{2})) \end{matrix} \} (p(piv, a)) \end{matrix} | \} (l)

The state on which the fold operation acts is a triple: the first and third component are the lists containing elements “less than or equal to” and “greater than” the pivot piv respectively; the pivot is in the second component.

Next we define a map which extracts the pivot from a list and then divides the list using split list.

divide{p} : list(A) ⟶ btree(list(A), A);

l ↦ \{ \begin{matrix}nil & ↦ & leaf(nil) \\ cons(a, tail) & ↦ & \{ (l_{1}, (a, l_{2})) ↦ node(leaf(l_{1}), (a, leaf(l_{2}))) \} (split list\{p\}(tail, a)) \end{matrix} \} (l)

If the list l is empty an empty leaf is produced, otherwise a node with the pivot a and two leaves containing the sublists l_{1} and l_{2} is produced.

The map divide produces a tree type from the list type. Now we must apply divide to all the leaves of the tree for which we may use the map expression of btree:

node it{p} : btree(list(A), B) ⟶ btree(btree(list(A), A), B);

t ↦ btree \{ \begin{matrix}x & ↦ & divide\{p\}(x) \\ y & ↦ & y \end{matrix} \} (t)

Notice how this map expression can perform two actions. This map will be applied to data of type btree(a, b) where a and b are instantiated instances of A and B. The first and second phrases describe the actions to be performed on the elements of type a and b respectively, thus divide will be applied to the leaves, and nodes will be left unchanged.

Since divide is applied to all the leaves of the tree, they will no longer contain lists of data, but will instead contain trees of data; this is also reflected in the type definition of node it where list(A) becomes btree(list(A), A). To return the tree back to the proper form where leaves contain lists of data, a map btree flatten is used:

btree flatten : btree(btree(A, B), B) ⟶ btree(A, B);

t ↦ \{| \begin{matrix}leaf : (b) & ↦ & b \\ node : (c, (a, c′)) & ↦ & node(c, (a, c′)) \end{matrix} |\} (t).

All of the leaves in the tree are replaced by the subtree that the leaf contains, effectively attaching the top node of the subtree back into the tree.

The maps node it and btree flatten can be used to provide one pass of the sort, thus these maps must be applied to the tree until all of the leaves contain empty lists (ie. the input elements are in sorted order in the tree). When the number of passes is at least the number of input elements this condition is met.

apply{p} : list(A) ⟶ btree(list(A), A);

l ↦ \{| \begin{matrix}zero : () & ↦ & leaf(l) \\ succ : (t) & ↦ & btree flatten(node it\{p\}(t)) \end{matrix} |\} (length(l))

The map length : list(A) ⟶ N returns the length of the list.

After there have been enough passes, the ordered tree can be gathered to produce an ordered list:

gather : btree(list(A), A) ⟶ list(A); t ↦ \{| \begin{matrix}leaf : (b) & ↦ & b \\ node : (l_{1}, (a, l_{2})) & ↦ & append(l_{1}, cons(a, l_{2})) \end{matrix} |\} (t).

The top level map, sort, requires a predicate p and the unordered list:

sort{p} : list(A) ⟶ list(A); l ↦ gather(apply{p}(l)).

While the above algorithm implements the idea of Quicksort it fails to achieve the expected n log n complexity. The main reason for this is because node it and btree flatten always work over the whole tree when we only really need to be working on the leaves. The inefficiency is resolved by using a right btree in section 4.6.

4.5 Infinite lists

Up to this point all of the examples have used left datatypes exclusively. The right datatypes allow us to use possibly infinite data. Possibly the first infinite datatype that comes to mind is the infinite list.

data S ⟶ inflist(A) =
head : S ⟶ A
| tail : S ⟶ S

An infinite list, which takes a state of type S and produces an infinite list of type A, is described by the operations given for the head and tail.

4.5.1 The unfold expression

The unfold expression can be used to define the increasing infinite list of natural numbers ( 0, 1, 2, ... ):

nats : 1 ⟶ inflist(N); () ↦ (|S ↦ \begin{matrix}head : S \\ tail : succ(S) \end{matrix} |) (zero)

which says that the initial state is zero, the operation associated with head simply returns the state, and the operation associated with tail increments the state.

Both the head and the tail threads have operations which can work on the state S. The operation for head is not recursive (which is determined by the datatype declaration) and so returns a “value” by applying the map of the head thread to the state, while the operation for tail, which is recursive, produces a new state for the unfold expression.

head(nats) = zero

head(tail(nats)) = head (() ↦ (|S ↦ \begin{matrix}head : S \\ tail : succ(S) \end{matrix} |) (\underline{succ(zero)})) = succ(zero)

We could also use the unfold expression to define an infinite list of the powers of 2 (2^{0}, 2^{1}, 2^{2}...) by doubling the value of the previous state:

powersof2 : 1 ⟶ inflist(N); () ↦ (|S ↦ \begin{matrix}head : S \\ tail : S + S \end{matrix} |) (zero).

4.5.2 The record expression

The record expression is useful for adding some constant data onto the front of an infinite list. If we wanted to add an extra zero to the front of nats we could do it simply by:

zeronats : 1 ⟶ inflist(N); () ↦ (head : zero, tail : nats)

which would represent the infinite list (0, 0, 1, 2, ... ).

4.5.3 The map expression

The effect of using the map expression is conceptually the same as the map expression on finite lists, in that it performs some operation on every element of the list. The difference is that the map expression on infinite lists must be lazy as it would take a very long time to do an operation on every element of an infinite list.

To get the infinite list of even numbers:

evens : 1 ⟶ inflist(N); () ↦ inflist {x ↦ x + x} (nats)

An alternative definition of getting the powersof2:

powersof2 : 1 ⟶ inflist(N); () ↦ inflist {x ↦ 2^{x}} (nats)

4.5.4 The Fibonacci Sequence

When working with finite objects an element of the Fibonacci sequence can be calculated by the following defining equations

fib(0) = 1
fib(1) = 1
fib(n) = fib(n − 1) + fib(n − 2), n ≥ 2.

Using an infinite list, we can conceptually create the whole sequence and then select the element that we want. Then the Fibonacci sequence is (a_{0}, a_{1}, a_{2}, ...) such that:

a_{0} = 1
a_{1} = 1
a_{n} = a_{n−1} + a_{n−2}, n ≥ 2.

Using an unfold, the above definition is given simply by

fib : 1 ⟶ inflist(N); () ↦ (|(x, y) ↦ \begin{matrix}head : & x \\ tail : & (y, x + y) \end{matrix} |) (1, 1)

which uses a pair for the state: the first and second components contain the value of the current element, and the next element respectively. The calculation of the new state (through the tail thread) is done by making the old next element the new current element, and calculating the new next element by adding the two old values together.

To get the nth value in the sequence (or any infinite list for that matter), we would do n tails and then a head:

get : N × inflist(A) ⟶ A; (n, L) ↦ head (\{| \begin{matrix}zero : () & ↦ & L \\ succ : (L) & ↦ & tail(L) \end{matrix} |\} (n)) .

4.5.5 The Ackermann’s function

Using an infinite list of infinite lists to build an infinite table, we can define the Ackermann’s function. This is significant because the initial datatypes had restricted us to the domain of primitive recursive functions, but with the power of final datatypes we can define a combinator which is not primitive recursive.

The defining equations for the Ackermann’s function are:

ack(0, n) = s(n)  (1)
ack(s(m), 0) = ack(m, 1)  (2)
ack(s(m), s(n)) = ack(m, ack(s(m), n))  (3)

Letting m and n be the column and row index respectively, equation 1 tells us that column 0 is an infinite list where the ith value is i + 1:

\begin{aligned}& 0 & ⋯ \\ 0 & 1 & ⋯ \\ 1 & 2 & ⋯ \\ 2 & 3 & ⋯ \\ ⋮ & ⋮ & ... \end{aligned}

That is column 0 is the infinite list of successive numbers starting from 1:

col_{0} = tail(nats)

Equation 2 tells us that the values in row 0 of a column are the same as the value in row 1 of the previous column.

0 1 ⋯
0 1 2 ⋯
1 2 ? ⋯
2 3 ? ⋯
⋮ ⋮ ⋮ ...

Finally, equation 3 tells us that the value in position (s(m), s(n)) is the same as the value in position (m, i) where i is the value in position (s(m), n):

0 1 ⋯
0 1 \underline{2} ⋯
1 2 3 ⋯
2 3 ? ⋯
⋮ ⋮ ⋮ ...

Thus, the value in position (1,1) is determined by taking the value 2 from position (1,0) and using it as an index into the previous column.

Since, all values are determined by previously calculated values, we can generate the Ackermann’s table:

0 1 2 3 ⋯
0 1 2 3 5 ⋯
1 2 3 5 13 ⋯
2 3 4 7 29 ⋯
⋮ ⋮ ⋮ ⋮ ⋮ ...

To calculate column m we use the values from column m − 1:

col_{m} : inflist(N) ⟶ inflist(N);

L ↦ (|(nxt, L) ↦ \begin{matrix}head : & head(L) \\ tail : & \{newL ↦ (head(newL) . − nxt, newL)\} \\ & ( \{| \begin{matrix}zero : () & ↦ & L \\ succ : s & ↦ & tail(s) \end{matrix} |\} (nxt)) \end{matrix} |) (pred(head(tail(L))), tail(L))

The variable L is the previous column in the table. The variable nxt is used to store the offset (number of tails needed) to the next value.

The Ackermann’s table is then simply the infinite list of all the columns:

ack table : 1 ⟶ inflist(inflist(N));

() ↦ (|L ↦ head : L tail : col_{m}(L) |) (col_{0})

To get the value in position (m,n), we could use the get combinator to first find the proper column, and then the proper row in that column:

ack : N × N ⟶ N; (m, n) ↦ get(n, get(m, ack table))

4.6 Quicksort revisited

Here we show how the Quicksort can be more efficiently implemented using a final datatype to hold the partially sorted data.

Again, the datatype to store the data is a binary tree, the difference this time is that the binary tree is defined as a final datatype and may be infinite (although our trees will be finite).

data S ⟶ rbtree(A, B) =
look : S ⟶ S × (B × S) + A

Every time the destructor look is applied to the tree, a node (b_{0}) or a leaf (b_{1}) value will be returned.

Now by using the pivot map defined above, a map, tree, which creates a sorted binary tree given a predicate and input list can be defined:

tree{p} : list(A) ⟶ rbtree(1, A); (l) ↦ (|x ↦ look : pivot{p}(x)|) (l)

So the creation of the sorted tree is quick, the real problem comes when we try to convert the tree to a sorted list. This was easy when the tree was an initial datatype because we could use the fold operation to iterate over it. The procedure that we will use to collect the tree will be to create a state consisting of three components: the accumulated list (L), the current part of the tree we are looking at (T), and the dump (D). We will then manipulate the state as follows:

• If we are looking at the node of a tree on T then we will push the node value and the right subtree onto the dump, and continue with the left subtree on T:

(L, (Tleft, value, Tright), D) ⇒ (L, Tleft, (value, Tright).D)

• If we are looking at a leaf on T then we will pop an element (a, T) from the dump; the value a will be added to L and we will work on T:

(L, (), (a, T).D) ⇒ (a.L, T, D)

To calculate the number of times that the above operations must be done, we note that for a list of length n there will be n nodes and n + 1 leaves, so we will require 2n + 1 pushs and pops to collect up the tree.

The collect algorithm follows:

pop : list(A) × list(A × rbtree(1, B)) ⟶ list(A) × (rbtree(1, B) × list(A × rbtree(1, B)));

(acc, dump) ↦ \{ \begin{matrix}nil() & ↦ & (acc, ((look : b_{1}()), [])) \\ cons((a, t), dump′) & ↦ & (cons(a, acc), (t, dump′)) \end{matrix} \} (dump)

The push is so straightforward that we directly put it into the collect map.

collect : rbtree(1, A) × N ⟶ list(A) × (rbtree(1, A) × list(A ∗ rbtree(1, A)));

(tree, size) ↦ \{ | \begin{matrix}zero : () & ↦ & ([], (tree, [])) \\ succ : (L, (T, D)) ↦ \\ \{ \begin{matrix}b_{1}() & ↦ & pop(L, D) \\ b_{0}(T l, (a, T r)) & ↦ & (L, (T l, cons((a, T r), D))) \end{matrix} \} (look(T)) \end{matrix} | \} (size)

Since the collect map makes only one pass over the whole tree, as opposed to the n passes that the previous Quicksort made, we can see that this sort is more efficient.

To calculate the expected complexity of the above algorithm, we assume that any permutation of the input is equally likely. The collect map takes time kn for some constant k. The generation of the tree depends on the unsorted input list: if we select the ith smallest element as the pivot, it will take time T (i − 1) and T (n − i) to sort the subtrees. This gives us the relationship:

T (n) ≤ kn + \frac{1}{n} ∑_{i=1}^{n}(T (i − 1) + T (n − i)).

In [AVA74] this is shown to have O(n log n) as expected.

5 Proving equality of maps

The term logic has rules of inference for handling equations which make it logically equivalent to the category itself. The purpose of this section is to show informally how the term logic can be used to prove equivalence of programs.

5.1 Case analysis

A common method of proving that two maps are equal in a distributive category is by a case analysis. This involves splitting the domain into coproduct components over each of which the argument for equality can be made. While this works in any category with coproducts, it works particularly well when the coproducts are universal because the components can be chosen to reflect the splitting on the intermediate domains which occur naturally in the proof.

A case analysis can be lain out somewhat like a decision tree, allowing each subcase to be further split in a non–uniform way in the manner required to complete the proof down that branch. Often the branchings can be arranged naturally using propositions (maps p : X ⟶ 1 + 1) and the splitting induced by assuming in turn that they are true or false (p(x) = true and p(x) = false).

As a trivial example consider the following two formulations of ∧:

∧ : Bool × Bool ⟶ Bool; (x_{0}, x_{1}) ↦ \{ \begin{matrix}true & ↦ & x_{1} \\ false & ↦ & false \end{matrix} \} (x_{0})

∧′ : Bool × Bool ⟶ Bool; (x_{0}, x_{1}) ↦ \{ \begin{matrix}true & ↦ & x_{0} \\ false & ↦ & false \end{matrix} \} (x_{1})

To prove they are the same we perform the following case analysis:

Case 1: x_{0} = true.

This means that x_{0} ∧ x_{1} = x_{1} and it remains to do a case analysis on x_{1} to obtain the values of ∧′.

Case 1.1: x_{1} = true.

x_{0} ∧′ x_{1} = x_{0} = true = x_{1} = x_{0} ∧ x_{1}.

Case 1.2: x_{1} = false.

x_{0} ∧′ x_{1} = false = x_{1} = x_{0} ∧ x_{1}.

Case 2: x_{0} = false.

This means that x_{0} ∧ x_{1} = false and it remains to do a case analysis on x_{0} to obtain the values for ∧′.

Case 2.1: x_{1} = true.

x_{0} ∧′ x_{1} = x_{0} = false = x_{0} ∧ x_{1}.

Case 2.2: x_{1} = false.

x_{0} ∧′ x_{1} = false = x_{0} ∧ x_{1}.

Below we will consider a less trivial example.

5.2 Structural induction

Particularly important is the case analysis associated with an initial datatype. Given the datatype declaration of section 3.2, suppose we wish to prove that

f, g : L(A) × X ⟶ Z

are equal. It suffices to prove that their equalizer is the whole of L(A) × X. Let (E, e) be the equalizer of f and g, then it suffices to prove that e is an isomorphism, which given that e is necessarily monic is established if we can find an a with a; e = 1. This in turn is provided if we can show that E is “closed under the action” in the sense

[figure: F_{i}(A, E) × X; e_{i}; E; F_{i}(1, e) × 1; F_{i}(A, L(A) × X) × X; e; F_{i}(1, p_{0}) × 1; F_{i}(A, L(A)) × X; c_{i} × 1; L(A) × X]

that there is an e_{i} : F_{i}(A, E) × X ⟶ E such that e_{i}; e = (F (1, e; p_{0}); c_{i}) × 1. If we have such a factorization then we have

[figure: F_{i}(A, L(A)) × X; c_{i}; L(A) × X; ⟨θ_{R}^{F_{i}}, p_{1}⟩; F_{i}(A, L(A) × X) × X; a; F_{i}(1, a) × 1; F_{i}(A, E) × X; e_{i}; E; F_{i}(1, e; p_{0}) × 1; e; p_{0}; F_{i}(A, L(A)) × X; c_{i} × 1; p_{0}; L(A)]

in which a; e; p_{0} = p_{0} by the uniqueness of the fold map. But also a; e; p_{1} is determined by

(c_{i} × 1); a; e; p_{1} = ⟨θ_{R}^{F_{i}}, p_{1}⟩; ((F_{i}(1, a; e; p_{0}); c_{i}) × 1); p_{1}
= ⟨θ_{R}^{F_{i}}, p_{1}⟩; p_{1}
= p_{1}

so certainly a; e; p_{1} = p_{1}. But this makes a; e = 1 and so e is an isomorphism.

Specializing this argument to that of determining whether f, g : N × X ⟶ Z are equal shows that it suffices to prove that f(0, x) = g(0, x) and that if f(n, x) = g(n, x) then f(s(n), x) = g(s(n), x). Similarly to determine whether f, g : list(A) × X ⟶ Z are equal it suffices to prove f(nil, x) = g(nil, x) and if f(z, x) = g(z, x) then f(cons(a, z), x) = g(cons(a, z), x).

As an example we shall now sketch a proof that the naive reverse is equal as a map to the “fast” reverse. To do this we start by proving a lemma:

Let

q(y_{0}, y_{1}) = \{ \begin{matrix}nil & ↦ & (y_{0}, y_{1}) \\ cons(a, y′_{1}) & ↦ & (cons(a, y_{0}), y′_{1}) \end{matrix} \} (y_{1})

then clearly reverse′(z) = p_{0}(q^{length(z)}(nil, z)). Lemma 5.1

q^{length(z_{0})}(z_{1}, z_{2}) = (append(p_{0}(q^{length(z_{0})}(nil, z_{2})), z_{1}), tail^{length(z_{0})}(z_{2})).

Proof. We shall do a structural induction on z_{0}: Case 1: z_{0} = nil.

The equality is immediate. Case 2: z_{0} = cons(a, z′_{0}) and the result holds for z′_{0}.

q^{length(cons(a,z′_{0}))}(z_{1}, z_{2}) = q(q^{length(z′_{0})}(z_{1}, z_{2}))
= q(append(p_{0}(q^{length(z′_{0})}(nil, z_{2})), z_{1}), tail^{length(z′_{0})}(z_{2}))

To complete the proof we must pull the append through an application of q. To show that this may be done we resort to a case analysis on the form of tail^{length(z′_{0})}(z_{2}). Case 2.1: tail^{length(z′_{0})}(z_{2}) = nil.

then the effect of q is the identity and the result holds. Case 2.2: tail^{length(z′_{0})}(z_{2}) = cons(a′, z′_{2}).

Setting w = p_{0}(q^{length(z′_{0})}(nil, z_{2})) we have:

q(append(w, z_{1}), cons(a′, z′_{2})) = (cons(a′, append(w, z_{1})), z′_{2})
= (append(cons(a′, w), z_{1}), z′_{2})

Finally cons(a′, w) = p_{0}(q^{length(z_{0})}(nil, z_{2})).

□

So now we have: Proposition 5.2

reverse(z) = reverse′(z).

Proof. By structural induction on z: Case 1: z = nil.

Clear. Case 2: z = cons(a, z′) and the result holds for z′.

We have using the above lemma:

reverse(cons(a, z′)) = append(reverse(z′), cons(a, nil))
= append(reverse′(z′), cons(a, nil))
= append(p_{0}(q^{length(z′)}(nil, z′), cons(a, nil))
= p_{0}(q^{length(z′)}(cons(a, nil), z′))
= p_{0}(q^{length(cons(a,z′))}(nil, cons(a, z′)))
= reverse′(cons(a, z′)).

□

Arguments by structural induction are already very familiar: it is significant that they can be used in this setting. However, the real significance of this setting is that there are many other proof techniques available of the “theorems for free” kind[Wad89].

6 Evaluating Categorical Combinators

It was Tatsuya Hagino’s contribution to show that categories constructed from datatypes can be used directly as programming languages. The languages that result have some rather special properties: the principle one being that one cannot write non-terminating programs in them.

6.1 Eager evaluation in a category

In order to see how evaluation comes about in a category it is useful to trace the ideas through some simpler steps in order to arrive at the by-value machine currently used in charity.

Towards this end we explore a simple categorical rewriting system. It relies on the fact that any composition of primitive symbols of the category can always be associatively rearranged into a left– associated expression followed by a right–associated expression. The place where these expressions meet is denoted by a ⋆ and will indicate the position of the rewriting head

(..(((1; a_{1}); a_{2}); a_{3}); …; a_{i}) ⋆ (a_{i+1}; (…; (a_{n−2}; (a_{n−1}; (a_{n}; 1)))..).

Any computer scientist will instantly realize that the way to implement this is as two stacks. The rewriting head then starts on the left and traverses the composition once, to the right, by popping things off the right stack and pushing them onto the left stack. Whenever a situation is detected to be one in which a reduction can be performed the reduction is performed rather than the popping and pushing. This detection process will involve looking only at the top cells of each stack.

Consider the following rules:

\begin{matrix}a_{1}; f ⟹ a_{2} & a_{1}; g ⟹ a_{3} \\ a_{2}; f ⟹ a_{3} & a_{2}; g ⟹ a_{1} \\ a_{3}; f ⟹ a_{1} & a_{3}; g ⟹ a_{1} \end{matrix}

The following is a chain rewriting on the term:

a_{1}; f; g; g

as follows:

⋆a_{1}; f; g; g
⟹ a_{1} ⋆ f; g; g
⟹ a_{2} ⋆ g; g
⟹ a_{1} ⋆ g
⟹ a_{3}⋆

In fact, this is a good stab at what a full blown abstract machine for rewriting any functional language looks like. Traditionally the left stack is called the value stack and the right stack is called the code stack. Obviously this is still overly simple as sometimes we will meet a situation in which a major sub-reduction must be performed before one can continue with the rewriting of the main chain. To facilitate this, one just needs one more stack, traditionally called the dump, on which to push intermediate states of the calculation to which one must return. With this addition, a full blown categorical abstract machine is obtained.

6.2 Using a predistributive category

To illustrate how the abstract machine works consider the rewriting rules associated with a predistributive category.

\begin{aligned}z; ! & ⟹ & ! \\ ⟨x, y⟩; p_{0} & ⟹ & x \\ ⟨x, y⟩; p_{1} & ⟹ & y \\ ⟨z; b_{0}, x⟩; ⟨f | g⟩ & ⟹ & ⟨z, x⟩; f \\ ⟨z; b_{1}, x⟩; ⟨f | g⟩ & ⟹ & ⟨z, x⟩; g \\ z; ⟨x, y⟩ & ⟹ & ⟨z; x, z; y⟩ \end{aligned}

The transitions for the corresponding abstract machine are:

value  code  dump  value code dump
1 v  !.c  d  ⟶ !  c  d
2 ⟨v_{0}, v_{1}⟩  p_{0} .c  d  ⟶ v_{0}  c  d
3 ⟨v_{0}, v_{1}⟩  p_{1} .c  d  ⟶ v_{1}  c  d
4 ⟨v_{0}. b_{0}, v_{1}⟩ ⟨c_{0} | c_{1}⟩.c d  ⟶ ⟨v_{0}, v_{1}⟩ c_{0}  c(c).d
5 ⟨v_{0}. b_{1}, v_{1}⟩ ⟨c_{0} | c_{1}⟩.c d  ⟶ ⟨v_{0}, v_{1}⟩ c_{1}  c(c).d
6 v  ⟨c_{0}, c_{1}⟩.c d  ⟶ v  c_{0}  pr_{0}(v, c_{1}, c).d
7 v_{0}  [ ]  pr_{0}(v, c_{1}, c).d ⟶ v  c_{1}  pr_{1}(v_{0}, c).d
8 v_{1}  [ ]  pr_{1}(v_{0}, c).d  ⟶ ⟨v_{0}, v_{1}⟩ c  d
9 v  u.c  d  ⟶ v.u  c  d
10 v  [ ]  c(c)  ⟶ v  c  d
11 v  [ ]  [ ]  ⟶  STOP

Transitions 1 to 5 correspond closely to the rewriting rules.

Transitions 6 to 8 give us the distributive rule. Transition 6 says that when we encounter a pair, evaluate the first component of the pair and for the product, hold the second component on the dump for later evaluation. When the first component has been evaluated, we will reach transition 7, which stores away the result for the first component of the pair and evaluates the second component. Transition 8 puts the reduced pair on the value stack and resumes execution with the code following the pair.

Transitions 9 to 11 are generic. Transition 9 says that if there is no action associated with the value on the top of the code stack (ie. b_{0} and b_{1}), push it onto the value stack. Transition 10 says that if the code stack is empty and there is a continuation on the dump then execute the continuation. Transition 11 indicates that the rewriting is complete: the result is on the value stack.

6.3 Adding the initial datatypes

When we add initial datatypes there are some associated rewrite rules that must be added to the system. With each datatype (defined as in section 3.2) come constructors, a case, a fold and a map.

The new constructors are handled by transition 9.

The case combinator gives the simplest rewrite rule. Given a list of maps, we simply chose the map that positionally corresponds to the constructor on the value stack.

⟨v_{0}; c_{i}, v_{1}⟩; case^{L}{f_{1}, ..., f_{n}} ⟹ ⟨v_{0}, v_{1}⟩; f_{i}

The fold is more complex. From the diagram for the fold we obtain a rewrite rule going from the expression c_{i} × 1; fold^{L} to the more defined expression ⟨θ_{R}^{E_{i}}, p_{1}⟩; E_{i}(1, fold^{L}) × 1; g_{i}. The latter map can be written using the map combinator as ⟨map^{E_{i}}{p_{0}, fold^{L}{g_{1}, ..., g_{n}}}, p_{1}⟩; g_{i}. This gives us:

⟨v_{0}; c_{i}, v_{1}⟩; fold^{L}{g_{1}, ..., g_{n}} ⟹ ⟨v_{0}, v_{1}⟩; ⟨map^{E_{i}}{p_{0}, fold^{L}{g_{1}, ..., g_{n}}}, p_{1}⟩; g_{i}

From the defining diagram for map we get:

⟨v_{0}; c_{i}, v_{1}⟩; map^{L}{h_{1}, ..., h_{m}} ⟹ ⟨v_{0}, v_{1}⟩; map^{E_{i}}{h_{1}, ..., h_{m}, map^{L}{h_{1}, ..., h_{m}}}; c_{i}.

The corresponding transitions for the above rules are

value  code  dump  value code  dump
12 ⟨v_{0}.c_{i}, v_{1}⟩ case^{L}{f_{1}, ..., f_{n}}.c d  ⟶ ⟨v_{0}, v_{1}⟩ f_{i}  c(c).d
13 ⟨v_{0}.c_{i}, v_{1}⟩ fold^{L}{g_{1}, ..., g_{n}}.c d  ⟶ ⟨v_{0}, v_{1}⟩ ⟨map^{E_{i}}{p_{0}, fold^{L}{g_{1}, ..., g_{n}}}, c(c).d
p_{1}⟩.g_{i}
14 ⟨v_{0}.c_{i}, v_{1}⟩ map^{L}{h_{1}, ..., h_{m}}.c d ⟶ ⟨v_{0}, v_{1}⟩ map^{E_{i}}{h_{1}, ..., h_{m}, c(c).d
map^{L}{h_{1}, ..., h_{m}}}.c_{i}

For the factorizers, a table is needed which holds the name of the constructor c_{i}, its type, and its corresponding position in the definition of L. The case combinator uses the position to select the proper f_{i} from the list. The fold uses the position to select the proper g_{i} and then uses the type information to do the proper substitutions (ie. to use p_{0} or fold^{L}{g_{1}, ..., g_{n}}). For the map combinator, the type information is used to select the proper h_{j} or map^{L}{h_{1}, ..., h_{m}}.

6.4 Adding finite products

The rewrite rules for the finite products of which there are only three, are as follows:

⟨v_{0}, v_{1}⟩; map^{1} ⟹ v_{0}
⟨v_{0}, v_{1}⟩; map^{Id}{f} ⟹ ⟨v_{0}, v_{1}⟩; f
⟨⟨v_{0}, v_{1}⟩, v_{2}⟩; map^{×}{f, g} ⟹ ⟨⟨v_{0}, v_{2}⟩, ⟨v_{1}, v_{2}⟩⟩; f × g

These produce the following machine transitions:

value  code  dump  value code dump
15 ⟨v_{0}, v_{1}⟩  map^{1} .c  d  ⟶ v_{0}  c  d
16 v  map^{Id}{f}.c d  ⟶ v  f  c(c).d
17 ⟨⟨v_{0}, v_{1}⟩, v_{2}⟩ map^{×}{f, g}.c d  ⟶ ⟨v_{0}, v_{2}⟩ f  pr_{0}(⟨v_{1}, v_{2}⟩, g, c).d

6.5 Adding the final datatypes

For the final datatypes, rules must be added for the destructors. The unfold, record and map are inactive combinators and so are handled by transition 9. The destructor behaves differently depending on what type of data it is destructing.

unfold^{R}{f_{1}, ..., f_{n}}; d_{i} ⟹ ⟨f_{i}, p_{1}⟩; map^{F_{i}}{p_{0}, unfold^{R}{f_{1}, ..., f_{n}}}
record^{R}{g_{1}, ..., g_{n}}; d_{i} ⟹ g_{i}
map^{R}{h_{1}, ..., h_{m}}; d_{i} ⟹ d_{i} × 1; map^{F_{i}}{h_{1}, ..., h_{m}, map^{R}{h_{1}, ..., h_{m}}}

The corresponding transitions for the rules are:

value  code dump  value code  dump
18 v. unfold^{R}{f_{1}, ..., f_{n}} d_{i}.c d  ⟶ v  ⟨f_{i}, p_{1}⟩. map^{F_{i}}{p_{0},  c(c).d
unfold^{R}{f_{1}, ..., f_{n}}}
19 v. record^{R}{g_{1}, ..., g_{n}} d_{i}.c d  ⟶ v  g_{i}  c(c).d
20 v. map^{R}{h_{1}, ..., h_{m}} d_{i}.c d  ⟶ v  ⟨p0.d_{i}, p1⟩. map^{F_{i}}{h_{1}, ..., h_{m}, c(c).d
map^{R}{h_{1}, ..., h_{m}}}

7 Translating the term logic

The categorical combinators (despite what some category theorist seem to think) are totally unreadable! We really want to use the term logic as the programming language as this is much more friendly. However, to do so we need a translation process from the term logic into the combinators for evaluation. This raises all sorts of nasty issues like how one does an efficient translation. However, one of the essential points to note is that unlike the initial stabs at translating into Curry’s combinators (which turned out to be exponential and only after considerable work was brought down by Turner to polynomial[Tur79b, Tur79a] and later Statman to n log n), we enter the competition with an n log n translation. As this is the theoretical limit (don’t forget the constants where there is room for improvement) we can be reasonably happy.

We shall set up the term logic for a predistributive category with datatypes and then describe the translation to combinators. A proof of the translation is given in [CS92]. We assume that the datatype declarations are of the form given in section 3.2.

7.1 Variable bases

For each type in the category we shall suppose that we have a set of variables (in fact the type is inferred) {x, y, z, ...}.

A variable base is then defined by

• () is a variable base of type 1,

• If x is a variable then x is a variable base with type type(x),

• If v_{0} and v_{1} are variable bases with no variables in common then (v_{0}, v_{1}) is a variable base

where

type((v_{0}, v_{1})) = type(v_{0}) × type(v_{1}).

7.2 Terms

A term is defined by: • () is a term of type type(()) = 1,

• If t is a term where type(t) = X × Y then p_{0}(t) and p_{1}(t) are terms where type(p_{0}(t)) = X and type(p_{1}(t)) = Y,

• If t_{0} and t_{1} are terms then (t_{0}, t_{1}) is a term where type((t_{0}, t_{1})) = type(t_{0}) × type(t_{1}),

• If w is a variable base and t is a term where type(w) = type(t) then

{w ↦ t′}(t)

is a term of type type(t′), and the variables in w are bound in t′.

• If t is a term b_{0}(t) and b_{1}(t) are terms where type(b_{0}(t)) = type(t) + X and type(b_{1}(t)) = X + type(t) (where X is an indeterminate type).

• If t is a term where type(t) = A_{0} + A_{1} and v_{0} and v_{1} are variable bases where type(v_{i}) = A_{i}, and t_{0} and t_{1} are terms where type(t_{0}) = type(t_{1}) = B then

\{ \begin{matrix}b_{0}(v_{0}) & ↦ & t_{0} \\ b_{1}(v_{1}) & ↦ & t_{1} \end{matrix} \} (t)

is a term of type B. The variables in v_{0} and v_{1} are bound in t_{0} and t_{1} respectively.

• If t_{1}, ..., t_{n} are terms where type(t_{i}) = E_{i}(A, L(A)) then c_{1}(t_{1}), ..., c_{n}(t_{n}) are terms where type(c_{i}(t_{i})) = L(A).

• If t is a term where type(t) = L(A) and v_{1}, ..., v_{n} are variable bases where type(v_{i}) = E_{i}(A, L(A)) and t_{1}, ..., t_{n} are terms where type(t_{1}) = ... = type(t_{n}) = B then

{ c_{1}(v_{1}) ↦ t_{1} ; ⋮ ; c_{n}(v_{n}) ↦ t_{n} } (t)

is a term (the case expression) of type B. The variables in v_{1}, ..., v_{n} are bound in t_{1}, ..., t_{n} respectively.

• If t is a term where type(t) = L(A) and v_{1}, ..., v_{n} are variable bases where type(v_{i}) = E_{i}(A, X) and t_{1}, ..., t_{n} are terms where type(t_{1}) = ... = type(t_{n}) = X then

{ ; | c_{1} : v_{1} ↦ t_{1} ; ⋮ ; c_{n} : v_{n} ↦ t_{n} | ; } (t)

is a term (the fold) of type X. The variables in v_{1}, ..., v_{n} are bound in t_{1}, ..., t_{n} respectively.

• If t is a term where type(t) = L(A_{1}, ..., A_{m}) and v_{1}, ..., v_{m} are variable bases where type(v_{j}) = A_{j} and t_{1}, ..., t_{m} are terms where type(t_{j}) = B_{j} then

L { v_{1} ↦ t_{1} ; ⋮ ; v_{m} ↦ t_{m} } (t)

is a term (the map expression) of type L(B_{1}, ..., B_{m}). The variables in v_{1}, ..., v_{m} are bound in t_{1}, ..., t_{m} respectively.

• If t is a term where type(t) = S and v is a variable base where type(v) = S and t_{1}, ..., t_{n} are terms where type(t_{j}) = F_{j}(A, S) then

(|v ↦ d_{1} : t_{1} ; ⋮ ; d_{n} : t_{n} |) (t)

is a term (the unfold) of type R(A). The variables in v are bound in t_{1}, ..., t_{n} respectively.

• If t_{1}, ..., t_{n} are terms where type(t_{j}) = F_{j}(A, R(A)) then

( d_{1} : t_{1} ; ⋮ ; d_{n} : t_{n} )

is a term (the record) of type R(A).

7.3 Abstracted maps

A program is not a term but an abstracted map this is a pair

{v ↦ t}

where v is a variable base containing all the free variables of the term t.

The abstracted maps are what we must translate into combinators so that we can evaluate them.

7.4 Translation to categorical combinators

The translation T from the term logic is described as follows: • T [v ↦ ()] =!,

• T [x ↦ x] = 1,

• T [(v_{0}, v_{1}) ↦ x] = p_{i}; T [v_{i} ↦ x]where i = 0 if x occurs in v_{0} otherwise i = 1,

• T [v ↦ {w ↦ t′}(t)] = ⟨T [v ↦ t], 1⟩; T [(w, v) ↦ t′], • T [v ↦ p_{i}(t)] = T [v ↦ t]; p_{i} for i = 0, 1,

• T [v ↦ (t_{0}, t_{1})] = ⟨T [v ↦ t_{0}], T [v ↦ t_{1}]⟩,

• T [v ↦ b_{i}(t)] = T [v ↦ t]; b_{i} for i = 0, 1,

• T [v ↦ \{ \begin{matrix}b_{0}(v_{0}) & ↦ & t_{0} \\ b_{1}(v_{1}) & ↦ & t_{1} \end{matrix} \} (t)] = ⟨T [v ↦ t], 1⟩; case\{T [(v_{0}, v) ↦ t_{0}], T [(v_{1}, v) ↦ t_{1}]\},

• T [v ↦ c_{i}(t)] = T [v ↦ t]; c_{i},

• T [v ↦ { c_{1}(v_{1}) ↦ t_{1} ; ⋮ ; c_{n}(v_{n}) ↦ t_{n} } (t)] = ⟨T [v ↦ t], 1⟩; case^{L}{T [(v_{1}, v) ↦ t_{1}], ..., T [(v_{n}, v) ↦ t_{n}]},

• T [v ↦ { ; | c_{1} : v_{1} ↦ t_{1} ; ⋮ ; c_{n} : v_{n} ↦ t_{n} | ; } (t)] = ⟨T [v ↦ t], 1⟩; fold^{L}{T [(v_{1}, v) ↦ t_{1}], ..., T [(v_{n}, v) ↦ t_{n}]},

• T [v ↦ L { v_{1} ↦ t_{1} ; ⋮ ; v_{m} ↦ t_{m} } (t)] = ⟨T [v ↦ t], 1⟩; map^{L}{T [(v_{1}, v) ↦ t_{1}], ..., T [(v_{m}, v) ↦ t_{m}]}.

• T [v ↦ (|w ↦ d_{1} : t_{1} ; ⋮ ; d_{m} : t_{m} |) (t)] = ⟨T [v ↦ t], 1⟩; unfold^{L}{T [(v, w) ↦ t_{1}], ..., T [(v, w) ↦ t_{n}]}

• T [v ↦ ( d_{1} : t_{1} ; ⋮ ; d_{m} : t_{m} )] = record^{L}{T [v ↦ t_{1}], ..., T [v ↦ t_{n}]}

8 Acknowledgements

Robin Cockett would like to acknowledge the financial support of the ARC and intellectual support of the Sydney category seminar for which he was a research fellow from January 1990 to June 1991 working under Ross Street of Macquarie University. Many of the ideas underlying charity were developed while he was in Sydney.

Tom Fukushima would like to acknowledge the support of the Formal Methods Group at the University of Calgary and NSERC who allowed and funded his trip to Macquarie University, Sydney, Australia so that the first version of the charity programming system could be developed with Robin Cockett, and Macquarie University who provided monetary support and facilities.

References

[AVA74] J. D. Ullman A. V. Aho, J. E. Hopcroft. The design and analysis of computer algorithms. Addison-Wesley, 1974.

[Bur87] R. Burstall. Inductively defined functions in functional programming languages. Laboratory for foundations of computer science, University of Edinburgh, 1987.

[BW85] M. Barrs and C. Wells. Toposes, Triples and Theories. Springer-Verlag, New York Berlin Heidelberg Tokyo, 1985.

[CC] J. R. B. Cockett and H. G. Chen. Categorical combinators. Submitted to 3rd Banff Higher-order Workshop.

[Coc90] J. R. B. Cockett. List-arithmetic distributive categories; locoi. J. Pure Appl. Algebra, 66:1–29, 1990.

[Coc91a] J. R. B. Cockett. The fundamental theorem of data structures for a locos (draft manuscript). Macquarie Univ., May 1991.

[Coc91b] J. R. B. Cockett. Notes on strength, datatypes, and shape (draft manuscript). Macquarie Univ., May 1991.

[CS92] J. R. B. Cockett and D. Spencer. Strong categorical datatypes II. Submitted, 1992.

[EMP91] M. Fokkinga E. Meijer and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 124–144. Springer-Verlag, 1991.

[Hag87] T. Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987.

[Kel] G. M. Kelly. On clubs and data-type constructors. University of Sydney.

[Kel82] G. M. Kelly. Structures defined by finite limits in the enriched context i. Cahiers de Top. et Géom. Différentielle, 23:3–42, 1982.

[Lam69] J. Lambek. Deductive systems and categories II: Standard constructions and closed categories, volume 86 of Lecture notes in Mathematics, pages 76–122. Springer–Verlag, 1969.

[Mog89] E. Moggi. Computational lambda-calculus and monads. In Proc. IEEE Conf. on Logic in Computer Science, pages 14–23, 1989.

[Tur79a] D. A. Turner. Another algorithm for bracket abstraction. Journal of Symbolic Logic, 44(2):67–270, 1979.

[Tur79b] D. A. Turner. A new implementation technique for applicative languages. Software — Practice and Experience, 9:31–49, 1979.

[Wad89] Philip Wadler. Theorems for free! In The Fourth Internaltional Conferece on Functional Programming Languages and Computer Architecture, pages 347–359. Addison-Wesley, 1989.

[Wad90] P. Wadler. Comprehending monads. ACM Conference on Lisp and Functional Programming, June 1990.

[Wal91] R. F. C. Walters. Categories and computer science. Carslaw Publications, Sydney, 1991.

[Wra89] G. C. Wraith. A note on categorical datatypes. In Category theory and computer science, volume 389 of Lecture Notes in Computer Science, pages 118–127. Springer-Verlag, 1989.

A Charity programming system

The notation used in this document unfortunately does not translate directly into ascii. Therefore we summarize the differences between the mathematical notation above and the charityprogramming system’s notation. For a complete description of the charity programming system of which only a part of is described here, we refer the reader to the Charity User’s Manual. Spacing is not important in the following examples. All system commands must be followed by a “.” (period).

Both the charity programming system and the Charity User’s Manual are available via anonymous ftp from cpsc.ucalgary.ca in pub/charity.

A.1 Datatype definition

The differences in the datatype definition are that the “⟶” is replaced by “->”, and the “×” (product) is replaced by “*” (asterisk) for type expressions.

                             data L(A) -> C =

c_{1}: E_{1}(A,C) -> C
⋮
| c_{n}: E_{n}(A,C) ->C.

For example, the definition for btree would be

        data btree(A,B) -> C =
                leaf : A -> C
              | node : (C * (B * C)) -> C.

The definitions for natural numbers and booleans are predefined in the system as

        data nat -> C = Z : 1 -> C | S : nat -> C.
        data bool -> C = true : 1 -> C | false : 1 -> C.

where Z is zero and S is the successor.

A.2 Terms

To define the map

k{f_{1}, ..., f_{n}} : X ⟶ Y; v ↦ t

to the system, one would write:

def k{f_{1}, ..., f_{n}}(v) = t.

and the notational changes for terms are:

• “↦” (maps to) is written “=>” (equals, greater than).

• The case operation

{ c_{1}(v_{1}) ↦ t_{1} ; ⋮ ; c_{n}(v_{n}) ↦ t_{2} } (t)  is written  { c_{1}(v_{1}) => t_{1} ; ⋮ ; | c_{n}(v_{n}) => t_{n} ; } (t)

• The fold operation

{ ; | c_{1} : patt_{1} ↦ expr_{1} ; ⋮ ; c_{m} : patt_{m} ↦ expr_{m} | ; } (expr)  is written  {| c_{1} : patt_{1} => expr_{1} ; | c_{2} : patt_{2} => expr_{2} ; ⋮ ; | c_{m} : patt_{m} => expr_{m} ; |} (expr)

• The map operation

L { v_{1} ↦ t_{1} ; ⋮ ; v_{m} ↦ t_{m} } (t)  is written  L { v_{1} => t_{1} ; ⋮ ; , v_{m} => t_{m} ; } (t)

• Abstraction is written:

{v=>t′}(t)

• The unfold operation

(|patt ↦ d_{1} : expr_{1} ; ⋮ ; d_{m} : expr_{m} |) (expr)  is written  (| patt => ; d_{1} : expr_{1} ; |  d_{2} : expr_{2} ; ⋮ ; |  d_{m} : expr_{m} ; |) (expr)

• The record operation

( d_{1} : expr_{1} ; ⋮ ; d_{m} : expr_{m} )  is written  ( d_{1} : expr_{1} ; , d_{2} : expr_{2} ; ⋮ ; , d_{m} : expr_{m} ; )

For example, the definition for divide (section 4.4) would be:

     def divide{p} (l) =
          { nil       () => leaf(nil)
          | cons(a,tail) =>
                { (l1,(a,l2)) => node(leaf(l1),(a,leaf(l2))) }
                                     (split_list{p}(tail,a))
          } (l).

Note that the definition of divide uses the previously defined definition split list. Recursive calls are not allowed.

The command eval is used to evaluate closed terms. For example:

     eval divide{gt}([S(S(Z)),S(Z),S(S(S(Z))),Z]).

would apply divide to the list of numbers [2,1,3,0] with predicate greater than.

A.3 Combinator notation

Combinator notation is also available but has to be translated into ascii. The differences are: • case^{L} is written case L,

• fold^{L} is written fold L,

• map^{L}; L is written map L.

The command used to define a combinator expression to the system under name ident is:

cdef ident{f_{1}, ..., f_{n}} = expr.

where expr is a combinator expression which uses maps f_{1}, ..., f_{n}.

The command ceval is used to evaluate closed combinator expressions. For example:

        ceval < Z, Z ; S > ; p1.

extracts 1 from the pair (0,1).

A.4 Example

To give a flavor for programming in the charity programming system we give a short example session. In this example, we show how to define the natural numbers and some maps to use them.

We will use a shorthand for lists supplied by the system:

[x_{1}, x_{2}, ..., x_{n}] ≡ cons(x_{1}, cons(x_{2}, ... cons(x_{n}, nil)))

When charity is started, it will give a message signaling that it is ready. User commands can be entered at the “>” prompt and the “+” prompt signals that the command is being continued over several lines.

        Charity ready
        >

The first command required for this example is

        > restart_base.

which erases all predefined datatypes and combinators, and thus allowing us to redefine our own natural numbers below.

We define the natural numbers by the command

        > data mynat -> X =
        +          zero : 1 -> X
        +        | succ : X -> X.

which says that mynat is a type and has constructors zero and succ (successor). Thus values of type mynat may be created by applying zero to () (ie. something of type 1) or by applying succ to an expression of type mynat. For convenience the () may be omitted. For example:

                                zero = 0
                    succ(succ(zero)) = 2
                             succ(n) = n + 1

After the command has been entered, the system will display information about the combinators created (this information is mainly for programming at the combinator level as opposed to the termlogic level).

Next, we define addition using the fold operation:

> def myadd(x,y) =
+       {| zero: () => y
+        | succ: n => succ(n)
+        |}(x).

We can think of x as being a code sequence of a zero followed by succs. The fold operation says that zero is replaced by y and then each succ is replaced by succ. For example, if x =

succ(succ(zero)) and y = succ(zero) then

               x = zero ; succ ; succ

replacing the zero by y gives

                  ⟹ succ(zero) ; succ ; succ

then replacing each succ by succ gives

                  ⟹ succ(zero) ; succ ; succ
                  = succ(succ(succ(zero))) = 3

To add 2 to 1 in the system we type:

> eval myadd(succ(succ(zero)),succ(zero)).
typing : 'a -> mynat
succ(succ(succ(zero)))

the type of the expression as well as the result is displayed.

The case operation can be used for the predecessor map.

> def mypred(x) =
+       { zero () => 0
+       | succ(n) => n
+       }(x).
> eval mypred(succ(succ(zero))).
typing : 'a -> mynat
succ(zero)

This says that if x is zero then return zero otherwise x is the successor of a number n in which case we return n.

An example of the map operation is “map” which given L which is of type list, apply f to every element x in the list.

> def mymap{f} (L) = list{x => f(x)}(L).

Now to double every element in a list of natural numbers:

> def double(x) = myadd(x,x).
> eval mymap{double} ([zero, succ(zero), succ(succ(zero))]).
typing : 'a -> list(mynat)
[zero,succ(succ(zero)),succ(succ(succ(succ(zero))))]