Refined Environment ClassifiersType- and Scope-safe Code Generation with Mutable Cells
Oleg Kiselyov, Yukiyoshi Kameyama, and Yuto Sudo
1

2

Tohoku University oleg@okmij.org
University of Tsukuba kameyama@acm.org

Abstract. Generating high-performance code and applying typical optimizations within the bodies of loops and functions involves moving or
storing open code for later use, often in a different binding environment.
There are ample opportunities for variables being left unbound or accidentally captured. It has been a tough challenge to statically ensurethat by construction the generated code is nevertheless well-typed andwell-scoped : all free variables in manipulated and stored code fragments
shall eventually be bound, by their intended binders.
We present the calculus for code generation with mutable state that for
the first time achieves type-safety and hygiene without ad hoc restrictions. The calculus strongly resembles region-based memory management, but with the orders of magnitude simpler proofs. It employs therightly abstract representation for free variables, which, like hypothesis
in natural deduction, are free from the bureaucracy of syntax imposedby the type environment or numbering conventions.
Although the calculus was designed for the sake of formalization and isdeliberately bare-bone, it turns out easily implementable and not too
bothersome for writing realistic program.

1

Introduction

Code generation exhibits the all-too-common trade-off: obtaining code with thehighest performance; statically ensuring the code quality; being able to use thecode-generating system in practice – choose two. Optimizing compilers and many
practical code-generating tools do all desired optimizations. The correctness of
the result is ensured however only by careful programming. This is not a problem
in case of a compiler written by a small team of experts and changed relatively
infrequently. The lack of static assurances is worrisome for code transformationand generation libraries written by domain experts, who have less time to devote
to proofs and have to continually tune their libraries to the domain knowledge
and circumstances. There is the attested danger of generating code with unbound, or worse, unexpectedly bound variables. At the very least, we would liketo guarantee that the generated code – at all times, even the code fragments – iswell-formed, well-typed, and all of its free variables will eventually be bound by
their intended binders. This guarantee should hold before we compile the generated code, which is typically unfit for human reading. Ideally, the guarantee
should hold even before we compile the generator.

2

On the other side of the trade-off are the staged calculi such as λ◦ and λα[1, 2] that express code generators with the desired static guarantees. They arecalled ‘staged’ because evaluation is stratified: the result of the present, or Level0, stage is the code to be evaluated at the next, Level-1, or future stage. The
calculi have been implemented as full-featured staged languages used in practice[3, 4]. Another example is Pouillard’s [5] code generation and analysis librarywith proven correctness. Alas, all these systems restrict the range of safe operations on open code: in particular, they limit or outlaw the operations thatmove or store open code, retrieving it later in a different binding environment.
Such operations are required for many optimizations such as let-insertion, memoization, loop interchange and tiling. There have been general approaches that
permit the desired open code motions and provide static guarantees: for example, [6]. Alas, they are too complex to use in practice or even to implement. For
more discussion, see §5 and especially [7].
StagedHaskell [7] overcomes the impasse, but partially. It is the library forcode generation that supports code movements, including movements via any
computational (monadic) effect. Using a contextual modal type system, thelibrary statically assures that at all times the generated code is well-formed,
well-typed and well-scoped : all free variables in manipulated and stored codefragments shall eventually be bound by their intended binders. However, thesafety properties have been argued only informally. The main reason is thatthe complexity of the Haskell implementation, specifically, the encoding of thecontextual modal type system, make the formal reasoning difficult.
The present paper takes the first step of formalizing StagedHaskell: it distills
the staged calculus <NJ> that safely permits open code movements across different binding environments via mutable cells. The calculus can express realistic
examples from StagedHaskell, such as the assert-insertion, see §4.
Although <NJ> was motivated by code generation with safety guarantees,
it turned a vantage point to view seemingly unrelated areas. First, there is anuncanny similarity between generating code of functions (or other blocks withlocal binders) and region-based memory management. Preventing the ‘extrusion’of free variables out of the bodies of generated functions is similar to keeping
reference cells allocated within a region from leaking out. We have consciously
used this similarity, adapting techniques from region calculi [8].
The key to ensuring hygiene and type safety when manipulating open code isreflecting free variables of a code fragment in its type – which evokes contextual
modal type theory [9] and, in general, sequent calculus. The structural rules
such as weakening now turn up in programs, e.g., as ‘shifts’ of De Bruijn indices[10]. After all, in metaprogramming, meta-level becomes the object level. ‘The
bureaucracy of syntax’ now worries not only logicians but also programmers.
A particularly elegant method to overcome the complexities and redundancies of concrete name and environment representations is environment classifiers[2] (recalled and discussed in §3.2). A single classifier represents a set of freevariables, abstracting from their order, quantity, or names. Unfortunately, in thepresence of effects, the original environment classifiers are too coarse, abstracting

3

away the information needed to ensure the type safety of effectful generators.
Inspired by the concept of local assumptions from Natural Deduction NJ, we
have identified the minimal necessary refinement of environment classifiers.
Contributions Our specific contributions are as follows:– Practical two-stage calculus <NJ> whose type system statically ensures hygiene and the type-safety of the generated code in the presence of mutablereference cells. The calculus distills the design of the practical StagedHaskell
library. The calculus itself is easily implementable.
– Refinement of environment classifiers – imposing partial order – that preserves all their simplicity and advantages and is compatible with effects.
<NJ> is close to the current MetaOCaml [3], which permits leaking of variables (scope extrusion) but raises a run-time error at the moment the code withleaked (extruded) variables is about to be used. Our calculus prevents such errors
statically.
The calculus has been implemented as a simple embedding in OCaml, whosetype checker checks <NJ> types and even infers them. Signatures are only needed
for functions that receive code values as arguments and use them in distinct
binding environments. One is immediately reminded of MLF [11]; this is not an
accident, as we shall see in §3.3. All examples in the paper are slightly reformatted running code. The implementation, with more examples, is available at
http://okmij.org/ftp/tagless-final/TaglessStaged/metaNJ.ml.
This paper is organized as follows: The next section introduces the calculus,
using many examples to illustrate its syntax and dynamic semantics. §3 describes the type systems and proves its soundness. §3.1 specifically demonstrates
the obvious and very subtle dangers arising from storing open code in mutable
cells, and how <NJ> prevents the dangers but not the free use of reference cells.
Responsible for this are refined environment classifiers; §3.2 discusses what, why
and how. §4 shows off a complex example: It is used exactly as was explainedin [7], deliberately to demonstrate that <NJ> is capable of representing practical
StagedHaskell examples.

2<NJ>, its Syntax and Semantics

Formally, the syntax of <NJ> is defined in Fig. 1. This section introduces thecalculus and its dynamic semantics more accessibly, on a series of small examples.
<NJ> is a lambda-calculus with reference cells and special constants to create
and combine code values. Whereas 1 : int is the familiar constant of the base typeint, cint 1 is an expression of the code type hintiγ which evaluates to h1i. The
code types are explained in §3. Here, cint is a special code-generating constant,also called code combinator3 [12, 13]. We underline all such constants. Likewise,cbool true evaluates to htruei. Since the cint and cbool expressions are common
3

