Lambda the Ultimate

Recent research has shown how boilerplate code, or repetitive code for traversing datatypes, can be eliminated using generic programming techniques already available within some implementations of Haskell. One particularly intractable kind of boilerplate is nameplate, or code having to do with names, name-binding, and fresh name generation. One reason for the difficulty is that operations on data structures involving names, as usually implemented, are not regular instances of standard map, fold , or zip operations. However, in nominal abstract syntax, an alternative treatment of names and binding based on swapping, operations such as alpha-equivalence, capture-avoiding substitution, and free variable set functions are much better-behaved. In this paper, we show how nominal abstract syntax techniques similar to those of FreshML can be provided as a Haskell library called FreshLib. In addition, we show how existing generic programming techniques can be used to reduce the amount of nameplate code that needs to be written for new datatypes involving names and binding to almost nothing—in short, how to scrap your nameplate.