Languages and systems for staged programming: Design and implementation

 
Strictly speaking, program specialization and generation do not require dedicated languages or systems: after all, one can generate code with mere printf. The experience with printf, however, has not been pleasant: even keeping the generated code syntactically correct has been a struggle -- let alone figuring out what went wrong when that code fails to compile. Staged programming languages ensure by design not only that the generated code is syntactically well-formed, but also that all its variables are bound -- to their intended binders. When the object language is typed, staged systems also statically guarantee that a well-typed generator produces only well-typed code. Providing such assurances, well-scopedness in particular, is not easy: Lisp-like quasiquotation alone does not suffice. Practical staging systems also offer code-generating facilities beside code templates, such as cross-stage persistence and code movement (e.g., let-insertion).

 

Tagless-Staged: Combinators for Impure yet Hygienic Code Generation

We present a combinator library to write (Haskell) programs that generate code in a subset of Haskell, OCaml, or other target language. The library embeds an extensible typed higher-order domain-specific language. It statically assures not only that all generated code is well-formed and well-typed but also that all generated variables are bound as expected. Such assurances are crucial for code generators to be written by domain experts rather than compiler writers; after all, the most profitable optimizations are domain-specific ones. These static guarantees are maintained in the presence of arbitrary effects, including IO. Effects are indispensable in code generators, to report failures, to generate alternatives to choose the fastest from, to introduce auxiliary variables, to interchange loops, etc.

Our framework is not a an experimental language with a new syntax and uncertain future. Rather, it is a regular, not a bleeding edge, library in mature Haskell. It is modular and extensible: one can add to the target language more features and constants or change it to be typed or untyped, first- or higher-order. Polymorphism over generated environments makes generators composable. The higher-order abstract syntax used in the library makes target functions and variables human-readable. Our library may be regarded as `staged Haskell'.

There are many code generation frameworks with one or the other of the features. Ours has all of them. Template Haskell, among other systems, falls short, assuring -- dynamically rather than statically -- the well-typedness of only the final code. Furthermore, although the generated code, after a type-check, is well-typed, it may still be ill-scoped.

The static types of our generator expressions not only ensure that a well-typed generator produces well-typed and well-scoped code. They also express the lexical scopes of generated binders and prevent mixing up variables with different scopes. For the first time we demonstrate, in an embedded domain-specific language, statically safe and well-scoped loop interchange and constant factoring from arbitrarily nested loops.

Joint work with Yukiyoshi Kameyama and Chung-chieh Shan.

Version
The current version is October 2015
References
beyond.pdf [412K]
Combinators for Impure yet Hygienic Code Generation
Science of Computer Programming, Volume 112, Part 2, 15 November 2015, pp. 120–144. doi:10.1016/j.scico.2015.08.007

beyond-talk.pdf [193K]
The annotated slides of the talk presented at PEPM 14 on January 20, 2014 in San Diego, CA, USA

Region Memory Management for Free Variables: Type- and Scope-Safe Code Generation with Mutable Cells
The formalization of one part of the combinator library, as the calculus <NJ>

TSCore.hs [29K]
The core of the code generation library
TSCPST.hs [17K]
Code generation with control effects reaching beyond the closest binder. Far-reaching let-insertion. The implementation of the CPSA applicative hierarchy.

Examples and Sample code

 

Typed Template Haskell is still not quite sound

Typed Template Haskell was introduced to guarantee that the generated code is well-typed by construction. In particular, splicing the generated code into the program being compiled should never give any type error. Alas, to make Typed Template Haskell more capable and expressive, side effects were allowed during the code generation. As a consequence, one could produce code with unbound variables, as we demonstrate below. Typed Template Haskell hence is ultimately unsound.

The original Template Haskell (Haskell Workshop, 2002) is essentially untyped, with no guarantees that the generated code is any good, or even well-typed. Writing code generators was akin to programming in `dynamically typed' languages: although we can easily tell that the fully generated program is untypable (because it cannot be compiled), we cannot easily point out which part of the generator was to blame. The dissonance with the type discipline of Haskell is jarring. On the other hand, Template Haskell is very expressive: it generates not only expressions but also definitions, type declarations, classes and instances, etc. -- all sort of things that may appear in Haskell code. Designing a type system for such broad code generation was, and still is, a great challenge.

