Syntactic sugars ease the definition of new language constructs by transforming them into an existing core language. Previous works lift independent typing rules and other semantics for these new constructs from the core language. The lifted semantics preserve the abstraction boundary of syntactic sugars, freeing users from inspecting desugared code that they did not write. While sugars may interact with contextual information during desugaring in general, these works are limited to simple sugars that do not. We identify a class of contextual sugars and present an extended algorithm for lifting their typing rules. With the addition of contexts, naïvely representing desugaring results in the core language may cause unexpected behavior and break hygiene. We introduce anchored terms that can point to the provenance of their contexts to represent desugaring results, which is similar to mechanisms used in Racket macros. Anchored terms need not concern authors or users of contextual sugars, but enable local reasoning. The lifted typing rules are sound with respect to the typing of anchored core language terms.

Syntactic sugar enhances the usability of a core language by providing intuitive syntax in a surface language; however, its interaction with the core-language type checker often results in error messages that are unclear to surface programmers. Existing techniques, such as type lifting, can automatically infer typing rules for syntactic sugar, but they do not consider localizing type errors directly in the surface syntax. This paper studies the problem of localizing and reporting type errors for syntactic sugar, addressing two key challenges: precisely localizing errors and ensuring that they are fixable. Inspired by the recently proposed marked lambda calculus (MLC), we develop ℓ MLC as our core language which tracks error provenance and locations via type annotations. Building on this, we propose the Ste llar framework, which automatically lifts the core language’s typing rules to the surface language while enabling error localization in the surface syntax. Ste llar also ensures that the reported errors are fixable by incorporating extra premises into the lifted typing rules. We implement Ste llar and evaluate it across various surface languages with different type structures, demonstrating that our approach precisely localizes errors and avoids unhelpful references to core-language constructs. Our evaluation suggests that Ste llar can help surface programmers address type errors more effectively, enhancing the practicality of syntactic sugar in language engineering.

Syntactic sugar plays a crucial role in engineering programming languages. It offers convenient syntax and higher-level of abstractions, as witnessed by its pervasive use in both general-purpose and domain-specific contexts. Unfortunately, the traditional approach of translating programs containing syntactic sugars into the host language can lead to abstraction leakage, breaking the promise of convenience and hindering program comprehension. To address this challenge, we introduce the idea of semantics lifting that aims to statically derive self-contained evaluation rules for syntactic sugars. More specifically, we propose a semantics-lifting framework that consists of (i) a general algorithm for deriving host-independent semantics of syntactic sugars from the semantics of the host language and the desugaring rules, (ii) a formulation of the correctness and abstraction properties for a lifted semantics, and (iii) a systematic investigation of sufficient conditions that ensure a lifted semantics is provably correct and abstract. To evaluate our semantics-lifting framework, we have implemented a system named Osazone and conducted several case studies, demonstrating that our approach is flexible, effective, and practical for implementing domain-specific languages.