3 Second Edition

9.3

Racket

3 Second Edition🔗ℹ

This module implements the miniKanren language used in the second edition of The Reasoned Schemer (Friedman, Byrd, Kiselyov, and Hemann, MIT Press, 2018). The language is smaller than that of the first edition: conde is the only disjunction and it interleaves, relations are defined with defrel, and most of the implementation consists of ordinary functions whose types can be read directly.

3.1 Implementation Basis🔗ℹ

The implementation is a Typed Racket rewrite of the official code of the second edition, https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd, which is the code of Chapter 10 (“Under the Hood”) and the appendix “Connecting the Wires”.

The differences from that code are:

Types. Every definition has a type, and defrel supplies the types of the relations it defines (see defrel).
Variables. A variable is a struct compared with eq? and named after the identifier introduced by fresh, rather than a vector compared with eqv?.
Literals. Literals are compared with equal? rather than eqv?, so that two equal strings unify even when they are different objects.
Occurs check. ext-s skips the occurs check when the value is ground, which cannot create a cycle. This does not change the results; it lets the type of ext-s say that such an extension always succeeds.

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

3.2 Types🔗ℹ

type
Literal
type
Data
type
Term

Literal is the type of atomic values: booleans, numbers, characters, byte strings, strings, keywords, symbols, and '(). Data is the type of ground terms, built from literals and pairs. Term is the type of all terms: literals, variables, and pairs of terms.

