Multi-stage programming with explicit annotations
- 1 December 1997
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 32 (12) , 203-217
- https://doi.org/10.1145/258993.259019
Abstract
We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize those published previously [25, 12, 7, 6]We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages.We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages.A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.Keywords
This publication has 14 references indexed in Scilit:
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- A type-directed, on-line, partial evaluator for a polymorphic languagePublished by Association for Computing Machinery (ACM) ,1997
- Monadic statePublished by Association for Computing Machinery (ACM) ,1997
- Reasoning about hierarchies of online program specialization systemsPublished by Springer Nature ,1996
- The essence of eta-expansion in partial evaluationHigher-Order and Symbolic Computation, 1995
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994
- Efficient self-interpretation in lambda calculusJournal of Functional Programming, 1992
- A partial evaluator for the untyped lambda-calculusJournal of Functional Programming, 1991
- Computing with rewrite systemsInformation and Control, 1985
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975