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

[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.