# The Algebra of Joy

*by Manfred von Thun*

*Abstract:* Joy is a functional programming language which is not based
on the application of functions to arguments but on the composition of functions.
The language makes extensive use of combinators which perform the role of higher
order functions. The algebra of Joy programs can be used to express formal properties
of many first and second order functions without using variables ranging over values
or over functions. Some of these properties are idempotency, inverses, converses,
commutativity, symmetry, associativity, homomorphisms and distribution. The paper
also gives several analogues of concepts from category theory.

*Keywords:* functional programming, function composition, algebra of programs,
monoids, categories, functors, natural transformations, monads.

## Introduction

This paper describes a rich algebra of Joy programs which can be used for formal manipulation of Joy programs. Concatenation of Joy programs denote the composition of the functions which the concatenated parts denote. Hence if` Q1 `

and ```
Q2
```

are programs which denote the same function and ```
P
```

and ` R `

are other programs, then the two concatenations ` P Q1 R `

and ` P Q2 R `

also denote the same function. In other words, programs
` Q1 `

and ` Q2 `

can replace each other in concatenations.
This can serve as a rule of inference for *rewriting*.

As premises one needs axioms such as in the first three lines below, and definitions such as in the fourth line:

(+) 2 3 + == 5 (dup) 5 dup == 5 5 (*) 5 5 * == 25 (def square) square == dup *A derivation using the above axioms and the definition looks like this:

2 3 + square == 5 square (+) == 5 dup * (def square) == 5 5 * (dup) == 25 (*)The comments in the right margin explain how a line was obtained from the previous line. The derivation shows that the expressions in the first line and the last line denote the same function, or that the function in the first line is identical with the function in the last line.

Consider the following equations in infix notation: The first says that multiplying
a number `x`

by 2 gives the same result as adding it to itself. The
second says that the `size` of a
`reverse`d list is the same as the `size`

of the original list.

2 * x = x + x size(reverse(x)) = size(x)In Joy the same equations would be written,

*without variables*, like this:

2 * == dup + reverse size == size

Other equivalences express algebraic properties of various operations. For example,
the predecessor `pred` of the successor
`succ` of a number is just the number itself. The conjunction `and` of a truth value with itself gives just the truth value. The less than relation
`<`

is the converse of the greater than relation `>`

.
Inserting a number with
`cons` into a list of numbers and then taking the
`sum` of that gives the same result as first taking the sum of the list
and then adding the other number.

In conventional notation these are expressed by

pred(succ(x)) = x x and x = x x <y = y > x sum(cons(x,y)) = x + sum(y)In Joy these are expressed

*without variables*

succ pred == id dup and == id < == swap > cons sum == sum +Some properties of operations have to be expressed by combinators. One of these is the

`dip`combinator which expects a program on top of the stack and below that another value. It saves the value, executes the program on the remainder of the stack and then restores the saved value.

In the first example below, the `dip`

combinator is used to express
the associativity of addition. Another combinator is the
`app2` combinator which expects a program on top of the stack and below
that two values. It applies the program to the two values. In the second example
below it expresses one of the De Morgan laws. In the third example it expresses
that the `size`

of two lists `concat`enated is the sum of the
`size`

s of the two concatenands. The last example uses both combinators
to express that multiplication distributes (from the right) over addition. (Note
that the program parameter for `app2`

is first constructed from the
multiplicand and `*`

.)

[+] dip + == + + and not == [not] app2 or concat size == [size] app2 + [+] dip * == [*] cons app2 +

The remainder of this paper is organised as follows: The next five sections give detailed examples of algebraic laws which Joy operators satisfy. All of these laws are well known when expressed in familiar notation, what is new here is that they can be expressed in Joy notation without the use of implicitly or explicitly universally quantified variables. Then follow three sections using concepts from category theory, but no previous knowledge is assumed.

## Idempotency, inverses and unit elements

A unary function`f(x)`

is said to be *idempotent*if applying it once is "as good as" applying it twice. In conventional notation this means that for all

`x`

f(f(x)) = f(x)For example, the function

`abs`which returns the absolute value of a number is idempotent. Another one is the function defined on lists or strings which returns a sorted version - sorting an already sorted sequence makes no difference.

abs(abs(n)) = abs(n) sort(sort(s)) = sort(s)Composition can be used to express that stack operations are

*idempotent*. The following express the idempotency of

`abs`and

`sort`:

abs abs == abs sort sort == sortAnother idempotent Joy function, one which has no counterpart in conventional notation, is the

`newstack`function, it throws away anything that is on the stack. Doing it twice in succession gives the same result as doing it once:

newstack newstack == newstack

The remainder of this section illustrates the use of the *identity
function* in Joy algebra. This function is denoted by the symbol
`id`. It has the property that for all programs
`P`

,

id P == P == P id

Let `f(x)`

be a unary function. Another unary function
`g(x)`

