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.
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 reversed 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 == sizeOther 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
app2unary2 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 concatenated is the sum of the
sizes 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
app2unary2 is first constructed from the
multiplicand and *.):
[+] dip + == + +
and not == [not] unary2 or (* app2 *)
concat size == [size] unary2 + (* app2 *)
[+] dip * == [*] cons unary2 + (* 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.
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 == newstackThe 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 idLet 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 inverses of each other:
pred succ == id succ pred == idThe 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 == idSome 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 == idLet 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 * nThe 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 == idThis 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 == idThe 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 trueThe 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 == popThis 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 == idLet 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 == swoncatOne 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 == concatA 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 concatenation, merging
is commutative:
swap merge == mergeA 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 == idSome operators leave two elements on top of the stack, and two such
operators 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 == dupTwo 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 popThis 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 combinators.
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 mergeThe following law expresses that the dip combinator
leaves one value unchanged:
dip pop == [pop] dip iThis section illustrates the use of the
app2unary2 combinator in Joy algebra.
The app2unary2 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 qIn Joy the app2unary2 combinator can be used
to express homomorphism laws, and these all take the form:
f h == [h] unary2 g (* app2 *)Some such laws are:
+ double == [double] unary2 +
* square == [square] unary2 *
max succ == [succ] unary2 max
concat size == [size] unary2 +
concat sum == [sum] unary2 +
concat product == [product] unary2 *
concat charset == [charset] unary2 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] unary2 merge (* app2 *)The app2unary2 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] unary2 or (* app2 *)
or not == [not] unary2 and (* app2 *)
concat reverse == [reverse] unary2 swoncat (* app2 *)
swoncat reverse == [reverse] unary2 concat (* app2 *)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 app2unary2 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 app2unary2 to compute its values
for the second and third data parameters and to combine the two values
with the other function:
[+] dip * == [*] cons unary2 + (* app2 *)
[and] dip or == [or] cons unary2 and (* app2 *)
[or] dip and == [and] cons unary2 or (* app2 *)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 app2unary2 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:
+ * == [*] unary2 + [pop] dip (* app2 *)
or and == [and] unary2 or [pop] dip (* app2 *)
and or == [or] unary2 and [pop] dip (* app2 *)Apart from app2unary2 there are similar
combinators app1i and
app3unary3. 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] i == succ [not] i == not
[pop] dip i == unary2 pop
[swap] dip unary2 == unary2 swap
[dup] dip unary2 == i dupThe arities of these combinators are expressed by:
i pop == pop pop
unary2 pop pop == pop pop pop
unary3 pop pop pop == pop pop pop popThere 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 == idThe 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 == idThe 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 which 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.
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 objects and for any two objects a collection of morphisms, 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 monoids: 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 functors. These take objects and morphisms of one
category into objects and morphisms of another category. In computer
science the most familiar functors are the type constructors.
They take integers, characters, truth values and so on into
LISTs of integers, LISTs of characters,
SETs of integers and so on. The functors must also
take integer functions such as squaring into corresponding functions on
LISTs or SETs 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 *] mapBetween any two functors F and G there can
be functions called natural transformations. 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 reverseIn 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 unary2 concat (* app2 *)
[[] cons] dip map == i [] cons
[unitlist] dip map == i unitlistNote that in the third equation on the right the
app2unary2 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 ]
ifteThe 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 sizeAn important combinator for any aggregate is filter,
which expects an aggregate und below that a quotation which implements 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 unary2 concat (* app2 *)For 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 filterThe following laws concern the sums and
products 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 == QAs 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
types. 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 unary2 or (* app2 *)
[{} cons] dip map == i {} cons
[cons] dip map == dup [dip] dip map consNow 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 bags; 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 matrix is first transposed and then mapped elementwise through a function, or whether it is first mapped and then transposed:
[transpose] dip mmap == mmap transposeThe 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, zipping the
two lists and then mmaping has the same effect as
mapping and then zipping:
[zip] dip mmap == [map] unary2 zip (* app2 *)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] unary2 cartproduct (* app2 *)Another useful datatype is that of trees, also called
recursive lists. 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 [] consProper trees can be treeflattened to form a one-level
list. For example:
[ [1 [2 3] [] 4] [5] ] treeflatten == [ 1 2 3 4 5 ]The treeflattening 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 reverseA 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 stripped 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 stripThis 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 a value object 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 a value object 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 flattenThe 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 flattenAs 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 flattened to
produce a single level list. The same original list of lists can first
be flattened 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 mapA 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
mapped 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.