Meta-programming with names and necessity.
Meta-programming languages provide infrastructure to generate and execute object programs at run-time. In a typed setting, they contain a modal type constructor which classifies object code. These code types generally come in two flavors: closed and open. Closed code expressions can be invoked at run-time, but the computations over them are more rigid, and typically produce less efficient residual object programs. Open code provides better inlining and partial evaluation of object programs, but once constructed, expressions of this type cannot in general be evaluated.Recent work in this area has focused on combining the two notions into a sound system. We present a novel way to achieve this. It is based on adding the notion of names from the work on Nominal Logic and FreshML to the  -calculus of proof terms for the necessity fragment of modal logic S4. The resulting language provides a more fine-grained control over free variables of object programs when compared to the existing languages for meta-programming. In addition, this approach lends itself well to addition of intensional code analysis, i.e. ability of meta programs to inspect and destruct object programs at run-time in a type-safe manner, which we also undertake.
Introduction
Meta-programming can be broadly defined as a discipline of algorithmic manipulation
of programs written in a certain object language, through a program written
in another (or meta) language. The operations on object programs that the meta
program may describe can be very diverse, and may include, among others: gen-
eration, inspection, specialization, and, of course, execution of object programs at
run-time.
To illustrate the concept we present the following scenario, and refer to (Sheard,
2001) for a more comprehensive treatment. For example, rather than using one
general procedure to solve many di#erent instances of a problem, a program can
generate specialized (and hence more e#cient) subroutines for each particular case.
If the language is capable of executing thus generated procedures, the program
can choose dynamically, depending on a run-time value of a certain variable or
expression, which one is most suitable to invoke. This is the idea behind the work on
run-time code generation (Lee & Leone, 1996; Wickline et al., 1998b; Wickline et al.,
1998a) and the functional programming concept of staged computation (Ershov,
1977; Gl-uck & J-rgensen, 1995; Davies & Pfenning, 2001).
A. Nanevski, F. Pfenning
Languages in which object programs can not only be composed and executed
but also have their structure inspected add further advantages. In particular, e#-
ciency may benefit from various optimizations that can be performed knowing the
structure of the code. For example, (Griewank, 1989) reports on a way to reuse
common subexpressions of a numerical function in order to compute its value at a
certain point and the value of its n-dimensional gradient, but in such a way that the
complexity of both evaluations performed together does not grow with n. There are
other applications as well which seem to call for the capability to execute a certain
function and also inspect its structure: see (Rozas, 1993) for examples in computer
graphics and numerical analysis, and (Ramsey & Pfe#er, 2002) for an example in
machine learning and probabilistic modeling.
In this paper, we are concerned with typed functional languages for meta-pro-
even more precisely, we limit the considerations to only homogeneous
meta-programming, which is the especially simple case when the object and the
meta language are the same. Recent developments in this direction have been centered
around two particular modal lambda calculi: # and # . The # -calculus
is the proof-term language for the modal logic S4, whose necessity constructor #
annotates valid propositions (Davies & Pfenning, 2001; Pfenning & Davies, 2001).
The type #A has been used in run-time code generation to classify generators of
code of type A (Wickline et al., 1998b; Wickline et al., 1998a). The # -calculus is
the proof-term language for discrete linear-time temporal logic, and the type #A
classifies terms associated with the subsequent time moment. The intended application
of # is in partial evaluation because the typing annotation of a # -program
can be seen as a binding-time specification (Davies, 1996). Both calculi provide a
distinction between levels (or stages) of terms, and this explains their use in meta-
programming. The lowest level is the meta language, which is used to manipulate
the terms at the next level (terms of type #A in # and #A in # ), which is
the meta language for the subsequent level containing another stratum of boxed or
circled types, etc.
For purposes of meta-programming, the type #A is also associated with closed
code - it classifies closed object terms of type A. On the other hand, the type #A
is the type of postponed code, because it classifies object terms of type A which
are associated with the subsequent time moment. The operational semantics of #
allows reduction under object-level #-binders, and that is why the the postponed
code of # is frequently conflated with the notion of open code.
This dichotomy between closed and open code has inspired most of the recent type
systems for meta-programming. The abstract concept of open code (not necessarily
that of # ) is more general than closed code. In a specific programming environment
(as already observed by (Davies, 1996)), working with open code is more flexible
and results in better and more optimized residual object programs. However, we
also want to run the generated object programs when they are closed, and thus we
need a type system which integrates modal types for both closed and open code.
There have been several proposed type systems providing this expressiveness,
most notable being MetaML (Moggi et al., 1999; Taha, 1999; Calcagno et al., 2000;
Calcagno et al., 2001). MetaML defines its notion of open code to be that of the
Names and Necessity 3
postponed code of # and then introduces closed code as a refinement - as open
code which happens to contain no free variables.
The approach in our calculus (which we call # ) is opposite. Rather than refining
the notion of postponed code of # , we relax the notion of closed code of # . We
start with the system of # , but provide the additional expressiveness by allowing
the code to contain specified object variables as free (and rudiments of this idea have
already been considered in (Nielsen, 2001)). If a given code expression depends on a
set of free variables, it will be reflected in its type. The object variables themselves
are represented by a separate semantic category of names (also called symbols or
atoms), which admits equality. The treatment of names is inspired by the work on
Nominal Logic and FreshML (Gabbay & Pitts, 2002; Pitts & Gabbay, 2000; Pitts,
2001; Gabbay, 2000). This design choice leads to a logically motivated and easily
extendable type system. For example, we describe in (Nanevski, 2002) an extension
with intensional code analysis which allows object expressions to be compared for
structural equality and destructed via pattern-matching, much in the same way as
one would work with any abstract syntax tree.
This paper is organized as follows: Section 2 is a brief exposition of prior work
on # . The type system of # and its properties are described in Section 3, while
Section 4 describes parametric polymorphism in sets of names. We illustrate the
type system with example programs, before discussing the related work in Section 5.
Modal # -calculus
This section reviews the previous work on the modal # -calculus and its use in
meta-programming to separate, through the mechanism of types, the realms of
meta-level programs and object-level programs. The # -calculus is the proof-term
calculus for the necessitation fragment of modal logic S4 (Pfenning & Davies, 2001;
Davies & Pfenning, 2001). Chronologically, it came to be considered in functional
programming in the context of specialization for purposes of run-time code generation
(Wickline et al., 1998b; Wickline et al., 1998a). For example, consider the
exponentiation function, presented below in ML-like notation.
The function exp1 : int -> int -> int is written in curried form so that it
can be applied when only a part of its input is known. For example, if an actual
parameter for n is available, exp1(n) returns a function for computing the n-th
power of its argument. In a practical implementation of this scenario, however, the
outcome of the partial instantiation will be a closure waiting to receive an actual
parameter for x before it proceeds with evaluation. Thus, one can argue that the
following reformulation of exp1 is preferable.
4 A. Nanevski, F. Pfenning
else
let val
in
#x:int. x * u(x)
Indeed, when only n is provided, but not x, the expression exp2(n) performs computation
steps based on the value of n to produce a residual function specialized
for computing the n-th power of its argument. In particular, the obtained residual
function will not perform any operations or take decisions at run-time based on
the value of n; in fact, it does not even depend on n - all the computation steps
dependent on n have been taken during the specialization.
A useful intuition for understanding the programming idiom of the above ex-
ample, is to view exp2 as a program generator; once supplied with n, it generates
the specialized function for computing n-th powers. This immediately suggests a
distinction in the calculus between two stages (or levels): the meta and the object
stage. The object stage of an expression encodes #-terms that are to be viewed as
data - as results of a process of code generation. In the exp2 function, such terms
would be (#x:int.1) and (#x:int. x * u(x)). The meta stage describes the specific
operations to be performed over the expressions from the object stage. This is
why the above-illustrated programming style is referred to as staged computation.
The idea behind the type system of # is to make explicit the distinction between
meta and object stages. It allows the programmer to specify the intended staging of
a term by annotating object-level subterms of the program. Then the type system
can check whether the written code conforms to the staging specifications, making
staging errors into type errors. The syntax of # is presented below; we use b to
stand for a predetermined set of base types, and c for constants of those types.
Types A ::= b | A 1 # A 2 | #A
erms e ::= c | x | u | #x:A. e | e 1 e 2 |
alue variable contexts #, x:A
Expression variable contexts #, u:A
alues v ::= c | #x:A. e | box e
There are several distinctive features of the calculus, arising from the desire to
di#erentiate between the stages. The most important is the new type constructor #.
It is usually referred to as modal necessity, as on the logic side it is a necessitation
modifier on propositions (Pfenning & Davies, 2001). In our meta-programming
application, it is used to classify object-level terms. Its introduction and elimination
forms are the term constructors box and let box, respectively. As Figure 1 shows, if
e is an object term of type A, then box e would be a meta term of type #A. The box
term constructor wraps the object term e so that it can be accessed and manipulated
by the meta part of the program. The elimination form let box does
Names and Necessity 5
the opposite; it takes the object term enclosed in e 1 and binds it to the variable u
to be used in e 2 .
The type system of # distinguishes between two kinds of variables, and consequently
has two variable contexts: # for variables bound to meta terms, and #
for variables bound to object terms. We implicitly assume that exchange holds for
both; that is, that the order of variables in the contexts is immaterial.

Figure

2 presents the small-step operational semantics of # . We have decided on
a call-by-value strategy which, in addition, prohibits reductions on the object level.
Thus, if an expression is boxed, its evaluation will be suspended. Boxed expressions
themselves are considered values. This choice is by no means canonical, but is
necessary for the applications in this paper.
We can now use the type system of # to make explicit the staging of exp2.
else
let box
in
box (#x:int. x * u(x))
Application of exp3 at argument 2 produces an object-level function for squaring.
val (#x:int. x *
(#y:int. y *
(#z:int.
In the elimination form let box , the bound variable u belongs to the
context # of object-level variables, but it can be used in e 2 in both object positions
(i.e., under a box) and meta positions. This way the calculus is not only capable
of composing object programs, but can also explicitly force their evaluation. For
example we can use the generated function sqbox in the following way.
val
val
This example demonstrates that object expressions of # can be reflected; that
is, coerced from the object-level into the meta-level. The opposite coercion which
is referred to as reification, however, is not possible. This suggests that # should
be given a more specific model in which reflection naturally exists, but reification
does not. A possible interpretation exhibiting this behavior considers object terms
as actual syntactic expressions, or abstract syntax trees of source programs of the
calculus, while the meta terms are compiled executables. Because # is typed, in
this scenario the object terms represent not only syntax, but higher-order syntax
(Pfenning & Elliott, 1988) as well. The operation of reflection corresponds to the
6 A. Nanevski, F. Pfenning
#,
#,
Fig. 1. Typing rules for # .
(#x:A.
let box
let box
Fig. 2. Operational semantics of # .
natural process of compiling source code into an executable. The opposite operation
of reconstructing source code out of its compiled equivalent is not usually feasible,
so this interpretation does not support reification, just as required.
Modal calculus of names
3.1 Motivation, syntax and overview
If we adhere to the interpretation of object terms as higher-order syntax, then
the # staging of exp3 is rather unsatisfactory. The problem is that the residual
object programs produced by exp3 (e.g., sqbox), contain unnecessary variable-for-
variable redexes, and hence are not as optimal as one would want. This may not
be a serious criticism from the perspective of run-time code generation; indeed,
variable-for-variable redexes can easily be eliminated by a compiler. But if object
terms are viewed as higher-order syntax (and, as we argued in the previous section,
this is a very natural model for the # -calculus), the limitation is severe. It exhibits
that # is too restrictive to allow for arbitrary composition of higher-order syntax
trees. The reason for the deficiency is in the requirement that boxed object terms
must always be closed. In that sense, the type #A is a type of closed syntactic
expressions of type A. As can be observed from the typing rules in Figure 1, the
#-introduction rule erases all the meta variables before typechecking the argument
term. It allows for object level variables, but in run-time they are always substituted
by other closed object expressions to produce a closed object expression at the end.
Names and Necessity 7
Unfortunately, if we only have a type of closed syntactic expressions at our disposal,
we can't ever type the body of an object-level #-abstraction in isolation from the
#-binder itself - subterms of a closed term are not necessarily closed themselves.
Thus, it would be impossible to ever inspect, destruct or recurse over object-level
expressions with binding structure.
The solution should be to extend the notion of object level to include not only
closed syntactic expressions, but also expressions with free variables. This need has
long been recognized in the meta-programming community, and Section 5 discusses
several di#erent meta-programming systems and their solutions to the problem.
The technique predominantly used in these solutions goes back to the Davies' # -
calculus (Davies, 1996). The type constructor # of this calculus corresponds to
discrete temporal logic modality for propositions true at the subsequent time mo-
ment. In meta-programming setup, the modal type #A stands for open object
expression of type A, where the free variables of the object expression are modeled
by meta-variables from the subsequent time moment, bound somewhere outside of
the expression.
Our # -calculus adopts a di#erent approach. It seems that for purposes of higher-order
syntax, one cannot equate bound meta-variables with free variables of object
expressions. For, imagine recursing over two syntax trees with binding structure
to compare them for syntactic equality modulo #-conversion. Whenever a
#-abstraction is encountered in both expressions, we need to introduce a new entity
to stand for the bound variable of that #-abstraction, and then recursively proceed
comparing the bodies of the abstractions. But then, introducing this new entity
standing for the #-bound variable must not change the type of the surrounding
term. In other words, free variables of object expressions cannot be introduced into
the computation by a type introduction form, like #-abstraction, as it is the case
in # and other languages based on it.
Thus, we start with the # -calculus, and introduce a separate semantic category
of names, motivated by (Pitts & Gabbay, 2000; Gabbay & Pitts, 2002), and also
(Odersky, 1994). Just as before, object and meta stages are separated through the
#-modality, but now object terms can use names to encode abstract syntax trees
variables. The names appearing in an object term will be apparent from
its type. In addition, the type system must be instrumented to keep track of the
occurrences of names, so that the names are prevented from slipping through the
scope of their introduction form.
Informally, a term depends on a certain name if that name appears in the meta-level
part of the term. The set of names that a term depends on is called the support
of the term. The situation is analogous to that in polynomial algebra, where one is
given a base structure S and a set of indeterminates (or generators) I and then freely
adjoins S with I into a structure of polynomials. In our setup, the indeterminates are
the names, and we build "polynomials" over the base structure of # expressions.
For example, assuming for a moment that X and Y are names of type int, and that
the usual operations of addition, multiplication and exponentiation of integers are
8 A. Nanevski, F. Pfenning
primitive in # , the term
would have type int and support set {X, Y }. The names X and Y appear in e 1 at
the meta level, and indeed, notice that in order to evaluate e 1 to an integer, we first
need to provide definitions for X and Y . On the other hand, if we box the term e 1 ,
we obtain
which has the type #X,Y int, but its support is the empty set, as the names X and
Y only appear at the object level (i.e., under a box). Thus, the support of a term
(in this case e 1 ) becomes part of the type once the term itself is boxed. This way,
the types maintain the information about the support of subterms at all stages. For
example, assuming that our language has pairs, the term
would have the type int -# Y int with support {X}.
We are also interested in compiling and evaluating syntactic entities in # when
they have empty support (i.e., when they are closed). Thus, we need a mechanism
to eliminate a name from a given expression's support, eventually turning
non-executable expressions into executable ones. For that purpose, we use explicit
substitutions. An explicit substitution provides definitions for names which appear
at a meta-level in a certain expression. Note the emphasis on the meta-level; explicit
substitutions do not substitute under boxes, as names appearing at the object level
of a term do not contribute to the term's support. This way, explicit substitutions
provide extensions (i.e., definitions) for names, while still allowing names under
boxes to be used for the intensional information of their identity (which we utilize
in a related development described in (Nanevski, 2002)).
We next present the syntax of the # -calculus and discuss each of the constructors

Names X # N
Types A ::= b | A 1 # A 2 | A 1 # A 2 | #CA
substitutions # ::= - | X # e, #
erms e ::= c | X | x | #u | #x:A. e | e 1 e 2 |
#X :A. e | choose e
alue variable contexts #, x:A
Expression variable contexts #, u:A[C]
Name contexts #, X :A
Just as # , our calculus makes a distinction between meta and object levels, which
here too are interpreted as the level of compiled code and the level of source code
(or abstract syntax expressions), respectively. The two levels are separated by a
modal type constructor #, except that now we have a whole family of modal type
Names and Necessity 9
constructors - one for each finite set of names C. In that sense, values of the type
#CA are the abstract syntax trees of the calculus freely generated over the set of
names C. We refer to the finite set C as a support set of such syntax trees. All the
names are drawn from a countably infinite universe of names N .
As before, the distinction in levels forces a split in the variable contexts. We
have a context # for meta-level variables (we will also call them value variables),
and a context # for object-level variables (which we also call syntactic expression
variables, or just expression variables). The context # must keep track not only of
the typing of a given variable, but also of its support set.
The set of terms includes the syntax of the # -calculus from Section 2. How-
ever, there are two important distinctions in # . First, we can now explicitly refer
to names on the level of terms. Second, it is required that all the references
to expression variables that a certain term makes are always prefixed by some
explicit substitution. For example, if u is an expression variable bound by some
let box then u can only appear in e 2 prefixed by an explicit
substitution # (and di#erent occurrences of u can have di#erent substitutions associated
with them). The explicit substitution is supposed to provide definitions for
names in the expression bound to u. When the reference to the variable u is pre-fixed
by an empty substitution, instead of #u we will simply write u. The explicit
substitutions used in # -calculus are simultaneous substitutions. We assume that
the syntactic presentation of a substitution never defines a denotation for the same
name twice.
Example 1 Assuming that X and Y are names of type int, the code segment below
creates a polynomial over X and Y and then evaluates it at the point
2).
in
val
The terms #x:A. e and choose e are the introduction and elimination form for
the type constructor A # B. The term #X :A. e binds a name X of type A that can
subsequently be used in e. The term choose picks a fresh name of type A, substitutes
it for the name bound in the argument #-abstraction of type A # B, and proceeds
to evaluate the body of the abstraction. To prevent the bound name in #X :A. e
from escaping the scope of its definition and thus creating an observable e#ect, the
type system must enforce a discipline on the use of X in e. An occurrence of X at
a certain position in e will be allowed only if the type system can establish that
that occurrence of X will not be encountered during evaluation. Such possibilities
arise in two ways: if X is eventually substituted away by an explicit substitution,
A. Nanevski, F. Pfenning
or if X appears in a computationally irrelevant (i.e., dead-code) part of the term.
Needless to say, deciding these questions in a practical language is impossible. Our
type system provides a conservative approximation using a fairly simple analysis
based on propagation of names encountered during typechecking.
Finally, enlarging an appropriate context by a new variable or a name is subject to
the usual variable conventions: the new variables and names are assumed distinct, or
are renamed in order not to clash with already existing ones. Terms that di#er only
in the syntactic representation of their bound variables and names are considered
equal. The binding forms in the language are #x:A. e, let box
#X :A. e. As usual, capture-avoiding substitution [e 1 /x]e 2 of expression e 1 for the
variable x in the expression e 2 is defined to rename bound variables and names
when descending into their scope. Given a term e, we denote by fv(e) and fn(e) the
set of free variables of e and the set of names appearing in e at the meta-level. In
addition, we overload the function fn so that given a type A and a support set C,
fn(A[C]) is the set of names appearing in A or C.
Example 2 To illustrate our new constructors, we present a version of the staged
exponentiation function that we can write in # -calculus. In this and in other
examples we resort to concrete syntax in ML fashion, and assume the presence of
the base type of integers, recursive functions and let-definitions.
choose (#X : int.
let fun exp' (m
else
let box
in
in
let box
in
box (#x:int. #X -> x# v)
end)
val
The function exp takes an integer n and generates a fresh name X of integer type.
Then it calls the helper function exp' to build the expression
| {z }
of type int and support {X}. Finally, it turns the expression v into a function by
explicitly substituting the name X in v with a newly introduced bound variable x.
Names and Necessity 11
Notice that the generated residual code for sq does not contain any unnecessary
redexes, in contrast to the # version of the program from Section 2.
3.2 Explicit substitutions
In this section we formally introduce the concept of explicit substitution over names
and define related operations. As already outlined before, substitutions serve to
provide definitions for names, thus e#ectively removing the substituting names from
the support of the term in which they appear. Once the term has empty support,
it can be compiled and evaluated.
its domain and range)
An explicit substitution is a function from the set of names to the set of terms
Given a substitution #, its domain dom(#) is the set of names that the substitution
does not fix. In other words
Range of a substitution # is the image of dom(#) under #:
For the purposes of this work, we only consider substitutions with finite domains.
A substitution # with a finite domain has a finitary syntactical representation as a
set of ordered pairs X # e, relating a name X from dom(#), with its substituting
expression e. The opposite also holds - any finite and functional set of ordered pairs
of names and expressions determines a unique substitution. We will frequently
equate a substitution and the set that represents it when it does not result in
ambiguities. Just as customary, we denote by fv(#) the set of free variables in the
terms from range(#). The set of names appearing either in dom(#) or range(#) is
denoted by fn(#).
Each substitution can be uniquely extended to a function over arbitrary terms
in the following way.
Given a substitution # and a term e, the operation {#}e of applying # to the meta
level of e is defined recursively on the structure of e as given below. Substitution
A. Nanevski, F. Pfenning
application is capture-avoiding.
{#x:A.
{#} (let box
{#} (choose choose {#}e
The most important aspect of the above definition is that substitution application
does not recursively descend under box. This property is of utmost importance for
the soundness of our calculus as it preserves the distinction between the meta and
the object levels. It is also justified, as explicit substitutions are intended to only
remove names which are in the support of a term, and names appearing under box
do not contribute to the support.
The operation of substitution application depends upon the operation of substitution
composition which we define next.
Definition 3 (Composition of substitutions)
Given two substitutions # 1 and # 2 with finite domains, their composition # 1 # 2
is the substitution defined as
The composition of two substitutions with finite domains is well-defined, as the
resulting mapping from names to terms is finite. Indeed, for every name X #
finite, the syntactic
representation of the composition can easily be computed as the set
It will occasionally be beneficial to represent this set as a disjoint union of two
smaller sets # 1
defined as:
It is important to notice that, though the definitions of substitution application
and substitution composition are mutually recursive, both the operations are ter-
minating. Substitution application is defined inductively over the structure of its
argument, so the size of terms on which it operates is always decreasing. Composing
substitutions with finite domain also terminates because # 1 # 2 requires only
applying # 1 to the defining terms in # 2 .
Names and Necessity 13
3.3 Type system
The type system of the # -calculus consists of two mutually recursive judgments:
and
Both of them are hypothetical and work with three contexts: context of names #,
context of expression variables #, and a context of value variables # (the syntactic
structure of all three contexts is given in Section 3.1). The first judgment is the
typing judgment for expressions. Given an expression e it checks whether e has type
A, and is generated by the support set C. The second judgment types the explicit
substitutions. Given a substitution # and two support sets C and D, the substitution
has the type [C] # [D] if it maps expressions of support C to expressions of
support D. This intuition will be proved in Section 3.4.
The contexts deserve a few more words. Because the types of # -calculus depend
on names, and types of names can depend on other names as well, we must impose
some conditions on well-formedness of contexts. Henceforth, variable contexts #
and # will be well-formed relative to # if # declares all the names that appear in
the types of # and #. A name context # is well-formed if every type in # uses
only names declared to the left of it. Further, we will often abuse the notation and
to define the set # obtained after removing the name X from
the context #. Obviously, # does not have to be a well-formed context, as types in
it may depend on X , but we will always transform # into a well-formed context
before using it again. Thus, we will always take care, and also implicitly assume,
that all the contexts in the judgments are well-formed. The same holds for all the
types and support sets that we use in the rules.
The typing rules of # are presented in Figure 3. A pervasive characteristic of
the type system is support weakening. Namely, if a term is in the set of expressions
of type A freely generated by a support set C, then it certainly is among the
expressions freely generated by some support set D # C. We make this property
admissible to both judgments of the type system, and it will be proved as a lemma
in Section 3.4.
Explicit substitutions. A substitution with empty syntactic representation is the
identity substitution. When an identity substitution is applied to a term containing
names from C, the resulting term obviously contains names from C. But the support
of the resulting term can be extended by support weakening to a superset D, as
discussed above, so we bake this property into the side condition C # D for the
identity substitution rule. We implicitly require that both the sets are well-formed;
that is, they both contain only names already declared in the name context #.
The rule for non-empty substitutions recursively checks each of its component
terms for being well typed in the given contexts and support. It is worth noticing
however, that a substitution # can be given a type [C] # [D] where the "domain"
support set C is completely unrelated to the set dom(#). In other words, the sub-
14 A. Nanevski, F. Pfenning
Explicit substitutions
Hypothesis
#,
#,
#-calculus
#,
Modality
Names
Fig. 3. Typing rules of the # -calculus.
stitution can provide definitions for more names or for fewer names than the typing
judgment actually expresses. For example, the substitution
has domain dom(#) = {X, Y }, but it can be given (among others) the typings:
as well as [X, Y, Z] # [Z]. And indeed, # does map a term of
another term with support [ ], a term of support [X ] into a term
with support [ ], and a term with support [X, Y, Z] into a term with support [Z].
Hypothesis rules. Because there are three kinds of variable contexts, we have three
hypothesis rules. First is the rule for names. A name X can be used provided it has
been declared in # and is accounted for in the supplied support set. The implicit
assumption is that the support set C is well-formed; that is, C # dom (#). The
rule for value variables is straightforward. The typing x:A can be inferred, if x:A
is declared in #. The actual support of such a term can be any support set C as
long as it is well-formed, which is implicitly assumed. Expression variables occur
in a term always prefixed with an explicit substitution. The rule for expression
variables has to check if the expression variable is declared in the context # and if
its corresponding substitution has the appropriate type.
Names and Necessity 15
#-calculus fragment. The rule for #-abstraction is quite standard. Its implicit assumption
is that the argument type A is well-formed in name context # before
it is introduced into the variable context #. The application rule checks both the
function and the application argument against the same support set.
Modal fragment. Just as in # -calculus, the meaning of the rule for #-introduction
is to ensure that the boxed expression e represents an abstract syntax tree. It checks
e for having a given type in a context without value variables. The support that
e has to match is supplied as an index to the # constructor. On the other hand,
the support for the whole expression box e is empty, as the expression obviously
does not contain any names at the meta level. Thus, the support can be arbitrarily
weakened to any well-formed support set D. The #-elimination rule is also a
straightforward extension of the corresponding # rule. The only di#erence is that
the bound expression variable u from the context # now has to be stored with its
support annotation.
Names fragment. The introduction form for names is #X :A. e with its corresponding
type A # B. It introduces an "irrelevant" name X :A into the computation
determined by e. It is assumed that the type A is well-formed relative to the context
#. The term constructor choose is the elimination form for A # B. It picks
a fresh name and substitutes it for the bound name in the #-abstraction. In other
words, the operational semantics of the redex choose (#X :A. e) (formalized in Section
proceeds with the evaluation of e in a run-time context in which a fresh
name has been picked for X . It is justified to do so because X is bound by # and,
by convention, can be renamed with a fresh name. The irrelevancy of X in the
above example means that X will never be encountered during the evaluation of e
in a computationally significant position. Thus, (1) it is not necessary to specify its
run-time behavior, and (2) it can never escape the scope of its introducing # in any
observable way. The side-condition to #-introduction serves exactly to enforce this
irrelevancy. It e#ectively limits X to appear only in "dead-code" subterms of e or
in subterms from which it will eventually be removed by some explicit substitution.
For example, consider the following term
#X:int. #Y:int.
box (let box
in
end)
It contains a substituted occurrence of X and a dead-code occurrence of Y , and is
therefore well-typed (of type int # int #int).
One may wonder what is the use of entities like names which are supposed to
appear only in computationally insignificant positions in the computation. The
fact is, however, that names are not insignificant at all. Their import lies in their
identity. For example, in a related development on intensional analysis of syntax
(Nanevski, 2002), we compare names for equality - something that cannot be done
A. Nanevski, F. Pfenning
with ordinary variables. For, ordinary variables are just placeholders for some val-
ues; we cannot compare the variables for equality, but only the values that the
variables stand for. In this sense we can say that #-abstraction is parametric, while
#-abstraction is deliberately designed not to be.
It is only that names appear irrelevant because we have to force a certain discipline
upon their usage. In particular, before leaving the local scope of some name
X , as determined by its introducing #, we have to "close up" the resulting expression
if it depends significantly on X . This "closure" can be achieved by turning the
expression into a #-abstraction by means of explicit substitutions. Otherwise, the
introduction of the new name will be an observable e#ect. To paraphrase, when
leaving the scope of X , we have to turn the "polynomials" depending on X into
functions. An illustration of this technique is the program already presented in
Example 2.
The previous version of this work (Nanevski, 2002) did not use the constructors
# and choose, but rather combined them into a single constructor new. This is also
the case in the (Pitts & Gabbay, 2000). The decomposition is given by the equation
new X :A in choose (#X :A. e)
We have decided on this reformulation in order to make the types of the language
follow more closely the intended meaning of the terms and thus provide a stronger
logical foundation for the calculus.
3.4 Structural properties
This section explores the basic theoretical properties of our type system. The lemmas
developed here will be used to justify the operational semantics that we ascribe
to # -calculus in Section 3.5, and will ultimately lead to the proof of type preservation
(Theorem 12) and progress (Theorem 13).
Lemma 4 (Structural properties of contexts)
1. Weakening Let # and # . Then
(a) if
2. Contraction on variables
(a) if #, x:A,
(b) if #, x:A,
#,
(c) if #, u:A[D], v:A[D]);
#,
(d) if #, u:A[D],
#,
Proof
By straightforward induction on the structure of the typing derivations.
Names and Necessity 17
Contraction on names does not hold in # . Indeed, identifying two di#erent
names in a term may make the term syntactically ill-formed. Typical examples
are explicit substitutions which are in one-one correspondence with their syntactic
representations. Identifying two names may make a syntactic representation assign
two di#erent images to a same name which would break the correspondence with
substitutions.
The next series of lemmas establishes the admissibility of support weakening, as
discussed in Section 3.3.
Lemma 5 (Support weakening)
Support weakening is covariant on the right-hand side and contravariant on the
left-hand side of the judgments. More formally, let C # C # dom(#) and D #
dom(#) be well-formed support sets. Then the following holds:
1. if
2.
3. if #, u:A[D]);
4.
Proof
The first two statements are proved by straightforward simultaneous induction on
the given derivations. The third and the fourth part are proved by induction on the
structure of their respective derivations.
Lemma 6 (Support extension)
Let D # dom(#) be a well-formed support set. Then the following holds:
1. if #, u:A[C 1
2.
Proof
By induction on the structure of the derivations.
Lemma 7 (Substitution merge)
dom(#,
Proof
By induction on the structure of # .
The following lemma shows that the intuition behind the typing judgment for
explicit substitutions explained in Section 3.3 is indeed valid.
Lemma 8 (Explicit substitution principle)
the following holds:
1. if
2.
Proof
A. Nanevski, F. Pfenning
By simultaneous induction on the structure of the derivations. We just present the
proof of the second statement.
Given the substitutions # and # , we split the representation of # into two
disjoint sets:
and set out to show that
These two typings imply the result by the substitution merge lemma (Lemma 7).
To establish (a), observe that from the typing of # it is clear that # 1
dom(# [D]. By definition of dom(# fixed
by # . Thus, either X does not appear in the syntactic representation of # , or the
syntactic representation of # contains a sequence of mappings
. , In the second case, X is the substituting term for Xn , and thus
In the first case, X # C by inductively appealing to the typing rules for
substitutions until the empty substitution is reached. Either way, C 1 \dom(# C,
and furthermore C 1 \ dom(# C \ dom(# ). Now the result follows by support
weakening (Lemma 5.4).
The establish (b) observe that if X # dom(# ), and X :A #, then #
[C]. By the first induction hypothesis, # (X)) : A [D]. The
typing (b) is now obtained by inductively applying the typing rules for substitutions
for each X # (C 1 # dom(# )).
The following lemma establishes the hypothetical nature of the two typing judgment
with respect to the ordinary value variables.
Lemma 9 (Value substitution principle)
[C]. The following holds:
1. if #, x:A) # e
2. if #,
Proof
Simultaneous induction on the two derivations.
The situation is not that simple with expression variables. A simple substitution
of an expression for some expression variable will not result in a syntactically well-formed
term. The reason is, as discussed before, that occurrences of expression
variables are always prefixed by an explicit substitution to form a kind of closure.
But, explicit substitutions in # -calculus can occur only as part of closures, and
cannot be freely applied to arbitrary terms 1 . Hence, if a substitution of expression e
for expression variable u is to produce a syntactically valid term, we need to follow
1 Albeit this extension does not seem particularly hard, we omit it for simplicity.
Names and Necessity 19
it up with applications over e of explicit name substitutions that were paired up
with u. This operation also gives us a control over not only the extensional, but also
the intensional form of boxed expressions. The definition below generalizes capture-avoiding
substitution of expression variables in order to handle this problem.
(Substitution of expression variables)
The capture-avoiding substitution of e for an expression variable u is defined recursively
as follows
choose e
Note that in the first clause #u of the above definition the resulting expression is
obtained by carrying out the explicit substitution.
Lemma 11 (Expression substitution principle)
Let e 1 be an expression without free value variables such that # e
Then the following holds:
1. if #, u:A[C]); # e
2. if #,
Proof
By simultaneous induction on the two derivations. We just present one case from
the proof of the first statement.
case
1. by derivation,
2. by the second induction hypothesis, #[[e
3. by explicit substitution (Lemma 8.1), # {[[e 1
4. but this is exactly equal to
3.5 Operational semantics
We define the small-step call-by-value operational semantics of the # -calculus
through the judgment
#, e # , e #
A. Nanevski, F. Pfenning
#,
#, (e1 e2) # ,
#, e2 # , e # 2
#, (v1 e2
#x:A. e) v #, [v/x]e
#,
#, (let box
#, (let box
#, e # , e #
#, choose e # , choose e #, choose (#X:A. e) #, X:A), e
Fig. 4. Structured operational semantics of # -calculus.
which relates an expression e with its one-step reduct e # . The relation is defined
on expressions with no free variables. An expression can contain free names, but
it must have empty support. In other words, we only consider for evaluation those
terms whose names appear exclusively at the object level, or in computationally
irrelevant positions, or are removed by some explicit substitution. Because free
names are allowed, the operational semantics has to account for them by keeping
track of the run-time name contexts. The rules of the judgment are given in Figure 4,
and the values of the language are generated by the grammar below.
alues v ::= c | #x:A. e | box e | #X :A. e
The rules are standard, and the only important observation is that the #-redex
for the type constructor # extends the run-time context with a fresh name before
proceeding. This extension is needed for soundness purposes. Because the freshly introduced
name may appear in computationally insignificant positions in the reduct,
we must keep the name and its typing in the run-time context.
The evaluation relation is sound with respect to typing, and it never gets stuck,
as the following theorems establish.
Theorem 12 (Type preservation)
If extends #, and # e
Proof
By a straightforward induction on the structure of e using the substitution principles

Theorem 13 (Progress)
If
1. e is a value, or
2. there exist a term e # and a context # , such that #, e # , e # .
Proof
Names and Necessity 21
By a straightforward induction on the structure of e.
The progress theorem does not indicate that the reduct e # and the context #
are unique for each given e and #. In fact, they are not, as fresh names may be
introduced during the course of the computation, and two di#erent evaluations of
one and the same term may choose the fresh names di#erently. The determinacy
theorem below shows that the choice of fresh names accounts for all the di#erences
between two reductions of the same term. As customary, we denote by # n the
n-step reduction relation.
Theorem 14 (Determinacy)
If #, e # there exists a permutation of names
fixing dom(#), such that #
Proof
By induction on the length of the reductions, using the property that if #, e # n
# , e # and # is a permutation on names, then #(e) # n #(e # ). The only
interesting case is when choose (#X :A. e # ). In that case, it must
be
are fresh. Obviously, the involution these
two names has the required properties.
It is frequently necessary to write programs which are polymorphic in the support
of their syntactic object-level arguments, because they are intended to manipulate
abstract syntax trees whose support is not known at compile time. A typical
example would be a function which recurses over some syntax tree with binding
structure. When it encounters a #-abstraction, it has to place a fresh name instead
of the bound variable, and recursively continue scanning the body of the
#-abstraction, which is itself a syntactic expression but depending on this newly
introduced name. 2 For such uses, we extend the # -calculus with a notion of explicit
support polymorphism in the style of Girard and Reynolds (Girard, 1986;
Reynolds, 1983).
The addition of support polymorphism to the simple # -calculus starts with
syntactic changes that we summarize below.
Support variables p, q # S
sets C, D # P(N # S)
Types A ::= . | #p. A
erms e ::= . | #p. e | e [C]
Name context #, p
alues v ::= . | #p. e
2 The calculus described here cannot support this scenario in full generality yet because it lacks
type polymorphism and type-polymorphic recursion, but support polymorphism is a necessary
step in that direction.
22 A. Nanevski, F. Pfenning
We introduce a new syntactic category of support variables, which are intended
to stand for unknown support sets. In addition, the support sets themselves are
now allowed to contain these support variables, to express the situation in which
only a portion of a support set is unknown. Consequently, the function fn(-) must
be updated to now return the set of names and support variables appearing in
its argument. The language of types is extended with the type #p. A expressing
universal support quantification. Its introduction form is #p. e, which abstracts
an unknown support set p in the expression e. This #-abstraction will also be a
value in the extended operational semantics. The corresponding elimination form
is the application e [C] whose meaning is to instantiate the unknown support set
abstracted in e with the provided support set C. Because now the types can depend
on names as well as on support variables, the name contexts must declare both. We
assume the same convention on well-formedness of the name context as before.
The typing judgment has to be instrumented with new rules for typing support-
polymorphic abstraction and application.
The #-introduction rule requires that the bound variable p does not escape the
scope of the constructors # and # which bind it. In particular it must be p # C.
The convention also assumes implicitly that p #, before it can be added. The
rule for #-elimination substitutes the argument support set D into the type A. It
assumes that D is well-formed relative to the context #; that is, D # dom(#). The
operational semantics for the new constructs is also not surprising.
#, e # , e #
#,
The extended language satisfies the following substitution principle.
Lemma 15 (Support substitution principle)
the operation of substituting
D for p. Then the following holds.
1. if
2.
Proof
By simultaneous induction on the two derivations. We present one case from the
proof of the second statement.
case
1. by derivation,
2. by first induction hypothesis,
3. by second induction hypothesis,
4. because (C # 1 \ {X}) # (C 1 \ {X}) # , by support weakening (Lemma 5.4),
Names and Necessity 23
5. result follows from (2) and (4) by the typing rule for non-empty substitution

The structural properties presented in Section 3.4 readily extend to the new
language with support polymorphism. The same is true of the type preservation
(Theorem 12) and progress (Theorem 13) whose additional cases involving support
abstraction and application are handled using the above Lemma 15.
Example 3 In a support-polymorphic # -calculus we can slightly generalize the
program from Example 2 by pulling out the helper function exp' and parametrizing
it over the exponentiating expression. In the following program, we use [p] in the
function definition as a concrete syntax for #-abstraction of a support variable p.
else
let box
in
choose (#X : int.
let box
in
box (#x:int. #X -> x# w)
end)
val
Example 4 As an example of a more realistic program we present the regular expression
matcher from (Davies & Pfenning, 2001) and (Davies, 1996). The example
assumes the declaration of the datatype of regular expressions:
datatype
Empty
| Plus of regexp * regexp
| Times of regexp * regexp
| Star of regexp
| Const of char
A. Nanevski, F. Pfenning
(*
* val acc1 : regexp -> (char list -> bool) ->
* char list -> bool
| acc1 (Plus (e1,
| acc1 (Times (e1,
(acc1 e1 (acc1 e2 k)) s
| acc1 (Star e) k
else acc1 (Star e) k s')
| acc1 (Const c) k
case s
of nil => false
| (x::l) =>
(*
* val accept1 : regexp -> char list -> bool
Fig. 5. Unstaged regular expression matcher.
We also assume a primitive predicate null : char list -> bool testing if the
input string is empty. Figure 5 presents an ordinary ML implementation of the
matcher, and # and # versions can be found in (Davies & Pfenning, 2001; Davies,
1996).
We would now like to use the # -calculus to stage the program from Figure 5
so that it can be specialized with respect to a given regular expression. For that
purpose, it is useful to view the helper function acc (called acc1 in Figure 5) as a
code generator. It takes a regular expression e and emits code for parsing according
to e, and at the end, it appends k to the generated code. This is the main idea behind
the program in Figure 6. Here, for simplicity, we use the name S for the input string
to be parsed by the code that acc generates. We also want to allow the continuation
code k to contain further names standing for yet unbound variables, and hence the
support-polymorphic typing acc : regexp -> #p.(# S,p bool -> # S,p bool). The
support polymorphism pays o# when generating code for alternation Plus(e 1 , e 2 )
and iteration Star(e). Indeed, observe in the alternation case that the generated
code does not duplicate the continuation k. Rather, k is emitted as a separate
function which is a joining point for the computation branches corresponding to
e 1 and e 2 . Similarly, in the case of iteration, we set up a loop in the output code
that would attempt zero or more matchings against e. The support polymorphism
of acc enables us to produce code in chunks without knowing the exact identity
of the above-mentioned joining or looping points. Once all the parts of the output
code are generated, we just stitch them together by means of explicit substitutions.
Names and Necessity 25
(*
* val accept : regexp ->
* #(char list -> bool)
choose list.
(*
* -> #S,p bool)
let fun acc (Empty) [p]
| acc (Plus (e1, e2)) [p]
choose list
-> bool.
let box
acc e1 [JOIN] box(JOIN S)
acc e2 [JOIN] box(JOIN S)
in
box(let fun join
in
orelse
end)
| acc (Times (e1, e2)) [p]
acc e1 (acc e2
| acc (Star e) [p]
choose list
choose list
-> bool.
let box
acc e [T, LOOP]
else LOOP S)
in
box(let fun loop
orelse
in
loop S
end)
| acc (Const c) [p]
let box
in
box(case S
of (x::xs) =>
| nil => false)
in
box (#s:char list. <S->s>code)
Fig. 6. Regular expression matcher staged in the # -calculus.
At this point, it may be illustrative to trace the execution of the program on
a concrete input. Figure 7 presents the function calls and the intermediate results
that occur when the # -staged matcher is applied to the regular expression
Star(Empty). Note that the resulting specialized program does not contain variable-
for-variable redexes, but it does perform unnecessary boolean tests. It is possible
to improve the matching algorithm to avoid emitting this extraneous code. The
improvement involves a further examination and preprocessing of the input regular
expression, but the thorough description is beyond the scope of this paper. We refer
to (Harper, 1999) for an insightful analysis.
5 Related work
The work presented in this paper lies in the intersection of several related ar-
eas: staged computation and partial evaluation, run-time code generation, meta-
programming, modal logic and higher-order abstract syntax.
An early reference to staged computation is (Ershov, 1977) which introduces
26 A. Nanevski, F. Pfenning
else LOOP S))
null (t) orelse
in
loop S
end)
# box (#s. let fun loop
null (t) orelse
in
loop s
end)
Fig. 7. Example execution trace for a regular expression matcher in # . Function calls
are marked by # and the corresponding return results are marked by an aligned #.
staged computation under the name of "generating extensions". Generating extensions
for purposes of partial evaluation were also foreseen by (Futamura, 1971), and
the concept is later explored and eventually expanded into multi-level generating
extensions by (Jones et al., 1985; Gl-uck & J-rgensen, 1995; Gl-uck & J-rgensen,
1997). Most of this work is done in an untyped setting.
The typed calculus that provided the direct motivation and foundation for our
system is the # -calculus. It evolved as a type theoretic explanation of staged
computation (Davies & Pfenning, 2001; Wickline et al., 1998a), and run-time code-generation
(Lee & Leone, 1996; Wickline et al., 1998b), and we described it in
Section 2.
Another important typed calculus for meta-programming is # . Formulated by
(Davies, 1996), it is the proof-term calculus for discrete temporal logic, and it
provides a notion of open object expression where the free variables of the object
expression are represented by meta variables on a subsequent temporal level. The
original motivation of # was to develop a type system for binding-time analysis in
the setup of partial evaluation, but it was quickly adopted for meta-programming
through the development of MetaML (Moggi et al., 1999; Taha, 1999; Taha, 2000).
MetaML adopts the "open code" type constructor of # and generalizes the
language with several features. The most important one is the addition of a type
refinement for "closed code". Values classified by these "closed code" types are those
"open code" expressions which happen to not depend on any free meta variables.
It might be of interest here to point out a certain relationship between our concept
of names and the phenomenon which occurs in the extension of MetaML with
references (Calcagno et al., 2000; Calcagno et al., 2001). A reference in MetaML
Names and Necessity 27
must not be assigned an open code expression. Indeed, in such a case an eventual free
variable from the expression may escape the scope of the #-binder that introduced
it. For technical reasons, however, this actually cannot be prohibited, so the authors
resort to a hygienic handling of scope extrusion by annotating a term with the list of
free variables that it is allowed to contain in dead-code positions. These dead-code
annotations are not a type constructor in MetaML, and the dead-code variables
belong to the same syntactic category as ordinary variables, but they nevertheless
very much compare to our names and #-abstraction.
Another interesting calculus for meta-programming is Nielsen's # [ described in
(Nielsen, 2001). It is based on the same idea as our # -calculus - instead of defining
the notion of closed code as a refinement of open code of # or MetaML, it relaxes
the notion of closed code of # . Where we use names to stand for free variables
of object expression, # [ uses variables introduced by box (which thus becomes a
binding construct). Variables bound by box have the same treatment as #-bound
variables. The type-constructor # is updated to reflect the types (but not the names)
of variables that its corresponding box binds. This property makes it unclear if # [
can be extended with a concept corresponding to our support polymorphism.
Nielsen and Taha present another system for combining closed and open code in
(Nielsen & Taha, 2003). It is based on # but it can explicitly name the object
stages of computation through the notion of environment classifiers. Because the
stages are explicitly named, each stage can be revisited multiple times and variables
declared in previous visits can be reused. This feature provides the functionality of
open code. The environment classifiers are related to our support variables in several
respects: they both are bound by universal quantifiers and they both abstract over
sets. Indeed, our support polymorphism explicitly abstracts over sets of names,
while environment classifiers are used to name parts of the variable context, and
thus implicitly abstract over sets of variables.
Coming from the direction of higher-order abstract syntax, probably the first
work pointing to the importance of a non-parametric binder like our #-abstraction
is (Miller, 1990). The connection of higher-order abstract syntax to modal logic
has been recognized by Despeyroux, Pfenning and Sch-urmann in the system presented
in (Despeyroux et al., 1997), which was later simplified into a two-level
system in Sch-urmann's dissertation (Sch-urmann, 2000). There is also (Hofmann,
which discusses various presheaf models for higher-order abstract syntax,
then (Fiore et al., 1999) which explores untyped abstract syntax in a categorical
setup, and an extension to arbitrary types (Fiore, 2002).
However, the work that explicitly motivated our developments is the series of
papers on Nominal Logic and FreshML (Gabbay & Pitts, 2002; Pitts & Gabbay,
2000; Pitts, 2001; Gabbay, 2000). The names of Nominal Logic are introduced
as the urelements of Fraenkel-Mostowsky set theory. FreshML is a language for
manipulation of object syntax with binding structure based on this model. Its
primitive notion is that of swapping of two names which is then used to define the
operations of name abstraction (producing an #-equivalence class with respect to
the abstracted name) and name concretion (providing a specific representative of
an #-equivalence class). The earlier version of our paper (Nanevski, 2002) contained
28 A. Nanevski, F. Pfenning
these two operations, which were almost orthogonal to add. Name abstraction was
used to encode abstract syntax trees which depend on a name whose identity is not
known.
Unlike our calculus, FreshML does not keep track of a support of a term, but
rather its complement. FreshML introduces names in a computation by a construct
new X in e, which can roughly be interpreted in # -calculus as
new X in choose (#X. e)
Except in dead-code position, the name X can appear in e in a scope of an abstraction
which hides X . One of the main di#erences between FreshML and # is that
names in FreshML are run-time values - it is possible in FreshML to evaluate a term
with a non-empty support. On the other hand, while our names can have arbitrary
types, FreshML names must be of a single type atm (though this can be generalized
to an arbitrary family of types disjoint from the types of the other values of the
language). Our calculus allows the general typing for names thanks to the modal
distinction of meta and object levels. For example, without the modality, but with
names of arbitrary types, a function defined on integers will always have to perform
run-time checks to test if its argument is a valid integer (in which case the function
is applied), or if its argument is a name (in which case the evaluation is suspended,
and the whole expression becomes a syntactic entity). An added bonus is that #
can support an explicit name substitution as primitive, while substitution must be
user-defined in FreshML.
On the logic side, the direct motivation for this paper comes from (Pfenning &
Davies, 2001) which presents a natural deduction formulation for propositional S4.
But in general, the interaction between modalities, syntax and names has been of
interest to logicians for quite some time. For example, logics that can encode their
own syntax are the topic of G-odel's Incompleteness theorems, and some references in
that direction are (Montague, 1963) and (Smory-nski, 1985). Viewpoints of (Attardi
and contexts of (McCarthy, 1993) are similar to our notion of support,
and are used to express relativized truth. Finally, the names from # resemble non-rigid
designators of (Fitting & Mendelsohn, 1999), names of (Kripke, 1980), and
virtual individuals of (Scott, 1970), and also touch on the issues of existence and
identity explored in (Scott, 1979). All this classical work seems to indicate that
meta-programming and higher-order syntax are just but a concrete instance of a
much broader abstract phenomenon. We hope to draw on the cited work for future
developments.
6 Conclusions and future work
This paper presents the # -calculus, which is a typed functional language for meta-
programming, employing a novel way to define a modal type of syntactic object
programs with free variables. The system combines the # -calculus (Pfenning &
Davies, 2001) with the notion of names inspired by developments in FreshML and
Nominal Logic (Pitts & Gabbay, 2000; Gabbay & Pitts, 2002; Pitts, 2001; Gabbay,
2000). The motivation for combining # with names comes from the long-recognized
Names and Necessity 29
need of meta-programming to handle object programs with free variables (Davies,
1996; Taha, 1999; Moggi et al., 1999). In our setup, the # -calculus provides a
way to encode closed syntactic code expressions, and names serve to stand for the
eventual free variables. Taken together, they provide a way to encode open syntactic
program expressions, and also compose, evaluate, inspect and destruct them. Names
can be operationally thought of as locations which are tracked by the type system,
so that names cannot escape the scope of their introduction form. The set of names
appearing in the meta level of a term is called support of a term. Support of a term
is reflected in the typing of a term, and a term can be evaluated only if its support
is empty. We also considered constructs for support polymorphism.
The # -calculus is a reformulation of the calculus presented in (Nanevski, 2002).
Some of the adopted changes involve simplification of the operational semantics and
the constructs for handling names. Furthermore, we decomposed the name introduction
form new into two constructors # and choose which are now introduction
and elimination form for a new type constructor A # B. This design choice gives a
stronger logical foundation to the calculus, as now the level of types follows much
more closely the behavior of the terms of the language. We hope to further investigate
these logical properties. Some immediate future work in this direction would
include the embedding of discrete-time temporal logic and monotone discrete temporal
logic into the logic of types of # , and also considering the proof-irrelevancy
modality of (Pfenning, 2001) and (Awodey & Bauer, 2001) to classify terms of
unknown support.
Another important direction for exploration concerns the implementation of # .
The calculus presented in this paper was developed with a particular semantical
interpretation in mind of object level expressions as abstract syntax trees representing
templates for source programs. But this need not be the only interpretation. It
is quite possible that boxed expressions of # -calculus with support polymorphism
can be stored at run-time in some intermediate or even compiled form, which might
benefit the e#ciency of programs. It remains an important future work to explore
these implementation issues.

Acknowledgment

We would like to thank Dana Scott, Bob Harper, Peter Lee and Andrew Pitts for
their helpful comments on the earlier versions of the paper and Robert Gl-uck for
pointing out some missing references.



--R

A formalization of viewpoints.
Propositions as
Closed types as a simple approach to safe imperative multi-stage programming
Closed types for a safe imperative MetaML.
A temporal logic approach to binding-time analysis
A modal analysis of staged computation.
Journal of the ACM
Primitive recursion for higher-order abstract syntax
On the partial computation principle.
Semantic analysis of normalization by evaluation for typed lambda calculus.
Abstract syntax and variable binding.

Partial evaluation of computation process - an approach to a compiler-compiler


A new approach to abstract syntax with variable binding.
The system F of variable types

An automatic program generator for multi-level specialization
On automatic di

Semantical analysis of higher-order abstract syntax
An experiment in partial evaluation: the generation of a compiler generator.
Naming and necessity.
Optimizing ML with run-time code generation
Pages 137-148 of: Conference on Programming Language Design and Implementation

An extension to ML to handle bound variables in data structures.
Pages 323-335 of: <Proceedings>Proceedings of the first esprit BRA workshop on logical frameworks

Syntactical treatment of modalities

Combining closed and open code.

A functional theory of local names.

A judgmental reconstruction of modal logic.
Mathematical structures in computer science

Nominal logic: A first order theory of names and binding.
Pages 219-242 of: Kobayashi
A metalanguage for programming with bound names modulo renaming.


Translucent procedures


Advice on modal logic.
and existence in intuitionistic logic.
Accomplishments and research challenges in meta-programming
Pages 2-44 of


A sound reduction semantics for untyped CBN multi-stage compu- tation


--TR
A functional theory of local names
A modal analysis of staged computation
Run-time code generation and modal-ML
Modal types as staging specifications for run-time code generation
First-order modal logic
A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract)
Stochastic lambda calculus and monads of probability distributions
Accomplishments and Research Challenges in Meta-programming
Nominal Logic
Primitive Recursion for Higher-Order Abstract Syntax
A Metalanguage for Programming with Bound Names Modulo Renaming
An Idealized MetaML
A temporal-logic approach to binding-time analysis
Translucent Procedures, Abstraction without Opacity
Multistage programming

--CTR
Marcos Viera , Alberto Pardo, A multi-stage language with intensional analysis, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
Chiyan Chen , Hongwei Xi, Implementing typeful program transformations, ACM SIGPLAN Notices, v.38 n.10, p.20-28, October
Kevin Donnelly , Hongwei Xi, Combining higher-order abstract syntax with first-order abstract syntax in ATS, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.58-63, September 30-30, 2005, Tallinn, Estonia
Ik-Soon Kim , Kwangkeun Yi , Cristiano Calcagno, A polymorphic modal type system for lisp-like multi-staged languages, ACM SIGPLAN Notices, v.41 n.1, p.257-268, January 2006
Geoffrey Washburn , Stephanie Weirich, Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism, ACM SIGPLAN Notices, v.38 n.9, p.249-262, September
Chiyan Chen , Rui Shi , Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, v.69 n.1-2, p.103-121, January 2006
Yosihiro Yuse , Atsushi Igarashi, A modal type system for multi-level generating extensions with persistent code, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, ACM SIGPLAN Notices, v.38 n.9, p.263-274, September
Chiyan Chen , Hongwei Xi, Meta-programming through typeful code representation, ACM SIGPLAN Notices, v.38 n.9, p.275-286, September
Derek Dreyer, A type system for well-founded recursion, ACM SIGPLAN Notices, v.39 n.1, p.293-305, January 2004
Chiyan Chen , Hongwei Xi, Meta-programming through typeful code representation, Journal of Functional Programming, v.15 n.6, p.797-835, November 2005
Aleksandar Nanevski , Frank Pfenning, Staged computation with names and necessity, Journal of Functional Programming, v.15 n.6, p.893-939, November 2005
Walid Taha , Michael Florentin Nielsen, Environment classifiers, ACM SIGPLAN Notices, v.38 n.1, p.26-37, January
modal lambda-calculus;higher-order abstract syntax