is said to be its *inverse* if for all
`x`

g(f(x)) = xFor example, the predecessor function on integers is the inverse of the successor function on integers: for all integers

`x`

pred(succ(x)) = xIt may or may not be that if one function is the inverse of a second then the second is the inverse of the first. This is true of the predecessor and successor functions when defined on integers, but not when defined on natural numbers. The identity function can be used to express that one function is the inverse of another and that certain values are unit elements.

The atomic program `succ` denotes a function which takes a stack as argument
and yields a stack as value. The argument stack has to have an integer (or a character)
on top. The value stack is like the argument stack except that the integer (or
character) has been incremented by 1. The semantics for `pred` is analogous,
it decrements the integer (or character). The following express that the functions
denoted by the symbols `succ`

and
`pred`

are *inverse*s of each other:

pred succ == id succ pred == id

The `cons` function expects a list on top of the argument stack. Below
that it expects another value. The value that is returned is another stack which
is like the argument stack except that the two top elements of the argument stack
have been replaced by a new list which has the value inserted into it at the front.
The
`uncons` function undoes this. It expects a non-empty list and leaves
the first and the rest of the list. The two functions are inverses of each other:

cons uncons == id uncons cons == idIt is worth pointing out this cannot be expressed in conventional notation because there the

`uncons`

operation makes no sense. Actually, both functions
are polymorphic in that instead of lists they can operate on strings or on sets The
two equations still hold applied to strings. Only the right equation holds for sets.
The symbols `pairlist`, `pairstring` and
`pairset` denote functions which expect two potential members of lists,
strings or sets on top of the stack. They return a new stack with the two members
replaced by a single list, string or set. The polymorphic `unpair` function
is their inverse, but not vice versa. Since `unpair`

leaves two results,
the following have no counterpart in conventional notation.

pairlist unpair == id pairstring unpair == id pairset unpair == id

Some functions are inverses of themselves. Examples of
*self-inverse* functions are the Boolean negation function and the list
reversal function: for all Boolean values `b`

and for all lists `l`

not(not(b)) = b reverse(reverse(l)) = lIn Joy the two unary operators

`not`and

`reverse`are polymorphic. The

`not`

operator expects a truth value or a set on top of the stack
and returns a stack which has the complementary truth value or set on top of the
stack. The
`reverse`

operator expects a list or a string on top of the stack and
returns a stack which has the reversal the list or string on top of the stack. The
two functions are self-inverses, and this is expressed by
not not == id reverse reverse == id

Let `f(x,y)`

be a binary function. A constant
`c`

is called a left or right *unit element* if the first or
the second equation holds for all `x`

f(c,x) = x f(x,c) = xLeft and right unit elements often coincide, and then they are just called unit elements. In particular, this is true for the unit elements of commutative functions. For example, 0 is the unit element for addition, and 1 is the unit element for multiplication. In conventional infix notation:

n + 0 = n = 0 + n n * 1 = n = 1 * n

The identity function can also be used to express that certain literals are *right unit* elements for binary operations: 0 for addition, 1 for multiplication, the *empty string*`""`

or the *empty list*`[]`

for concatenation, the
truth value `false` and the *empty
set*`{}`

for logical disjunction and set union, and the truth value
`true` for logical conjunction.

0 + == id 1 * == id "" concat == id [] concat == id false or == id {} or == id true and == id

## Idempotency, zero elements and arities

This section illustrates the`dup`

and `pop`

operators in
Joy algebra. The Joy operator `dup`expects one value on top of the stack and pushes a duplicate on top. For example,

42 dup == 42 42Both sides of the equation denote compositions of two functions. On the left the first function pushes a number and the second makes a duplicate of the top element. On the right the two functions are the same, each pushes a number. The equation says that the function on the left is identical to the one on the right. Both functions are defined for all stacks, and both return a stack which is like the argument stack except that two copies of the number 42 have been pushed.

A binary function `f(x,y)`

is called *idempotent* if for all
`x`

f(x,x) = xTwo examples are the Boolean conjunction and disjunction operations: for all

`b`

b and b = b b or b = bIn Joy the

`dup`

operator can express idempotency of the Boolean
operations `and`and

`or`which are defined for truth values and for sets. It can also express the idempotency of the numeric binary

`min`and

`max`operators:

dup and == id dup or == id dup min == id dip max == id

The Joy operator `pop` expects one value on top of the stack and removes
it. For example

17 42 pop == 17On the left the composition of three functions first pushes two numbers and then pops the second. On the right the function just pushes the first number. The two functions are identical since for all argument stacks they have the same result stack.

Let `f(x,y)`

be a binary function. A constant
`c`

is called a left or right *zero element* of
`f(x,y)`

if the first or second equation holds for all
`x`

:

f(c,x) = c f(x,c) = cFor example, the number zero is a left and right zero element for multiplication, and in conventional infix notation the laws looks like this:

