I’ve been learning and using Haskell on-and-off for the past couple
of years. One of my early complaints was that I couldn’t find a good
library for working with variables and binding that used locally
nameless terms. Recently though, I found
checks all my previously unfilled boxes.
Abstract binding trees (or ABTs) are abstract syntax trees (ASTs) augmented with the ability to capture the binding structure of a program. ABTs are one of the first topics we cover in 15-312 Principles of Programming Languages because variables show up in every interesting feature of a programming language.
I recently wrote at length about the various strategies for dealing with
variables and binding and their implementations. While it’s a good
exercise1 to implement ABTs from scratch, in most cases I’d
rather just use a library. In school we used
abbot, which is an ABT
library for Standard ML. For tinkering with Haskell, I recently found
unbound-generics, which provides a similar API.
I gave it a test drive while learning how to implement type inference
for the simply-typed lambda calculus (STLC) and was rather pleased. The
source code for my STLC inference program is on GitHub if
you’re looking for an example of
unbound-generics in action.
To pluck a few snippets out, here’s the definition of STLC terms:
Bind is the abstract type for locally nameless terms that bind a
variable. It’s cool in Haskell (compared to SML) because the compiler
can automatically derive the locally nameless representation from this
data type definition (with help from the
Here’s what it looks like in use:
out being called
into being called
the API is pretty similar. Also, unlike
abbot, which required a
standalone build step to generate SML code,
unbound-generics uses the
derive Generic to bake the code generation for capture
avoiding substitution and alpha equivalence right into the compiler. All
unbound-generics is really pleasant to use!