WG211/M10Kameyama

Staging, Effects, and Polymorphism Yukiyoshi Kameyama

Multi-stage programming is a means for run-time program generation with the assurance of safety properties such as the absence of scope extrusion (no free variables are generated). Our long-run goal is to extend the pure multi-stage calculus into a practical (full-scale) one, while keeping the safety assurance. We have been working on this
issue for several years, and obtained multi-stage calculi with control operators (to express computational effects).

In this talk, we show how polymorphism can be introduced in this setting without breaking the safety properties. The key issue is to identify a suitable condition for introducing polymorphic types. We show that so called value restriction is too restrictive in this setting, and propose a new condition which is more liberal than value restriction. We argue that our new condition allows one to express interesting examples which combine staging, computational effects via control operators, and ML-style polymorphism.