Programming Languages

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.

This publication is related to the Effekt: Algebraic Effect Handlers research project.

Abstract

A well known technique to implement a programming language with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to implement a family of control operators shift_i and 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.

News

Shonan Meeting on Programming and Reasoning with Algebraic Effects and Effect Handlers

Philipp Schuster
Researcher
Philipp Schuster
attends the Shonan meeting on “Programming and Reasoning with Algebraic Effects and Effect Handlers” from March 25 to 29, 2019.

Read more ...

Presentation at Type-Driven Development 2018

Philipp Schuster
Researcher
Philipp Schuster
presents the functional pearl Typing, Representing, and Abstracting Control at Type-Driven Development 2018.

Read more ...