Table of Contents

• OCanren
  • Injecting and Projecting User-Type Data
  • Bool, Nat, List
  • Syntax Extensions
  • Run
  • Sample
  • Installation
• More info

OCanren

OCanren is a strongly-typed embedding of miniKanren relational programming language into [Objective Caml] (http://ocaml.org). More precisely, OCanren implements microKanren with [disequality constraints] (http://scheme2011.ucombinator.org/papers/Alvis2011.pdf).

The correspondence between original MiniKanren and OCanren constructs is shown below:

miniKanren	OCanren
#u	success
#f	failure
((==) a b)	(a === b)
((=/=) a b)	(a =/= b)
(conde (a b ...) (c d ...) ...)	conde [a &&& b &&& ...; c &&& d &&& ...; ...]
(fresh (x y ...) a b ... )	fresh (x y ...) a b ...

In addition, OCanren introduces explicit disjunction (|||) and conjunction (&&&) operators for goals.

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

inj : 'a -> 'a logic

can be used for this purpose:

inj 1

inj true

inj "abc"

There is also a prefix synonym !! for inj.

If the type is parametric (but non-recursive), then (as a rule) all its type parameters have to be injected as well:

!! (gmap(option) (!!) (Some x))

!! (gmap(pair) (!!) (!!) (x, y))

Here gmap(type) is a type-indexed morphism for the type type; it can be written by hands, or constructed using one of the existing generic programming frameworks (the library itself uses GT).

If the type is recursive, then, as a rule, it has to be abstracted from itself, and then injected as in the previous case, for example,

type tree = Leaf | Node of tree * tree

is converted into

type 'self tree = Leaf | Node of 'self * 'self

let rec inj_tree t = !! (gmap(tree) inj_tree t)

Pragmatically speaking, it is desirable to make a type fully abstract, thus logic variables can be placed in arbitrary position, for example,

type ('a, 'b, 'self) tree = Leaf of 'a | Node of 'b * 'self * 'self

let rec inj_tree t = !! (gmap(tree) (!!) (!!) inj_tree t)

instead of

type tree = Leaf of int | Node of string * t * t

Symmetrically, there is a projection function prj (and a prefix synonym !?), which can be used to project logical values into regular ones. Note, that this function is partial, and can raise Not_a_value exception. There is failure-continuation-passing version of prj, which can be used to react on this situation. See autogenerated documentation for details.

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:

(fun st -> Lazy.from_fun (fun () -> g st))

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 GT
open MiniKanren

(* Abstracted type for the tree *)
@type ('a, 'self) tree = Nil | Node of 'a * 'self * 'self with gmap, show

(* A shortcut for "ground" tree we're going to work with in "functional" code *)
type gtree = (int, gtree) tree

(* Logic counterpart *)
type ltree = (Nat.logic, ltree) tree logic

(* Printing ground tree function *)
let rec show_tree t = show(tree) (show(int)) show_tree t

(* Injection *)
let rec inj_tree : gtree -> ltree = fun t ->
  !! (gmap(tree) inj_nat inj_tree t)

(* Projection *)
let rec prj_tree : ltree -> gtree = fun t ->
  gmap(tree) prj_nat prj_tree (prj t)

(* Relational insert into a search tree *)
let rec inserto a t t' = conde [
  (t === !!Nil) &&& (t' === !!(Node (a, !!Nil, !!Nil)));
  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 a t =
  run q (fun q  -> inserto (inj_nat a) (inj_tree t) q)
        (fun qs -> prj_tree @@ Stream.hd qs)

(* Top-level wrapper for "inverse" insertion --- returns an integer, which
   has to be inserted to convert t into t' *)
let insert' t t' =
  run q (fun q  -> inserto q (inj_tree t) (inj_tree t'))
        (fun qs -> prj_nat @@ Stream.hd qs)  

Installation

OCanren can be installed using opam:

• opam pin add ocanren https://github.com/dboulytchev/ocanren.git -n -y
• opam install ocanren

More info

See autogenerated documentation or samples in /regression and /samples subdirectories.