ABTs in Haskell

November 12, 2017

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 unbound-generics, which 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:

data Term
  = Tvar Tvar
  | Tlam (Bind Tvar Term)
  | Tapp Term Term
  | Tlet Term (Bind Tvar Term)
  | Tz
  | Ts Term
  | Tifz Term Term (Bind Tvar Term)
  | Tbool Bool
  | Tif Term Term Term
  deriving (Show, Generic, Typeable)

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 unbound-generics library).

Here’s what it looks like in use:

-- (This is a snippet from the type inference code)
constraintsWithCon ctx (Tlam bnd) = do
  -- 'out' the ABT to get a fresh variable
  -- (x used to be "locally nameless", but now has a globally unique name)
  (x, e) <- unbind bnd
  -- Generate fresh type variable to put into the context
  t1 <- Cvar <$> fresh (string2name "t1_")
  let ctx' = Map.insert x t1 ctx
  t2 <- constraintsWithCon ctx' e
  return $ Carrow t1 t2

Apart from out being called unbind and into being called bind, the API is pretty similar. Also, unlike abbot, which required a standalone build step to generate SML code, unbound-generics uses the Haskell’s derive Generic to bake the code generation for capture avoiding substitution and alpha equivalence right into the compiler. All in all, unbound-generics is really pleasant to use!

  1. In fact, it’s hw1 for 15-312! If you’re curious, check out the handout.

Variables and Binding

Nearly every interesting programming language feature derives its power from variables. Functions wouldn’t be functions if not for variables. Modularity and linking reduce to variables and substitution. I’ve written in the past about all sorts of cool variables in types, as well as how parametric polymorphism in System F is the result of using type variables in two ways within the same system. Continue reading

System Fω and Parameterization

Published on September 27, 2017

Variables in Types

Published on September 25, 2017