I am pleased to announce the release of Bindlib 5.0.1, which is a library for handling structures with bound (and free) variables (typical applications include the development of languages and proof systems). It has already been available on Opam for several weeks, and the source code of the latest version can be found in the development repository.
This new version provides a simpler, more concise interface. It is extensively documented, and includes a small tutorial. An introductory paper has also been recently presented at the LFMTP 2018 workshop.
Bindlib has already been used in fairly big projects (from the most recent): Lambdapi, PMLâ‚‚, SubML, PML, and many other smaller prototypes.
The implementation is very efficient (in terms of substitution), and it handles renaming to avoid capture.
Interesting. Is it possible to handle telescopes with the library? Do you know whether it would be easy to use @fpottier’s visitors PPX on types using bindlib binders?
I cannot say, I’m not very familiar with these techniques. Sorry.
What I do know is that it is possible to define a form of mapper that traverses the AST while applying some partial transformation, and that is called back on every node (defaulting to the identity if the transformation is not defined). Is that the kind of things you are interested in?
In any case, I don’t think that visitor classes can be generated automatically using François’s PPX. However, it might be possible to provide a specific class by hand.
It is actually hosted on “GitHub pages” already! And accessible through the project link on GitHub. I guess this is not visible enough, so I added links in the readme, and corrected some typos in the documentation at the same time.
Yes.
OK. François’s work is precisely a PPX to generate such an "AST mapper. It’s pretty flexible so I guess it must be possible to use it, possibly writing a few adaptors by hand. I just wondered if anyone had tried that.
Concerning telescopes, it’s a whole different matter, that is sometimes handled in binding libraries, hence my question. A telescope is a binding of multiple variables where every variable may depend on other variables bound just before.
E.g. in classic math, you sometimes see something like: forall x : E, y : {x} Ă— F . P(x,y).
In a programming language, you may imagine: let x = 5, y = 2 * x in blah blah.
This kind of thing can be done easily with Bindlib, since you can build nested Binders. So, in other words, you can bind variable x in a binder that binds y in 2 * x and in blah blah.
And accessible through the project link on GitHub. I guess this is not visible enough, so I added links in the readme, and corrected some typos in the documentation at the same time.