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:

• Edwin Westbrook, Nicolas Frisby, Paul Brauner.Hobbits for Haskell: A Library for Higher-Order Encodings in Functional Programming Languages. Proceedings of the Haskell Symposium 2011 (Haskell ’11).
• Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java Multi-stage Programming Using Weak Separability. ACM SIGPLAN 2010 Conference on ProgrammingLanguage Design and Implementation (PLDI ’10).
• Edwin Westbrook, Aaron Stump, and Evan Austin. The Calculus of Nominal Inductive Constructions. 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP ’09).
• Edwin Westbrook. Free Variable Types. 7th Symposium on Trends in Functional Programming (TFP ’06).