Type-Safe Code Generation with Algebraic Effects and Handlers

Abstract

Staged computation is a means to achieve maintainability and high performance simultaneously, by allowing a programmer to express domain-specific optimizations in a high-level programming language. Multi-stage programming languages such as MetaOCaml provide a static safety guarantee for generated programs by sophisticated type systems provided that program generators have no computational effects. Despite several studies, it remains a challenging problem to design a type-safe multi-stage programming language with advanced features for computational effects. This paper introduces a two-stage programming language with algebraic effects and handlers. Based on two novel principles 'handlers as future-stage binders' and 'handlers are universal', we design a type system and prove its soundness. We also show that our language is sufficiently expressive to write various effectful staged computations including multi-level let-insertion, which is a key technique to avoid code duplication in staged computation.