4 Comparing the Editions
Both editions describe the same relational language at its core: terms, substitutions, unification with the occurs check (in this package), and reification are essentially the same, and a program that uses only ==, fresh, conjunction, disjunction, and recursion denotes the same relation in both. The editions differ in the forms they offer and in how they search. In this section, code in the style of First Edition links to typed/miniKanren/trs1, and code in the style of Second Edition links to typed/miniKanren/trs2.
4.1 The Language
| first edition |
| second edition | |
run |
|
| ||
relations |
| define with a type annotation |
| |
disjunction |
|
| conde (interleaving) | |
conjunction |
|
| ||
last line |
| may be else |
| no else |
reified names |
| '.0 |
| '0 |
4.2 Streams
The first edition has three kinds of streams: empty, one answer, and an answer followed by a suspension.
(define-type (Streamof a) (∪ Null (Boxof a) (Pair a (→ (Streamof a)))))
The second edition also has three, but a suspension stands on its own:
(define-type (Streamof a) (∪ Null (Pair a (Streamof a)) (Suspension a)))
In the first edition, a computation can only give up control after it has produced an answer; in the second, it can give up control at any call to a relation defined with defrel. This has two consequences. The first is for types: in the first edition, “one answer” and “an answer and a suspension” cannot be told apart for an arbitrary answer type, so typed/miniKanren/trs1 needs a box; in the second edition, the three cases are told apart by the shape of the stream alone. The second consequence is for search, and is shown next.
4.3 Search
A branch that runs forever without producing an answer stops the first edition’s search, even under condi, because the interleaving operators only switch after an answer:
(: anyo (→ Goal Goal)) (define (anyo g) (conde [g] [else (anyo g)])) (define nevero (anyo fail)) (run 1 (q) (condi [nevero] [succeed])) ; does not terminate
In the second edition, every call to nevero suspends, and append-inf switches to the other branch at each suspension:
Interleaving search in the style of the second edition finds every answer of a pure program; the first edition’s conde and all are depth-first and do not. Where both editions interleave, they switch at different points (after each answer in the first, at each suspension in the second), so the order of answers, and hence the first n answers returned by run, are not guaranteed to agree.
4.4 Committed Choice
conda and condu are not relational, so their results can depend on details that the pure part of the language leaves open. One such detail differs between the editions. In the first edition, the last line of a form built with cond-aux (such as conde or condu) is always run as a plain conjunction, since it is normally an else line; so when the last line of a condu is not an else line, its test is not committed to one answer:
In the second edition, condu wraps every test in once: