Abstracting gradual references
Sun 15 Nov 2020 21:00 - 21:20 at SPLASH-I - S-2 Chair(s): Atsushi Igarashi, Hidehiko Masuhara
Gradual typing is an effective approach to integrate static and dynamic typing, which supports the smooth transition between both extremes via the imprecision of type annotations. Gradual typing has been applied in many scenarios such as objects, subtyping, effects, ownership, typestates, information-flow typing, parametric polymorphism, etc. In particular, the combination of gradual typing and mutable references has been explored by different authors, giving rise to four different semantics—invariant, guarded, monotonic and permissive references. These semantics were specially crafted to reflect different design decisions with respect to precision and efficiency tradeoffs. Since then, progress has been made in the formulation of methodologies to systematically derive gradual counterparts of statically-typed languages, but these have not been applied to study mutable references.
In this article, we explore how the Abstracting Gradual Typing (AGT) methodology, which has been shown to be effective in a variety of settings, applies to mutable references. Starting from a standard statically-typed language with references, we systematically derive with AGT a novel gradual language, called λREF˜. We establish the properties of λREF˜; in particular, it is the first gradual language with mutable references that is proven to satisfy the gradual guarantee. We then compare λREF˜ with the main four existing approaches to gradual references, and show that the application of AGT does justify one of the proposed semantics: we formally prove that the treatment of references in λREF˜ corresponds to the guarded semantics, by presenting a bisimilation with the coercion semantics of Herman et al. In the process, we uncover that any direct application of AGT yields a gradual language that is not space-efficient. We consequently adjust the dynamic semantics of λREF˜ to recover space efficiency. We then show how to extend λREF˜ to support both monotonic and permissive references as well. Finally, we provide the first proof of the dynamic gradual guarantee for monotonic references. As a result, this paper sheds further light on the design space of gradual languages with mutable references and contributes to deepening the understanding of the AGT methodology.
Sun 15 NovDisplayed time zone: Central Time (US & Canada) change
21:00 - 22:20
S-2Research Papers at SPLASH-I
Chair(s): Atsushi Igarashi Kyoto University, Japan, Hidehiko Masuhara Tokyo Institute of Technology
|Abstracting gradual referencesSCICO Journal-First|
Matías Toro University of Chile, Éric Tanter University of ChileLink to publication DOI Media Attached
|Don't Panic! Better, Fewer, Syntax Errors for LR Parsers|
Lukas Diekmann King's College London, Laurence Tratt King's College LondonLink to publication DOI Pre-print Media Attached
|Blame for Null|
Abel Nieto Aarhus University, Marianna Rapoport University of Waterloo, Gregor Richards University of Waterloo, Ondřej Lhoták University of WaterlooLink to publication DOI Pre-print Media Attached
|Perfect is the Enemy of Good: Best-Effort Program Synthesis|
Hila Peleg University of California at San Diego, Nadia Polikarpova University of California at San DiegoLink to publication DOI Media Attached