Thursday, December 31, 2015

HobbitLib, a Haskell Library for Name-Binding

Having the right data representation can vastly affect the ease with which we write programs. Unfortunately, it is difficult to build the "right" representation of programs themselves, because of constructs which bind variables, such as function definitions:

foo (int x) { ... }

HobbitLib is a Haskell library that provides a data-type for representing variable-binding constructs in programming languages. This representation satisfies the following four properties:
  1. Freshness (also called "Shadowing"): foo (int x) { ... } introduces a new variable x that is distinct from any previously-bound variables, even if those were also written "x";
  2. Renaming (also called "Alpha-Equivalence"): foo (int x) { ... x ... } = foo (int y) { ... y ... };
  3. Scoping: variable x should not occur outside of a foo (int x); and
  4. Typing: Variable x in foo (int x) { ... } should only be used as a term variable of type int.
The upshot is that any code that uses the HobbitLib representation for variable-bindings is statically guaranteed to never violate these properties, as the properties are built into the representation. This eliminates whole classes of bugs. In addition, we can use these to build representations of all and only the well-typed programs of a language, allowing us to further guarantee that all of our program-manipulating code is type-preserving.

HobbitLib can be downloaded using Haskell's cabal tool, by typing "cabal install hobbits" at a command prompt, or by using the above link.

HobbitLib and other Name-Binding Publications:


Get in touch with me


Kestrel Institute 3260 Hillview Avenue Palo Alto, California 94304 USA


westbrook at