Type-Safe Code Generation With Algebraic Effects and HandlersDistinguished Research Paper Award
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 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.
Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | Session 3 on Code OptimizationsGPCE at San Marino Chair(s): Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) | ||
14:00 30mTalk | Type-Safe Code Generation With Algebraic Effects and HandlersDistinguished Research Paper Award GPCE Kanaru Isoda University of Tsukuba, Ayato Yokoyama University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba | ||
14:30 30mTalk | Hot Call-Chain Inlining for the Glasgow Haskell Compiler GPCE | ||
15:00 30mTalk | Restaging Domain-Specific Languages: A Flexible Design Pattern for Rapid Development of Optimizing Compilers GPCE Amir Shaikhha University of Edinburgh |