Release of Bindlib 4.0.4

Community
1

I’m pleased to announce the release of bindlib 4.0.4, which is a library for handling structures with bound (and free) variables. The typical application of the library is the development of programming languages and proof systems.

Bindlib has already been used in fairly big projects (from the most recent):

The implementation is very efficient (substitution amounts to function application), and it handles renaming to avoid capture.

Feel free to give feedback!

5 Likes
2
2 Likes
3

Any tutorials about this? Even if they are not OCaml-Bindlib specific.

4

Seems like the API documentation of the main module (https://github.com/rlepigre/ocaml-bindlib/blob/master/bindlib.mli ) comes with a full example about lambda-calculus which can serve as kind of a tutorial.

5

Something introductory to the theory, the idea, behind this?

6

Well, as @zozozo pointed out, the main (and only) module of Bindlib is a good start. There are also a few examples (with explanations) in the repository. We used to have a proper document describing the way things work, but it is completely outdated (it is in the repository as well).

Roughly, the idea behind Bindlib is that of so-called “higher-order abstract syntax” (HOAS): a binder should be implemented as a function in the meta-language (here, OCaml). Following this idea, the terms of the lambda-calculus can be encoded as:

type term =
| Var of string (* free variable *)
| Abs of term -> term (* lambda-abstraction *)
| App of term * term (* application *)

Here, it is important to note that substitution only amounts to application in the meta-language. This is how this approach is (probably) the most efficient.

Now, what Bindlib gives you is a way to keep track of the free variables of terms. This means that when you are constructing a term, you can decide to bind a variable to construct a new binder. This is done in a very efficient way since we store using a form of closure representation at the time they are built. This means that all the parts handling renaming of variables only happens at the construction of a term, not during its evaluation. One drawback of this approach is that the names may be messed up during evaluation, so it is necessary to perform an update on terms, before they can be safely printed. Otherwise, there might be some “visual capture” (that is, different variables with the same name appearing in the same context). Note that there can never be actual capture of variables since we rely on HOAS.

1 Like