Against this background, Typed Template Haskell was introduced. It produces code only for expressions (and not for declarations, etc.). On the other hand, we can finally write typed generators. Typed Template Haskell is quite similar to the lambda-circle calculus or MetaOCaml, but restricted to two levels. Here is the sample typed generator.

    t1 :: Q (TExp Int)
    t1 = do
      c1 <- [|| (1::Int) + 2 ||]
      c2 <- [|| 3 + $$(return c1) ||]
      return c2
As in MetaOCaml, the type of code values TExp is indexed by the type of the expression to be generated. [|| ... ||] is the typed antiquotation, corresponding to the brackets .< ... >. of MetaOCaml. The brackets enclose, or quote, the code to generate, which must be a well-typed expression. The unquotation, or typed splice, is $$( ... ). The splice is evaluated and must produce (a possibly open) code, which is then spliced into the enclosing typed quotation. If the splice appears outside a quotation, it is called top-level. In that case, the splice must produce a closed expression, which is inserted into the code being compiled. The sample generator t1 produces the following code:
    3 GHC.Num.+ ((1 :: GHC.Types.Int) GHC.Num.+ 2)
or, hiding the module qualifications, 3 + (1 + 2).

The problematic example is very short:

    t2 :: Q (TExp Int)
    t2 = do
      r <- runIO $ newIORef undefined
      c1 <- [|| \x -> (1::Int) +
                      $$(do
                         xv <- [||x||]
                         runIO $ writeIORef r xv
                         return xv) ||]
      runIO $ readIORef r
It generates x_0: just the single, unbound variable. It is clearly not typable. Such code cannot be compiled or spliced-in at the top level. The culprit is runIO, which runs IO computations from within typed splices. It is highly desirable, for error handling and many other reasons. It is also responsible for breaking type soundness.

Once again we see the tension between safety and expressiveness. Without effects, we cannot generate all the code we want and cannot handle errors well. With side effects, maintaining type safety is a challenge. Fortunately, the challenge has recently been met, outside GHC and Typed Template Haskell.

The problem sprang to attention during the lecture by Simon Peyton Jones at the First Metaprogramming Summer School in Cambridge, UK in August 2016 -- when runIO was mentioned.

Version
The current version is August 2016
References
THProblem.hs [<1K]
The complete Haskell code illustrating the problem

Tagless-Staged: Combinators for Impure yet Hygienic Code Generation
Type sound code generation with arbitrary side-effects

MetaOCaml resolves the tension between expressiveness and safety in a different, easy to implement way

 

MetaScheme, or untyped MetaOCaml

