Welcome to OCanren’s documentation!¶
OCanren is a strongly-typed embedding of miniKanren relational programming language into OCaml. Nowadays, implementation of OCanren strongly reminds faster-miniKanren. 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 User-Type Data¶
To make it possible to work with OCanren, user-type data have to be injected into logic domain. In the simplest case (non-parametric, non-recursive) 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
(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
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
(_, 'b) injected values to
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 built-in 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:
There are two constructs, implemented as syntax extensions:
defer. The latter
is used to eta-expand enclosed goal (“inverse-eta delay”).
However, neither of them actually needed. Instead of
defer (g) manual expansion can
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)
(Fresh.succ Fresh.two) (fun x y z -> g)
The top-level primitive in OCanren is
run, which can be used in the following
run n (fun q1 q2 ... qn -> g) (fun a1 a2 ... an -> h)
n stands for numeral (some value, describing the number of arguments,
qn — free logic variables,
an — streams
of answers for
g — some goal,
h — a
handler (some piece of code, presumable making use of
There are a few predefined numerals (
qrst etc.) and a
succ, which can be used to “manufacture” greater
numerals from smaller ones.
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') ]) ] (* Top-level wrapper for insertion --- takes and returns non-logic 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) (* Top-level 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'