![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
xacidCapability-Passing Style for Zero-Cost Effect Handlers
http://ps.informatik.uni-tuebingen.de/publications/schuster20capability.pdf
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
We present a language for effect handlers in capability-passing style (λCap) and an implementation of this language as a translation to simply-typed lambda calculus in iterated continuation-passing style. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is very general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λCap to λCap with a more restrictive type system. We present a type-directed translation for λCap that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
Zero-cost Effect Handlers by Staging (Technical Report)
http://ps.informatik.uni-tuebingen.de/publications/schuster19zero.pdf
Effect handlers offer ways to structure programs with complex control-flow patterns. Yet, current imple- mentations of effect handlers incur a significant price in performance for doing so. We present a language that makes it possible to eliminate the overhead introduced by using effect handlers to abstract over effect operations. We present a translation of this language to simply typed lambda calculus in continuation passing style that preserves the well-typedness of terms. We present a second translation that, guided by automatically inserted staging annotations, guarantees to eliminate abstractions and applications related to effect handlers. We implement the translations and generate code in multiple languages. We validate the efficiency of the generated code theoretically, by proving that the use of certain language constructs never leads to run-time reductions, and practically, with a suite of benchmarks comparing with existing implementations of effect handlers and control operators.
Typing, Representing, and Abstracting Control
http://ps.informatik.uni-tuebingen.de/publications/schuster18typing.pdf
A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti . This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation.
http://ps.informatik.uni-tuebingen.de/publications/schuster20capability.pdf
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
We present a language for effect handlers in capability-passing style (λCap) and an implementation of this language as a translation to simply-typed lambda calculus in iterated continuation-passing style. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is very general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λCap to λCap with a more restrictive type system. We present a type-directed translation for λCap that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
Zero-cost Effect Handlers by Staging (Technical Report)
http://ps.informatik.uni-tuebingen.de/publications/schuster19zero.pdf
Effect handlers offer ways to structure programs with complex control-flow patterns. Yet, current imple- mentations of effect handlers incur a significant price in performance for doing so. We present a language that makes it possible to eliminate the overhead introduced by using effect handlers to abstract over effect operations. We present a translation of this language to simply typed lambda calculus in continuation passing style that preserves the well-typedness of terms. We present a second translation that, guided by automatically inserted staging annotations, guarantees to eliminate abstractions and applications related to effect handlers. We implement the translations and generate code in multiple languages. We validate the efficiency of the generated code theoretically, by proving that the use of certain language constructs never leads to run-time reductions, and practically, with a suite of benchmarks comparing with existing implementations of effect handlers and control operators.
Typing, Representing, and Abstracting Control
http://ps.informatik.uni-tuebingen.de/publications/schuster18typing.pdf
A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti . This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation.
