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 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 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:
Regular lists |
OCanren |
---|---|
|
|
|
|
|
|
|
|
|
|
|
|
Syntax Extensions¶
There are two constructs, implemented as syntax extensions: fresh
and 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
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 top-level 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')
])
]
(* 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'