The StagedHaskell library, the prototype of <NJ>, is a code-combinator library.

4

we adopt the abbreviated notation % that stands for either constant, dependingon the context.
The bracketed expressions like h1i cannot appear in source programs; theycome only during and as the result of reductions. This is the most visible distinction from stage calculi like λα [2] and MetaOCaml. Neither do we have ‘splicing’(or, ‘escape’, unquotation). Bracketed expressions are essentially constants: theycannot be decomposed, inspected, or substituted into. Only a subset of expressions may be bracketed: underlined constants and the brackets themselves are
excluded. <NJ> therefore is the two-stage calculus, for generating code but not
for generating code generators4 . We will sometimes use the superscript e1 to emphasize the distinction between the host language and the generated language.
Most of the time the superscript is elided for ease of notation.
Figure 2 defines the constants of <NJ>. They come in different arities. Seenearlier 1 and true are zero-ary constants, denoted as c0 in Fig. 1. On the other
hand, cint and cbool have the arity 1, and are not considered expressions per se:
only their applications to one argument are expressions, see Fig. 1. Likewise, + isan arity-2 constant, requiring two arguments to be regarded as an expression. We
write such an expression in the conventional infix notation 1+2, which evaluates
to 3. Besides cint and cbool, there are constants that combine already built codevalues: %1 + %2 of the code type hintiγ evaluates as follows according to therules of Fig. 3 and 4.
%1 + %2

h1i + %2

h1i + h2i

h1+2iHere, + is an arity-2 constant, which we also write in infix. Again, all constants
must be fully applied: there are no partial applications, sections, or other sugar.
<NJ> is the lambda-calculus, with the standard abstractions λx. e and applications e1 e2 . We let let x = e1 in e2 stand as the abbreviation for (λx. e2 ) e1 ,and e1 ; e2 for let x = e1 in e2 where x does not appear free in e2 . The semantics
of <NJ> is the standard small-step left-to-right call-by-value, see Fig. 3. (Heaps
will be explained later on and can be ignored for now). <NJ> can also generate
the code of functions, using the expression form λx. e with peculiar semantics,
which we explain in detail. For example, the expression λx. x + %3 eventually
generates the code of the function that increments its argument by 3:
λx. x + %3

λy.hyi + %3

λy.hyi + h3i

λy.hy+3ihλy. y+3i

First, the expression λx. x + %3 reduces by choosing a fresh variable name y,
replacing all free occurrences of x in its body with hyi and wrapping the resultin λy. (Expressions of the form λy.e come up during the evaluation and do notappear in source programs.) Next, the body of thus built λy.hyi + %3 reduces as
described earlier. The final reduction in the sequence builds the resulting code.
Thus producing the code for functions has two separate phases: generating thename for the bound variable, and generating the binder for that name at the4This restriction certainly simplifies the formalism. It is also realistic: in all our experience of using MetaOCaml, the multi-stage language, we are yet to come across any
real-life example needing more than two stages. Template Haskell is also two-stage.

5

end. In many staged calculi the two phases can be (and are) combined. The
effects force them apart however, as we shall see soon.
Variables
Classifier
Location
Types
Level 1 Types

x,y,z,u,f,n,r. . .
γlt ::= int | bool | t → t | t ref | htiγ
t1 ::= int | bool | t1 → t1 | t1 refe ::= x | l | c0 | c1 e | c2 e e | c3 e e e | λx. e | λx. e | e e| if e then e else e
λx. e | he1 iInternal Expressions
Level 1 Expressions e1 ::= e without code combinators, internal expressions, locationsv ::= c0 | l | λx. e | hei
ValuesLevel 0 Expressions

Fig. 1. Syntax of <NJ>. The constants ci with their arities i are defined in Fig. 2.
Arity 0
1,2,3, . . . : int
true, false : bool
Arity 1
int → h int iγ
cint :
cbool: bool → hbooliγ
fix : ((t1 →t2 )→(t1 →t2 ))→(t1 →t2 )fix : h(t1 →t2 )→(t1 →t2 )iγ → ht1 →t2 iγ!:
ht refiγ → htiγ
ref : t → t ref
ref : htiγ → ht refiγ

Arity 2+: int → int → int+: h int iγ → hintiγ → hintiγ=: int → int → bool=: h int iγ → hintiγ → hbooliγ@: ht1 →t2 iγ → ht1 iγ → ht2 iγ:=: t ref → t → t:=: ht refiγ → htiγ → htiγ
Arity 3
cif : hbooliγ → htiγ → htiγ → htiγ

Fig. 2. The constants ci of <NJ> with their arities i. The underlined constants, whose
result type is code type, are code combinators. The shown types are schematic: tdenotes any suitable type and γ any suitable classifier. We silently add other arithmetic
and comparison constants and code combinators, similar to + and =. Although theconstants may have function types, they are not expressions, unless applied to the rightnumber of arguments.

For another illustration we take the familiar power example: generating afunction that raises its argument to the given power by repeated multiplications.
let body = λf n x. if n=0 then %1 else x ∗ f (n−1) x in
λn. λx. ( fix body) n x

Applying the result to, say, 3 produces hλy. y ∗ y ∗ y ∗ 1i.
<NJ> has mutable state in the form of the familiar mutable cells, such as thosefound in ML and many other languages. Correspondingly, the calculus has theform ref e to create a fresh reference cell holding the value of e, ! e to dereference
it, obtaining the held value, and e1 := e2 to replace the value of the cell e1 withthe value of e2 , returning the latter value. The semantics is standard, involving
locations l and the heap H, the finite map from locations to values. The empty
heap is denoted as []; (l:v,H) is the heap that contains the association of l withv plus the associations in H. The domain of the latter does not include l. FromλU [14] we borrow the heap-like name heap N, which is the set of names usedfor variables in the generated code. As we shall see throughout the paper, there6
E ::= [] | E e | v E | c1 E | c2 E e | c2 v E| if E then e else e | λx. E
H ::= [] | l:v,H
N ::= [] | y,Ne1 [x:=e2 ]N1 ;H1 ;e1N2 ;H2 ;e2N1 ; H1 ; e1N2 ; H2 ; e2Contexts
Heap
Names
Substitutions
Reductions
Context compatibility

N1 ; H1 ; E[e1 ]N2 ; H2 ; E[e2 ]Primitive reductions
N;H; (λx.e) v
N;H; if true then e1 else e2
N;H; if false then e1 else e2
N;H; λx. e
N;H; λy.hei
N;H; ref v
N;(l :v,H); ! l
N;(l :v,H); l := v2

N;H; e[x:=v]
N;H; e1
N;H; e2(y,N);H; λy. e[x:=hyi]
N;H; hλy.ei
N;(l :v,H); l
N;(l :v,H); v
N;(l :v2 ,H); v2

Fig. 3. Dynamic semantics of <NJ>: reductions e1(code-generating) constants are defined in Fig. 4.
cint ncbool bhe1 i + he2 i
he1 i = he2 i
he1 i @ he2 i
fix heihni
hbi
he1 + e2 i
he1 = e2 i
he1 e2 ih fix eicif he1 i he2 i he3 i
fix (λf. e)
ref hei! hei
he1 i := he2 iy 6∈ Nl 6∈ domH

