Space-Efficient Monotonic References
Integrating static typing and dynamic typing has been popular in academia and industry. Gradual typing is one approach to this integration that preserves type soundness by casting values at run-time. For higher order values such as functions and references, a cast typically wraps them in a proxy that performs casts at use sites. This approach suffers from two problems: (1) chains of proxies can grow and consume unbounded space, and (2) statically typed code regions need to check whether the value being used is proxied. Monotonic references [Siek et al. 2015c] solve the latter problem for mutable references by directly casting the heap cell instead of wrapping the reference in a proxy. In this paper we show that monotonic references can also solve the former problem. We present a space-efficient version of the semantics for monotonic references and prove an upper bound on space overhead. Furthermore, the prior semantics for monotonic references involved storing cast expressions (not yet values) on the heap and it is not obvious how to implement this behavior efficiently in a compiler and run-time system. In our new semantics, only values are written to the heap, making the semantics straightforward to implement.
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30 | |||
10:30 30mTalk | Gradual Algebraic Data Types WGT Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile Pre-print File Attached | ||
11:00 30mTalk | Gradual Typing for Extensibility by Rows WGT Pre-print | ||
11:30 30mTalk | Foreign Function Typing: Semantic Type Soundness for FFIs WGT Pre-print | ||
12:00 30mTalk | Space-Efficient Monotonic References WGT Pre-print |