Welcome to OCanren’s documentation!¶
OCanren is a stronglytyped embedding of miniKanren relational programming language into OCaml. Nowadays, implementation of OCanren strongly reminds fasterminiKanren. Previous implementation was based on microKanren with disequality constraints.
OCanren vs. miniKanren¶
The syntax between OCanren and vanilla miniKanren is a little bit different: OCanren vs. miniKanren. The correspondence between original miniKanren and OCanren constructs is shown below:
Injecting and Projecting UserType Data¶
To make it possible to work with OCanren, usertype data have to be injected into logic domain. In the simplest case (nonparametric, nonrecursive) the function
val inj : ('a, 'b) injected > ('a, 'b logic) injected
val lift : 'a > ('a, 'a) injected
can be used for this purpose:
inj @@ lift 1
inj @@ lift true
inj @@ lift "abc"
If the type is a (possibly recursive) algebraic type definition, then, as a rule, it has to be abstracted from itself, and then we can write smart constructor for constructing injected values,
type tree = Leaf  Node of tree * tree
is converted into
module T = struct
type 'self tree = Leaf  Node of 'self * 'self
let fmap f = function
 Leaf > Leaf
 Node (l, r) > Node (f l, f r)
end
include T
module F = Fmap2(T)
include F
let leaf () = inj @@ distrib @@ T.Leaf
let node b c = inj @@ distrib @@ T.Node (b,c)
Using fully abstract type we can construct type of ground
(without logic values) trees and type of logic trees
–
the trees that can contain logic variables inside.
Using this fully abstract type and a few OCanren builtins we can
construct reification
procedure which translates ('a, 'b) injected
into it’s right counterpart.
type gtree = gtree T.t
type ltree = ltree X.t logic
type ftree = (rtree, ltree) injected
Using another function reify
provided by the functor application we can
translate (_, 'b) injected
values to 'b
type.
val reify_tree : ftree > ltree
let rec reify_tree eta = F.reify LNat.reify reify_tree eta
And using this function we can run query and get lazy stream of reified logic answers
let _: Tree.ltree OCanren.Stream.t =
run q (fun q > q === leaf ())
(fun qs > qs#reify Tree.reify_tree)
Bool, Nat, List¶
There is some builtin support for a few basic types — booleans, natural numbers in Peano form, logical lists. See corresponding modules.
The following table summarizes the correspondence between some expressions on regular lists and their OCanren counterparts:
Regular lists 
OCanren 













Syntax Extensions¶
There are two constructs, implemented as syntax extensions: fresh
and defer
. The latter
is used to etaexpand enclosed goal (“inverseeta delay”).
However, neither of them actually needed. Instead of defer (g)
manual expansion can
be used:
delay (fun () > g)
To get rid of fresh
one can use Fresh
module, which introduces variadic function
support by means of a few predefined numerals and a successor function. For
example, instead of
fresh (x y z) g
one can write
Fresh.three (fun x y z > g)
or even
(Fresh.succ Fresh.two) (fun x y z > g)
Run¶
The toplevel primitive in OCanren is run
, which can be used in the following
pattern:
run n (fun q1 q2 ... qn > g) (fun a1 a2 ... an > h)
Here n
stands for numeral (some value, describing the number of arguments,
q1
, q2
, …, qn
— free logic variables, a1
, a2
, …, an
— streams
of answers for q1
, q2
, …, qn
respectively, g
— some goal, h
— a
handler (some piece of code, presumable making use of a1
, a2
, …, an
).
There are a few predefined numerals (q
, qr
, qrs
, qrst
etc.) and a
successor function, succ
, which can be used to “manufacture” greater
numerals from smaller ones.
Sample¶
We consider here a complete example of OCanren specification (relational binary search tree):
open Printf
open GT
open OCanren
open OCanren.Std
module Tree = struct
module X = struct
(* Abstracted type for the tree *)
@type ('a, 'self) t = Leaf  Node of 'a * 'self * 'self with gmap,show;;
let fmap eta = GT.gmap t eta
end
include X
include Fmap2(X)
@type inttree = (int, inttree) X.t with show
(* A shortcut for "ground" tree we're going to work with in "functional" code *)
@type rtree = (LNat.ground, rtree) X.t with show
(* Logic counterpart *)
@type ltree = (LNat.logic, ltree) X.t logic with show
type ftree = (rtree, ltree) injected
let leaf () : ftree = inj @@ distrib @@ X.Leaf
let node a b c : ftree = inj @@ distrib @@ X.Node (a,b,c)
(* Injection *)
let rec inj_tree : inttree > ftree = fun tree >
inj @@ distrib @@ GT.(gmap t nat inj_tree tree)
(* Projection *)
let rec prj_tree : rtree > inttree =
fun x > GT.(gmap t) LNat.to_int prj_tree x
end
open Tree
(* Relational insert into a search tree *)
let rec inserto a t' t'' = conde [
(t' === leaf ()) &&& (t'' === node a (leaf ()) (leaf ()) );
fresh (x l r l')
(t' === node x l r)
Nat.(conde [
(t'' === t') &&& (a === x);
(t'' === (node x l' r )) &&& (a < x) &&& (inserto a l l');
(t'' === (node x l l' )) &&& (a > x) &&& (inserto a r l')
])
]
(* Toplevel wrapper for insertion  takes and returns nonlogic data *)
let insert : int > inttree > inttree = fun a t >
prj_tree @@ RStream.hd @@
run q (fun q > inserto (nat a) (inj_tree t) q)
(fun qs > qs#prj)
(* Toplevel wrapper for "inverse" insertion  returns an integer, which
has to be inserted to convert t into t' *)
let insert' t t' =
LNat.to_int @@ RStream.hd @@
run q (fun q > inserto q (inj_tree t) (inj_tree t'))
(fun qs > qs#prj)
(* Entry point *)
let _ =
let insert_list l =
let rec inner t = function
 [] > t
 x::xs >
let t' = insert x t in
printf "Inserting %d into %s makes %s\n%!" x (show_inttree t) (show_inttree t');
inner t' xs
in
inner Leaf l
in
ignore @@ insert_list [1; 2; 3; 4];
let t = insert_list [3; 2; 4; 1] in
let t' = insert 8 t in
Printf.printf "Inverse insert: %d\n" @@ insert' t t'