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
`[]`	`nil`
`[x]`	`!< x`
`[x; y]`	`x %< y`
`[x; y; z]`	`x % (y %< z)`
`x::y::z::tl`	`x % (y % (z % tl))`
`x::xs`	`x % xs`

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'