Haskell projects looking for contributors?

Sure. First, it makes sense to distinguish ABTs in general from the various ABT implementations that have proliferated.

"Abstract binding trees" were first used, if I recall correctly, in Nuprl for the representation of its uniform syntax. An ABT consists of one of the following:

  1. A variable "x"
  2. A binding of a variable into an ABT, "x. E"
  3. An application of an 'operator' to a list of ABTs conforming to its arity.

The idea is that each language contains a set of operators, and each operator has an arity. An arity is a list of valences, and a valence is simply a number which counts how many variables are to be bound in a particular slot. So an example operator might be "Pi" whose arity would be "[0,1]"; then an abstract binding tree involving Pi might be "Pi{Unit{}; x. Unit{}}". (Arities may also be generalized to involve sorts, to separate different syntactic categories; in papers and books this is very useful, but leads to a lot of complexity in an implementation.). Alpha equivalence and substitution are defined generically on ABTs, as are a number of other useful operations.

So the point of ABTs is that once you have implemented them in general, you can define a language by giving a set of its "op codes" and explaining their arities: then, there is no need to implement substitution or alpha equivalence, since this comes for free from the underlying ABT structure.

A great place to learn about ABTs is Bob Harper's Practical Foundations for Programming Languages, where he uses them as the basis for his entire book.


Typically, an ABT implementation is done in a nominal manner, by assuming a type of variables that can be generated freely (or in a monad), and has decidable equality. Then, the primary interface is via a "view" type parameterized over some interpretation phi, which gives you one layer of syntax: it is either a named variable, or it is the binding of (named) variable into a piece of syntax in phi, or it is an application of an op code to a list of parameters with the appropriate valences.

Then, there is a concrete term representation Tm, which usually is locally nameless, and you have injections and projections between Tm and View Tm (i.e. letting phi be Tm). The conversion from Tm to View Tm lets you convert whatever binding style is implemented in Tm to a nominal one which is suitable for programming with as a human being, and the conversion from View Tm to Tm will convert the nominal representation into whatever you have chosen to use for Tm (probably locally nameless). So this takes care of what you usually use unbind for in Unbound from the Penn folks.


In practice, using the abt library is similar to using Unbound, except that it does not use any code generation, and is a lot easier to understand in my opinion. There may be some cases where Unbound gives you a bit finer control over binding too, but since abt is based on a nominal interface, it seems to suffice perfectly.

On the other hand, whilst Bound is extremely elegant, it is simply not practical to use it for serious work in type checkers. Why? Try going under a binder and adding a variable to a context, and you will know what I mean. I have seen tricks for making this work (by Francesco Mazzoli and perhaps others), but it is extremely complicated. I am sure that in the use-cases that it was intended for, Bound is a wonderful solution; but it is clear that when it was written, the most basic tasks of writing type checkers with hypothetico-general judgements were not even being considered.

Finally, abt requires a level of boilerplate somewhere in between Bound and Unbound. You do not need to write any tricky Monad instances for anything. All the kit is built-in from the start. The only thing you have got to do is define the arities of your operators, and their string representation (so they can be shown); you also have to demonstrate a decidable equality on op codes.

Also, abt is very light on dependencies. Currently, it has a profunctors dependency, but I will be removing this shortly, since the prisms which I provide can be moved into a separate package. I have found them useful, but they are by no means necessary for successfully using abt.

/r/haskell Thread