-
Continuing WebAssembly with Effect Handlers
Authors:
Luna Phipps-Costin,
Andreas Rossberg,
Arjun Guha,
Daan Leijen,
Daniel Hillerström,
KC Sivaramakrishnan,
Matija Pretnar,
Sam Lindley
Abstract:
WebAssembly (Wasm) is a low-level portable code format offering near native performance. It is intended as a compilation target for a wide variety of source languages. However, Wasm provides no direct support for non-local control flow features such as async/await, generators/iterators, lightweight threads, first-class continuations, etc. This means that compilers for source languages with such fe…
▽ More
WebAssembly (Wasm) is a low-level portable code format offering near native performance. It is intended as a compilation target for a wide variety of source languages. However, Wasm provides no direct support for non-local control flow features such as async/await, generators/iterators, lightweight threads, first-class continuations, etc. This means that compilers for source languages with such features must ceremoniously transform whole source programs in order to target Wasm. We present WasmFX, an extension to Wasm which provides a universal target for non-local control features via effect handlers, enabling compilers to translate such features directly into Wasm. Our extension is minimal and only adds three main instructions for creating, suspending, and resuming continuations. Moreover, our primitive instructions are type-safe providing typed continuations which are well-aligned with the design principles of Wasm whose stacks are typed. We present a formal specification of WasmFX and show that the extension is sound. We have implemented WasmFX as an extension to the Wasm reference interpreter and also built a prototype WasmFX extension for Wasmtime, a production-grade Wasm engine, piggybacking on Wasmtime's existing fibers API. The preliminary performance results for our prototype are encouraging, and we outline future plans to realise a native implementation
△ Less
Submitted 13 September, 2023; v1 submitted 16 August, 2023;
originally announced August 2023.
-
Soundly Handling Linearity
Authors:
Wenhao Tang,
Daniel Hillerström,
Sam Lindley,
J. Garrett Morris
Abstract:
We propose a novel approach to soundly combining linear types with effect handlers. Linear type systems statically ensure that resources such as file handles are used exactly once. Effect handlers provide a modular programming abstraction for implementing features ranging from exceptions to concurrency. Whereas linear type systems bake in the assumption that continuations are invoked exactly once,…
▽ More
We propose a novel approach to soundly combining linear types with effect handlers. Linear type systems statically ensure that resources such as file handles are used exactly once. Effect handlers provide a modular programming abstraction for implementing features ranging from exceptions to concurrency. Whereas linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded or invoked more than once. This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs.
We formalise control flow linearity in a System F-style core calculus Feffpop equipped with linear types, effect types, and effect handlers. We define a linearity-aware semantics to formally prove that Feffpop preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control flow linearity can be made practical, we adapt Links based on the design of Feffpop, in doing so fixing a long-standing soundness bug.
Finally, to better expose the potential of control flow linearity, we define an ML-style core calculus Qeffpop, based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control flow linearity. Both linearity and effects are captured by qualified types. Qeffpop overcomes a number of practical limitations of Feffpop, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control flow linearity.
△ Less
Submitted 2 January, 2024; v1 submitted 18 July, 2023;
originally announced July 2023.
-
Structural Subty** as Parametric Polymorphism
Authors:
Wenhao Tang,
Daniel Hillerström,
James McKinna,
Michel Steuwer,
Ornela Dardha,
Rongxiao Fu,
Sam Lindley
Abstract:
Structural subty** and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literat…
▽ More
Structural subty** and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature.
In this paper, we systematically study the relative expressive power of structural subty** and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subty** for variant and record types. We base our study on various Church-style $λ$-calculi extended with records and variants, different forms of structural subty**, and row and presence polymorphism.
We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subty** cannot be encoded via polymorphism, but we show that several restricted forms of subty** can be encoded via particular forms of polymorphism.
△ Less
Submitted 11 September, 2023; v1 submitted 17 April, 2023;
originally announced April 2023.
-
Effects for Efficiency: Asymptotic Speedup with First-Class Control
Authors:
Daniel Hillerström,
Sam Lindley,
John Longley
Abstract:
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language $λ_b$ and its extension with effect handlers $λ_h$. We show that $λ_h$ admits an asymptotically more efficient implementation of generic…
▽ More
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language $λ_b$ and its extension with effect handlers $λ_h$. We show that $λ_h$ admits an asymptotically more efficient implementation of generic count than any $λ_b$ implementation. We also show that this efficiency gap remains when $λ_b$ is extended with mutable state. To our knowledge this result is the first of its kind for control operators.
△ Less
Submitted 13 July, 2020; v1 submitted 1 July, 2020;
originally announced July 2020.
