Abstract:
A type-preserving compiler converts a well-typed input program into a well-typed output program. Previous studies have developed type-preserving compilers for various source languages, including the simply-typed lambda calculus and calculi with control constructs. Our goal is to realize type-preserving compilation of languages that have facilities for manipulating first-class continuations. In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations. Specifically, we choose an effect handler calculus and a typed stack-machine-based assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler. The main challenge posed by first-class continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks. We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without first-class continuations to a stack-based assembly language. To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs. We believe that our contributions could lead to correct and efficient compilation of continuation-manipulating facilities in general.
Reference:
An Intrinsically Typed Compiler for Algebraic Effect Handlers (Syouki Tsuyama, Youyou Cong and Hidehiko Masuhara), In Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation (PEPM 2024), ACM, 2024.
Bibtex Entry:
@inproceedings{tsuyama2024pepm,
author = {Syouki Tsuyama and Youyou Cong and Hidehiko Masuhara},
title = {An Intrinsically Typed Compiler for Algebraic Effect Handlers},
year = {2024},
isbn = {9798400704871},
publisher = {{ACM}},
address = {New York, NY, USA},
url = {https://popl24.sigplan.org/details/pepm-2024/1/An-Intrinsically-Typed-Compiler-for-Algebraic-Effect-Handlers},
doi = {10.1145/3635800.3636968},
abstract = {A type-preserving compiler converts a well-typed input program into a well-typed output program.
Previous studies have developed type-preserving compilers for various source languages,
including the simply-typed lambda calculus and calculi with control constructs.
Our goal is to realize type-preserving compilation of languages that have facilities for manipulating first-class continuations.
In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations.
Specifically, we choose an effect handler calculus and a typed stack-machine-based assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler.
The main challenge posed by first-class continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks.
We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without first-class continuations to a stack-based assembly language.
To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs.
We believe that our contributions could lead to correct and efficient compilation of continuation-manipulating facilities in general.},
booktitle = {Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation (PEPM 2024)},
pages = {134–145},
numpages = {12},
pdf = {pepm2024-paper.pdf},
slides = {pepm2024-slide.pdf},
month = jan
}