[ANN] SWIPl-OCaml v0.5 - Never write your own unification algorithms again!

[Gopiandcode]

Hey all! I am just posting to announce a new package I’ve been working on: OCaml bindings to SWI-Prolog (ver 8.5 or higher)!

It’s currently in the process of being submitted to OPAM, but it’s my first time writing a package with bindings to C (using ctypes), so some further changes might be needed? maybe?, but you can find the source code repository here: repo/github mirror.

As a sneak peek of what the API looks like, here’s a hello world:

(* initialise SWIProlog *)
let () = Swipl.initialise ()
(* setup the prolog database with some facts *)
let () = Swipl.load_source "hello :- writeln('hello world')."
(* construct a Swipl term in OCaml *)
let hello = Swipl.Syntax.(!"hello")
(* send the term to the Prolog engine *)
let () = Swipl.with_ctx @@ fun ctx -> Swipl.call ctx hello

I’ve taken care to provide some detailed documentation + quick start guide using odoc (see index (swipl.index)) - the quick start guide shows a step by step walkthrough on using the library to write a type inference algorithm for lambda calculus using OCaml+Prolog (no need to write your own UF).

Anyway, hope this might be useful for others - I have spent way too long racking my brains on writing dumb custom unification algorithms, but now, no more!

[Gopiandcode]

If you’re interested, here are a couple of interesting snippets from the type-checking example.

The following is the definition of the type inference algorithm (there was a haskell cafe thread about using prolog for type-inference, with Oleg pointing out some flaws in a naieve implementation, but I have updated the code to fix those issues):

let () = Swipl.load_source "
typeof(Gamma, Term, Type) :-
        atom(Term),
        member(type(Term, Tvar), Gamma),
        !,
        unify_with_occurs_check(Type, Tvar).

typeof(Gamma, lam(A,B), Type) :-
        atom(A),
        typeof([type(A, TvarA)|Gamma], B, TvarB),
        unify_with_occurs_check(Type, fun(TvarA, TvarB)).

typeof(Gamma, app(A,B), Type) :-
        typeof(Gamma, A, TvarA),
        unify_with_occurs_check(TvarA, fun(TvarIn, TvarOut)),
        typeof(Gamma, B, TvarIn),
        unify_with_occurs_check(Type, TvarOut).
"

With that defined, the final type-checking code was as follows:

let typecheck term =
  (* create a variable context for the typechecking query *)
  Swipl.with_ctx (fun ctx ->
    (* create a fresh variable to hold the result *)
    let result = Swipl.fresh ctx in
    (* construct a Prolog term to represent the query  *)
    let term = (typeof Swipl.(encode_list ctx []) (encode term) result) in
    (* send the query to the Prolog engine *)
    let query = Swipl.eval ctx term in
    (* if the prolog engine found a solution, extract it *)
    if Swipl.first_solution query
    then decode ctx (TermMap.empty, 0) result |> Option.map fst
    else None
  )
(* val typecheck: t -> ty option *)

I’ve omitted some steps for brevity here, but the quick-start goes in more detail, so check it out if this has piqued your interest.

[sid]

I don’t know if it satisfies your use case but have you checked out GitHub - LPCIC/elpi: Embeddable Lambda Prolog Interpreter ?

[gasche]

I was about to mention Elpi; Elpi supports Lambda-Prolog, a dialect of Prolog that has native support for variable bindings, which is very useful for prototyping programming languages and type systems. Elpi also works well through js_of_ocaml, so those prototypes can be easily exposed as a web interface, which is nice.

(The reference Lambda-Prolog implementation, Teyjus, is also in OCaml, but it is not designed for easy embedding within an OCaml program. Another Prolog dialect that is close to Lambda-Prolog and is explicitly designed for language prototyping is Antonis Stampoulis’ Makam.)

[Gopiandcode]

@sid

I don’t know if it satisfies your use case but have you checked out GitHub - LPCIC/elpi: Embeddable Lambda Prolog Interpreter ?

@gasche

I was about to mention Elpi; Elpi supports Lambda-Prolog, a dialect of Prolog that has native support for variable bindings, which is very useful for prototyping programming languages and type systems. Elpi also works well through js_of_ocaml, so those prototypes can be easily exposed as a web interface, which is nice.

