1 microKanren

9.3

Racket

1 microKanren🔗ℹ

This module is microKanren (Hemann and Friedman, μKanren: A Minimal Functional Core for Relational Programming, Scheme Workshop 2013) with its streams replaced by amb. It follows typed/microKanren of the miniKanren-typed package, the Typed Racket rewrite of the code at https://github.com/jasonhemann/microKanren, definition by definition; the definitions that only exist to manipulate streams are gone.

1.1 From Streams to amb🔗ℹ

In microKanren, a goal returns a stream of states: every answer at once, lazily. The stream type is a monad, and the connectives are its operations. With amb, the nondeterminism is an effect of evaluation rather than a value, so it disappears from the type of goals: a goal returns a single state, chooses among its answers with amb, and fails by calling (amb).

	typed/microKanren	typed/microKanren/amb
Goal	(→ State (Streamof State))	(→ State State)
success	(unit s/c)	s/c
failure	mzero	(amb)
disj	(mplus (g1 s/c) (g2 s/c))	((amb g1 g2) s/c)
conj	(bind (g1 s/c) g2)	(g2 (g1 s/c))
Zzz	(λ (s/c) (λ () (g s/c)))	(λ (s/c) (suspend) (g s/c))
take	force and collect the stream (g empty-state)	collect (in-amb/do (g empty-state))

So success returns the state unchanged, conjunction is plain function composition, and disjunction is a choice made by amb. The monadic structure has not gone away: it now lives in the continuation captured by amb, and in-amb/do is what turns that control effect back into a sequence of answers.

The definitions that remain are those of typed/microKanren, with these changes:

unit, mzero, mplus, bind, pull, and the stream types are removed.
take and take-all take a thunk that performs the nondeterministic computation, instead of a stream, and call/goal returns a state.
Zzz calls suspend (see below).

1.1.1 Suspension and the Order of Answers🔗ℹ

In microKanren, Zzz wraps a goal so that it returns an immature stream, and mplus swaps its two streams whenever the first one is immature; this is what lets a disjunction leave a branch that never produces an answer. Here, Zzz calls suspend, which lets the computations already waiting in amb’s frontier run first:

Examples:

> (: relo (→ Term Goal))
> (define (relo x) (fresh (a d) (== x `(,a . ,d)) (relo x)))
> (run 1 (x) (disj+ (relo '(5 . 6)) (== x 3)))
- : (Listof Term)
'(3)

The two schedules produce the same answers but not always in the same order. mplus swaps a suspended stream only with the other side of the disjunction it belongs to, while suspend sends the computation to the back of a single, global frontier, which is closer to breadth-first search. All the tests of microKanren-test.scm give the same results as microKanren; of the examples of miniKanren-wrappers.scm, the two that use rember*o return their answers in a different order.

1.2 Types🔗ℹ

type
Literal
type
Term

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

type
Var
struct
(struct var (c)
    #:transparent)
  c : Natural
procedure
(var=? x1 x2) → Boolean
  x1 : Var
  x2 : Var

Logic variables. A variable is identified by its counter c, and var=? compares counters.

type
Substitution
type
State

Substitution is defined as (Listof (Pair Var Term)), a triangular association list. State is defined as (Pair Substitution Natural): a substitution and the counter of the next fresh variable.

type
Goal

Defined as (→ State State).

Examples:

> ((== 1 1) empty-state)
- : State
'(() . 0)
> ((call/fresh (λ (q) (== q 5))) empty-state)
- : State
(cons (list (cons (var 0) 5)) 1)
> (take-all (λ () ((call/fresh (λ (q) (disj (== q 5) (== q 6)))) empty-state)))
- : (Listof State)
(list (cons (list (cons (var 0) 5)) 1) (cons (list (cons (var 0) 6)) 1))

1.3 The Core🔗ℹ

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

Unifies u and v in the substitution of the state, and calls (amb) if they cannot be unified.

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

Applies f to a new variable, numbered by the counter of the state, and runs the resulting goal in a state whose counter is incremented.

procedure
(disj g1 g2) → Goal
  g1 : Goal
  g2 : Goal
procedure
(conj g1 g2) → Goal
  g1 : Goal
  g2 : Goal

Disjunction runs g1 or g2, as chosen by amb; conjunction runs g2 on the state returned by g1.

Example:

> (take-all
   (λ ()
     ((conj (call/fresh (λ (a) (== a 7)))
            (call/fresh (λ (b) (disj (== b 5) (== b 6)))))
      empty-state)))
- : (Listof State)
(list
(cons (list (cons (var 1) 5) (cons (var 0) 7)) 2)
(cons (list (cons (var 1) 6) (cons (var 0) 7)) 2))

procedure
(walk u s) → Term
  u : Term
  s : Substitution
procedure
(ext-s x v s) → Substitution
  x : Var
  v : Term
  s : Substitution
procedure
(unify u v s) → (Option Substitution)
  u : Term
  v : Term
  s : Substitution

Walking, extending a substitution, and unification. There is no occurs check.

1.4 User-Level Forms🔗ℹ

These are the forms of miniKanren-wrappers.scm.

procedure
(suspend) → Void

Sends the rest of the computation to the back of amb’s frontier: it makes a choice point with current-amb-depth-first? set to #f, and then a second one, which is placed behind the choices already waiting.

syntax
(Zzz goal)

The inverse-η-delay: a goal that calls suspend before running goal, so that a recursive relation gives the other choices a turn instead of looping.

syntax
(conj+ goal ...+)
syntax
(disj+ goal ...+)
syntax
(fresh (x ...) goal ...+)
syntax
(conde [goal ...+] ...+)

N-ary conjunction and disjunction of suspended goals, fresh variables, and disjunction of conjunctions.

Examples:

> (: appendo (→ Term Term Term Goal))
> (define (appendo l s out)
    (conde
      [(== '() l) (== s out)]
      [(fresh (a d res)
         (== `(,a . ,d) l)
         (== `(,a . ,res) out)
         (appendo d s res))]))
> (run* (x y) (appendo x y '(1 2 3)))
- : (Listof Term)
'(() (1) (1 2) (1 2 3))

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

n : Natural
syntax
(run* (x ...+) goal ...+)

Runs the goals with fresh variables x ... and returns at most n (or all) values of the first variable, reified.

value
empty-state : State
procedure
(call/goal g) → State
  g : Goal
procedure
(take n th) → (Listof a)
  n : Natural
  th : (→ a)
procedure
(take-all th) → (Listof a)
  th : (→ a)

Running goals: call/goal runs g in empty-state, and take and take-all collect at most n (or all) results of (th) with in-amb/do.

procedure
(reify-1st s/c) → Term
  s/c : State
procedure
(walk* v s) → Term
  v : Term
  s : Substitution
procedure
(reify-s v s) → Substitution
  v : Term
  s : Substitution
procedure
(reify-name n) → Symbol
  n : Natural

Reification of the value of the first variable, with the names '.0, '.1, and so on.

procedure
(fresh/nf n f) → Goal
n : Natural
f : (→ Var * Goal)

Applies f to n fresh variables.

1.1	From Streams to amb
1.2	Types
1.3	The Core
1.4	User-Level Forms