0 * n = 0 n * 0 = 0The

`pop`

operator can also be used to express that particular
values are zero elements for binary operations: 0 for multiplication, `false`

and the empty set `{}`

for logical conjunction and set intersection, and
`true`

for logical disjunction.
0 * == pop 0 false and == pop false {} and == pop {} true or == pop true

The two operators `dup`

and `pop`

are related by the identity

dup pop == idThe

`pop`

operator can also be used to express the
*arity*of a function, the number of parameters which it expects. For example, numbers are nullary, the successor function is unary, and addition is binary. There is no way to express this in conventional notation. In Joy it is expressed by:

42 pop == id succ pop == pop + pop == pop popSimilar laws express that some operators return two results on the stack:

uncons pop pop == pop dup pop pop == pop

## Converses, commutativity and symmetry

This section illustrates the use of the`swap`

operator in Joy algebra.
The Joy operator `swap`expects two values of any type on top of the stack; its effect is to interchange them. The operator is its own inverse:

swap swap == id

Let `f(x,y)`

be a binary function. Another binary function
`g(x,y)`

is its *converse* if for all `x`

and `y`

f(x,y) = g(y,x)For example, the numeric comparison relation

`<`

has as its
converse the relation `>`

:
(i <j) = (j > i)In Joy notation the

`swap`

operator can express that comparison
predicates `<`

and `<=`

have as their converses the predicates
`>`

and `>=`

by the laws
swap > == < swap >= == <=The operator

`swons`is similar to

`cons`

, it expects
an aggregate and a new value on top of the stack. It leaves a new aggregate with
the value inserted. But whereas `cons`

expects the aggregate on top and
the value below, `swons`

expects them in the opposite order, the value
on top and the aggregate below. It follows that `swons`

is the converse
of
`cons`

. In the same way, a binary string or list operation
`swoncat`is defined to be the converse of

`concat`

.
swap cons == swons swap concat == swoncat

One function is the converse of a second function if and only if the second is the
converse of the first. This says that converseness is a symmetric relation. In
Joy it is expressed by the following: for all programs `P`

and `Q`

swap P == Q if and only if swap Q == PFrom this rule and the previous equalities it follows that

swap < == > swap <= == >= swap swons == cons swap swoncat == concat

A binary function `f(x,y)`

is *commutative* if it is its own
converse - if for all `x`

and `y`

f(x,y) = f(y,x)For example, addition of numbers is commutative, for all integers

`x`

and `y`

i + j = j + iIn Joy the

`swap`

operator can express that a function is commutative.
swap + == + swap * == * swap and == and swap or == or swap max == max swap min == minTwo sorted sequences can be combined with the

`merge`operator to form one new sorted sequence. Unlike

`concat`enation, merging is commutative:

swap merge == merge

A function which yields a truth value is often called a
*predicate*. Commutative predicates are often called
*symmetric*. For example, the *identity relation*` = `

, a binary predicate, is commutative or symmetric. Another is the
`equal` predicate which tests lists for identity, including sublists and
their sublists. In conventional notation, for all integers or lists `x`

and `y`

(i = j) = (j = i) equal(x,y) = equal(y,x)Turning these concepts on themselves, the converse relation is symmetric: for all functions

`f`

and `g`

(g is the converse of f) = (f is the converse of g)The same is not true for the inverse relation. The

`swap`

operator
can express that a binary predicate is *symmetric*. The following express that

` = `

and `equal`

are symmetric:
swap = == = swap equal == equalWith

`swap`

one can express that elements are *left unit*elements for binary operations. In the case of operations such as addition and the Boolean operations this already follows from their commutativity. On the other hand, concatenation of strings or lists is not commutative, but the empty string and the empty list are both right and left unit elements for concatenation. They are also both right unit elements for

`merge`.

0 swap + == id 1 swap * == id false swap or == id {} swap or == id true swap and == id "" swap concat == id [] swap concat == id "" swap merge == id [] swap merge == id

Some operators leave two elements on top of the stack, and two such operator may
be related in the sense that they just leave the elements in a different order.
This can also be expressed by
`swap`

:

uncons swap == unswons unswons swap == unconsThere is even one operator which is related to itself in this way, and that is

`dup`

:
dup swap == dup

Two operators related to `swap`

are `rollup` and
`rolldown`. The `rollup`

operator moves the third and second
element on the stack into second and first position, and it moves the original
first element into third position. The
`rolldown`

operator moves the second and first element on the stack
into third and second position, and it moves the original third element into first
position. They can express laws such as

rolldown concat concat == concat swoncat rollup swoncat concat == swoncat swoncat rollup merge merge == merge mergeTheir arities are expressed by

swap pop pop == pop pop rollup pop pop pop == pop pop pop rolldown pop pop pop == pop pop pop

## Associativity

This section illustrates the use of the `dip`

combinator in Joy algebra.

