1 microKanren

9.3.900

Racket

1 microKanren🔗ℹ

This module is a Typed Racket rewrite of microKanren (Hemann and Friedman, μKanren: A Minimal Functional Core for Relational Programming, Scheme Workshop 2013), from the code at https://github.com/jasonhemann/microKanren: the core of microKanren.scm and the user-level forms of miniKanren-wrappers.scm. The core is a handful of functions over states and streams; everything else is defined on top of them.

The differences from that code are:

Types. Every definition has a type.
Variables. A variable is a struct holding its counter, (var 0), rather than the vector #(0), so that variables are distinguished from the other values of a term.
Literals. Literals are compared with equal? rather than eqv?, as in the other modules of this package.
Stream operations. The representation of streams is the paper’s, but mplus, bind, and Zzz reach it only through a few operations (stream-first, stream-rest, stream-cons, and so on), which read a suspension as an element pause. The same operations are used by typed/miniKanren/trs2. The paper’s mzero and unit are empty-stream and stream, and its pull, take, and take-all are stream-force, stream-force-take, and stream->list, named after racket/stream.

1.1 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 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 (mature), or a suspension that produces a stream when called (immature). Read element by element, a suspension is a pause followed by the stream it produces, so a stream is a lazy list of (Maybe a).

type
Goal

Defined as (→ State (Streamof State)).

Examples:

> ((== 1 1) empty-state)
- : (Streamof State)
'((() . 0))
> ((call/fresh (λ (q) (== q 5))) empty-state)
- : (Streamof State)
(list (cons (list (cons (var 0) 5)) 1))

1.2 Streams🔗ℹ

The definitions of this section are the only code that knows how Streamof is represented. They read a stream element by element, a suspension being the element pause; the rest of the code, mplus and bind included, is written with them.

1.2.1 Pauses🔗ℹ

type
Pause
value
pause : Pause
procedure
(pause? v) → Boolean
v : Any
type constructor
(Maybe a)

pause is the only value of Pause, the element that stands for a suspension, and (Maybe a) is defined as (∪ Pause a). It is a union rather than a tagged sum, so the answers themselves must not be pauses.

1.2.2 Constructing Streams🔗ℹ

value
empty-stream : Null
syntax
(stream a ...)
syntax
(stream-cons a d)
(stream-cons pause d)
syntax
(stream-lazy d)

empty-stream is '(), the paper’s mzero, and (stream a ...) is the mature stream of the states a ..., the paper’s unit when there is one. (stream-cons a d) is (cons a d), and (stream-cons pause d), written with the identifier pause itself, is the suspension (λ () d): d is evaluated only when the suspension is forced. (stream-lazy d) is (stream-cons pause d).

1.2.3 Reading Streams🔗ℹ

procedure
(stream-empty? $) → Boolean
  $ : (Streamof a)
procedure
(stream-first $) → a
  $ : (Pair a (Streamof a))
(stream-first $) → (Maybe a)
  $ : (∪ (Pair a (Streamof a)) (Suspension a))
procedure
(stream-rest $) → (Streamof a)
  $ : (∪ (Pair a (Streamof a)) (Suspension a))
procedure
(stream-take $ n) → (Streamof a)
  $ : (Streamof a)
  n : Natural

stream-empty? recognizes empty-stream. The first element of a mature stream is its answer and the rest is the stream after it; the first element of an immature stream is pause and the rest is the stream produced by calling the suspension, so stream-rest forces it. (stream-take $ n) is the stream of the first n elements of $, pauses included.

1.2.4 Forcing Streams🔗ℹ

procedure
(stream-force $) → (∪ Null (Pair a (Streamof a)))
  $ : (Streamof a)
procedure
(stream-force-take $ n) → (Listof a)
  $ : (Streamof a)
  n : Natural
procedure
(stream->list $) → (Listof a)
  $ : (Streamof a)

These force pauses instead of returning them, so they count and collect only states. stream-force skips the pauses at the front of a stream, so that it is empty or mature; it is the paper’s pull. (stream-force-take $ n) is the list of the first n states of $, the paper’s (take n $), and stream->list is the list of all of them, the paper’s (take-all $). They do not return if a stream pauses forever before it has as many states as they need.

Examples:

> (define $ (stream-lazy (stream 1 2)))
> (stream-force $)
- : (U (Pairof Positive-Byte (Streamof Positive-Byte)) Null)
'(1 2)
; the pause is the first element
> (stream->list (stream-take $ 2))
- : (Listof Positive-Byte)
'(1)
> (stream-force-take $ 1)
- : (Listof Positive-Byte)
'(1)
> (stream->list $)
- : (Listof Positive-Byte)
'(1 2)

1.2.5 The Stream Monad🔗ℹ

procedure
(mplus $1 $2) → (Streamof a)
  $1 : (Streamof a)
  $2 : (Streamof a)
procedure
(bind $ g) → (Streamof b)
  $ : (Streamof a)
  g : (→ a (Streamof b))

The stream monad, with stream as unit and empty-stream as zero. mplus appends two streams, swapping them when the first element of the first is a pause, which is what makes the search interleave; bind runs g on every state of $ and combines the results with mplus.

1.3 The Core🔗ℹ

The core of microKanren.scm: the four goal constructors, and the unification they are built on.

1.3.1 Goal Constructors🔗ℹ

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

Unifies u and v in the substitution of the state.

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 combines the streams of g1 and g2 with mplus; conjunction runs g2 on every state of g1 with bind.

Example:

> (stream->list
   ((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))

1.3.2 Unification🔗ℹ

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.

1.4.1 Goal Forms🔗ℹ

syntax
(Zzz goal)

The inverse-η-delay: a goal that suspends before running goal, so that a recursive relation produces an immature stream instead of looping. It is defined as (λ ([s/c : State]) (stream-lazy (goal s/c))).

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))

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

Applies f to n fresh variables.

1.4.2 Running Goals🔗ℹ

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) → (Streamof State)
g : Goal

Running goals: call/goal runs a goal in empty-state. run collects its states with stream-force-take, and run* with stream->list.

1.4.3 Reification🔗ℹ

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.

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