e2 . The reductions involving

h if e1 then e2 else e3 i
e[ f :=fix (λf. e )]h ref eih!ei
he1 := e2 iFig. 4. Constant (code-generating) reductions

is an uncanny similarity between reference cells and the future-stage variablenames.
The full dynamic semantics of <NJ> thus deals with reductions between configurations, made of the name and location heaps, and an expression, see Fig.
3. We will often elide the heaps when presenting reductions, especially in examples. As an illustration, the following reductions show the evaluation of a sample
imperative code, and the generation of the imperative code:∗
N;H;let r = ref (2+3) in r := 0; ! r∗N;(l :5, H); l := 0; ! l
N;(l :0, H);! l
N;(l :0, H);0
clet r = ref (%2 + %3) in clet z = r := %0 in !r≡∗@ ref (%2 + %3)(λr. (λz. ! r) @ r := %0)∗(λy. (λu. ! hyi) @ hyi := %0) @ ref (%2 + %3)∗(λy. hλu. !yi @ hy := 0i)@ ref (%2 + %3)h(λy. (λu. !y) (y := 0)) ( ref (2 + 3))iwhere we used clet x = e1 in e2 to stand for (λx. e2 ) @ e1 . In the first example,
l denotes a fresh location. We elided the heaps in the second example.
So far, the lambda-calculus fragment of <NJ>, the code generating and thereference cell fragments looked like orthogonal extensions. There is one part of

7

the semantics where they interact non-trivially. It has to do with generating
functions and using reference cells to store open code. The following is an example of how not to use reference cells to store open code: it is the infamous
scope-extrusion example.
N;H;let r = ref %0 in (λx. r := x); ! r(y,N);( l : h0i,H); (λy. l := hyi ); ! l(y,N);( l : hyi ,H); hλy. yi ; ! l(y,N);( l : hyi ,H); ! l

N;(l : h0i,H); (λx. l := x); ! l(y,N);( l : hyi ,H): (λy. hyi ); ! l(y,N);( l : hyi ,H); hyi

When building the functions’s body we store the code with the yet-to-be-boundvariable y in the reference cell. After the function is constructed we retrieve fromthe reference cell the code with what is by now the unbound variable y. We havejust seen the most blatant example of scope extrusion; alas, there are also subtle,
and hence far more dangerous cases; we discuss them in §3.1.
Our dynamic semantics is really non-chalant about unbound future-stage
variables, treating them essentially as constants. To be pedantic, y in the resultof the scope-extrusion example is bound, technically: it occurs in the name heap.
Real staged languages such as MetaOCaml and Scala-Virtualized [15] likewise
allow unbound variables to appear in code values (in case of MetaOCaml, fora short interval). We will show in the next section that a well-typed <NJ> program never generates code with unbound variables. The scope-extrusion program
above does not type-check.
Storing open code in reference cells has many legitimate uses. Here we show
one simple example. It is again the power function, but now with reference cells.
Merely computing xn looks in <NJ> asλn.λx. let r = ref 1 infix (λf.λn. if n = 0 then 0 else (r := !r ∗ x; f (n−1))) n; ! r

To obtain the code for computing xn for a fixed n, we turn the above program
into the generator, in a rather straightforward way:
let body = λn.λx. let r = ref %1 in
fix (λf.λn. if n = 0 then 0 else (r := !r ∗ x; f (n−1))) n; ! rin λn. λx. body n x

Applying the result to, say, 3 produces, as before, hλy. y ∗ y ∗ y ∗ 1i. The reference cell r accumulates progressively longer code for the product, containing
multiple occurrences of the free variable y, to be bound at the end. §4 shows moreinteresting, realistic example of reference cells in code generators, of assertion
insertion.

3

Type System

Fig. 1 also defines the syntax of types t, which include the standard, base typesof int and bool, the arrow (function) type and the reference type t ref. Nonstandard is the code-type htiγ , containing the so-called classifier γ – similar in
intent, but more precise than the environment classifier of [2], as mentioned in

8the Introduction. One may think of the classifier γ as a type-level representation, or ‘name’, of a Level-1 variable – although strictly speaking a classifier
represents a binding environment. We delay the further discussion of classifiers
till §3.2, after we explained the typing rules that govern classifiers, the partial
order on classifiers and classifier subtyping. Since <NJ> is a two-level system –the generated code does not contain any code generating expressions – we distinguish level 1 types t1 from level 0 types t: the former omits code types. To
relieve the notation burden, however, we will often use the same meta-variable
t for both sorts of types, using t1 only where necessary for disambiguation.
Level indication L
Environment
Heap typing
Name heap typing
Judgement

either empty or γ
Γ ::= [] | Γ , γ | Γ , (γ1 γ2 ) | Γ , (x:t)L
Θ ::= [] | Θ, (l:t)Υ ::= [] | Υ , γ | Υ , (γ1 γ2 ) | Υ , (y:t1 )γΥ ;Θ;Γ `L e: t
Fig. 5. Judgements, environments, classifiers

Figure 5 defines judgements and their components. The main typing judgement – the expression e has the type t at the level L – has the form Υ ;Θ;Γ `L e: t.
Here, Γ is the standard environment, an ordered sequence associating types withfree variables in an expression. Free variables in e1 expressions (that is, expressions within brackets) are Level-1 free variables; their associations (y:t1 )γ in Γ
are annotated with the classifier γ. Besides the free variable bindings, Γ also
contains classifiers γ and classifier subtyping witnesses γ1 γ2 to be explained
shortly. Υ and Θ are essentially the typings of the name and location heaps. Θ
is indeed a finite map from locations to types; Υ on the other hand, has morestructure. It is an ordered sequence. It contains the classifier γ for each name in
N. Like Γ , it also contains the types associated with each name (Level-1 variable) and the classifier subtyping witnesses. One may think of Γ as a local typeenvironment and Υ as a ‘global’ one. The initial Υ contains only the pre-definedclassifier γ0 . We use the standard ∈ notation to assert that Γ or Υ sequences
contain a particular element. In addition, we write l ∈ Θ to say the location isin the domain of the finite map Θ. The notation b ∈ (Γ ] Υ ) means that somebinding b is an element of Γ , or else it is an element of Υ (note the asymmetry).
Some judgements are generic, so we use superscript L that stands for either
empty or a classifier. If L is not empty, then, strictly speaking, the judgement
should be written as Υ ;[];Γ `γ e1 : t1 , meaning that only a subset of expressions(and types) are allowed at level 1. In particular, locations cannot appear at Level
1 5 : normally locations result from evaluating expressions ref e; although such
expressions may appear in the generated code, they remain unevaluated. There
are no code combinators in <NJ> that could produce the value hli. A substitution
cannot insert a location either, since the generated code cannot be substituted
5

If we generate code for later use, e.g., as a library of specialized algorithms, it makes
no sense for the generated code to contain pointers into the generator’s heap. By
the time the produced code is run, the generator will be long gone. Although sharedheap may be useful in run-time-code specialization, none of the staged calculi to ourknowledge consider this case.

9into. Therefore, the heap typing Θ is irrelevant in such judgements. We willalmost always drop the superscript in e1 and t1 (we keep it in the rule (Code)as reminder).
` Υ ok` [] ok` Υ okγ∈Υy 6∈ Υ

