WG211/M11Rhiger

A lexically scoped type system for multi-stage languages by Morten Rhiger

Static type systems for multi-stage programming languages must guarantee that well-typed programs only generate, combine, and execute code values that are themselves well typed.

We present "lambda open box", a simple core type system for a statically typed, hygienic, multi-stage lambda-calculus that supports 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. This type system demonstrates that alpha-equivalence is compatible with code types that carry type environments.

We then outline a general polymorphic extension to lambda open box that provides a significant increase in expressiveness. We compare the resulting polymorphic type system to existing multi-stage calculi.