Sound Type-Dependent Syntactic Language Extension

Florian Lorenzen, Sebastian Erdweg

Research output: Contribution to journalArticleScientificpeer-review

38 Downloads (Pure)


Syntactic language extensions can introduce new facilities into a programming language while requiring little implementation effort and modest changes to the compiler. It is typical to desugar language extensions in a distinguished compiler phase after parsing or type checking, not affecting any of the later compiler phases. If desugaring happens before type checking, the desugaring cannot depend on typing information and type errors are reported in terms of the generated code. If desugaring happens after type checking, the code generated by the desugaring is not type checked and may introduce vulnerabilities. Both options are undesirable. We propose a system for syntactic extensibility where desugaring happens after type checking and desugarings are guaranteed to only generate well-typed code. A major novelty of our work is that desugarings operate on typing derivations instead of plain syntax trees. This provides desugarings access to typing information and forms the basis for the soundness guarantee we provide, namely that a desugaring generates a valid typing derivation. We have implemented our system for syntactic extensibility in a language-independent fashion and instantiated it for a substantial subset of Java, including generics and inheritance. We provide a sound Java extension for Scala-like for-comprehensions.
Original languageEnglish
Pages (from-to)204-216
Number of pages13
JournalACM SIGPLAN Notices
Issue number1
Publication statusPublished - 2016
EventPOPL 2016: 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - St. Petersburg, FL, United States
Duration: 20 Jan 201623 Jan 2016


  • Language extensibility
  • type soundness
  • type-dependent desugaring
  • automatic verification
  • metaprogramming
  • macros


Dive into the research topics of 'Sound Type-Dependent Syntactic Language Extension'. Together they form a unique fingerprint.

Cite this