2.1 Implementation Basis🔗ℹ

The implementation follows the one described in the first edition: unification and reification are those of Chapter 9 (“Under the Hood”), and the stream operators and goal constructors are those of the appendix “Connecting the Wires”. The second edition is a different language (see Second Edition and Comparing the Editions).

The differences from the first edition are:

• Stream representation. The book uses #f for the empty stream and the answer itself for exactly one answer. Here the empty stream is '() and a stream of exactly one answer is a one-element list, which supports arbitrary answer types. This preserves the book’s suspension points and search strategies. See Streamof for the two representations and the book’s restrictions on answers. Streams are accessed only through a small set of operations (stream-first, stream-rest, and so on; see Streams). The book’s case∞ is defined in terms of them, and its mzero, unit, and choice are written empty-stream, (stream a), and (stream-cons a e), where e is the rest itself rather than a thunk that produces it.

• Occurs check. The book’s ext-s never checks for circularity; a separate checked variant is introduced in Chapter 9. Here ext-s always performs the occurs check (skipping it when the value contains no variables), so == is the checked unification and there is no separate checked variant.

• Spelling. succeed and fail stand for the book’s #s and #u; λG and λF are typed versions of the book’s goal and thunk lambdas. Superscripts become suffixes: conde, condi, alli, ife, and so on.

• Omissions. The helper forms that the book introduces in passing to explain a point (such as the bounded lambda of Chapter 5 and project of Chapter 9) are not part of the library.

Throughout this section, “Chapter n” refers to the first edition.

2.2 Types🔗ℹ

(define-type (Streamof a)

(∪ Null (Pair a (∪ Null (Suspension a)))))

(define-type (Suspension a)

(→ (Streamof a)))

A stream is empty (Null), or an answer followed by its rest. The rest is either known to be empty, so that the stream is the one-element list (list a), or a suspension that produces the rest when called. The three cases are built by empty-stream, stream, and stream-cons. A suspension is a thunk that produces a stream when called.

The book uses a different representation: #f for the empty stream, the answer itself for exactly one answer, and an answer paired with a suspension for the remaining stream. Expressed in Typed Racket notation, this is:

(define-type (Streamof a)

(∪ False a (Pair a (Suspension a))))

The book requires that an answer be neither #f nor a pair whose cdr is a procedure, so that the three cases do not overlap. Substitutions satisfy this restriction.

The Streamof defined above has no such restriction: the three cases are told apart by null? on the stream and on its cdr, so Typed Racket can distinguish them for any answer type without inspecting the answers.

Read element by element, a stream is a list whose answers are all computed when they are reached and whose rest is delayed: the rest of a stream-cons is produced by a suspension, and only a (stream a) is known to end without calling one. The operations of Streams present it in exactly these terms.

2.3 Running Programs🔗ℹ

Unassociated variables in an answer are reified as the symbols '.0, '.1, and so on, in order of first appearance.

2.4 Goals🔗ℹ

all explores the answers of the first goal one at a time: for the first answer it exhausts the rest of the conjunction before moving to the second answer. alli (“all, interleaved”) alternates between the answers produced for different answers of the earlier goals, so a later answer of the first goal is reached even when an earlier one leads to infinitely many results. (all, Chapter 6; alli, Chapter 6.)

In the examples below, the first goal chooses 'L or 'R, and counto then relates n to a list of 'Is of any length. The first choice already has infinitely many answers, so all never reaches 'R; alli alternates between the two choices.

conde is depth-first: it produces all the answers of the first clause before any answer of the second, so a clause with infinitely many answers hides every clause after it. condi (“cond, interleaved”) alternates between the clauses. (conde, Chapter 1; condi, Chapter 6.)

In conda (“soft cut”), every answer of the chosen test is passed to the rest of its clause. In condu (“committed choice”), only the first answer of the test is kept. Neither form is relational in general: the result can depend on how much is already known about the variables. (Chapter 10.)

2.5 Substitutions and Unification🔗ℹ

These are the operations of Chapter 9.

2.6 Streams🔗ℹ

The operators of the appendix “Connecting the Wires” are written here with a few stream operations, which are the only code that knows how Streamof is represented: the book’s mzero, unit, and choice become empty-stream, (stream a), and (stream-cons a e), and its case∞ is defined with them. A reader who wonders what case∞ does with a stream can read it off its definition below. Everything is exported so that goals can be written and examined at the level of streams.