Presentation at Type-Driven Development 2018
AlumniPhilipp Schuster presents the functional pearl Typing, Representing, and Abstracting Control at Type-Driven Development 2018.
A well known technique to implement a programming language with delimited control operators
reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to implement a family of control operators
reset_i . 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. In contrast, we allow different parts of the program to live at different levels. It turns out that taking
shift_0 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. Guided by the types, the translation applies well known techniques to avoiding administrative beta- and eta-redexes at all levels of the CPS hierarchy.
Typing, Representing, and Abstracting Control: Functional Pearl
by Philipp Schuster and Jonathan Brachthäuser
In Proceedings of the International Workshop on Type-Driven Development. ACM Press, 2018.Learn More