γ 6∈ Υ` Υ okγ1 ∈ Υ

γ2 ∈ Υ` Υ , γ ok
` Υ , γ1 γ2 ok(y’:t’)γ 6∈ Υ (i.e., Υ has no other binding marked by γ)` Υ , (y:t1 )γ ok∀ l ∈ Θ such that Θ(l) is hti . γ ∈ ΥγΥ ` Θ okΥ ` Γ okγ 6∈ Υ
Υ ` [] okΥ ` Γ okγ 6∈ ΓΥ ` Γ , γ okΥ ` Γ okγ ∈ (Γ ] Υ )Υ ` Γ , (x:ht1 iγ ) ok

Υ ` Γ okγ1 ∈ (Γ ] Υ )γ2 ∈ (Γ ] Υ )Υ ` Γ , (γ1 γ2 ) okγ ∈ (Γ ] Υ )Υ ` Γ , (y:t1 )γ ok

Fig. 6. Well-formedness of environments and heap typings ` Υ ok, Υ ` Θ ok, Υ ` Γ ok

Figure 6 states the well-formedness constraints on the environments and heap
typings, which can be summarized as the absence of duplicates and the classifiers
being defined before use. It becomes clear that each Level-1 variable binding
recorded in the global Υ or local Γ environment has its own classifier. Indeed, aclassifier acts as a type-level ‘name’ of a Level-1 variable. To ease the notation,
hereafter we shall assume well-formedness of all environments and heap typings.
We write Γ ,Γ ’ and Υ ,Υ ’ for the concatenation of two sequences such that theresult must be well-formed.
Υ ;[]; Γ `γ e1 : t1

(x: t) L ∈ (Γ ] Υ )ConstΥ ;Θ;Γ ` c: tc

Υ ;Θ;Γ `L x: t

( l : t) ∈ ΘLocΥ ;Θ;Γ ` l: tΥ ;Θ;Γ `γ1 e: t Υ ;Γ |= γ2 γ1Υ ;Θ;Γ `γ2 e: tVarΥ ;Θ;Γ ` he1 i: ht1 iγ
γ1Υ ;Θ;Γ ` e: hti
Υ ;Γ |= γ2 γ1

Code
Sub0

Υ ;Θ;Γ ` e: htiγ2Sub1Υ ;Θ;Γ `L e1 : t1 →t2

Υ ;Θ;Γ `L e2 : t1AppΥ ;Θ;Γ `L e1 e2 : t2

Υ ;Θ;(Γ , (x:t1 )L ) `L e: t2AbsΥ ;Θ;Γ `L λx.e: t1 →t2
Υ ;Θ;Γ `L e: bool Υ ;Θ;Γ `L e1 : t

Υ ;Θ;Γ `L e2 : tIfΥ ;Θ;Γ `L if e then e1 else e2 : tγ ∈ (Γ ] Υ )γ1 6∈ (Γ ] Υ ) Υ ;Θ;(Γ , γ1 , (γ1 γ), (x:ht1 iγ1 )) ` e: ht2 iγ1CAbsΥ ;Θ;Γ ` λx.e: ht1 →t2 iγ
Υ = Υ ’, γ1 , (γ1 γ), (y:t1 )γ1 , Υ ’’
∀ γ2 . Υ |= γ1 γ2 and γ2 6= γ1 imply Υ |= γγ2 Υ ;Θ;[] ` e: ht2 iγ1Υ ;Θ;[] ` λy.e: ht1 →t2 iγ
Fig. 7. Type system: typing of expressions

IAbs

10

The typing of expressions is presented in Fig. 7 whereas Fig. 9 defines thetyping of heaps. Most of the type system is standard. The rule (Const) uses
the types of constants tc, given in Fig. 2. We abuse the notation and treat, fortype-checking purposes, constant expressions such as c2 e1 e2 as applications to
c2 , although c2 is not an expression per se. The rules (Sub0) and (Sub1) relyon the partial order on classifiers specified in Fig. 8 in the straightforward way:
Υ ,Γ |= γ2 γ1 if either γ2 γ1 literally occurs in the environments as a witness,or can be derived by reflexivity and transitivity.
(γ2 γ1 ) ∈ (Γ ] Υ )Υ ;Γ |= γγΥ ;Γ |= γ1 γ2Υ ;Γ |= γ2 γ1Υ ;Γ |= γ2 γ3Υ ;Γ |= γ1 γ3Fig. 8. Partial order on classifiers Υ ;Γ |= γ1 γ2γ∀ ( l :v) ∈ H. Υ ;Θ;[] ` v : Θ(l)∀ y ∈ N. (y: t) ∈ ΥΥ `NΥ ;Θ ` H
Fig. 9. Type system: typing of heaps Υ ` N and Υ ;Θ ` H

The most interesting are the rules (CAbs) and (IAbs). To explain them andto illustrate the type system, we show two sample typing derivations. The firstdeals with the term λx1 .λx2 .x1 + x2 – generating the curried addition function – in the initial environment, in which Υ contains only the predefined classifier γ0 , and Θ and Γ are empty. In the following derivation, Γ2 stands for
γ1 , (γ1 γ0 ), (x1 :hintiγ1 ), γ2 , (γ2 γ1 ), (x2 :hintiγ2 ).
Υ ;Θ;Γ2 ` x1 : hintiγ1 Υ ;Γ2 |= γ2 γ1Υ ;Θ;Γ2 ` x1 : hintiγ2

Υ ;Θ;Γ2 ` x2 : hintiγ2

Υ ;Θ;Γ2 ` x1 + x2 : hintiγ2
Υ ;Θ;(γ1 , (γ1 γ0 ), (x1 :hintiγ1 )) ` λx2 . x1 + x2 : hint→intiγ1
Υ ;Θ;[] ` λx1 .λx2 . x1 + x2 : hint→int→intiγ0

The side-conditions of (CAbs) tell that the classifiers γ1 and γ2 are ‘fresh’. §3.1
shows another attempted (but not completed) derivation, in case of scope extrusion. The second derivation is for the expression λy1 .λx2 . hy1 i + x2 , which
results from the one-step reduction of the expression in the previous derivation.
Now, Υ1 stands for γ0 , γ1 , γ1 γ0 , (y1 :int)γ1 and Γ2 for γ2 ,γ2 γ1 ,(x2 :hintiγ2 ).
Υ1 ;Θ;Γ2 `γ1 y1 : int
Υ1 ;Θ;Γ2 ` hy1 i: hintiγ1 Υ1 ;Γ2 |= γ2 γ1
Υ1 ;Θ;Γ2 ` hy1 i: hintiγ2

Υ1 ;Θ;Γ2 ` x2 : hintiγ2