I have actually looked at Elpi before - in fact, I even mentioned it in another reply to @gasche (see Writing type inference algorithms in OCaml - #7 by Gopiandcode), but the documentation story is very lacking, and it seems like the main audience is just Coq developers.

To quote myself:

@Gopiandcode

I hope there’s at least some space left for more discussion, as there are at least a couple of questions in this thread that remain unanswered, and the only example of elpi being used to handle the type inference for a language no longer compiles .

I find that using Elpi is more attractive in theory than it is in practice. because the lack of documentation makes it pretty much unapproachable for anyone who isn’t already in the know (in fact it was easier for me to write C bindings to a foreign library, than to use an OCaml Prolog implementation primarily because of the lack of documentation).

@Gopiandcode

Looking through the Elpi repository, there seem to be enough examples there that I feel reasonably confident that I could work out how to embed a type system into the language - the problem I’m having is that it’s rather challenging to access it programmatically - the compiler/parser part is somewhat straightforward, but I’ve been stumped on which API endpoints I would use to convert my syntax tree (parsed elsewhere) into a query to submit to Elpi.

So actually this binding actually draws from my experiences with Elpi, I’ve tried to make the documentation as thorough and comprehensive as possible, with several examples, both in the quick start and in the repo (that compile, mind you), and all the public functions of the API documented.

[Gopiandcode]

Here’s another example that might be interesting for those who have experience with SWI-Prolog.

You can even get native interaction with CHR: Constraint Handling Rules - Wikipedia is a very elegant framework which comes bundled with SWI Prolog that allows users to write complex domain specific constraint solving engines in a concise declaritive way.

Here’s a CHR system that models the interaction between salt and water (basic I know, but look up CHR to see some more powerful examples):

let () = Swipl.load_source "
:- use_module(library(chr)).

:- chr_constraint salt/0, water/0, salt_water/0.

salt, water <=> salt_water.

reducesTo_(Goal, C) :-
        call(Goal),
        call(user:'$enumerate_constraints'(C)).
reducesTo(Goal, Constraints) :-
        findall(Constraint, reducesTo_(Goal, Constraint), Constraints).
"

Which we can then embed into OCaml using the following code:

let solve_constraints ls =
  (* Create a new term variable context *)
  Swipl.with_ctx (fun ctx ->
    (* create a term for the result *)
    let result = Swipl.fresh ctx in    
    (* encode the constraint store *)
    let goal = encode ls in
    (* send the query to the Prolog engine *)
    Swipl.call ctx (reducesTo goal result);
    (* extract the result *)
    decode ctx result
  )
(* val solve_constraints: t list -> t list *)

(Again, some steps have been omitted for brevity, and you should check out the quick start guide for a step by step walkthrough).

[shonfeder]

As a long-time user of SWI-Prolog, I am very glad to see this work making it easier to interface! I have also spent a nontrivial time playing around with Elpi, and while Lambda Prolog is lovely and Elpi is super fun to play with, and I can imagine very useful for some PLT purposes, I don’t suppose it can (currently) compete with the amount of the optimizations, features, and libraries that are available for SWI-Prolog. I would think that a brief look at the SWI standard library should suffice to demonstrate that SWI-Prolog -- Manual (consider, e.g. the various CLP libraries, the DCG libraries, the support for tabling)?

One use case I’m excited for: I often wish I could just use a Prolog database rather than sqlite. It provides a git and human friendly database format, and makes many kinds of queries trivial. With this library, that should be very easy

Thank you for this work!!

(It is worth noting that Elpi also has support for CHR. See elpi/ELPI.md at master · LPCIC/elpi · GitHub – I am really looking forward to Elpi continuing to mature, as it’s a lovely project and Lambda Prolog is amazing ).

[Kakadu]

@Gopiandcode Did you consider to use something more lightweight, for example, any EDSL from miniKanren family?

[Gopiandcode]

@Kakadu

Did you consider to use something more lightweight, for example, any EDSL from miniKanren family?

For the examples I’ve listed above, sure, a simpler DSL like miniKanren might suffice, but my intention was really more to open up the full power of Prolog while using OCaml, and secondly I’m not aware of any versions of the miniKanren family that offer nice FFIs and I wasn’t too keen on implementing yet another unification engine (especially seeing as my main aim was to not write unification algorithms).

I’ve also looked at OCanren, but it’s very experimental, and couldn’t get it to compile.

[Kakadu]

@Gopiandcode

I’ve also looked at OCanren, but it’s very experimental, and couldn’t get it to compile.

Well, it passed opam CI, so there is no obvious problem on OCanren’s side.