1 microKanren

9.3

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.

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

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 The Core🔗ℹ

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:

> (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
(unit s/c) → (Streamof a)
  s/c : a
value
mzero : Null
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. mplus appends two streams, swapping them when the first is immature, which is what makes the search interleave.

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.3 User-Level Forms🔗ℹ

These are the forms of miniKanren-wrappers.scm.

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.

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) → (Streamof State)
  g : Goal
procedure
(pull $) → (∪ Null (Pair a (Streamof a)))
  $ : (Streamof a)
procedure
(take n $) → (Listof a)
  n : Natural
  $ : (Streamof a)
procedure
(take-all $) → (Listof a)
  $ : (Streamof a)

Running goals: pull forces a stream until it is mature or empty, and take and take-all collect its states.

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	micro Kanren
2	First Edition
3	Second Edition
4	Comparing the Editions