The three previous sections have shown how a few Joy operations can express a variety
of well-known laws. In the sections to follow more difficult Joy concepts will
be needed. These resemble higher order functions, but like everything else in Joy
they really are just functions from stacks to stacks. They differ from what are
called the operators in that they expect on top of the stack not just a passive
datum, but a quoted program which they execute. In accordance with an older terminology
they are here called *combinator*s.

One of these is the `dip` combinator. It expects a quoted program on the
top of the stack, and below at least one value of any type. During execution it
removes the program and the value from the stack and saves them. Then it executes
the program on the remainder of the stack. Finally it restores the saved value
to the top of the stack. In most applications the program will be pushed just before
the combinator is to be applied. The combinator is useful for doing something to
the stack without disturbing the top value.

Here is an example:

1 2 3 4 + * 5 == 1 14 5 1 2 3 4 5 [+ *] dip == 1 14 5In the first line on the left the 3 and the 4 are immediately added, the result is multiplied by the 2 to give 14, and then the 5 is pushed on top. In the second line the 5 is pushed immediately after the 4, and consequently it is not possible to add the 3 and 4 without popping the 5 first. So, the program

`[+ *]`

is pushed and then executed by `dip`

. The results are the same as those
in the two (identical) right sides.
A binary function `f(x,y)`

is said to be
*associative* if the result of applying it twice to three values is independent
of the order of application:

f(x,f(y,z)) = f(f(x,y),z)For example, addition of numbers is associative:

i + (j + k) = (i + j) + kIf

`g(x,y)`

is the converse of an associative
`f(x,y)`

, then `g(x,y)`

is also associative.
In Joy the `dip`

combinator can be used to express associativity:

[+] dip + == + + [*] dip * == * * [and] dip and == and and [or] dip or == or or [max] dip max == max max [min] dip min == min min [concat] dip concat == concat concat [swoncat] dip swoncat == swoncat swoncat [merge] dip merge == merge merge

The following law expresses that the `dip`

combinator leaves one value
unchanged:

dip pop == [pop] dip i

## Homomorphisms, De Morgan and distribution

This section illustrates the use of the`app2`

combinator in Joy algebra.
The `app2` combinator expects a quoted program on top of the stack, and
below that two data parameters. As with all combinators, the program will be executed,
in this case twice. In case the program computes a unary function, the effect is
to replace the two data parameters by two corresponding values of that function.
The two evaluations could be done in parallel. The more general case where the
program does not denote a unary function is described further down.

Let `f(x1,x2)`

be a binary function defined on a type
`X`

, and let `g(y1,y2)`

be a binary function defined on a
type `Y`

. Let `h(x)`

be a function from `X`

to
`Y`

. Then `h(x)`

is a
*homomorphism* from `X`

and its binary function to
`Y`

and its binary function when the following holds for all `x1`

and `x2`

:

