Scrap your nameplate: (functional pearl)

ABSTRACT

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 α-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 genericmprogramming 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.

REFERENCES

• 1: Glasgow Parallel Haskell, June 2005. http://www.macs.hw.ac.uk/-~dsg/gph/.
• 2: M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375--416, 1991.
• 3: Andrea Asperti , Stefano Guerrini, The optimal implementation of functional programming languages, Cambridge University Press, New York, NY, 1999
• 4: Lennart Augustsson, Mikael Rittri, and Dan Synek. On generating unique names. J. Funct. Program., 4(1):117--123, 1994.
• 5: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark Challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), 2005. To appear.
• 6: Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones , Simon Marlow, Associated types with class, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 12-14, 2005, Long Beach, California, USA
• 7: J. Cheney and C. Urban. Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In Proc. 20th Int. Conf. on Logic Programming (ICLP 2004), number 3132 in LNCS, pages 269--283, 2004.
• 8: Koen Claessen , John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.268-279, September 2000
• 9: N. G. de Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae, 34(5):381--392, 1972.
• 10: Murdoch Gabbay , Andrew Pitts, A New Approach to Abstract Syntax Involving Binders, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.214, July 02-05, 1999
• 11: M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13:341--363, 2002.
• 12: Ralf Hinze, Generics for the masses, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 13: Ralf Hinze and Simon Peyton Jones. Derivable type classes. In Graham Hutton, editor, Proceedings of the 2000 ACM SIGPLAN Haskell Workshop, volume 41.1 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.
• 14: J. Hughes. Restricted data types in Haskell. In E. Meijer, editor, Proceedings of the 1999 Haskell Workshop, number UU-CS-1999-28 in Technical report, Utrecht University, Department of Computer Science, 1999.
• 15: Simon Peyton Jones , Simon Marlow, Secrets of the Glasgow Haskell Compiler inliner, Journal of Functional Programming, v.12 n.5, p.393-434, July 2002 [doi>10.1017/S0956796802004331]
• 16: Ralf Lämmel, Towards generic refactoring, Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming, p.15-28, October 05, 2002, Pittsburgh, Pennsylvania [doi>10.1145/570186.570188]
• 17: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate: a practical design pattern for generic programming, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 18: Ralf Lämmel , Simon Peyton Jones, Scrap more boilerplate: reflection, zips, and generalised casts, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 19: Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class. In Benjamin Pierce, editor, Proceedings of the 10th International Conference on Functional Programming (ICFP 2005), Tallinn, Estonia, 2005.
• 20: Andres Löh and Johan Jeuring (editors). The Generic Haskell user's guide, version 1.42 - coral release. Technical Report UU-CS-2005-004, Utrecht University, 2005.
• 21: Conor McBride, First-order unification by structural recursion, Journal of Functional Programming, v.13 n.6, p.1061-1075, November 2003 [doi>10.1017/S0956796803004957]
• 22: James Mckinna , Robert Pollack, Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, v.23 n.3, p.373-409, November 1999 [doi>10.1023/A:1006294005493 ]
• 23: G. Nadathur and D. Miller. Higher-order logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5,chapter 8, pages 499--590. Oxford University Press, 1998.
• 24: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 25: Andrew M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, v.186 n.2, p.165-193, 01 November 2003 [doi>10.1016/S0890-5401(03)00138-X]
• 26: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 27: François Pottier. An overview of Cαml, June 2005. Available at http://cristal.inria.fr/~fpottier/publis/-fpottier-alphacaml.pdf.
• 28: Tim Sheard, March 2005. Personal communication.
• 29: Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
• 30: Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.263-274, August 25-29, 2003, Uppsala, Sweden
• 31: Olin Shivers and Mitchell Wand. Bottom-up β-reduction: Uplinks and λ-DAGs. In M. Sagiv, editor, Proceedings of the 14th European Symposium on Programming (ESOP 2005), number 3444 in LNCS, pages 217--232, 2005.
• 32: J. Staples , P. J. Robinson , R. A. Paterson , R. A. Hagen , A. J. Craddock , P. C. Wallis, Qu-Prolog: an extended Prolog for meta level programming, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 33: Christian Urban , Andrew M. Pitts , Murdoch J. Gabbay, Nominal unification, Theoretical Computer Science, v.323 n.1-3, p.473-497, 14 September 2004 [doi>10.1016/j.tcs.2004.06.016]
• 34: C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In Proceedings of the 20th International Conference on Automated Deduction (CADE 2005), 2005. To appear.
• 35: Phil Wadler, Andrew Pitts, and Koen Claessen, September 2003. Personal communication.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages

Keywords:
binding, generic programming, names, substitution