Closing the stage: From staged code to typed closures

Yukiyoshi Kameyama, Oleg Kiselyov, Chung Chieh Shan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Citations (Scopus)

Abstract

Code generation lets us write well-abstracted programs without performance penalty. Writing a correct code generator is easier than building a full-scale compiler but still hard. Typed multistage languages such as MetaOCaml help in two ways: they provide simple annotations to express code generation, and they assure that the generated code is well-typed and well-scoped. Unfortunately, the assurance only holds without side effects such as state and control. Without effects, generators often have to be written in a continuation-passing or monadic style that has proved inconvenient. It is thus a pressing open problem to combine effects with staging in a sound type system. This paper takes a first step towards solving the problem, by translating the staging away. Our source language models MetaOCaml restricted to one future stage. It is a call-by-value language, with a sound type system and a small-step operational semantics, that supports building open code, running closed code, cross-stage persistence, and non-termination effects. We translate each typing derivation from this source language to the unstaged System F with constants. Our translation represents future-stage code using closures, yet preserves the typing, α-equivalence (hygiene), and (we conjecture) termination and evaluation order of the staged program. To decouple evaluation from scope (a defining characteristic of staging), our translation weakens the typing environment of open code using a term coercion reminiscent of Goedel's translation from intuitionistic to modal logic. By converting open code to closures with typed environments, our translation establishes a framework in which to study staging with effects and to prototype staged languages. It already makes scope extrusion a type error.

Original languageEnglish
Title of host publicationPEPM'08 - Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
Pages147-157
Number of pages11
DOIs
Publication statusPublished - 2008 Dec 1
Externally publishedYes
Event2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'08 - San Francisco, CA, United States
Duration: 2008 Jan 72008 Jan 8

Publication series

NameProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation

Other

Other2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'08
CountryUnited States
CitySan Francisco, CA
Period08/1/708/1/8

Keywords

  • Closures
  • Multistage programming
  • Mutable state and control effects
  • Parametric polymorphism
  • Type abstraction

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Closing the stage: From staged code to typed closures'. Together they form a unique fingerprint.

Cite this