Υ1 ;Θ;Γ2 ` hy1 i + x2 : hintiγ2
Υ1 ;Θ;[] ` λx2 . hy1 i + x2 : hint→intiγ1
Υ1 ;Θ;[] ` λy1 .λx2 . hy1 i + x2 : hint→int→intiγ011It should be clear, already from (IAbs) in fact, that λy. is not really a binding
form. The environment Γ in (IAbs) is empty since λy.e shows up only during
evaluation and it is not a value.
Proposition 1 (Canonical Forms). The only values of base types int and bool
are zero-ary constants (numerals and booleans, respectively). Values of reference
types t ref are locations. Values of code types are all bracketed expressions hei
and of the function types t1 →t2 are abstractions λx.e.
Although constants of arity 1 and above also have function types (see Fig. 2), notapplied to the right number of arguments they are not regarded as expressions.
Proposition 2 (Weakening). If Υ ;Θ;Γ `L e:t, Υ ` N, and Υ ;Θ ` H hold, sodo (Υ ,Υ ’);(Θ,Θ’);(Γ ,Γ ’) `L e:t and (Υ ,Υ ’) ` N and (Υ ,Υ ’);(Θ,Θ’) ` H.
Recall that comma denotes concatenation that preserves well-formedness; which
implies Θ and Θ’ are disjoint. The proof is straightforward.
Theorem 1 (Subject Reduction). If Υ ;Θ;[] ` e: t, Υ ` N, Υ ;Θ ` H, andN;H;e
N’;H’;e’, then Υ ’;Θ’;[] ` e’: t, Υ ’ ` N’, Υ ’;Θ’ ` H’, for some Υ ’ and Θ’that are the extensions of the corresponding unprimed things.
We outline the proof in Appendix A.
Theorem 2 (Progress). If Υ ;Θ;[] ` e:t, Υ ` N and Υ ;Θ ` H, then either e isa value or there are N’,H’ and e’ such that N;H;e
N’;H’;e’.
The proof is the easy consequence of the canonical forms lemma. For example,
if the last rule in the derivation of Υ ;Θ;[] ` e:t is (IAbs), then e must have theform λy.e’ for some e’, where e’ must itself be typeable in the same Υ and Θ.
By induction hypothesis, e’ either reduces, or is a value. In the latter case, by
the canonical forms lemma, it should be of the form he2 i for some e2 – meaning
λy.he2 i can reduce.
Corollary 1. If ([],γ0 );[];[] ` e:htiγ0 and [];[];eand ([],γ0 );[];[] `γ0 e1 :t.

N;H;v then v has the form he1 i

That is, if a well-typed program of the type htiγ0 terminates it generates thecode well-typed in the empty environment. The generated code hence has nounbound variables.
3.1

Scope Extrusion

When generating the body of a function, its formal argument is available as acode value – as the free variable. Scope extrusion occurs when that open codevalue is used outside the dynamic scope of the function generator and hence thefree variable can never be properly bound. Although the error is obvious once we
attempt to compile the generated code, it is not at all obvious what part of thegenerator is responsible. Debugging generated code is very difficult in general.
We now demonstrate how <NJ> prevents scope extrusion.
We start with the example of blatant scope extrusion, from §2:

12
let r = ref %0 in (λx. r := x); ! r

We have seen that its evaluation indeed produces the code with an unboundvariable. The example does not type check however. Specifically, the type error
occurs not when the open code is retrieved from the reference cell r at the end.
Rather, the generator of the function body, specifically, r := x fails to type-check.
Here is the attempt at the derivation, where we assumed γ ∈ (Γ ] Υ ) and so is γ1(which may be the same as γ). We take Γ2 to be Γ ,(r:hintiγ1 ref),γ2 ,γ2 γ,(x:hintiγ2 )where γ2 is fresh.
Υ ;Θ;Γ2 ` r := x: hintiγ2

Υ ;Θ;(Γ ,(r:h int iγ1 ref)) ` (λx. r := x) : h int →intiγ
Υ ;Θ;Γ ` let r = ref cint 0 in (λx. r := x) : h int →intiγ

The derivation cannot be completed since r has the type hintiγ1 ref but x is of
the type hintiγ2 where γ2 is specifically chosen by (CAbs) to be different fromany other classifiers in Γ and Υ , including γ1 .
If such examples were our only worry, a simpler type system would havesufficed. Instead of named classifiers, we would annotate code types with justa natural number: the nesting level of λ. Our blatant example will likewise failto type-check. The error will be reported later, however, when type checking
the last expression !r retrieving the code with the already leaked variable as the
program result. The program result must be closed: be at the 0th nesting level.
The type system of [10] (extended with reference cells) likewise rejects the blatantexample, as was described in that paper. (After all, their type system annotatescode types with the typing environment sequence, which is the refinement of
the nesting depth.) MetaOCaml also reports the scope extrusion error – whenrunning the program and executing the !r expression. In contrast, <NJ> rejects
r := x, when merely attempting to leak out the free variable.
Alas, scope extrusion can be subtle. Consider a small modification of theearlier example:
let r = ref %0 in (λx. r := x); (λz. ! r)

The simpler type system with mere level counting accepts the code: the freevariable leaks out of one binder into another, at the same nesting level of λ.
Likewise, the calculus of [10] (extended with reference cells as described therein)
will type-check and even run the example, producing the code for the identity
function. This is not what one may expect from the generator λz. !r. Our <NJ>
rejects r := x in the first part of the example as described earlier: it rejects evenan attempt to leak the variable.
Finally, scope extrusion may be harmless, as in the following, yet anothervariation of the example:
let r = ref (λz.z) in (λx. r := (λz. (x; z )); %0); !r

When generating the body of the function, we incorporate the free variable x in
the closure λz. (x; z), but in a way that it does not contribute to the result andhence is not reflected in the closure’s type, which remains int→int. Technically,
the free variable has leaked – but in a useless way, embedded in dead code.

13<NJ> accepts the latter example. When run, it indeed produces the closure
with an unbound variable – which remains typeable since the unbound variable
is still in the global heap N and its classifier in Υ . Such open code must havebeen dead, however: it cannot be the result of a well-typed generator, since thetype of such result would have contained the classifier γ that is different from γ0 .
The well-typed generator program must have the type htiγ0 . We have seen before
that even a fragment, let alone the whole program, that attempts to ‘usefully
leak’ a bound variable will fail to type-check.
Accepting unbound variables in dead code has many precedents. Most region
calculi (see [8] and references therein) and their implementations (such as runSTmonad in Haskell) allow dangling references, provided they are not accessed –that is, remain embedded in essentially dead code.

3.2

Environment Classifiers, Binding Abstractions, and LexicalScope

