research-article

Binders unbound

Authors:

Stephanie Weirich,

Brent A. Yorgey,

Tim SheardAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 9

Pages 333 - 345

https://doi.org/10.1145/2034574.2034818

Published: 19 September 2011 Publication History

Abstract

Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected. Furthermore, their implementations are tedious, requiring "boilerplate" code that must be updated whenever the object language definition changes.

Many researchers have therefore sought to specify binding syntax declaratively, so that tools can correctly handle the details behind the scenes. This idea has been the inspiration for many new systems (such as Beluga, Delphin, FreshML, FreshOCaml, Cαml, FreshLib, and Ott) but there is still room for improvement in expressivity, simplicity and convenience.

In this paper, we present a new domain-specific language, Unbound, for specifying binding structure. Our language is particularly expressive - it supports multiple atom types, pattern binders, type annotations, recursive binders, and nested binding (necessary for telescopes, a feature found in dependently-typed languages). However, our specification language is also simple, consisting of just five basic combinators. We provide a formal semantics for this language derived from a locally nameless representation and prove that it satisfies a number of desirable properties.

We also present an implementation of our binding specification language as a GHC Haskell library implementing an embedded domain specific language (EDSL). By using Haskell type constructors to represent binding combinators, we implement the EDSL succinctly using datatype-generic programming. Our implementation supports a number of features necessary for practical programming, including flexibility in the treatment of user-defined types, best-effort name preservation (for error messages), and integration with Haskell's monad transformer library.

Supplementary Material

MP4 File (_talk6.mp4)

Download
57.31 MB

References

[1]

B. Aydemir and S. Weirich. LNgen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, Computer and Information Science, University of Pennsylvania, June 2010.

[2]

B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering formal metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3--15, Jan. 2008.

Digital Library

[3]

C. Calvès. A Haskell nominal toolkit. http://www.inf.kcl.ac.uk/pg/calves/hnt/, Jan. 2009.

[4]

A. Charguéraud. The locally nameless representation. Journal of Automated Reasoning, Special Issue on the POPLmark Challenge, 2011. To appear.

[5]

J. Cheney. Toward a general theory of names: binding and scope. In Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, MERLIN '05, pages 33--40, New York, NY, USA, 2005\natexlaba. ACM.

Digital Library

[6]

J. Cheney. Scrap your nameplate: (functional pearl). In Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, ICFP '05, pages 180--191, New York, NY, USA, 2005. ACM. ISBN 1-59593-064-7.

Digital Library

[7]

H. Cirstea, C. Kirchner, L. Liquori, and B. Wack. Rewrite strategies in the rewriting calculus. In B. Gramlich and S. Lucas, editors, Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain, June 2003. Electronic Notes in Theoretical Computer Science.

[8]

N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34 (5): 381--392, 1972.

[9]

N. G. de Bruijn. Telescopic mappings in typed lambda calculus. Information and Computation, 91 (2): 189--204, 1991.

Digital Library

[10]

G. Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, 1969. Edited by Mandred Szabo.

[11]

A. D. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In J. Joyce and C. Seger, editors, Higher-order Logic Theorem Proving And Its Applications, Proceedings, 1993, volume 780 of Lecture Notes in Computer Science, pages 414--426. Springer, 1994.

Digital Library

[12]

D. Herman and M. Wand. A theory of hygienic macros. In ESOP '08: Proceedings of the Seventeenth European Symposium On Programming, Mar. 2008.

Digital Library

[13]

S. Kleene. Introduction to Metamathematics. ban Nostrand Rheinhold, Princeton, USA, 1952.

[14]

R. Lämmel and S. Peyton Jones. Scrap your boilerplate with class: extensible generic functions. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), pages 204--215. ACM Press, Sept. 2005.

Digital Library

[15]

C. McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999. Available from http://www.lfcs.informatics.ed.ac.uk/reports/00/ECS-LFCS-00-419/.

[16]

J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23 (3-4): 373--409, 1999.

Digital Library

[17]

U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.

[18]

B. Pientka and J. Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In J. Giesl and R. Hähnle, editors, IJCAR, volume 6173 of Lecture Notes in Computer Science, pages 15--21. Springer, 2010.

Digital Library

[19]

A. M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186: 165--193, 2003.

Digital Library

[20]

A. Poswolsky and C. Schürmann. System description: Delphin - a functional programming language for deductive systems. Electron. Notes Theor. Comput. Sci., 228: 113--120, January 2009.

Digital Library

[21]

F. Pottier. An overview of Cαml. In ACM Workshop on ML, pages 27--52, Mar. 2006.

Digital Library

[22]

F. Pottier. Static name control for FreshML. In In IEEE Symposium on Logic in Computer Science, pages 356--365, 2007.

Digital Library

[23]

N. Pouillard and F. Pottier. A fresh look at programming with names and binders. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, ICFP '10, pages 217--228, New York, NY, USA, 2010. ACM. ISBN 978-1-60558-794-3.

Digital Library

[24]

D. Prawitz. Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm, 1965.

[25]

A. Rodriguez, J. Jeuring, P. Jansson, A. Gerdes, O. Kiselyov, and B. C. d. S. Oliveira. Comparing libraries for generic programming in Haskell. SIGPLAN Not., 44: 111--122, September 2008.

Digital Library

[26]

S. Sarkar, P. Sewell, and F. Zappa Nardelli. Binding and substitution. www.cl.cam.ac.uk/~pes20/ott/bind-doc.pdf, Oct. 2007.

[27]

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strniša. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20 (1): 71--122, 2010.

Digital Library

[28]