We implement the four MetaOCaml special forms -- bracket, escape, cross-stage persistence (aka `lift'), and run -- in R5RS Scheme. A Scheme system thus becomes untyped MetaOCaml, in which we can write and run code with an arbitrary number of stages. We point out how distinct the staging annotations are from Scheme's quasiquotation, despite superficial similarity. Our implementation of cross-stage persistent (CSP) values closely corresponds to the one in MetaOCaml and so helps explain the latter.

Here is a sample MetaOCaml code and its Scheme translation

    # let eta = fun f -> .<fun x -> .~(f .<x>.)>.
      in .<fun x -> .~(eta (fun y -> .<x + .~y>.))>.
    - : (int -> int -> int) code = .<fun x_1 -> fun x_2 -> (x_1 + x_2)>.
  
   (let ((eta (lambda (f) (bracket (lambda (x) (escape (f (bracket x))))))))
      (bracket (lambda (x) (escape (eta (lambda (y) (bracket (+ x (escape y)))))))))
Translating MetaOCaml code into Scheme seems trivial: code values are like S-expressions, MetaOCaml's bracket is like quasiquote, escape is like unquote, and `run' is eval. If we indeed replace bracket with the quasiquote and escape with the unquote in the above Scheme code and then evaluate it, we get the S-expression (lambda (x) (lambda (x) (+ x x))), which is a wrong result, quite different from the code expression .<fun x_1 -> fun x_2 -> (x_1 + x_2)>. produced by MetaOCaml. The latter is the code of the curried function that adds two integers. The S-expression produced by the naive Scheme translation represents the curried function that disregards the first argument and doubles the second. This demonstrates that the often mentioned `similarity' between the bracket and the quasiquote is flawed. MetaOCaml's bracket respects alpha-equivalence; in contrast, Scheme's quasiquotation, being the general form for constructing arbitrary S-expressions (not necessarily representing any code), is oblivious to the binding structure.

Our implementation still uses S-expressions for code values (so we can print them and eval-uate them) and treats escape as unquote. To maintain the hygiene, we need to make sure that every run-time evaluation of a bracket form such as (bracket (lambda (x) x)) gives '(lambda (x_new) x_new) with the unique bound variable x_new. Two examples in the source code demonstrate why the static renaming of manifestly bound identifiers is not sufficient. We implement the very clever suggestion by Chung-chieh Shan and represent a staged expression such as .<(fun x -> x + 1) 3>. by the sexp-generating expression `(,(let ((x (gensym))) `(lambda (,x) (+ ,x 1))) 3) which evaluates to the S-expression ((lambda (x_1) (+ x_1 1)) 3). Thus bracket is a complex macro that transforms its body to the sexp-generating expression, keeping track of the levels of brackets and escapes. The macro bracket is implemented as a CEK machine with the defunctionalized continuation. In our implementation, the Scheme translation of the eta-example yields the S-expression (lambda (g6) (lambda (g8) (+ g6 g8))). Just as in MetaOCaml, the result represents the curried addition.

CSP poses another implementation problem. In MetaScheme we can write the MetaOCaml expression .<fun x -> x + 1>. as (bracket (lambda (x) (+ x 1))), which yields the S-expression (lambda (g1) (+ g1 1)). When we pass this code to eval, the identifier + will be looked up in the environment of eval, which is generally different from the environment that was in effect when the original bracket form was evaluated. That might not look like much of a difference since + is probably bound to the same procedure for adding numbers in either environment. This is no longer the case if we take the following MetaOCaml code and its putative MetaScheme translation:

    let test = let id u = u in
                  .<fun x -> id x>.
   
    (define test (let ((id (lambda (u) u)))
                   (bracket (lambda (x) (id x)))))
The latter definition binds test to the S-expression (lambda (x) (id x)) that contains the free identifier id, unlikely to be bound in the environment of eval. Our code values therefore should be `closures', being able to include values that are (possibly locally) bound in the environment when the code value was created. Incidentally, the problem of code closures closed over the environment of the generator also appears in syntax-case macros. R6RS editors made a choice to prohibit the occurrence of locally-bound identifiers in the output of a syntax-case transformer.

MetaOCaml among other staged systems does permit the inclusion of values from the generator stage in the generated code. Such values are called CSP; they are evident in the output of the MetaOCaml interpreter for the above test:

    val test : ('a -> 'a) code =
    .<fun x_1 -> (((* cross-stage persistent value (as id: id) *)) x_1)>.
In MetaScheme, we have to write CSP explicitly: (% e), which is often called `lift'.
    (define test
      (let ((id (lambda (u) u)))
        (bracket (lambda (x) ((% id) x)))))
One may think that such a lifting is already available in Scheme: (define (lift x) (list 'quote x)). Although this works in the simple cases of x being a number, a string, etc., it is neither universal nor portable: attempting this way to lift a closure or an output-port could be an error. According to R5RS, the argument of a quotation is an external representation of a Scheme datum. Closures, for example, are not guaranteed to have an external representation. For portability, we implement CSP via a reference in a global array, taking advantage of the fact that both the index (a number) and the name of the array (an identifier) have external representations and hence are trivially liftable by quotation. This is precisely the mechanism once used by MetaOCaml.

The source code contains many more examples of the translation of MetaOCaml code into MetaScheme -- including the examples with many stages and CSP.

Joint work with Chung-chieh Shan.

Version
The current version is 1.4, Aug 20, 2008
References
meta-scheme.scm [15K]
The complete implementation with many comments. It should work with any R5RS Scheme system. The code has been tested with Scheme 48 1.3, SCM 5e1, and Petite Chez Scheme 6.0a.