As we have seen from §3.1, the key to preventing scope extrusion is annotating
the type of a code value with some representation of free variables that may becontained therein. This section discusses a few choices for the representation andthe position of <NJ> among them as the most abstract while still sufficient toprevent scope extrusion. By free variables we always mean Level-1 free variables:
all values and terms produced and evaluated in stage calculi are closed withrespect to Level-0 variables.
On one end of the spectrum is annotating the type of a code value with thenames of the containing free variables, or the typing environment: the set or thesequence listing the free variables and their types. Taha and Nielsen [2, §1.4]
describe many difficulties of this approach (the sheer size of the type being oneof them), which makes it hard to implement, and use in practice.
On the other extreme is the most abstract representation of a set of freevariables: as a single name (the environment classifier, [2]) or a number, thecardinality of the set. §3.1 showed that this is not sufficient to prevent the scope
extrusion, of the devious, most harmful sort.
The approach of [10] also annotates the code types with the type environment; however, by using De Bruijn indices, it avoids many difficulties of thenominal approach, such as freshness constraints, α-renaming, etc. The approachis indeed relatively easy to implement, as the authors have demonstrated. Alas,although preventing blatant scope extrusion, it allows the devious one, as we
saw in §3.1.
The representation of [10] is also just too concrete: the code type hinti(int,bool,int)
tells not only that the value may contain three free variables with the indices 0,
1 and 2. The type also tells that the int and the bool variables will be boundin that order and there is no free variable to be bound in between. There is noneed to know with such exactitude when free variables will be bound. In fact,
there is no need to even know their number, to prevent scope extrusion. The
concreteness of the representation has the price: the system of [10, §3.3] admits

14

the term, in our notation, λf.λx.λy.f y, which may, depending on the argumentf, generate either hλx.λy.yi or, contrary to any expectation, hλx.λy.xi.
Such a behavior is just not possible in <NJ>: consider λx. f x where f is somefunction on code values. The function receives the code of a Level-1 variable
and is free to do anything with it: discard it, use it once or several times in thecode it is building, store in global reference cells, as well as do any other effects,
throw exceptions or diverge. Still, we are positive that whatever f may do, if
it eventually returns the code that includes the received Level-1 variable, thatvariable shall be bound by λx. of our expression – regardless of whatever binders
f may introduce. This is what we call ‘lexical’ scope for Level-1 variables: theproperty, not present in [16] (by choice) or [10].
<NJ> avoids the problematic ‘variable conversions’ because it does not exposes in types or at run-time any structure of the Level-1 typing environment.
The environment classifier in <NJ> is the type-level representation of the variablename. There is a partial order on classifiers, reflecting the nesting order of thecorresponding λx generators. The relation γ2 γ1 tells that the variable corresponding to γ1 is (to be) introduced earlier than the free variable correspondingto γ2 , with no word on which or how many variables are to be introduced inbetween. The code type is annotated not with the set of free variables, not withthe set of the corresponding classifiers – but only with the single classifier, themaximal in the set. The type system ensures that there is always the maximal element. To be precise, any free Level-1 variable that may appear within
λy. hei : ht1 →t2 iγ2 is marked by such a classifier γ1 that γ2 γ1 . Therefore, anysuch variable will be bound by an ancestor of λy. This is another way to state
the property of ‘lexical scope’ for free variables.
3.3

Classifier Polymorphism

The classifier polymorphism and its importance are best explained on examples.
The following generator
λx. let f = λz. cint x + %1 + z in let f ’ = λz’. ( cint x + %1) ∗ z’ in e

contains the repeated code that we would like to factor out, to make the generators clearer and more modular:
λx. let u = cint x + %1 in let f = λz. u + z in let f ’ = λz’. u ∗ z’ in e

One may worry if the code type-checks: after all, u is used in contexts associatedwith two distinct classifiers. The example does type-check, thanks to (Sub0)
rule: u can be given the type hintiγ0 , and although z:hintiγ1 and z’:hintiγ2 areassociated with unrelated classifiers, γ1 γ0 and γ2 γ0 hold.
Alas, the classifier subtyping gets us only that far. It will not help in the
more interesting and common example of functions on code values:
λx. let u = λz.cint x + z in let f = λz. u z + z in let f ’ = λz’. u z’ ∗ z’ in e

where the function u is applied to code values associated with unrelated classifiers. To type-check this example we need to give u the type ∀ γ. hintiγ →hintiγ .

15Before, γ was used as a (sometimes schematic) constant; now we use it as aclassifier variable.
Extending <NJ> with let-bound classifier polymorphism with attendant value
restriction is unproblematic and straightforward. In fact, our implementation
already does it, inheriting let-polymorphism from the host language, OCaml.
Sometimes we may need more extensions, however.
For example, we may write a generator that introduces an arbitrary, statically unknown number of Level-1 variables, e.g., as let-bound variables to share
the results of computed expressions. Such pattern occurs, for example, when
specializing dynamic programming algorithms. Appendix B demonstrates thelet-sharing on the toy example of specializing the Fibonacci-like function, described in [7, §2.4]. As that paper explains, the generator requires polymorphic
recursion – which is well-understood. Both Haskell and OCaml supports it, andhence our implementation of <NJ>. Polymorphic recursion also shows in [10].
There are, however, times (not frequent, in our experience) where even morepolymorphism is needed. The poster example is the staged eta-function, the motivating example in [2]: λf. λx. f x, whose type is, (ht1 iγ → ht2 iγ ) → ht1 →t2 iγ ,approximately. The type is not quite right: f accepts the code value that contains a fresh free variable, which comes with a previously unseen classifier. Hence
we should assign eta at least the type (∀ γ1 . ht1 iγ1 → ht2 iγ1 ) → ht1 →t2 iγ – therank-2 type. This is still not quite right: we would like to use eta in the expression such as λu. eta (λz. u + z), where f combines the open code received asargument with some other open code. To type-check this combination we needΥ ,Γ |= γ1 γ. Hence the correct type for eta should be∀ γ. (∀ γ1 γ. ht1 iγ1 → ht2 iγ1 ) → ht1 →t2 iγwith the bounded quantification. One is immediately reminded of MLF . Suchbounded quantification is easy to implement, however, by explicit passing ofsubtyping witnesses (as done in the implementation of the region calculus [8])Our implementation of <NJ> supports it too – and how it cannot: eta is just thefirst-class form of λ. Thus the practical drawback is the need for explicit typesignatures for the sake of the rank-2 type (just as signatures are required in MLF
when the polymorphic argument function is used polymorphically). Incidentally,
the original environment classifiers calculus of [2] gives eta the ordinary rank-1
type: here the coarseness of the original classifiers is the advantage. The formal
treatment of rank-2 classifier polymorphism is the subject of the future research.

4

Complex Example

To demonstrate the expressiveness of <NJ>, we show a realistic example of assertinsertion – exactly the same example that was previously written in StagedHaskell. The latter is the practical Haskell code-generation library, too complex
to reason about formally and prove correctness. The example was explained indetail in [7]; therefore, we elide many explanations here.
For the sake of the example, we add the following constants to <NJ>:

16
/
/

: int → int → int: h int iγ → hintiγ → hintiγ

assertassertPos: bool → bool
: h int iγ → htiγ → htiγ

