Staged computation with staged lexical scope

Abstract

We present a simple core type system, λ [ ] - pronounced "lambda open box" - for a statically typed, hygienic, and multi-stage lambda-calculus supporting evaluation under future-stage binders, open-code manipulation, a first-class eval function, and mutable state. The type system provides one type of lexically scoped code that precisely accounts for the contexts in which code values can be inserted. In particular, this type can distinguish between open and closed code. We show how to extend λ [ ] with subtype polymorphism over program contexts. The soundness and simplicity of λ [ ] demonstrate that the notion of staging is orthogonal to features that have been presented as instrumental in existing type systems for staged computation, such as polymorphism, nameless term representations, explicit substitutions, and delimited continuations. © 2012 Springer-Verlag.