Z. Shao. Implementing typed intermediate language. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), pages 313--323, Baltimore, Maryland, September 1998.

Digital Library

[29]

T. Sheard and S. P. Jones. Template meta-programming for Haskell. SIGPLAN Not., 37: 60--75, December 2002.

Digital Library

[30]

M. Shinwell and A. Pitts. Fresh Objective Caml User Manual. Cambridge University Computer Laboratory, Feb. 2005.

[31]

M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. FreshML: Programming with binders made simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263--274. ACM Press, Aug. 2003.

Digital Library

[32]

C. Urban. How to prove false using the variable convention. Appears as a poster at TTVSI, 1 page, mar 2008.

[33]

C. Urban. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning, 40: 327--356, 2008. ISSN 0168-7433. URL http://dx.doi.org/10.1007/s10817-008-9097-2.

Digital Library

[34]

C. Urban and C. Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. In G. Barthe, editor, Programming Languages and Systems, volume 6602 of Lecture Notes in Computer Science, pages 480--500. Springer Berlin / Heidelberg, 2011. URL http://dx.doi.org/10.1007/978-3-642-19718-5_25.

Digital Library

[35]

S. Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1--12, Portland, OR, USA, Sept. 2006.

Digital Library

[36]

F. Zappa Nardelli. A locally-nameless backend for Ott. moscova.inria.fr/~zappa/projects/ln_ott/, 2009.

Cited By

Maziarz KEllis TLawrence AFitzgibbon APeyton Jones SFreund SYahav E(2021)Hashing modulo alpha-equivalenceProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454088(960-973)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454088
ABEL AALLAIS GHAMEER APIENTKA BMOMIGLIANO ASCHÄFER SSTARK K(2019)POPLMark reloaded: Mechanizing proofs by logical relationsJournal of Functional Programming10.1017/S095679681900017029Online publication date: 10-Dec-2019
https://doi.org/10.1017/S0956796819000170
Pombrio JKrishnamurthi SWand M(2017)Inferring scope through syntactic sugarProceedings of the ACM on Programming Languages10.1145/31102881:ICFP(1-28)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110288
Show More Cited By

Index Terms

Binders unbound

Recommendations

Binders unbound
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution ...
Layout-sensitive language extensibility with SugarHaskell
Haskell '12: Proceedings of the 2012 Haskell Symposium

Programmers need convenient syntax to write elegant and concise programs. Consequently, the Haskell standard provides syntactic sugar for some scenarios (e.g., do notation for monadic code), authors of Haskell compilers provide syntactic sugar for more ...
Layout-sensitive language extensibility with SugarHaskell
Haskell '12

Programmers need convenient syntax to write elegant and concise programs. Consequently, the Haskell standard provides syntactic sugar for some scenarios (e.g., do notation for monadic code), authors of Haskell compilers provide syntactic sugar for more ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 9

ICFP '11

September 2011

456 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2034574

Issue’s Table of Contents

ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
September 2011
470 pages
ISBN:9781450308656
DOI:10.1145/2034773
General Chairs:
Manuel Chakravarty
University of New South Wales, Australia
,
Zhenjiang Hu
National Institute of Informatics, Japan
,
Program Chair:
Olivier Danvy
Aarhus University, Denmark

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2011

Published in SIGPLAN Volume 46, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
361
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Maziarz KEllis TLawrence AFitzgibbon APeyton Jones SFreund SYahav E(2021)Hashing modulo alpha-equivalenceProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454088(960-973)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454088
ABEL AALLAIS GHAMEER APIENTKA BMOMIGLIANO ASCHÄFER SSTARK K(2019)POPLMark reloaded: Mechanizing proofs by logical relationsJournal of Functional Programming10.1017/S095679681900017029Online publication date: 10-Dec-2019
https://doi.org/10.1017/S0956796819000170
Pombrio JKrishnamurthi SWand M(2017)Inferring scope through syntactic sugarProceedings of the ACM on Programming Languages10.1145/31102881:ICFP(1-28)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110288
Yanok INystrom N(2016)TapirACM SIGOPS Operating Systems Review10.1145/2883591.288360249:2(51-56)Online publication date: 20-Jan-2016
https://dl.acm.org/doi/10.1145/2883591.2883602
Yanok INystrom NLu S(2015)TapirProceedings of the 8th Workshop on Programming Languages and Operating Systems10.1145/2818302.2818303(33-38)Online publication date: 4-Oct-2015
https://dl.acm.org/doi/10.1145/2818302.2818303
Ni YWang Y(2024)Generic Reasoning of the Locally Nameless RepresentationProgramming Languages and Systems10.1007/978-981-97-8943-6_3(42-62)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_3
Fiore MSzamozvancev D(2022)Formal metatheory of second-order abstract syntaxProceedings of the ACM on Programming Languages10.1145/34987156:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498715
ALLAIS GATKEY RCHAPMAN JMCBRIDE CMCKINNA J(2021)A type- and scope-safe universe of syntaxes with binding: their semantics and proofsJournal of Functional Programming10.1017/S095679682000007631Online publication date: 19-Oct-2021
https://doi.org/10.1017/S0956796820000076
Eisenberg RSchrijvers T(2020)Stitch: the sound type-indexed type checker (functional pearl)Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell10.1145/3406088.3409015(39-53)Online publication date: 27-Aug-2020
https://dl.acm.org/doi/10.1145/3406088.3409015
Blanchette JGheri LPopescu ATraytel D(2019)Bindings as bounded natural functorsProceedings of the ACM on Programming Languages10.1145/32903353:POPL(1-34)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290335
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents