Abstract:
Joy is a functional programming language which is not based on the
application of functions to arguments but on the composition of
functions. This paper describes the theoretical basis of the
language. The denotation of Joy programs maps a syntactic monoid of
program concatenation to a semantic monoid of function composition.
Instead of lambda abstraction Joy uses program quotation, and higher
order functions can be simulated by first order functions which
dequote quoted programs.
Keywords: functional programming, syntactic and semantic
monoids, function composition, quotation and dequotation of programs,
combinators, elimination of recursive definitions.
Joy programs are built from smaller programs by just two constructors:
concatenation and quotation.
Concatenation is a binary constructor, and since it is associative it
is best written in infix notation and hence no parentheses are
required. Since concatenation is the only binary constructor of its
kind, in Joy it is best written without an explicit symbol.
Quotation is a unary constructor which takes as its operand a program.
In Joy the quotation of a program is written by enclosing it in square
brackets. Ultimately all programs are built from atomic programs
which do not have any parts.
The semantics of Joy has to explain what the atomic programs mean, how
the meaning of a concatenated program depends on the meaning of its
parts, and what the meaning of a quoted program is. Moreover, it has
to explain under what conditions it is possible to replace a part by
an equivalent part while retaining the meaning of the whole program.
Joy programs denote functions which take one argument and yield one
value. The argument and the value are states consisting of
at least three components. The principal component is a
stack, and the other components are not needed here. Much of
the detail of the semantics of Joy depends on specific properties of
programs.
However, central to the semantics of Joy is the following:
The concatenation of two programs
denotes the composition of the functions denoted by the two programs.
Function composition is associative, and hence denotation maps the
associative syntactic operation of program concatenation onto the
associative semantic operation of function composition. The quotation
of a program denotes a function which takes any state as argument and
yields as value the same state except that the quotation is pushed
onto the stack.
One part of a concatenation may be replaced by another part denoting
the same function while retaining the denotation of the whole
concatenation.
One quoted program may be replaced by another denoting the same
function only in a context where the quoted program will be dequoted
by being executed. Such contexts are provided by the
combinators of Joy. These denote functions which behave like
higher order functions in other languages.
The above may be summarised as follows: Let P,
Q1, Q2 and R be programs, and
let C be a combinator. Then this principle holds:
IF Q1 == Q2
THEN P Q1 R == P Q2 R
AND [Q1] C == [Q2] C
The principle is the prime rule of inference for the algebra of
Joy which deals with the equivalence of Joy programs, and hence
with the identity of functions denoted by such programs. A few laws
in the algebra can be expressed without combinators, but most require
one or more combinators for their expression.
The remainder of this paper is organised as follows. The next
sections deal with program concatenation and function composition.
The first of these reviews certain algebras called monoids, and
homomorphisms between them. In the following section the meaning of
Joy programs is shown to be a homomorphism from a syntactic monoid to
a semantic monoid. The last of these sections explains the semantic
monoid in a little more detail, in particular function composition and
the identity function.
The other sections deal with quotations and combinators. The first
treats combinators that do not involve the stack, the second those
that do. The next section illustrates how these very basic
combinators can be used to emulate recursion without explicit
definitions. The summary section recapitulates the main conclusions
and hints at a connection with category theory.
The design of Joy was motivated by {Quine71} and {Backus78} who in
quite different fields examine how variables of one kind or another
can be eliminated and how their work can be done by combinators. In
turn their work is based on the pioneers Schönfinkel and Curry.
Backus has argued that concepts of programming languages should be
selected on the basis of yielding strong and clean mathematical laws.
In particular he favours concepts that allow simple algebraic
manipulations, where possible replacing variables by combinators or
higher order functions. With these goals in mind his research
culminated in the language FP. The language Joy offers a
very different solution to the same goals.
Paulson {Paulson92} remarked that “Programming and pure mathematics
are difficult to combine into one formal framework”. Joy attempts
this task.
Much of the elegance of Joy is due to the simple algebraic structure
of its syntax and the simple algebraic structure of its semantics and
to the fact that the two structures are so similar. In particular,
the two structures are monoids and the meaning function which
maps syntax into semantics is a homomorphism.
Monoids and homomorphisms are familiar from abstract algebra. A
monoid M consists of a nonempty set {m, m1, including a special element
m2 ...}m, and a
binary operation, written, say, as infix period ".". The
special element has to be a left and right unit element for
the binary operation, and the binary operation has to be
associative. In symbols, for all x,
y and z from the set,
m . x = x = x . m
(x . y) . z = x . (y . z)
For example, these are monoids: the integers with 0 as
the unit element and addition as the binary operation, or the integers
with 1 as the unit element and multiplication as the
binary operation. Two examples from logic are the truth values with
falsity as the unit element and disjunction as the binary operation,
or truth as the unit element and conjunction as the binary operation.
Two examples from set theory are sets with the nullset as the unit
element and set union as the binary operation, or the universal set as
the unit element and set intersection as the binary operation. It so
happens that in the preceding examples the binary operation is
commutative, but this is not essential for monoids. Two other
examples consists of lists with the empty list as the unit element and
concatenation as the binary operation, or strings of characters with
the empty string as the unit element and concatenation as the binary
operation. Concatenation is not commutative.
Because of the associative law, parentheses are not needed. Also, if
there are no other binary operations, the infix operator itself can be
omitted and the operation indicated by juxtaposition. Unit elements
are often called identity elements, but the word “identity” is already
needed with a different meaning in Joy. Unit elements are sometimes
called neutral elements, too.
Unit elements should be distinguished from zero elements,
which behave the way the number 0 interacts with
multiplication: a product containing a zero factor is equal to zero.
In logic falsity is the zero element for conjunction, and truth is the
zero element for disjunction. For sets the nullset is the zero
element for intersection, and the universal set is the zero element
for union. In commutative monoids there is always at most one zero
element.
Let M over {m m1 ..} and N over
{n n1 ..} be two monoids. A function h from
{m m1 ..} to {n n1 ..} is called a
homomorphism if and only if it maps unit elements onto unit
elements and commutes with the binary operation:
h(m) = n h(x . y) = h(x) . h(y)
In the second equation, the binary operation on the left is that of
M, and the one on the right is that of N.
One example is the logarithm function which is a homomorphism from the
multiplicative monoid onto the additive monoid. Another example of a
homomorphism is the size (or length) function on lists
which maps the list monoid onto the additive monoid: the size of the
empty list is zero, and the size of the concatenation of two lists is
the sum of the sizes of the two lists:
log(1) = 0 log(x * y) = log(x) + log(y)
size([]) = 0 size(x ++ y) = size(x) + size(y)
(In the last two equations, the symbols [] and
++ are used for the empty list and for concatenation.)
Other examples are the function which takes a list (or string) as
argument and returns the set of its elements. So this function
removes duplicates and forgets order. It maps the list monoid onto
the set monoid with the nullset as the unit and union as the binary
operation.
Homomorphisms can be defined over other algebras which are not
monoids. Examples are groups, rings, fields and Boolean algebras.
They are studied in universal algebra and in category theory. One
particular homomorphism can only be described as mind-blowing: this is
Gödel’s arithmetisation of syntax – all syntactic operations on
formulas of a theory are mapped onto corresponding arithmetic
operations on their Gödel numbers. (See for example
{Mendelson64}.)
In propositional logic the equivalence classes of formulas constitute
a Boolean algebra of many elements. A valuation is a homomorphism
from that algebra to the two element Boolean algebra of truth values.
One can go further: the meaning of a formula is the set of valuations
that make it true. The meaning function then is a homomorphism from
the Boolean algebra of equivalence classes to the Boolean algebra of
sets of valuations. This situation is typical in semantics: the
meaning function is a homomorphism. The same holds for Joy – the
meaning function is a homomorphism from Joy syntax to Joy semantics.
The syntax of Joy programs is very simple: the basic building
blocks are atomic programs, and larger programs are formed by
concatenation as one of the main modes of program construction.
Concatenation is associative, and hence no parentheses are required.
Also, concatenation is the only binary constructor, so no explicit
symbol is required, and hence concatenation can be expressed by
juxtaposition. It is useful to have a left and right unit element
id. Collectively these constitute the syntactic monoid.
Now to the semantics. In the introduction it was said that
Joy uses postfix notation for the evaluation of arithmetic
expressions. To add two numbers they are pushed onto a stack and then
replaced by their sum. This terminology is helpful but can be
misleading in several ways. The phrasing suggest a procedural or
imperative interpretation: Joy programs consist of commands such as
push this, push that, pop these and push their sum. But there is
nothing procedural about Joy, as described here it is a purely
functional language.
However, the terminology of commands does suggest something useful.
Commands, when executed, produce changes. Exactly what is changed
depends on the nature of the command. But in the most general terms
what changes is the state of a system. In particular the execution of
a postfix expression produces changes in the state of a stack. For
each change there is a before-state and an after-state. The
after-state of one change is the before-state of the next change.
So, changes are essentially functions that take states as arguments
and yield states as values. There is only one before-state, so they
are functions of one argument. Therefore they can be composed. The
composite of two functions can be applied to a state as argument and
yields as value the state that is obtained by first applying the one
function to the argument and then applying the other function to the
resulting value. This is essentially the semantics of Joy: All
programs denote functions from states to states.
The state does not have to be the state of a stack. It just so
happens that evaluation of postfix expressions is so conveniently done
on a stack. But evaluation of expressions is by no means everything.
In what follows, the stack is an essential part of the state, but for
many purposes it is useful to ignore the whole state altogether.
The operation of function composition is associative and
there is a left and right unit element, the identity
function. Collectively they comprise the semantic monoid. The
meaning function maps a syntactic monoid onto a semantic monoid. The
concatenation of two programs denotes the composition of the functions
denoted by the two programs, and the unit element of concatenation
denotes the unit element of composition.
If the programs P and Q denote
the same function, then the functions P and
Q are identical. Two functions are identical
if for all values in the intersection of their domains they yield the
same value. This will be written
P == Q
The symbol == will be used to denote the identity of Joy
functions. The symbol does not belong to the language Joy but to its
metalanguage. The identity relation between functions is
clearly reflexive, symmetric and
transitive. Furthermore, identicals are indiscernible in
larger contexts such as compositions. Hence substitution of
identicals can be used as a rule of inference:
IF Q1 == Q2
THEN P Q1 R == P Q2 R
The symbol id will be used to denote the identity
function. The fact that function composition is associative and
that the identity function is a left and right unit is expressed by
(P Q) R == P (Q R)
id P == P == P id
The notation can be used to express what look like
identities of numbers; for example
2 3 + == 5
expresses that the composition of the three functions on the
left is identical with the one function on the right. On
the left, the first two functions push the numbers 2 and 3
onto the stack, and the third replaces them by their sum. On the
right, the function pushes the number 5. The left and the
right are defined for all stacks as arguments and yield the same stack
as value. Hence the left and the right are identical.
But it is important to be quite clear what the equation says. Each of
the four symbols 2, 3, + and
5 denotes a function which takes a stack as argument and
yields a stack as value. The three numerals 2,
3 and 5 denote functions which are
defined for all argument stacks. They yield as values other stacks
which are like the argument stacks except that a new number,
2, 3 and 5 has been pushed on top.
The symbol + does not denote a
binary function of two numbers, but like all Joy functions it
takes one argument only. That argument has to be a stack whose top
two elements are numbers. The value returned is another stack which
has the top two numbers replaced by their sum. It follows that the
above equation does not express the identity of numbers
but the identity of functions.
The associativity of composition has as a consequence about
currying: that there is no difference between standard and
curried operators. Consider the example
(2 3) + == 2 (3 +)
On the left the + takes two parameters supplied by
(2 3). On the right + is given one
parameter, 3. The resulting function (3 +)
expects one parameter to which it will add 3. Because of
associativity the two sides are identical and hence no parentheses are
required.
Let P be a program which pushes m values onto the
stack. Let Q be a program which expects n values on
the stack, m <= n. Now consider their concatenation P. Of the n expected by
QQ, n will be supplied
by P. So the program P Q only expects n -
m values on the stack.
+++HERE+++ assoc and curry
In the development of mathematics an explicit notation for the number
0 has been a rather recent innovation. The symbol
enables one to say more than just that 0 is a unit
element for addition. Similarly, in the algebra of functions an
explicit symbol for the identity function makes it possible to state
many laws. This is particularly true for the functions in Joy. The
following are some examples:
In arithmetic 0 and 1 are unit elements for
addition and multiplication, so adding 0 or multiplying
by 1 have no effect. For lists the empty list is a unit
element, so concatenation on the left or the right has no effect.
Similarly in logic, falsity and truth are unit elements for
disjunction and conjunction, so disjoining with falsity and conjoining
with truth make no difference. Also in logic, disjunction and
conjunction are idempotent, so disjoining or conjoining with a
duplicate yields the original. For any stack it holds that
swapping the top two elements twice has no net effect, and
that duplicating the top element and then popping off the
duplicate has no net effect.
There are many more laws: double negation has no net effect, reversing
a sequence twice just leaves the original, and taking the successor
and the predeccessor of a number – in either order – produces no net
effect.
In the algebra of Joy these are expressed by the following:
0 + == id 1 * == id
[] concat == id [] swap concat == id
false or == id true and == id
dup and == id dup or == id
swap swap == id dup pop == id
not not == id reverse reverse == id
succ pred == id pred succ == id
Note that no variables were needed to express these laws.
The identity function is a left and right unit element with respect to
function composition. It is appropriate to remark here that there is
also a left zero element and there is a right zero
element. Two such elements l and r
satisfy the following for all programs P:
l P == l P r == r
Since function composition is not commutative, the two zero elements
are not identical. In Joy the left zero l is the
abort operator, it ignores any program following it. The
right zero r is the clearstack operator, it
empties the stack and hence ignores any calculations that might have
been done before. The two operators have some theoretical interest,
and they are occasionally useful.
Any program enclosed in square brackets is called a quoted
program or quotation. The length or size
of the quotation [5] is 1, and the size of
the quotation [2 3 +] is 3. However, as
noted earlier, the two programs inside the brackets denote the same
function. What this shows is that we cannot substitute their
quotations for each other:
[5] size =/= [2 3 +] size
What forbids the substitution is the quotation – by the square
brackets. So quotations produce opaque contexts, quotation is an
intensional constructor.
However, there are contexts where substitution is permissable across
quotations. These are contexts where the content of the quote is not
treated as a passive datum but as an active program. In Joy such
treatment is due to combinators which in effect dequote one
or more of their parameters.
The i combinator expects a quoted program on top of the
stack. It pops that program and executes it. So, if the quoted
program [P] has just been pushed onto the stack, then the
i combinator will execute P:
[P] i == P
For example, each of the following four programs compute the same
function – the one which takes any stack as argument and returns as
value another stack which is like the argument stack but has the
number 5 pushed on top.
2 3 + 5
[2 3 +] i [5] i
If the program P computes the identity function, then the
effect of applying the i combinator is that of the
identity function:
[id] i == id [] i == id
Another law is this:
i == [] cons i i
Two programs P and Q may look very different
– for example, they may differ in their sizes. But it could be that
the compute the same function. In that case the dequotations of their
quotations also compute the same function:
Hence
IF P == Q
THEN [P] i == [Q] i
Suppose now that a quoted program, [P], is on top of the
stack. It could then be executed with the i combinator.
But it could also be manipulated as a passive data structure first.
For example, one could push the quotation [i] and then
use the cons operator to insert [P] into
[i] to give [[P] i]. What happens if this
is executed by the i combinator? The internal
[P] quote is pushed, and then the internal i
combinator is executed. So the net effect is that of executing
P.
Hence
[i] cons i == i
Note that it has been possible to state this law without reference to
the quoted program [P]. But it may help to spell out a
consequence:
[P] [i] cons i == [[P] i] i == [P] i == P
The i combinator is only one of many. Another is the
b combinator which expects two quoted programs on top of
the stack. It pops them both and then executes the program that was
second on the stack and continues by executing the program that was on
top of the stack. So, in the special case where two programs
[P] and [Q] have just been pushed onto the
stack, the b combinator will execute them in the order in
which they have been pushed:
[P] [Q] b == P Q
It follows that the b combinator actually dequotes both
of its parameters, and hence either or both can be replaced by an
equivalent program:
IF P1 == P2 AND Q1 == Q2
THEN [P1] [Q1] b == [P2] [Q2] b
If both programs compute the identity function, then the effect of the
b combinator is the identity function. If either of the
two programs computes the identity function, then the effect is the
same as that of executing the other, which is the same as applying the
i combinator to the other:
[] [] b == id
[] b == i
[] swap b == i
The second equation could be reversed, and this shows that the
i combinator could be defined in terms of the
b combinator.
Quotations are sequences, and sequences can be concatenated. In Joy
strings, lists and, more generally, quotations can be concatenated
with the concat operator. If [P] and
[Q] have just been pushed, then they can be concatenated
to become [P Q]. The resultant concatenation can be
executed by the i combinator. The net effect is that of
executing the two programs, and that is also achieved by applying the
b combinator:
[P] [Q] concat i == P Q == [P] [Q] b
But the two quoted programs do not have to be pushed immediately
before the concatenation or the application of the b
combinator. Instead they could have been constructed from smaller
parts or extracted from some larger quotation. Hence the more general
law:
concat i == b
The equation could be reversed, hence the b combinator
could be defined in terms of the i
combinator. The names i and b
of the two combinators have been chosen because of their similarity to
the I combinator and B combinator in combinatory
logic. The standard text is {Curry58}, but good expositions are
to be found in many other books, for example {Burge75}.
The two previous combinators require one or two quoted programs as
parameters, but the parameters merely have to be in an agreed place,
they do not need to be on a stack. There are several combinators
which only make sense if the data are located on a stack.
Sometimes it is necessary to manipulate the stack not at the top but
just below the top. That is what the dip combinator is
for. It is behaves like the i combinator by executing
one quotation on top of the stack, except that it leaves the item just
below the quotation unchanged. In detail, it expects a program
[P] and below that another item X. It pops
both, saves X, executes P and then restores
X.
For example, in the following the saved and restored item is 4:
2 3 4 [+] dip == 5 4
If a program computes the identity function, then the effect of
applying the dip combinator is to compute the identity
function:
[id] dip == id [] dip == id
Suppose a program [P] is on top of the stack, and it is
first duplicated and then the copy executed with dip just
below the original [P]. Now the original has been
restored, but suppose it is now popped explicitly. The net effect was
the same as executing just the original [P] with the
i combinator:
i == dup dip pop
Suppose that there are two programs [P] and
[Q] on top of the stack, with [Q] on top.
It is required to execute [P] while saving
[Q] above. One way to do that is this: First push
[i]. Now [Q] is the second element.
Executing dip will save [Q] and execute
[i] on the stack which now has [P] on the
top. That amounts to executing [P], and after that
[Q] is restored.
Suppose further that it is now required to execute [Q],
and that is easily done with the i combinator. The net
effect of all this is the same as executing first [P] and
then [Q], which could have been done with the
b combinator. Hence
b == [i] dip i
The last two equations show that the dip combinator could
be used to define both the i combinator and
the b combinator. The reverse is not possible.
The last two equations also serve to illustrate algebraic manipulation
of Joy programs. In the last equation the i combinator
occurs twice, once quoted and once unquoted. Both occurrences can be
replaced in accordance with the previous equation, and this yields
b == [dup dip pop] dip dup dip pop
The substitution of the unquoted occurrence is unproblematic. But the
other substitution requires comment. Quoted occurrences can be
substituted only in a context of dequotation, and in this case such a
context is given by the dip combinator.
Again suppose that there are two quoted programs [P] and
[Q] on the stack. If the dip combinator is
executed next, it will cause the topmost quotation [Q] to
be executed while saving and later restoring [P] below.
Suppose that the i combinator is executed next, this will
cause the restored [P] to be executed. So the net effect
of the two combinators is to execute first P and then
Q. That same effect could have been achieved by first
swapping [P] and [Q] around, so that
[P] is on top, and then executing the b
combinator. This is expressed in the left law below. The right law
says the same thing, and it shows another way in which the
b combinator could have been defined.
dip i == swap b b == swap dip i
b == swap dip dup dip pop
Function composition is associative, and hence the following holds:
[P] [Q] b [R] i == [P] i [Q] [R] b
To eliminate the three quotations from this equation observe that they
can be written on the left of both sides provided that the
b combinator and the i combinator are
applied appropriately. For the left side this is easy:
[P] [Q] b [R] i == [P] [Q] [R] [b] dip i
For the right side it is a little harder since the i
combinator has to be applied to [P] which is obscured not
by one but two other quotations. The dip combinator has
to be used on itself in this case, as follows:
[P] i [Q] [R] b == [P] [Q] [R] [[i] dip] dip b
Combining the two right hand sides and cancelling the common three
quotations we obtain the following to expressing the associativity of
function composition:
[b] dip i == [[i] dip] dip b
In this law we can even replace the i combinator and the
b combinator in accordance with earlier definitions:
[swap dip dup dip pop] dip dup dip pop
== [[dup dip pop] dip] dip swap dip dup dip pop
It is possible to cancel the final pop on both sides, but
it is not possible to cancel the prefinal dip on both
sides. This unlikely law also expresses the associativity of function
composition. But the most elegant way of expressing the associativity
is by using a variant of the dip combinator, called
dipd, which might be defined by
dipd == [dip] cons dip
Then the associativity can be expressed by
[b] dip i == [i] dipd b
({Henson87} criticises presentations of FP-systems, originally due to
{Backus78} in that they give no law to this effect although they use
it in proofs.)
The combination of the dip combinator immediately
followed by the i combinator is sometimes useful for
arranging the top few elements on the stack in a form that is suitable
for executing a quoted program [P] that is at the top of
the stack.
This is how it is done: first another quoted program
[Q] is pushed, and executed using the dip
combinator. This will save and restore the [P], but
arrange the stack in accordance with [Q]. Then the
restored [P] is executed by the i
combinator. Depending on the [Q] that is chosen, the
three part combination of [Q], the dip
combinator and the i combinator will prepare the stack
for the execution of [P].
Since such a combination still requires the [P] on the
stack, any such combination has the effect of a combinator. The
following illustrate some simple choices of [Q] that are
sometimes useful. The names of these combinators have been chosen
because of their similarity to the K combinator, W
combinator and the C combinator in combinatory
logic.
k == [pop] dip i
w == [dup] dip i
c == [swap] dip i
Suppose that there is a quoted program [P] on top of the
stack. This could now be executed by some combinator, say
C. Alternatively, one could push the quotation
[C] and then use the cons operator to insert
the earlier [P] into the later quotation, and this
produces [[P] C]. This of course may be executed by the
i combinator. When that happens the inner
[P] is pushed, thus partly undoing the cons
operation. But then C will be executed. The net effect
is the same as the earlier alternative. So we have: For all operators
or combinators C
[C] cons i == C
It should be remarked that this theorem also holds for operators, say
O, instead of combinators C.
Again suppose that there is a quoted program [P] on top
of the stack. It could be executed by some combinator C,
or one could do this: push the quotation [i],
cons the earlier [P] into that and now
execute C. The cons operation produced
[[P] i] and when this is executed by C, the
inner [P] is pushed partly undoing the cons.
Then the i combinator actually executes this. The net
effect is that of just executing C. Hence for all
combinators C
[i] cons C == C
The two laws above may be combined: for all combinators C
[i] cons C == [C] cons i
So far we have only encountered one combinator which takes two quoted
parameters – the b combinator. But Joy has a large
number of combinators which take two, three or even four quoted
parameters. The following concerns combinators which expect at least
two quoted programs as parameters. For such combinators the first
three laws holds unchanged, but these variations also hold:
[i] cons cons C == C
[C] cons cons i == C
[i] cons cons C == [C] cons cons i
The principle generalises to combinators with at least three quoted
parameters, by allowing three cons operations to occur.
Finally, the second law generalises to all parameters of a combinator:
any one parameter [P] can be replaced by [[P]. The replacement can of course be constructed by
i]
consing [P] into [i]. That of
course may be done for all quotation parameters. If there is just the
one parameter [P], then consing it into
[i] to produce [[P] i] is easy enough, as in
the second law.
If there are two parameters [P] and [Q] it
already becomes tedious to change them to [[P] i] and
[[Q] i]. If there are three or more quotation
parameters, then the program to produce the three changes could be
rather obscure.
Joy has a combinator which can use a function to map the
elements of a list to a list of the same length containing the results
of applying the function. Several special forms take as a parameter
not an arbitrary list but a specified number of one, two, three and so
on elements from the stack. These are the app1 combinator,
the app2 combinator, the app3 combinator and so
on. These are just the right combinators to produce the changes
required for the parameters of a combinator. The following laws hold
for combinators C1, C2 and C3
requiring one, two or three quotation parameters:
[[i] cons] app1 C1 == C1
[[i] cons] app2 C2 == C2
[[i] cons] app3 C3 == C3
To illustrate for a combinator C3:
[P] [Q] [R] [[i] cons] app3 C3
== [[P] i] [[Q] i] [[R] i] C3
== [P] [Q] [R] C3
Computationally it is of course pointless to replace a quotation such
as [P] by [[P] i] if the quotations are
being used as parameters for a combinator. But the replacements are
invaluable in a Joy interpreter written in Joy. This interpreter is
essentially a complex combinator, appropriately called joy,
and it has to behave just like the i combinator. In the
definition of the joy combinator, the implementation of
all combinators uses the above mapping combinators but with
[[joy] cons] instead of [[i] cons].
One of the problems of large pieces of software concerns the
complexity of interdependent parts and the need to make interfaces
lean. To some extent this is a matter of information hiding, and
programming languages achieve this in various ways. Most have local
symbols such as formal parameters of functions and local program
variables of procedures. Many have full block structure allowing
declarations of functions and procedures to be nested and hence
invisible from the outside. Some have modules or other compilation
units which allow further information hiding in larger program
components. Joy approaches the problem in a different way — the
information that needs to be hidden is minimised in the first place.
Mostly the problem arises from declarations of named functions and
procedures and their named formal parameters.
There are several reasons why one might want to declare
a function, because
- it requires recursion, or
- it is needed in several seemingly unrelated places in a program, or
- it makes the program clearer.
The third reason is always valid. In Joy the second reason is much
less compelling, and the first has almost no force at all.
Joy has a large number of combinators which permit computation of
anonymous functions which are normally defined recursively. It also
has combinators that permit repeated calls of such functions in some
related patterns. Joy programs which use suitable combinators to
allow the computation of anonymous functions with anonymous formal
parameters.
Consider the following recursive definition and use of the
factorial function in a (fantasy) functional language:
LET factorial(n) = if n = 0 then 1 else n * factorial(n - 1)
IN factorial(5)
The call in the second line should return 120. Joy has a
number of ways of doing essentially the same computation without
introducing the name factorial and without
introducing the name of the formal parameter n.
Several of these ways are still modelled on the recursive definition
and have approximately the same length. Two of them are based on the
fact that the definition has the pattern of linear recursion,
indeed primitive recursion. As in all languages the use of
accumulating parameters can avoid the recursion altogether,
but that is not the point here.
The humble i and dip combinators were
certainly not designed for recursion, so it will come as a surprise
that they can be used to emulate recursion without naming the function
or its formal parameter. To make the recursion possible, every call
of the anonymous function must be able to access itself again, and
this is done by giving it its own body as a quoted parameter on the
top of the stack. This is achieved by always duplicating the quoted
body first and then using the i combinator to execute the
duplicate. The dip combinator can be used to access the
stack below the quoted body. The only other combinator needed is the
ifte combinator which achieves the same kind of two-way
branching as the if-then-else in the conventional
definition above.
This is the program:
1 5 2 [ [pop 0 =] 3 [pop pop 1] 4 [ [dup 1 -] dip 5 dip i 6 * ] 7 ifte ] 8 dup i
The line numbers are only included for reference. Execution begins in
line 1 by pushing the actual parameter 5 onto the stack.
Then the long quotation extending from line 2 to line 7 is pushed onto
the stack. This quotation is the body of the function, it corresponds
to the right hand side of the conventional definition. Execution
continues in line 8 where the long quotation is duplicated and the top
copy is executed by the i combinator. This execution has
the effect of pushing the two short quotations in lines 2 and 3 and
also the longer quotation in lines 4 to 6. So at this point the stack
contains the parameter 5 and above that four quotations.
But now the ifte combinator in line 7 executes. It pops
the last three quotations and saves them elsewhere. Then it executes
the if-part, the saved quotation from line 2. That will pop what is
now the top of the stack, the body of the function from lines 2 to 7.
This exposes the number which is the parameter, and it is compared
with 0.
The comparison will yield a truth value which the ifte
combinator will use to determine whether to execute the saved
then-part from line 3 or the saved else-part from lines 4 to 6. In
either case the stack is first restored to what it was before the
if-part was executed: the quoted body of the function is again on top
of the stack and below it is the actual parameter for this particular
call. If the most recent comparison by the if-part was true, then the
saved then-part from line 3 is executed.
This results in the body and the actual parameter being popped off the
stack and replaced by 1, the factorial of 0.
On the other hand, if the most recent comparison was false, then the
saved else-part from lines 4 to 6 is executed. For the later
multiplication the parameter has to be duplicated and the top
duplicate has to be decremented. Since the body of the function is in
the way, the duplicating and decrementing is done via the
dip combinator in line 4.
At this point the top three elements on the stack are the original
parameter for this call, then the decremented duplicate, and right on
top of that the quoted body of the function. It is now necessary to
compute the factorial of the decremented duplicate, and this call may
need access to the body again. So the body cannot be simply executed
by the i combinator, but first the body is duplicated in
line 5 and then the duplicate is executed by the i
combinator. Execution of that duplicate body will eventually
terminate, and then the top two elements will be the original
parameter and the factorial of what was its decremented duplicate.
The two numbers are now multiplied in line 6, yielding the required
factorial of the parameter for this call. This completes the
execution of the else-part from lines 4 to 6. Irrespective of whether
the then-part or the else-part was executed, the execution of the
ifte combinator is now complete.
This completes the execution of the body of the function in lines 2 to
7. It also completes the execution of whichever occurrence of the
i combinator in lines 5 or 8 triggered this execution of
the body. Ultimately the execution of the i combinator
in line 8 will have completed, and at this point the parameter
5 from line 1 will have been replaced by its factorial
120 as required.
Two short comments are in order: Firstly, the description of
the program was given in an imperative or procedural mode which is
psychologically helpful. But this does not change the fact that all
Joy programs and all their parts denote functions. Secondly, the
program can be written using only the dip combinator and
the ifte combinator by substituting dup dip for the two calls of the
popi combinator in lines
5 and 8.
Of course this program is a tour de force, it is ugly and
inefficient. With more suitable combinators much crisper and more
efficient programs can be written. In particular, the repeated
pushing and saving of the quoted if-part, then-part and else-part is
not necessary. Also, the repeated duplication of the quoted body is
not necessary, and consequently the three parts do not have to work
around the quoted body when it is in the way on the top. In fact, the
essence of the if-part and most of the else-part are built into the
primrec combinator for primitive recursion. The entire
program then is
5 [1] [*] primrec
As mentioned before, even the use of recursion can be eliminated in
favour of a more efficient loop combinator which uses an accumulating
parameter.
This paper has attempted to explain the theoretical foundations of the
language Joy. Much of the semantics is summarised by observing that
the following are true:
2 3 + == 7 2 -
dup + == 2 *
dip i == swap b
The first seems to express the identity of numbers. The
second seems to express the identity of functions which both
double a given number which they expect on the stack. The third
seems to express the identity of functionals, or second order
functions which take two first order functions as parameter and
compose them.
While these readings are sometimes helpful, the unity of Joy semantics
really forces a different interpretation. All three equations express
identity of Joy functions which take one argument stack and yield one
value stack.
The mathematical discipline of category theory deals with
functions of one arguments. All Joy functions are of that kind, too.
In fact all monoids are special cases of categories, so Joy’s
syntactic monoid of concatenation and Joy’s semantic monoid of
function composition are categories. So some fundamental connections
should be expected. In particular, Joy is related to Cartesian closed
categories, and to the “Combinatory Abstract Machine” CAM,
see for example {Poigne92}.
The paper
j00ovr
contains an overview of Joy and references to other
papers dealing with specific aspects of Joy.