The first two are the integer division and the corresponding code combinator;
assert e returns the result of the boolean expression, if it is true. Otherwise, itcrashes the program. The constant assertPos is the corresponding combinator,
with the reduction rule assertPos he1 i he2 ihassert (e1 >0); e2 i.
The goal is to implement the guarded division, which makes sure that thedivisor is positive before attempting the operation. The naive version
let guarded div = λx.λy. assertPos y (x / y)to be used as
λy. complexExp + guarded div %10 yproduces hλx. complexExp + (assert (x>0); (10 / x))i. The result is hardly satisfactory: we check the divisor right before the division. If it is not positive, thetime spent computing complexExp is wasted. If the program is going to end up
in error, we had rather it end sooner than much later.
The solution is explained in [7], implemented in StagedHaskell and is reproduced below in <NJ>. Intuitively, we first reserve the place where it is appropriate
to place assertions, which is typically right at the beginning of a function. As wego on generating the body of the function, we determine the assertions to insert
and accumulate them in a mutable ‘locus’. Finally, when the body of the function is generated, we retrieve the accumulated assertion code and prepend it tothe body. The function add assert below accumulates the assertions; assert locus
allocates the locus at the beginning and applies the accumulated assertions at
the end.
let assert locus = λf.
let r = ref (λx.x) in let c = f r inlet transformer = !r in transformer c
let add assert locus transformer =locus := ( let oldtr = !locus in λx. oldtr ( transformer x))
let guarded div = λlocus.λx.λy. add assert locus (λz. assertPos y z ); (x / y)

They are to be used as in the example below:
λy. assert locus (λlocus. λz. complexExp + guarded div locus z y)

As we generate the code, the reference cell r within the locus accumulates thetransformer (code-to-code function), to be applied to the result. In our example,
the code transformer includes open code (embedded within the assertPos expression), which is moved from within the generator of the inner function. The
example thus illustrates all the complexities of imperative code generation. The
improved generated codehλx. assert (x>0); (λy. complexExp + y / x)ichecks the divisor much earlier: before we started on complexExp, before we even
apply the function (λy. complexExp + y / x). If we by mistake switch y and z in
guarded div locus z y, we get a type-error message.

17

5

Related WorkWe thoroughly review the large body of related work in [7]. Here we highlight
only the closest connections. First is Template Haskell, which either permits
effectful generators but then provides no guarantees by construction; or provides guarantees but permits no effects – the common trade-off. We discuss thisissue in detail in [7]. BER MetaOCaml [3] permits any effects and ensures wellscopedness, even in open fragments, using dynamic checks. StagedHaskell and<NJ> are designed to prevent scope extrusion even before running the generator.
Safe imperative multi-staged programming has been investigated in [17] and[4]. Safety comes at the expense of expressiveness: e.g., only closed code is allowed
to be stored in mutable cells (in the former approach).
We share with [2] the idea of using an opaque label, the environment classifier, to refer to a typing environment. The main advantage of environment
classifiers, their imprecision (they refer to infinite sets of environments), is also
their drawback. On one hand, they let us specify staged-eta §3.3 without any
first-class polymorphism. On the other hand, the imprecision is not enough tosafely use effects.
Chen and Xi [10] and Nanevski et al. [9] annotate the code type with the typeenvironment of its free variables. The former relies on the first-order syntax withDe Bruijn indices whereas the latter uses higher-order abstract syntax. Althoughinternally Chen and Xi use De Bruijn indices, they develop a pleasant surface
syntax a la MetaOCaml (or Lisp’s antiquotations). The De Bruijn indices arestill there, which may lead to unpleasant surprises, which they discuss in [10,§3.3]. Their type system indeed rejects the blatant example of scope extrusion.
Perhaps that is why [10] said that reference cells do not bring in significant
complications. However, scope extrusion is much subtler than its well-known
example: §3.1 presented a just slightly modified example, which is accepted in
Chen and Xi’s system, but produces an unexpected result. We refer to [7] forextensive discussion.
One may think that any suitable staged calculus can support reference cells
through a state-passing translation. The elaborate side-conditions of our (CAbs)
and (IAbs) rules indicate that a straightforward state-passing translation is notgoing to be successful to ensure type and scope safety.
Staged-calculi of [2, 10] have a special constant run to run the generated code.
Adding it to <NJ> is straightforward.
Our bracketed expressions are the generalization of data constructors of thecode data type in the ‘single-stage target language’ [14, Fig.2]. Our name heap
also comes from the same calculus. The latter, unlike <NJ>, is untyped, andwithout effects.

6Conclusions and Future Work

We have described the first staged calculus <NJ> for imperative code generators
without ad hoc restrictions – letting us even store open code in reference cells and18

retrieve it in a different binding environment. Its sound type system staticallyassures that the generated code is by construction well-typed and well-scoped,
free from unbound or surprisingly bound variables. The calculus has been distilled from StagedHaskell, letting us formally prove the soundness of the latter’s
approach. The distilled calculus is still capable of implementing StagedHaskell’s
examples that use mutation.
<NJ> has drawn inspiration from such diverse areas as region-based memory
management and Natural Deduction. It turns out a vantage point to overview
these areas.
<NJ> trivially generalizes to effects such as exceptions or IO. It is also easy toextend with new non-binding language forms. (Binding-forms like for-loops canalways be expressed via lambda-forms: see Haskell or Scala, for example.) <NJ>
thus serves as the foundation of real staged programming languages. In fact, it
is already implemented as an OCaml library. Although the explicit weakening
is certainly cumbersome, it turns out, in our experience, not as cumbersome as
we had feared. It is not a stretch to recommend the OCaml implementation of<NJ> as a new, safe, staged programming language.
Extension to effects such as delimited control or non-determinism is however
non-trivial and is the subject of on-going research. We are also investigating
adding first-class bounded polymorphism for classifiers, relating <NJ> more precisely to MLF .
Acknowledgments We thank anonymous reviewers for many helpful comments.
This work was partially supported by JSPS KAKENHI Grant Numbers 15K12007,
16K12409, 15H02681.

References[1] Davies, R.: A temporal logic approach to binding-time analysis. In: LICS. (1996)
184–195[2] Taha, W., Nielsen, M.F.: Environment classifiers. [18] 26–37[3] Kiselyov, O.: The design and implementation of BER MetaOCaml - system description. In: FLOPS. Number 8475 in LNCS, Springer (2014) 86–102[4] Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint:
Java multi-stage programming using weak separability. In: PLDI ’10, New York,ACM Press (2010)[5] Pouillard, N., Pottier, F.: A fresh look at programming with names and binders.
In: ICFP, New York, ACM Press (2010) 217–228[6] Pottier, F.: Static name control for freshML. In: LICS, IEEE Computer Society(2007) 356–365[7] Kameyama, Y., Kiselyov, O., Shan, C.c.: Combinators for impure yet hygienic
code generation. Science of Computer Programming 112 (part 2) (2015) 120–
144
[8] Fluet, M., Morrisett, J.G.: Monadic regions. Journal of Functional Programming
16 (2006) 485–545[9] Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. Transactions on Computational Logic 9 (2008) 23:1–49