h(f(x1,x2) = g(h(x1),h(x2))One example is the logarithm function which maps logarithms of products onto sums of logarithms. Two other examples are the doubling function which maps integers with addition into even integers with addition, and the squaring function which maps naturals with multiplication into square naturals with multiplication and the

`size`(or length) of string function which maps the size of concatenations onto sums of sizes. The

*De Morgan*laws are another example.

log(x * y) = log(x) + log(y) double(x + y) = double(x) + double(y) square(x * y) = square(x) * square(y) size(concat(x,y)) = size(x) + size(y) not(p and q) = not p or not q not(p or q) = not p and not q

In Joy the `app2`

combinator can be used to express
*homomorphism* laws, and these all take the form:

f h == [h] app2 gSome such laws are

+ double == [double] app2 + * square == [square] app2 * max succ == [succ] app2 max concat size == [size] app2 + concat sum == [sum] app2 + concat product == [product] app2 * concat charset == [charset] app2 orIn the above,

`charset`transforms a string of characters into a set of characters, and the

`or`

operator computes set union in this case.
Another homomorphism is the `sort`operator which maps unordered lists under concatenation onto ordered lists under a binary

`merge`operator which preseves ordering:

concat sort == [sort] app2 merge

The `app2`

combinator can also be used to express the familiar De Morgan
laws for Boolean algebra and a (perhaps surprising) isomorphic pair of laws for
strings or lists:

and not == [not] app2 or or not == [not] app2 and concat reverse == [reverse] app2 swoncat swoncat reverse == [reverse] app2 concat

Laws like the above generalise to *distribution* laws. In these the unary
function is replaced by a new binary function, and for each element in the domain
a unary function can be defined from the new binary function by letting one parameter
be the given element. It is useful to distinguish *right distribution* and
*left
distribution*.

A binary function `f(x,y)`

distributes from the right over another binary
function `g(x,y)`

if the following holds:

f(g(x,y),z) = g(f(x,z),f(y,z))In arithmetic we have the familiar example of multiplication distributing from the right over addition. In Boolean algebra the conjunction and disjunction operators distribute from the right over

*each other*. Here is the arithmetic law:

(i + j) * k = (i * k) + (j * k)

The `app2`

combinator can also express *right
distribution* laws. In each case there are three data parameters on the stack,
and the two ways of applying two functions are equivalent. The one way is to apply
the one function to the second and third parameters (using the `dip`

combinator) and then to apply the distributing function to the result and the first
parameters. The other way is to use the first parameter and the distributing function
to make a *constructed program* that computes a unary function, use `app2`

to compute its values for the second and third data parameters and to combine the
two values with the other function.

[+] dip * == [*] cons app2 + [and] dip or == [or] cons app2 and [or] dip and == [and] cons app2 or

A binary function `f(x,y)`

distributes from the left over another binary
function `g(x,y)`

if the following holds:

f(x,g(y,z)) = g(f(x,z),f(y,z))In arithmetic multiplication also distributes from the left over addition:

i * (j + k) = i * j + i * kThe

`app2`

combinator can also be applied to a quoted program which
does not compute a unary function, but accesses data elements further down in the
stack. In the examples below, these elements have to be explicitly deleted later
on, by ```
[pop]
dip
```

. It can be used to express *left distribution*laws.

+ * == [*] app2 + [pop] dip or and == [and] app2 or [pop] dip and or == [or] app2 and [pop] dip

Apart from `app2`

there are similar combinators
`app1` and `app3`. Each expects a program
`[P]`

on top of the stack and below that 1, 2 or 3 further parameters
and produces 1, 2 or 3 values. Some pertinent laws are

[succ] app1 == succ [not] app1 == not [pop] dip app1 == app2 pop [swap] dip app2 == app2 swap [dup] dip app2 == app1 dupThe arities of these combinators are expressed by

app1 pop == pop pop app2 pop pop == pop pop pop app3 pop pop pop == pop pop pop pop

There is a sense in which one might say that an integer has two parts: a sign and an absolute value. When the two parts are multiplied, the result is the same as the original. In the same way, a non-empty list has two parts, its first and its rest. When the first is consed into the rest, the result is the same as the original list. In conventional notation this might be expressed as

sign(x) * abs(x) = x cons(first(x),rest(x)) = xThe same may be expressed in Joy notation using the

`dip`

combinator:
dup [sign] dip abs * == id dup [first] dip rest cons == id

The laws look somewhat cleaner when expressed in terms of another combinator. The
`cleave` combinator expects two programs and below that another item.
It applies both programs to produce two results, for example

5 [pred] [dup *] cleave == 4 25The earlier laws about parts and wholes can then be expressed like this:

[sign] [abs] cleave * == id [first] [rest] cleave cons == id

The combinator `split` applied to a list and a test predicate produces
two lists, those members of the original list which pass the test and those with
fail. For any predicate, a list will have two parts which can be merged to reconstitute
the original list. In Joy notation:

[sort] dip split merge == pop sortThe law cannot be expressed in conventional notation because

`split`

produces two results.
## The LIST functor and its natural transformations

This section uses several concepts from category theory. The following brief sketch is unavoidably superficial, for a proper exposition see {Rydeheard85}{Poigne92}. For excellent short introductions for computer science see {Tennent91} and {Walters91}. Another short introduction with an extensive bibliography is {Pierce91}.
A *category* consists of a collection of *object*s and for any two
objects a collection of *morphism*s, each having the one object as their
*source* and the other object as their
*target*. In many categories the objects are just sets, or they are sets
with structure - algebras. Then the morphisms are unary functions from sets to
sets, or they are homomorphisms from algebras to algebras. For any object the morphisms
must include an
*identity morphism* with that object as source and target. Often there will
be other morphisms with that object as source and target. For any object and two
morphisms having a given object as target and source respectively, there must be
a composite morphism having as source the source of the one component and as target
the target of the other.

This composition of morphisms must be associative, with identity morphisms as left
and right unit elements. These requirements are satisfied for categories of sets
and functions and for categories of algebras and homomorphisms. But there are many
categories that are quite different. One kind of example are *monoid*s:
an associative binary operation over a set which includes a left and right unit
element. Here the category consists of just one object (which is of no interest),
but many morphisms, the elements of the monoid. There are many other kinds of categories
which are different again.

Categories deal with two sorts of things, objects and morphisms. So they are two-sorted
algebras. Between categories there are morphisms called *functor*s. These
take objects and morphims of one category into objects and morphisms of another
category. In computer science the most familiar functors are the *type constructor*s.
They take integers, characters, truth values and so on into
`LIST`

s of integers, `LIST`

s of characters,
`SET`

s of integers and so on. The functors must *
also* take integer functions such as squaring into corresponding functions on
`LIST`

s or `SET`

s of integers.

In computing circles the corresponding functions are usually written
`map(square,L)`

, for a list `L`

. In category theory the same
symbol is used for objects and morphisms, so the examples are written `LIST(integer)`

and
`LIST(square)`

. In Joy there is no explicit type notation at all, and
`map` is just one of many combinators. Programs to compute the list of
squares of a given list can be written in either of these two ways:

[square] map [dup *] map

Between any two functors `F`

and `G`

there can be functions
called *natural transformation*s. These take as arguments the values of
`F`

and `G`

at their objects. A function `n`

is
natural if for all morhisms
`m`

in the domains of `F`

and `G`

the following
holds for all `x`

:

n(F(m)(x)) = G(m)(n(x))Initially we shall only be concerned with the case where

`F`

and `G`

are the same functor
`LIST`

. Then an example of a natural transformation from lists to lists
is the `reverse`function: for all functions

`f`

and lists `L`

reverse(LIST(f)(L) = LIST(f)(reverse(L))or in conventional notation

reverse(map(f,L)) = map(f,reverse(L))In Joy algebra the naturality of

`reverse`

is expressed by
[reverse] dip map == map reverse

In computer science natural transformations are often called
*polymorphic* functions, in the case of lists they are independent of the
type of the elements of the lists. Four other naturality laws, expressed in conventional
notation:

map(f,rest(L)) = rest(map(f,L)) f(first(L)) = first(map(f,L)) map(f,concat(L1,L2)) = concat(map(f,L1),map(f,L2)) map(f,cons(x,[])) = cons(f(x),[]) map(f,unitlist(x)) = unitlist(f(x))The last two laws of course say the same thing. In Joy these would be expressed by

[rest] dip map == map rest [first] dip i == map first [concat] dip map == [map] cons app2 concat [[] cons] dip map == i [] cons [unitlist] dip map == i unitlistNote that in the third equation on the right the

`app2`

combinator
has to use a *constructed program*. The last two laws again say the same thing.

Somewhat more difficult is the naturality of `cons`. In conventional notation
this is expressed by

map(f,cons(x,L)) = cons(f(x),map(f,L))and in Joy notation by

[cons] dip map == dup [dip] dip map consThis is so complex that a step-by-step verification is called for. Let

`L`

and `x`

be the list and the additional member. Let `[F]`

be
a program which computes the function
`f`

. Let `x'`

be the result of applying
`f`

to `x`

, and let `L'`

be the result of applying
`f`

to all members of `L`

. The proof of the equivalence of
the LHS and the RHS consists in showing that both reduce to the same program. For
the LHS we have:
x L [F] [cons] dip map LHS == x L cons [F] map (dip) == [x L] [F] map (cons) == [x' L'] (map)For the RHS:

x L [F] dup [dip] dip map cons RHS == x L [F] [F] [dip] dip map cons (dup) == x L [F] dip [F] map cons (dip) == x' L [F] map cons (dip) == x' L' cons (map) == [x' L'] (cons)The two sides reduce to the same program, so they denote the same function.

A similar equation is the following:

map == [uncons] dip dup [dip] dip map consBut note that this is not suitable as a definition, since the RHS only applies to non-empty lists. The following is a suitable recursive definition:

map == [ pop null ] [ pop ] [ [uncons] dip dup [dip] dip map cons ] ifte

The fact that `map`

does not change the number of elements in a list
is expressed in conventional notation by

size(map(f,L)) = size(L)and in Joy notation by

map size == pop size

An important combinator for any aggregate is `filter`, which expects an
aggregate and below that a quotation which implememnts a predicate. It returns
an aggregate of the same type as the parameter containing only those members for
which the predicate yielded
`true`

. Given two aggregates, it does not matter whether they are first
combined and then filtered, or first filtered separately and then combined. For
sequences the law is this:

[concat] dip filter == [filter] cons app2 concatFor sets the combining operator has to be

`or`

instead of
`concat`

.
Another law concerns passing an aggregate first through one filter and then passing
the result through another filter. Passing the aggregate through the conjunction
of these filters produces the same result. The `conjoin` operator takes
two quoted predicates and returns one quoted predicate which is their conjunction.

[filter] dip filter == conjoin filter

The following laws concern the `sum`

s and
`product`

s of lists of integers:

cons sum == sum + sum == uncons sum + cons product == product * product == uncons product *(Only the equations on the left could be expressed in conventional notation.)

This holds:

P == uncons Q iff cons P == Q

## Other functors and their natural transformations

As indicated in the previous section, apart from`LIST`

there are other
functors such as `SET`

. So there is the type `SET(integer)`

,
the function `SET(square)`

which maps a set of integers into the set of
their squares, and similarly for other integer functions. Much of what was said about
lists and their natural transformations has counterparts for sets and their natural
transformations. In Joy there are several implementations of *set type*s. The simplest is in terms of bitstrings with potential elements

`0`

..
`31`

, such sets are written in curly braces, as in `{1 3 5}`

.
Values of this type can be manipulated by the combinator
`map`

and the operators `first`

,
`rest`

and `cons`

. Instead of the operator
`concat`

the set union operator `or`applies. The naturality of these operators is expressed by

[rest] dip map == map rest [first] dip map == map first [or] dip map == [map] cons app2 or [{} cons] dip map == i {} cons [cons] dip map == dup [dip] dip map cons

Now we have two functors, `LIST`

and `SET`

. Lists have order
and may have repetitions, sets have neither. A useful function from lists to sets
is the function `elements` which removes order and repetitions. For example,
in Joy notation

[ 3 1 5 1 ] elements == { 1 3 5 }It makes no difference whether the set of elements of a list is taken first and then the set is mapped through a function, or whether the list is first mapped through the same function and then the set of elements is taken. This is the naturality of the

`elements`

function, expressed by
[elements] dip map == map elementsFor example:

[ 3 1 5 1 ] [dup *] [elements] dip map == [ 3 1 5 1 ] elements [dup *] map == { 1 3 5 } [dup *] map == { 1 9 25 }and

[ 3 1 5 1 ] [dup *] map elements == [ 9 1 25 1 ] elements == { 1 9 25 }

Halfway between lists and sets are multisets or *bag*s; these have no order
but may have repetitions. A `BAG`

functor would be similar to `LIST`

and `SET`

, and there would be natural transformations from bags to bags,
from lists to bags, and from bags to sets. Currently Joy does not have an implementation
of bags.

A list can have as its members other lists, for example lists of integers. Formally
these are of type
`LIST(LIST(integer))`

. This uses the `LIST`

functor composed
with itself: `LIST`

°
`LIST`

. Such a list can be mapped through a function by mapping each
sublist, for example

[[1 2 3][4 5]] [[dup *] map] map == [[1 4 9][16 25]]Here the second

`map`

is applied to the whole list, the first or
inner `map`

is applied to the sublists. Alternatively a combinator `mmap`can be defined by

mmap == [map] cons mapand then one can write

[[1 2 3][4 5]] [dup *] mmap == [[1 4 9][16 25]]

Whereas a list is one-dimensional, a *matrix* is two-dimensional. Matrices
can be implemented as lists of lists, and the sublists can be interpreted either
as the rows or the columns. One important operation on matrices is the interchange
of rows and columns. The `transpose` operator does just that:

[[1 2][3 4]] transpose == [[1 3][2 4]]Transposition is another polymorphic function or natural transformation for matrices. It does not matter whether a matric is first transposed and then mapped elementwise through a function, or whether it is first mapped and then transposed.

[transpose] dip mmap == mmap transpose

The operator `zip` will transform two lists of the same length into a
list of pairs, for example

[1 2 3] [4 5 6] zip == [[1 4][2 5][3 6]]The

`zip`

operator can be defined by
zip == [] cons cons transposeThe

`zip`

function is natural, `zip`

ping the two lists
and then `mmap`

ing has the same effect as
`map`

ping and then `zip`

ping:
[zip] dip mmap == [map] app2 zip

A similar naturality law holds for the `cartproduct` operator which produces
the *cartesian product* of two aggregates which do not have to be of the
same type:

[cartproduct] dip mmap == [map] app2 cartproduct

Another useful datatype is that of *tree*s, also called
*recursive list*s. A tree of integers is either an integer or a list of
trees of integer. A *proper tree* is a list of trees. The type gives rise
to a functor `TREE`

, with the data type `TREE(integer)`

and
mapping functions such as
`TREE(square)`

. In Joy the combinator for tree mapping is
`treemap`. Most of the operations on lists also apply to proper trees.
Reversal can be done by `reverse`

just at the top level, or by `treereverse` all the way down into all sublists. Some naturality laws are:

[reverse] dip treemap == treemap reverse [treereverse] dip treemap == treemap treereverse [rest] dip treemap == treemap rest [first] dip i == treemap first [[] cons] dip treemap == treemap [] cons

Proper trees can be `treeflatten`ed to form a one-level list. For example

[ [1 [2 3] [] 4] [5] ] treeflatten == [ 1 2 3 4 5 ]The

`treeflatten`

ing function is a natural transformation between
the `TREE`

and `LIST`

functors, the order of treeflattening
and mapping does not matter:
[treeflatten] dip map == treemap treeflattenThe following also holds:

treereverse treeflatten == treeflatten reverse

A *bare tree* is either the empty list `[]`

or it is a list of
bare trees. Formally there is a functor
`BARETREE`

, and for (degenerate) functions which can only take `[]`

as parameters `BARETREE(f)`

maps bare trees with contained `[]`

into trees. Proper trees can also be `strip`ped of their leaves to form
a bare tree:

[ [1 [2 3] [] 4] [5] ] strip == [ [ [] [] ] [] ]The

`strip`

function commutes with `reverse`

and
`treereverse`

:
reverse strip == strip reverse treereverse strip == strip treereverseOnce stripped, there is nothing for

`treemap`

to do:
[strip] dip treemap == treemap strip == pop strip

## The LIST monad

This section gives a superficial sketch of monads, another useful concept from category theory. For a fuller exposition see {Arbib-Manes75}, {Asperti-Longo91} and especially {Wadler92}.
A *monad*`M`

over a category consists of a functor from the
category to itself, and two natural transformations. The first transformation `joinM`

takes as argument an object in the target of the square of the functor and gives
as value an object in the target of the functor. The second transformation
`unitM`

takes as argument an object in the category and gives as value
an object in the target of the functor. The two transformations must satisfy two
laws which are expressed in terms of two variants obtained by applying the functor
to the two transformations:

From the first transformation one can define a variant by applying the functor to it. This variant is again a natural transformation, it takes as argument an object in the target of the cube of the functor and gives as value an object in the target of the square of the functor. The first transformation or its variant may be composed with the first transformation. The two compositions are again natural transformations, they take as argument an object in the cube of the functor and give as value an object in the target of the functor. The first defining law for monads is that these two compositions must be identical.

Similarly, from the second transformation one can define a variant by applying the functor to it. This variant is again a natural transformation, it takes as argument and value objects in the target of the functor. The second transformation or its variant may be composed with the first transformation. The two compositions take as argument an value objects in the target of the functor. The second defining law for monads is that these two compositions must both be equal to the identity function.

The above will now be illustrated with the *LIST monad*. Its functor is
the `LIST`

functor. Its first natural transformation is usually called
`flatten`, which concatenates a two-level list to produce a single-level
list. Its second natural transformation is the unary `unitlist` operation
which takes any argument to produce its singleton list. Here are two examples:

[[1 2 3] [peter paul]] flatten == [1 2 3 peter paul] [[1 2 3] [peter paul]] unitlist == [[[1 2 3] [peter paul]]]The two required variants are obtained by applying the

`LIST`

functor, as `map`

.
The variant of the `flatten`

operator is the polymorphic operator

[flatten] mapwhich takes a list of (lists of lists) as argument and concatenates the (list of lists) but leaves the outer level list structure intact. This is an example:

[[[1 2] [3]] [[a] [b]]] [flatten] map == [[1 2 3] [a b]]The first monad law can now be written in Joy notation. It says that there are two equivalent ways of flattening a list of lists of lists to produce a list:

[flatten] map flatten == flatten flatten

The variant of `unitlist`

is the polymorphic operator

[unitlist] mapwhich takes a list of elements and produces the list of their unitlists. An example is

[1 2 [3 4]] [unitlist] map == [[1] [2] [[3 4]]]The second monad law can now be written in Joy as

[unitlist] map flatten == id == unitlist flatten

As natural transformations both `flatten`

and
`unitlist`

interact with the `LIST`

functor operating (as
`map`

) on arbitrary functions. There are two further laws that arise.
Because these two laws are more general than the preceding ones, they are also
more useful:

A list of lists can be mapped at the second level through an arbitrary function using
the `mmap`

combinator, producing another list of lists. That can then
be `flatten`

ed to produce a single level list. The same original list
of list can first be
`flatten`

ed to produce a single level list which can then be mapped
at the top level using `map`

. The two results are the same, and in Joy
this is expressed as

mmap flatten == [flatten] dip map

A function may be applied to an argument of any type, and then the
`unitlist`

can be taken. Alternatively the
`unitlist`

can be taken first and then the result can be
`map`

ped through the function. That the results are the same can be
written in Joy as

i unitlist == [unitlist] dip map

{Wadler92} shows that in any monad it is possible
to define another natural transformation, *monadic composition* which simultaneously
resembles function application and function composition. For the `LIST`

monad it takes as one of its arguments a list and as the other argument a function
which yields a list as value. The result is again a list. In Joy it might be defined
by

bind == map flattenIt satisfies the following laws:

[unitlist] dip bind == i [unitlist] bind == id [K [H] bind] bind == [K] bind [H] bindThe first two laws say that

`unitlist`

is a left and right identity
for `bind`

, the third says that `bind`

is associative. The
third law is here expressed with program variables `K`

and `H`

.
Alternatively it is expressed by
[bind] cons concat bind == [bind] dip bindWadler makes extensive use of many

`bind`

-like functions for monads
other than the `LIST`

monad.
A very general theory of lists, without the use of category theory, is given in
{Bird86}. A very readable introduction to the
`LIST`

functor can be found in {Spivey89}.
The theory of lists is generalised by {Malcolm89} to what have been called rose trees. {Meijer-etal91} give a comprehensive collection of laws of functional programming using very
general functional forms for lists and other data types. {Bird-deMoor92} use categories, homomorphisms and algebraic techniques to solve sophisticated
optimisation problems in functional programming. It appears that most, and perhaps
even all, of the contributions in the above papers can be translated into Joy
notation.