In part 1 we learned that recursion underlies proof by induction, letting
us guarantee the behaviour of functions algebraically. In part 2 we saw how
defining functions as recursive equations enables lazy evaluation, so that the
program only computes those things that are essential to generate its output. In
this final part, I’d like to talk about what programs *mean*, and to do that I’m
going to show you a tiny programming language that supports time travel.

I am going show you the whole implementation of this programming language in JavaScript, which I’m using so you know I’m not cheating. We know that, compared to Haskell, JavaScript can’t do algebraic analysis of your code or run it lazily, and it certain can’t run functions backwards, so I want you to know that everything this language can do is a result of the functions you’re about to see.

First, the language has two kinds of values: variables and pairs. A variable is
simply a value that has a name. It just lets us talk *about* variables as
first-class objects rather than merely using them.

```
class Variable {
constructor(name) {
this._name = name
}
inspect() {
return this._name
}
}
```

We’ll give every type an `inspect()`

method so that we can display the results
of programs in the terminal.

A pair is a value with a left field and a right field; it is the only compound data structure in this language. Though simple, pairs can be used to simulate many other structures, for example they’re commonly used to build linked lists.

```
class Pair {
constructor(left, right) {
this.left = left
this.right = right
}
inspect() {
let left = inspect(this.left),
right = inspect(this.right)
return `(${left} . ${right})`
}
}
```

Then we come to the machinery for running programs, the first of which is a
*state*. A state is a mapping from variables to values. States are
immutable; every method on states will return a new state rather than mutating
the receiver.

We construct a state from a list of the variables it contains, and a map that stores the values those variables are bound to.

```
class State {
constructor(vars = [], values = new Map()) {
this._vars = vars
this._values = values
}
inspect() {
let pairs = Array.from(this._values).map((pair) => {
return pair.map(inspect).join(' = ')
})
return `{ state ${inspect(this._vars)} ${pairs.join(', ')} }`
}
// ...
```

States can be changed in two ways. First, we can add variables to them;
`create_vars`

takes a list of names and turns them into a list of variables, and
returns those variables plus a new state containing the current variables plus
the new ones. Second, we can bind those variables to values; `assign`

takes a
variable and a value, it copies the current map of values, adds a new mapping to
it, and returns a new state containing that mapping.

```
create_vars(...names) {
let new_vars = names.map((name) => new Variable(name))
return [
new State([...this._vars, ...new_vars], this._values),
new_vars
]
}
assign(variable, value) {
let new_values = new Map(Array.from(this._values))
new_values.set(variable, value)
return new State(this._vars, new_values)
}
```

For example, if we make a new state and create a variable called `x`

, then
assign `x`

to `42`

, we get a state in which `x`

is bound to `42`

.

```
let [s, [x]] = new State().create_vars('x')
s.assign(x, 42)
// -> { state [x] x = 42 }
```

Next, `State`

has operations built on these methods. First, `walk`

essentially
looks up the value of a variable in a state, including resolving chains of
variables that refer to each other. If `x`

is bound to `y`

, and `y`

to `3`

, then
walking `x`

gives `3`

. However, if `x`

is not bound to anything, then walking
`x`

returns `x`

itself. Walking a pair returns a new pair by walking both sides.
The purpose of this method is to find out what a variable ultimately refers to,
or to find out it’s bound to nothing and can be given a value.

```
walk(term) {
if (this._values.has(term)) {
return this.walk(this._values.get(term))
} else if (term instanceof Pair) {
return new Pair(this.walk(term.left), this.walk(term.right))
} else {
return term
}
}
```

Then there is `unify`

. This method simply asserts that two things are equal, and
tries to return a state in which this is so. It walks the two inputs, and if
they are equal, it returns the current state. If one is a variable after
walking, which means it is not yet bound to anything, then we use `assign`

to
return a new state in which the value is bound to the other input. If both
values are pairs, then we unify each side of them. If no way to unify the values
can be found, we return `null`

.

```
unify(x, y) {
[x, y] = [this.walk(x), this.walk(y)]
if (x === y) return this
if (x instanceof Variable) return this.assign(x, y)
if (y instanceof Variable) return this.assign(y, x)
if (x instanceof Pair && y instanceof Pair) {
let state = this.unify(x.left, y.left)
return state && state.unify(x.right, y.right)
}
return null
}
```

For example, let’s make a state and two variables, `x`

and `y`

. If we unify `x`

and `3`

, then unify `y`

and `x`

, then we get a state in which `x`

and `y`

both
equal `3`

. If we unify a pair of `3`

and `x`

with a pair of `y`

and a pair of
`5`

and `y`

, then we get a state in which `y`

is `3`

(by the left-hand side),
and `x`

is a pair of `5`

and `3`

(by the right-hand side and the value of `y`

).

```
let [s, [x, y]] = new State().create_vars('x', 'y')
s.unify(x, 3).unify(y, x)
// -> { state [x, y], x = 3, y = 3 }
s.unify(new Pair(3, x),
new Pair(y, new Pair(5, y)))
// -> { state [x, y] y = 3, x = (5 . 3) }
```