19[10] Chen, C., Xi, H.: Meta-programming through typeful code representation. Journalof Functional Programming 15 (2005) 797–835[11] Le Botlan, D., Rémy, D.: MLF : Raising ML to the power of System F. In: ICFP.
(2003) 27–38[12] Thiemann, P.: Combinators for program generation. Journal of Functional Programming 9 (1999) 483–525[13] Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. [18] 224–235[14] Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages
using ASTs, gensym, and reflection. In: GPCE. Number 2830 in LNCS (2003) 57–
76[15] Rompf, T., Amin, N., Moors, A., Haller, P., Odersky, M.: Scala-Virtualized:
linguistic reuse for deep embeddings. Higher-Order and Symbolic Computation(2013)[16] Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for Lisp-like
multi-staged languages. In: POPL. (2006) 257–268[17] Calcagno, C., Moggi, E., Taha, W.: Closed types as a simple approach to safe
imperative multi-stage programming. In: ICALP. Number 1853 in LNCS (2000)
25–36[18] POPL ’03: Conference Record of the Annual ACM Symposium on Principles ofProgramming Languages. In: POPL. (2003)

A

Proof outlines: Subject reduction theorem

Lemma 1 (Substitution). (1) If Υ ;Θ;(Γ ,(x:t1 )) ` e: t and Υ ,Θ,Γ ` e1 : t1 then
Υ ;Θ;Γ ` e[x:=e1 ]: t(2) If Υ ;Θ;(Γ ,γ2 ,γ2 γ1 ,Γ ’) `L e: t and γ1 ∈ Υ and γ2 ’ 6∈ (Γ ] Υ ), then(Υ ,γ2 ’,γ2 ’γ1 );Θ,(Γ ,Γ ’[γ2 :=γ2 ’]) `L e: t[γ2 :=γ2 ’] (if L was γ2 it is also replacedwith γ2 ’).
This lemma is proved straightforwardly.
Theorem 3 (Subject Reduction). If Υ ;Θ;[] ` e: t, Υ ` N, Υ ;Θ ` H, andN;H;e
N’;H’;e’, then Υ ’;Θ’;[] ` e’: t, Υ ’ ` N’, Υ ’;Θ’ ` H’, for some Υ ’ and Θ’that are the extensions of the corresponding unprimed things.
Proof. We consider a few interesting reductions. The first one is
N;H;λx. e(N,y);H;λ y. e[x:=hyi], y 6∈ N

We are given N’ is N,y, H’ is H, and Υ ;Θ;[] ` λx.e : ht1 →t2 iγ , which meansγ ∈ Υ and Υ ;Θ;(γ2 ,γ2 γ,(x:ht1 iγ2 )) ` e:ht2 iγ2 for a fresh γ2 . We choose Υ ’ as
Υ ,γ1 ,γ1 γ,(y:t1 )γ1 where γ1 is fresh, and Θ’ as Θ. Υ ’ is well-formed and is anextension of Υ . Furthermore, Υ ’ ` N,y. By weakening, Υ ’ ` Θ ok and Υ ’;Θ ` H
if it was for Υ . We only need to show that Υ ’;Θ;[] ` λy. e[x:=hyi] : ht1 →t2 iγ ,which follows by (IAbs) from Υ ’;Θ;[] ` e[x:=hyi] : ht2 iγ1 , which in turn follows
from from the fact that Υ ’;Θ;[] ` hyi :ht1 iγ1 and the substitution lemma.
The next reduction is
N;H;λy.hei

N;H;hλy.ei

20

We are given Υ ;Θ;[] ` λy.hei : ht1 →t2 iγ , Υ ` N and Υ ,Θ ` H. Since N and H are
unchanged by the reduction, we do not extend Υ and Θ. By inversion of (IAbs) weknow that Υ is Υ ’,γ1 ,γ1 γ,(y:t1 )γ1 ,Υ ’’ and ∀ γ2 . Υ |= γ1 γ2 and γ2 6= γ1 imply
Υ |= γγ2 and Υ ;Θ;[] ` hei : ht2 iγ1 , or, by inversion of (Code) Υ ;[];[] `γ1 e : t2 .
By weakening, Υ ;[];([],(y’:t)γ ) `γ1 e : t2 . An easy substitution lemma gives us
Υ ;[];([],(y’:t)γ ) `γ1 e’ : t2 where e’ is e[y:=y’], keeping in mind that Υ |= γ1 γ.
The crucial step is strengthening. Since we have just substituted away (y:t1 )γ1 ,which is the only variable with the classifier γ1 (the correspondence of variable names and classifiers is the consequence of well-formedness), the derivation
Υ ;[];([],(y’:t)γ ) `γ1 e’ : t2 has no occurrence of the rule (Var) with L equal to γ1 .
Therefore, any subderivation with L being γ1 must have the occurrence of the(Sub1) rule, applied to the derivation Υ ;[];([],(y’:t)γ ) `γ2 e’:t’ where Υ |= γ1 γ2and γ2 is different from γ1 . The inversion of (IAbs) gave us ∀ γ2 . Υ |= γ1 γ2 andγ1 6= γ2 imply Υ |= γγ2 . Therefore, we can always replace each such occurrenceof (Sub1) with the one that gives us Υ ;[];([],(y’:t)γ ) `γ e’:t’. All in all, we build
the derivation of Υ ;[];([],(y’:t)γ ) `γ e’ : t2 , which gives us Υ ;[];[] `γ λy.e : t1 →t2
and then Υ ;[];[] ` hλy.ei : ht1 →t2 iγ .
Another interesting case is
N;H;λy.E[ref hyi ]N;(H,l : hyi ); λy.E[ l ]Given, Υ ;Θ;[] ` λy.E[ref hyi] : ht1 →t2 iγ which means Υ = Υ ’, γ1 , γ1 γ, (y:t1 )γ1 , Υ ’’.
Take Θ’ = Θ,(l:ht1 iγ1 ref). It is easy to see that Υ ` Θ’ ok and Υ ,Θ’ ` H,(l:hyi).
The rest follows from the substitution lemma.

B

Generating Code with Arbitrary Many Variables

Our example is the Fibonacci-like function, described in [7, §2.4]:
let gib = fix (λf.λx.λy.λn.
if n=0 then x else if n=1 then y else f y (x+y) (n−1))

For example, gib 1 1 5 returns 8. The naive specialization to the given n
let gib naive =let body = fix (λf.λx.λy.λn.
if n=0 then x else if n=1 then y else f y (x+y) (n−1))
in λn.λx.λy. body x y n

is unsatisfactory: gib naive 5 generates
λx.λy. (y + (x + y)) + ((x + y) + (y + (x + y)))with many duplicates, exponentially degrading performance. A slight change
let gibs =let body : ∀ γ. h int iγ → hintiγ → int → h int iγ = fix (λf.λx.λy.λn.
if n=0 then x else if n=1 then y else clet z = (x+y) in f y z (n−1))
in λn.λx.λy. body x y ngives a much better result: gibs 5 produces
λx.λy. (λz. (λu. (λw. (λx1 .x1 ) (u + w)) (z + u)) (y + z)) (x + y)which runs in linear time. The improved generator relies on polymorphic recursion: that is why the signature is needed.