Log in

No account? Create an account


Typing, Representing, and Abstracting Control

Typing, Representing, and Abstracting Control

Previous Entry Share Next Entry

Typing, Representing, and Abstracting Control

Philipp Schuster and Jonathan Immanuel Brachthäuser, University of Tübingen, Germany

Abstract 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
Powered by LiveJournal.com