The final elements of the language are four *goals*. A goal is a function that
takes a `State`

and returns a list of states; specifically it returns the set of
states in which some condition is true, subject to the contraints imposed by the
input state. There are four core functions for generating goals.

The first is called `equal`

. It takes two values and returns a function that
tries to unify the two values in the current state. If we get a state, we return
it in a list, otherwise we return an empty list. For example, if we make a
variable and create a goal where it’s equal to `1`

, when we call that goal with
a state we get a state in which `x`

is `1`

.

```
function equal(a, b) {
return (state) => {
state = state.unify(a, b)
return state ? [state] : []
}
}
// e.g.
let [s, [x]] = new State().create_vars('x'),
goal = equal(x, 1)
goal(s) // -> [ { state [x] x = 1 } ]
```

The second is called `bind`

. It will be convenient to package up process of
creating variables and turning them into a goal, into a single expression, and
that’s what `bind`

does. It takes a list of names, and a function that generates
a goal. It converts the names into variables, and passes them to the given
function to get a goal. Then it calls the goal with the new state. So, if we use
`bind`

to create two variables and return a goal where they are equal, then
calling that goal returns a state in which they are equal.

```
function bind(names, build_goal) {
return (state) => {
let [new_state, vars] = state.create_vars(...names)
let goal = build_goal(...vars)
return goal(new_state)
}
}
// e.g.
let goal = bind(['x', 'y'], (x, y) => equal(x, y))
goal(new State())
// -> [ { state [x, y] x = y } ]
```

`either`

combines two goals and creates a goal that satisfies either of them. It
simply concatenates all the states in which goal `a`

is satisfied with all the
states in which goal `b`

is satisfied. If we ask for a goal where either `x`

is
`2`

or `x`

is `3`

, then we get one state where `x`

is `2`

and one where `x`

is
`3`

.

```
function either(a, b) {
return (state) => {
return [...a(state), ...b(state)]
}
}
// e.g.
let goal = bind(['x'], (x) =>
either(equal(x, 2), equal(x, 3)))
goal(new State())
// -> [ { state [x] x = 2 }, { state [x] x = 3 } ]
```

Finally, `both`

gets all the states that satisfy goal `a`

, then calls goal `b`

in
each of those states and combines the results, so it generates the states in
which both goals `a`

and `b`

are satisfied.

```
function both(a, b) {
return (state) => {
return a(state).reduce((states, a_state) => {
return [...states, ...b(a_state)]
}, [])
}
}
// e.g.
let goal = bind(['x', 'y'], (x, y) =>
both(equal(x, 8), equal(y, 9)))
goal(new State())
// -> [ { state [x, y] x = 8, y = 9 } ]
```

All these goals can be composed. For example if we ask for a goal that both `x`

is either `red`

or `blue`

, and `y`

is `yellow`

, then we get one state in which
`x`

is `red`

and `y`

is `yellow`

and one in which `x`

is `blue`

and `y`

is
`yellow`

.

```
let goal = bind(['x', 'y'], (x, y) =>
both(
either(equal(x, 'red'), equal(x, 'blue')),
equal(y, 'yellow')))
goal(new State())
// -> [
// { state [x, y] x = 'red', y = 'yellow' },
// { state [x, y] x = 'blue', y = 'yellow' }
// ]
```

Now, let’s write something interesting with this language. We can convert
JavaScript arrays into recursive list we’ve seen from Haskell: a list is either
`null`

or a pair of a value and a list. We’ll create some functions for creating
such structures from arrays and strings, and some functions for converting from
lists back to arrays and strings.

```
const NULL = {}
function from_array(array) {
if (array.length === 0)
return NULL
else
return new Pair(array[0], from_array(array.slice(1)))
}
function to_array(pair) {
if (pair === NULL)
return []
else
return [pair.left].concat(to_array(pair.right))
}
function from_string(string) {
return from_array(string.split(''))
}
function to_string(pair) {
return to_array(pair).join('')
}
```

Here’s a list operation from Haskell: if we append an empty list with any other list, then the result is just the second list. Otherwise, we pair the first element of the first list with the result of appending the rest of the first list to the second.

```
append :: [a] -> [a] -> [a]
append [] y = y
append (x:xs) y = x : append xs y
-- e.g. append [1, 2, 3] [4, 5]
-- = 1 : append [2, 3] [4, 5]
-- = 1 : (2 : append [3] [4, 5])
-- = 1 : (2 : (3 : append [] [4, 5]))
-- = 1 : (2 : (3 : [4, 5]))
-- = [1, 2, 3, 4, 5]
```

To express the same thing in this language, we describe `append`

as a
relationship between three values, rather than a function that takes two
arguments and returns one. `append`

is defined as follows: either `x`

is empty
and `y`

equals `z`

, or `x`

and `z`

have the same first element, and appending
the rest of `x`

with `y`

gives the rest of `z`

; the repeated use of `head`

here
means everywhere that variable appears must have the same value. This contains
exactly the same information as the Haskell version, it’s just expressed
differently.

