Abstract
Many languages use syntactic sugar to define parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules, are not immediately evident. Nevertheless, IDEs, refactorers, and other tools that traffic in source code depend on these rules to present information to users and to soundly perform their operations. In this paper, we show how to lift scoping rules defined on a core language to rules on the surface, a process of scope inference. In the process we introduce a new representation of binding structure---scope as a preorder---and present a theoretical advance: proving that a desugaring system preserves α-equivalence even though scoping rules have been provided only for the core language. We have also implemented the system presented in this paper.
Supplemental Material
Available for Download
Scope inference implementation & extended version of the paper
- Peter Aczel. 1978. A General Church-Rosser Theorem. Technical Report. University of Manchester.Google Scholar
- Michael D. Adams. 2015. Towards the Essence of Hygiene. In Principles of Programming Languages. ACM, New York, NY, USA, 457–469. DOI: Google ScholarDigital Library
- Sebastian Erdweg, Tijs van der Storm, and Yi Dai. 2014. Capture-Avoiding and Hygienic Program Transformations. In European Conference on Object-Oriented Programming . Springer-Verlag, Berlin, Heidelberg, 489–514. DOI: Google ScholarDigital Library
- Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. 2002. DrScheme: A Programming Environment for Scheme. Journal of Functional Programming 12 (2002), 159–182. DOI: Google ScholarDigital Library
- David Fisher and Olin Shivers. 2006. Static Analysis for Syntax Objects. In International Conference on Functional Programming. ACM, New York, NY, USA. Google ScholarDigital Library
- Matthew Flatt. 2016. Binding as Sets of Scopes. In Principles of Programming Languages. ACM. DOI: Google ScholarDigital Library
- David Herman and Mitchell Wand. 2008. A Theory of Hygienic Macros. In European Symposium on Programming Languages and Systems . Springer-Verlag, Berlin, Heidelberg, 48–62. DOI: Google ScholarCross Ref
- R. Kelsey, W. Clinger, and J. Rees (eds.). 1998. Revised Report on the Algorithmic Language Scheme. Cambridge University Press.Google Scholar
- J. W. Klop. 1992. Term Rewriting Systems. Handbook of Logic in Computer Science (1992). DOI: Google ScholarCross Ref
- Donald E. Knuth. 1968. Semantics of Context-Free Languages. In Mathematical Systems Theory. Springer-Verlag. DOI: Google ScholarCross Ref
- Eugene Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce Duba. 1986. Hygienic Macro Expansion. In ACM Conference on LISP and Functional Programming . ACM, New York, NY, USA, 11. DOI: Google ScholarDigital Library
- Gabrie Konat, Lennart Kats, Guido Wachsmuth, and Eelco Visser. 2012. Declarative Name Binding and Scope Rules. In Software Language Engineering . Springer-Verlag, Berlin, Heidelberg, 311–331. DOI: Google ScholarCross Ref
- Florian Lorenzen and Sebastian Erdweg. 2013. Modular and Automated Type-Soundness for Language Extensions. In International Conference on Functional Programming . ACM, New York, NY, USA, 12. DOI: Google ScholarDigital Library
- Pierre Neron, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth. 2015. A Theory of Name Resolution. In European Symposium on Programming Languages and Systems . Springer-Verlag, Berlin, Heidelberg, 205–231. DOI: Google ScholarCross Ref
- Justin Pombrio and Shriram Krishnamurthi. 2014. Resugaring: Lifting Evaluation Sequences through Syntactic Sugar. In Programming Languages Design and Implementation . ACM, New York, NY, USA, 361–371. DOI: Google ScholarDigital Library
- Justin Pombrio and Shriram Krishnamurthi. 2015. Hygienic Resugaring of Compositional Desugaring. In International Conference on Functional Programming . ACM, New York, NY, USA, 75–87. DOI: Google ScholarDigital Library
- François Pottier. 2005. An Overview of C α ml. In Electronic Notes in Theoretical Computer Science. DOI: Google ScholarDigital Library
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2010. Ott: Effective Tool Support for the Working Semanticist. Journal of Functional Programming (2010). DOI: Google ScholarDigital Library
- Simon Peyton Jones. 2003. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press.Google Scholar
- Paul Stansifer and Mitchell Wand. 2014. Romeo: a System For More Flexible Binding-Safe Programming. In International Conference on Functional Programming . ACM, New York, NY, USA, 53–65. DOI: Google ScholarDigital Library
- Stephanie Weirich, Brent Yorgey, and Tim Sheard. 2011. Binders Unbound. In International Conference on Functional Programming . ACM, New York, NY, USA, 333–345. DOI: Google ScholarDigital Library
Index Terms
- Inferring scope through syntactic sugar
Recommendations
Inferring type rules for syntactic sugar
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationType systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can ...
Inferring type rules for syntactic sugar
PLDI '18Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can ...
Layout-sensitive language extensibility with SugarHaskell
Haskell '12: Proceedings of the 2012 Haskell SymposiumProgrammers 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