type
Var
struct
(struct var (name)
    #:transparent)
  name : Symbol
procedure
(data? v) → Boolean
  v : Any

Logic variables, compared by identity, and the predicate for Data. (Chapter 10.)

type
Substitution

Defined as (Listof (Pair Var Term)), a triangular association list from variables to terms.

type constructor
(Streamof a)
type constructor
(Suspension a)

Defined as

(define-type (Streamof a)
(∪ Null (Pair a (Streamof a)) (Suspension a)))
(define-type (Suspension a)
(→ (Streamof a)))

A stream is empty, or an answer followed by a stream (a mature stream), or a suspension that produces a stream when it is called (an immature stream). (Chapter 10.)

The three cases are distinguished by null?, pair?, and procedure?, none of which inspects an answer, so no tagging is needed to tell them apart in Typed Racket. An immature stream need not be preceded by an answer: a computation can give up control before it has produced anything. This is what lets conde switch away from a branch that never produces an answer.

type
Goal

Defined as (→ Substitution (Streamof Substitution)).

Examples:

> ((== 1 1) empty-s)
- : (Streamof Substitution)
'(())
> ((== 1 2) empty-s)
- : (Streamof Substitution)
'()

3.3 Running Programs🔗ℹ

syntax
(run n q goal ...)
(run n (x ...+) goal ...)

n : (Option Natural)

Runs the conjunction of the goals and returns a list of at most n reified answers, or of all answers when n is #f. In the first form, q is bound to a fresh variable and each answer is its value. In the second form, each x is bound to a fresh variable and each answer is the list of their values. Unassociated variables are reified as '0, '1, and so on. (Chapter 1.)

Examples:

> (run* q (== q '(1 2)))
- : (Listof Term)
'((1 2))
> (run* (x y) (== x y))
- : (Listof Term)
'((_0 _0))
> (run 0 q succeed)
- : (Listof Term)
'()

syntax
(run* q goal ...)

Like run with n equal to #f. It also accepts the form (run* (x ...+) goal ...).

3.4 Goals and Relations🔗ℹ

value
succeed : Goal
value
fail : Goal

The book’s #s and #u. (Chapter 1.)

procedure
(== u v) → Goal
u : Term
v : Term

Unifies u and v, with the occurs check. (Chapter 1; implemented in Chapter 10.)

Examples:

> (run* q (fresh (x) (== q (cons x 2)) (== x 1)))
- : (Listof Term)
'((1 . 2))
> (run* q (== q (list q)))
- : (Listof Term)
'()

syntax
(fresh (x ...) goal ...)

Binds each x to a new variable, named after the identifier, and behaves as the conjunction of the goals. (Chapter 1.)

syntax
(defrel (name arg ...) goal ...)

arg = x
| [x : type]

Defines name as a relation: a function whose result is a Goal that suspends before running the conjunction of the goals. An argument written as a plain x has type Term; an argument written as [x : type] has the given type, which lets a relation take goals or other relations as arguments. For plain arguments, it expands to

(define (name [x : Term] ...) : Goal
  (λ (s)
    (λ ()
      ((conj goal ...) s))))

so the types of the relation are supplied by defrel itself. The inner (λ () ...) is the Suspension that makes the stream immature; this is the only place where the language suspends a computation, and therefore the only place where conde switches between branches. (Chapter 1; implemented in the appendix.)

Examples:

> (defrel (twiceo [g : Goal])
(conde [g] [g]))
> (run* q (twiceo (== q 'x)))
- : (Listof Term)
'(x x)

syntax
(conde [goal ...+] ...)

Interleaving disjunction of conjunctions. There is no else: every line has the same form. (Chapter 1.)

Examples:

> (defrel (repeato x l)
    (conde
      [(== l '())]
      [(fresh (d) (== l (cons x d)) (repeato x d))]))
> (run 6 q (conde [(repeato 'a q)] [(repeato 'b q)]))
- : (Listof Term)
'(() () (a) (b) (a a) (b b))

syntax
(conda [goal ...+] ...+)
syntax
(condu [goal ...+] ...+)

Committed choice: the first goal of each line is a test, and the first line whose test succeeds is the only one used. conda keeps every answer of the test; condu keeps only the first, by wrapping each test in once. (Chapter 9.)

Examples:

> (run* q (conda [(conde [(== q 1)] [(== q 2)])] [(== q 3)]))
- : (Listof Term)
'(1 2)
> (run* q (condu [(conde [(== q 1)] [(== q 2)])] [(== q 3)]))
- : (Listof Term)
'(1)

syntax
(project (x ...) goal ...)

Rebinds each x to its value under the current substitution (as by walk*) and runs the conjunction of the goals. (Chapter 10.)

Example:

> (run* q
    (fresh (n)
      (conde [(== n 3)] [(== n 4)])
      (project (n)
        (if (exact-integer? n) (== q (* n n)) fail))))
- : (Listof Term)
'(9 16)

syntax
(disj goal ...)
syntax
(conj goal ...)

N-ary disjunction and conjunction, built from disj2 and conj2; (disj) is fail and (conj) is succeed. (Appendix.)

procedure
(disj2 g1 g2) → Goal
  g1 : Goal
  g2 : Goal
procedure
(conj2 g1 g2) → Goal
  g1 : Goal
  g2 : Goal

Binary disjunction and conjunction: disj2 combines the streams of g1 and g2 with append-inf; conj2 runs g2 on every answer of g1 with append-map-inf, that is, it is composition in the Kleisli category of the stream monad. (Chapter 1; implemented in Chapter 10.)

procedure
(ifte g1 g2 g3) → Goal
  g1 : Goal
  g2 : Goal
  g3 : Goal
procedure
(once g) → Goal
  g : Goal

ifte runs g2 on every answer of g1 if g1 has an answer, and runs g3 otherwise; it is the function behind conda. once keeps only the first answer of g; it is what turns conda into condu. Both force suspensions only as far as needed to find out whether there is an answer. (Chapter 10.)

procedure
(call/fresh name f) → Goal
name : Symbol
f : (→ Var Goal)

Applies f to a new variable named name; the function behind fresh. (Chapter 10.)

procedure
(run-goal n g) → (Listof Substitution)
n : (Option Natural)
g : Goal

Runs g on empty-s and returns at most n of the resulting substitutions. (Chapter 10.)

3.5 Substitutions and Unification🔗ℹ

These are the operations of Chapter 10.

value
empty-s : Substitution

The empty substitution.

procedure
(ext-s x v s) → Substitution
  x : Var
  v : Data
  s : Substitution
(ext-s x v s) → (Option Substitution)
  x : Var
  v : Term
  s : Substitution

Extends s with the association of x to v, or returns #f if x occurs in v. Extending with a ground term always succeeds, and the type says so.

Examples:

> (define x (var 'x))
> (ext-s x '(1 2) empty-s)
- : Substitution
(list (list (var 'x) 1 2))
> (ext-s x (list 1 x) empty-s)
- : (U False Substitution)
#f

procedure
(walk v s) → Term
  v : Term
  s : Substitution
procedure
(walk* v s) → Term
  v : Term
  s : Substitution
procedure
(occurs? x v s) → Boolean
  x : Var
  v : Term
  s : Substitution
procedure
(unify u v s) → (Option Substitution)
  u : Term
  v : Term
  s : Substitution

walk follows the associations of a variable; walk* does so throughout a term; occurs? determines whether x occurs in the walked v; unify returns an extension of s that makes u and v equal, or #f.

Examples:

> (define x (var 'x))
> (define y (var 'y))
> (unify (cons x 2) (cons 1 y) empty-s)
- : (U False Substitution)
(list (cons (var 'y) 2) (cons (var 'x) 1))

procedure
(reify-name n) → Symbol
  n : Index
procedure
(reify-s v r) → Substitution
  v : Term
  r : Substitution
procedure
(reify v) → (→ Substitution Term)
  v : Term

Reification. reify is curried: (reify v) is the function that run maps over the substitutions it obtains.

Examples:

> (define x (var 'x))
> (define y (var 'y))
> ((reify (list x y x)) empty-s)
- : Term
'(_0 _1 _0)

3.6 Streams🔗ℹ

These are the stream operations of Chapter 10. They are polymorphic in the type of answers, and together they form the stream monad: a single answer (list a) is the unit, '() is zero, append-inf is the sum, and append-map-inf is the bind.

procedure
(append-inf s-inf t-inf) → (Streamof a)
s-inf : (Streamof a)
t-inf : (Streamof a)

Appends two streams. When s-inf is a suspension, the result is a suspension that, when called, continues with t-inf first and the rest of s-inf second: the swap is what makes the search interleave. (Chapter 10.)

Example:

> (take-inf #f (append-inf (λ () (list 1 2)) (list 3 4)))
- : (Listof Positive-Byte)
'(3 4 1 2)

procedure
(append-map-inf g s-inf) → (Streamof b)
g : (→ a (Streamof b))
s-inf : (Streamof a)

Applies g to every answer of s-inf and combines the results with append-inf. The type is the full monadic bind, with separate types for the answers before and after. (Chapter 10.)

procedure
(take-inf n s-inf) → (Listof a)
n : (Option Natural)
s-inf : (Streamof a)

Returns the first n answers of s-inf (all of them when n is #f), calling suspensions as needed. (Chapter 10.)

Example:

> (take-inf 3 (append-inf (list 'a) (λ () (list 'b 'c 'd))))
- : (Listof (U 'a 'b 'c 'd))
'(a b c)

1	micro Kanren
2	First Edition
3	Second Edition
4	Comparing the Editions

3.1	Implementation Basis
3.2	Types
3.3	Running Programs
3.4	Goals and Relations
3.5	Substitutions and Unification
3.6	Streams