Say “Hello World!” in OCanren

We first execute the program, and then we read and explain through the source code line by line.

Executing the Program

The source code has to be compiled and linked, for which you would need the Makefile. Now open terminal under your local copy ofthe helloWorld directory, and:

make

This would produce a native-code file hello.opt, execution of which by:

./hello.opt

will print hello world! in your terminal.

Reading the Program

The first line:

open OCanren

makes the names from the module OCanren available for later use.

Important Interfaces

The source code of the module OCanren resides in OCanren.ml (It does not have an accompanying .mli file). Inspecting the content thereof, we shall see that basically it includes three modules Logic, Core and module Stream, and finally defines the Std module. You should open the module OCanren at the beginning of every source file where you use OCanren features.

The second line:

let str = !!("hello world!\n")

associates the value name str with the expression that is the prefix operator !! (named primitive injection) applied to the string literal "hello world!\n".

Internal Representation

The operator !!, provided by the module Logic, makes type conversion to the OCanren internal representation, something like what a calculator program does when it receives an input string “1” and converts it to the integer or floating-point type for further processing. We could see from the interface that:

val (!!) : 'a -> ('a, 'a logic) injected

The injected type constructor is provided by the module Logic as an abstract type (so we do not concern ourselves with its implementation).

More information about various typed being used and the meaning of type parameters of the (‘a, ‘b) injected could be get from Digesting the Types.

Logic Variables

The logic type constructor which appears in the type of !! above is also provided by the module OCanren.Logic. It takes one type parameter and its type representation is exposed: we could see from the module interface that it has two constructors Var and Value, representing respectively a logic variable and a concrete value over/of the parameter type, in the sense that wrt. the arithmetic expression 1 + x we say that x is a logic variable over the integer type and 1 is a concrete value of the integer type.

Making a Query

The 3rd line:

let _ =
  List.iter print_string @@
  Stream.take ~n:1 @@
  run q (fun q -> ocanren { q == str }) project

is divided into three sub-expressions by the right associative infix operator @@ that is provided by OCaml’s core library Stdlib. The most important sub-expression is: run q (fun q -> ocanren { q == str }) project whose most important part is: q == str.

Note

The piece of code on the discussion uses an OCanren-specific syntax extension that doesn’t appear in other languages of miniKanren family. See OCanren-specific Camlp5 syntax extension for details.

Next we start with explaining the inner most and the most important part: q == str, followed by its immediate enclosing environment which is the run statement:

run q (fun q -> ocanren { q == str }) project

and finally the top most expression for taking and printing answers.

Syntactic Identity and Unification

Syntactic identity between two expressions \(expr_1\) and \(expr_2\) (of the same type) is denoted using two equation symbols: \(expr_1 == expr_2\). Usually we are given two different expressions both of which have zero or more sub-expressions considered as logic variables, and we are interested in finding (type sensitive) substitutes for these logic variables so that the resulting expressions are syntactically identical. Finding such substitutes is know as unification of the original expressions.

Example In order for both (x + 1) == (2 + y) and Node (x,1) == Node (2,y) to be true, we replace x by 2 and y by 1, making both sides of == the expression 2 + 1 or Node (2,1) respectively. We now unified (x + 1) with (2 + y). Moreover, Node (x,1) is unified with Node (2,y).

Example How to substitute the logic variable z so that z == "hello world!" ? Trivial: replacing z with the constant "hello world!". This is essentially what our program does: solving a unification problem.

The OCanren Top Level: the run expression

We can parse the run ... expression following the syntax below, which is given in EBNF except that occurrences of the meta-identifier etc signifies omission: there is no single syntactic category named etc.

top level = 'run',  size indicator, goal, answer handler ;

size indicator =  'one' | 'two' | 'three' | 'four' | 'five'
                | 'q'   | 'qr'  | 'qrs'   | 'qrst' | 'qrstu'
        | '(', size indicator, ')'
        | 'succ', size indicator ;

goal = 'fun', parameters, '->', goal body ;

parameters = etc ;

goal body = 'ocanren', '{', pretty goal body, '}' ;

pretty goal body = etc ;

answer handler = 'project' | etc ;

A goal asks: what values shall be assumed by the parameters so that the proposition as given by the goal body (in which these parameters are expected to occur) holds?

The ocanren { } environment in a goal body instructs the Camlp5 preprocessor to transform on the syntactic level the pretty goal body into the more verbose and less intuitive calls of OCanren’s functions. As a reference, the rules by which the preprocessing is done is given in pa_ocanren.ml where we could find, for example, the == symbol is transformed into the name unify.

Todo

fix links

The number of parameters shall agree with the size indicator, where q … qrstu are just alternative names for one … five respectively. If there are more than five parameters, the successor function succ can be applied to build larger size indicators, e.g., (succ (succ five)) is for seven parameters.

The answer handler is a type converter from the OCanren internal representation to a user-level representation. When there is no free logic variables in the answer we use project. The Not_a_value exeption (provided by OCanren.Logic) is thrown if we use project as the handler but the answer contains free logic variables: in this case some other handler shall be used.

Todo

Reference reifiers

The run function and the size indicators are provided by module OCanren.Core. Basic answer handlers are provided by module OCanren.Logic.

Taking and Displaying Answers

The top level constructs a lazy stream out of which an arbitrary number of answers could be pulled, subject to answer availability. We use a stream instead of a finite list to hold the answers because generally the set of all answers is enumerable. Omission of the optional argument ~n of take means “take all”. Finally we use OCaml standard functions to iterate through the taken list of answers and print each one in the terminal. Our program has only one answer.