Statically typed embedding of miniKanren relational programming language into Objective Caml
TeX OCaml Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
camlp5
papers
ppx
regression
samples
src
.gitignore
.merlin
META
Makefile
MiniKanren.odocl
README.md
_tags
myocamlbuild.ml
opam

README.md

Table of Contents

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: Expected workflow: add new test to try something out.

  • opam pin add camlp5 https://github.com/kakadu/camlp5.git
  • opam pin add GT https://github.com/dboulytchev/GT.git
  • opam pin add logger https://github.com/dboulytchev/logger.git
  • 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.