```
function append(x, y, z) {
return bind(['head', 'xs', 'zs'], (head, xs, zs) =>
either(
both(
equal(x, NULL),
equal(y, z)),
both(
both(
equal(x, new Pair(head, xs)),
equal(z, new Pair(head, zs))),
append(xs, y, zs))))
}
```

Let’s see what this function can do. First, we can say that both `x`

is equal to
`rec`

and `y`

is equal to `urse`

, and that appending `x`

and `y`

gives `z`

. As
we’re used to in conventional languages, the fact that `z`

is `recurse`

comes
out the other side. The `results`

function just grabs the first three variables
from the state and resolves their values.

```
let goal = bind(['x', 'y', 'z'], (x, y, z) =>
both(
both(
equal(x, from_string('rec')),
equal(y, from_string('urse'))),
append(x, y, z)))
goal(new State()).map(s => s.results(3).map(to_string))
// -> [ [ 'rec', 'urse', 'recurse' ] ]
```

Now, I said at the beginning that I was going to show you a language with time
travel. And, this `append`

function can be run *backwards*. We can remove the
assignment to `y`

and instead define `z`

, and it will figure out that `y`

has the
value `urse`

. It is as though time has been reversed, and we can supply the
return value of a function and get its arguments.

```
let goal = bind(['x', 'y', 'z'], (x, y, z) =>
both(
both(
equal(x, from_string('rec')),
equal(z, from_string('recurse'))),
append(x, y, z)))
goal(new State()).map(s => s.results(3).map(to_string))
// -> [ [ 'rec', 'urse', 'recurse' ] ]
```

We can use `either`

to define multiple possible values for `z`

, and `append`

will dutifully find the right `y`

value for each one.

```
let goal = bind(['x', 'y', 'z'], (x, y, z) =>
both(
both(
equal(x, from_string('rec')),
either(
equal(z, from_string('recurse')),
equal(z, from_string('reciprocal')))),
append(x, y, z)))
goal(new State()).map(s => s.results(3).map(to_string))
// -> [
// [ 'rec', 'urse', 'recurse' ],
// [ 'rec', 'iprocal', 'reciprocal' ]
// ]
```

Even more spooky: we can leave both `x`

and `y`

undefined and only define `z`

,
asserting merely that appending `x`

and `y`

gives `recurse`

. In this event, it
figures out all the possible values of `x`

and `y`

that can lead to the result.
Not only can we reverse time, we can walk back through every possible history
given the facts we have about the present.

```
let goal = bind(['x', 'y'], (x, y) =>
append(x, y, from_string('recurse')))
goal(new State()).map(s => s.results(2).map(to_string))
// -> [
// [ '', 'recurse' ],
// [ 'r', 'ecurse' ],
// [ 're', 'curse' ],
// [ 'rec', 'urse' ],
// [ 'recu', 'rse' ],
// [ 'recur', 'se' ],
// [ 'recurs', 'e' ],
// [ 'recurse', '' ]
// ]
```

But of course, time is not running backwards. What has really happened is that
we have banished time entirely from our program. Motion, just as Zeno said, is
inherently impossible. What we’ve done is describe `append`

in such a way that
the computer seems to understand what it *means*. But it doesn’t really, all
this language can do is follow assertions that structures are equal. It is the
expression of computations as structures, rather than as processes, that lets it
do these tricks.

The language we’ve just implemented is called μKanren. This particular implementation is derived from Tom Stuart’s excellent talk, Hello, declarative world. It is a member of the family of logic programming languages, which includes Prolog and Clojure’s core.logic. In part 1 we talked about proving things about programs by using equations between a function and its definition, and this sometimes required working “backwards”, replacing a definition with its name. Logic programs express relationships in a way that means the computer can carry this kind of proof process, and logic languages are excellent vehicles for doing formal proofs of program semantics.

Logic programming also plays an important role in type systems. Haskell’s type
system lets it pick a function implementation based on the requested return
type, rather than just on the argument types. For example, it has a `read`

function that tries to parse a string as the requested type:

```
> read "42" :: Int
42
> read "42" :: Bool
*** Exception: Prelude.read: no parse
> read "True" :: Bool
True
> read "True" :: Int
*** Exception: Prelude.read: no parse
> read "[1, 2, 3]" :: [Int]
[1,2,3]
```

Often the type can be inferred from context, for example the `!!`

operator takes
an `Int`

on the right, and so this figures out that `read`

needs to return an
`Int`

:

```
[4, 5, 6] !! (read "1")
```

In Generic returns in Rust we saw how Rust does a similar thing, selecting
a version of `collect()`

to use based on the returned collection type. This
mechanism of going “backwards” from outputs to inputs is a key feature of logic
programming, and it comes from expressing compution as recursive equations
between structures, rather than as procedural loops.

This style of programming is creeping in in surprising places, for example Yarn constraints are written in Prolog. Learning to use recursion effectively is essential in logic programming, and once you get the hang of it, it enables all sorts of other ways to think about and run programs.