Tagless staged interpreters for typed languages.
Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or mor.Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. .To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's H language to a multi-level setting. Building on H allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.
Introduction
In recent years, substantial effort has been invested in the development
of both the theory and tools for the rapid implementation
of domain specific languages (DSLs) [4, 22, 40, 47, 45, 23]. DSLs
are formalisms that provide their users with a notation appropriate
for a specific family of tasks. A promising approach to implementing
domain specific languages is to write a definitional interpreter
[42] for the DSL in some meta-language, and then to stage
this interpreter either manually, by adding explicit staging annotations
(multi-stage programming [55, 30, 45, 50]), or by applying an
automatic binding-time analysis (off-line partial evaluation [25]).
The result of either of these steps is a staged interpreter. A staged
interpreter is essentially a translation from a subject-language (the
DSL) to a target-language 1 . If there is already a compiler for the
target-language, the approach yields a simple compiler for the DSL.
In addition to the performance benefit of a compiler over an inter-
preter, the compiler obtained by this process often retains a close
syntactic connection with the original interpreter, inspiring greater
confidence in its correctness.
This paper is concerned with a subtle but costly problem which
can arise when both the subject- and the meta-language are statically
typed. In particular, when the meta-language is typed, there
is generally a need to introduce a "universal datatype" to represent
values uniformly (see [48] for a detailed discussion). Having such
a universal datatype means that we have to perform tagging and
untagging operations at run time. When the subject-language is un-
typed, as it would be when writing an ML interpreter for Scheme,
the checks are really necessary. But, when the subject-language is
also statically typed, as it would be when writing an ML interpreter
for ML, the extra tags are not really needed. They are only necessary
to statically type check the interpreter. When this interpreter is
staged, it inherits [29] this weakness, and generates programs that
contain superfluous tagging and untagging operations. Early estimates
of the cost of tags suggested that it produces up to a 2.6 times
slowdown in the SML/NJ system [54]. More extensive studies in
the MetaOCaml system show that slowdown due to tags can be as
high as 10 times [21].
How can we remove the tagging overhead inherent in the use of
universal types?
One recently proposed possibility is tag elimination [54, 53, 26],
a transformation that was designed to remove the superfluous tags
in a post-processing phase. Under this scheme, DSL implementation
is divided into three distinct stages (rather than the traditional
two). The extra stage, tag elimination, is distinctly different
from the traditional partial evaluation (or specialization) stage. In
essence, tag elimination allows us to type check the subject pro-
staging in a multi-stage language usually implies that
the meta-language and the target-language are the same language.
gram after it has been transformed. If it checks, superfluous tags
are simply erased from the interpretation. If not, a "semantically
equivalent" interface is added around the interpretation. Tag elim-
ination, however, does not statically guarantee that all tags will be
erased. We must run the tag elimination at runtime (in a multi-stage
language).
In this paper, we study an alternative approach that does provide
such a guarantee. In fact, the user never introduces these tags in the
first place, because the type system of the meta-language is strong
enough to avoid any need for them.
In what follows we describe the details of superfluous tags problem

1.1 Untyped Interpreters
We begin by reviewing how one writes a simple interpreter in an
untyped language. 2 For notational parsimony, we will use ML syntax
but disregard types. An interpreter for a small lambda language
can be defined as follows:
datatype int | V of string
| L of string * exp | A of exp * exp
fun eval e
case e of
| L (s,e) => fn v => eval e (ext env s v)
| A (f,e) => (eval f env) (eval e env)
This provides a simple implementation of subject programs represented
in the datatype exp. The function eval evaluates exps
in an environment env that binds the free variables in the term to
values.
This implementation suffers from a severe performance limita-
tion. In particular, if we were able to inspect the result of a an
interpretation, such as (eval (L("x",V "x")) env0), we would
find that it is equivalent to
This term will compute the correct result, but it contains an unexpanded
recursive call to eval. This problem arises in both call-by-
value and call-by-name languages, and is one of the main reasons
for what is called the "layer of interpretive overhead" that degrades
performance. Fortunately, this problem can be eliminated through
the use of staging annotations [48].
1.2 Untyped Staged Interpreters
Staging annotations partition the program into stages. Brackets
. surrounding an expression lift it to the next stage (building
code). Escape .-_ drops its surrounded expression to a previous
stage (splicing in already constructed code to build larger pieces
of code), and should only appear within brackets. Staging annotations
change the evaluation order of programs, even evaluating
under lambda abstraction, and force the unfolding of the eval function
at code-generation time. Thus, by just adding staging annotations
to the eval function, we can change its behavior to achieve
the desired operational semantics:
(case e of
2 Discussing the issue of how to prove the adequacy of representations
or correctness of implementations of interpreters is beyond
the scope of this paper. Examples of how this can done can be found
elsewhere [54].
| L (s,e) => .<fn v => .-(eval' e (ext env s . .
| A (f,e) => .-(eval' f env) .-(eval' e env))>.
Computing the application eval' (L("x",V "x")) env0 directly
yields a term .<fn v => v>.
Now there are no leftover recursive calls to eval. Multi-stage
languages come with a run annotation .!_ that allows us to execute
such a code fragment. A staged interpreter can therefore be viewed
as user-directed way of reflecting a subject program into a meta-
program, which then can be handed over in a type safe way to the
compiler of the meta-language.
1.3 Hindley-Milner Staged Interpreters
In programming languages, such as Haskell or ML, which use
a Hindley-Milner type system, the above eval function (staged or
unstaged) is not well-typed [48]. Each branch of the case statement
has a different type, and these types cannot be reconciled.
Within a Hindley-Milner system, we can circumvent this problem
by using a universal type. A universal type is a type that is rich
enough to encode values of all the types that appear in the result of
a function like eval. In the case above, this includes function as
well as integer values. A typical definition of a universal type for
this example might be:
I of int | F of V -> V
The interpreter can then be rewritten as a well-typed program:
fun unF
fun eval e
(case e of
| L (s,e) => F (fn v => eval e (ext env s v))
| A (f,e) => (unF (eval f env)) (eval e env));
Now, when we compute (eval (L("x",V "x")) env0) we get
back a value
Just as we did for the untyped eval, we can stage this version of
eval.
Now computing (eval (L("x",V "x")) env0) yields:
1.4 Problem: Superfluous Tags
Unfortunately, the result above still contains the tag F. While this
may seem like minor issue in a small program like this one, the effect
in a larger program will be a profusion of tagging and untagging
operations. Such tags would indeed be necessary if the subject-
language was untyped. But if we know that the subject-language
is statically typed (for example, as a simply-typed lambda calcu-
lus) the tagging and untagging operations are really not needed.
Benchmarks indicate that these tags add a 2-3 time overhead [54],
sometimes as large as 3-10 times [21].
There are a number of approaches for dealing with this prob-
lem. None of these approaches, however, guarantee (at the time of
writing the staged interpreter) that the tags will be eliminated before
runtime. Even tag elimination, which guarantees the elimination
of tags for these particular examples, requires a separate metatheoretic
proof for each subject language to obtain such a guarantee
[54].
Contributions
In this paper we propose an alternative solution to the superfluous
tags problem. Our solution is based on the use of a dependently
typed multi-stage language. This work was inspired by work on
writing dependently typed interpreters in Cayenne [2]. To illustrate
viability of combining dependent types with staging, we have designed
and implemented a prototype language we call Meta-D. We
use this language as a vehicle to investigate the issues that arise
when taking this approach. We built a compiler from an interpreter,
from beginning to end in Meta-D. We also report on the issues that
arise in trying to develop a dependently typed programming language
(as opposed to a type theory).
features
Basic staging operators
Dependent types (with help for avoiding redundant typing annotations

Dependently typed inductive families (dependent datatypes)
Separation between values and types (ensuring decidable type
checking)
A treatment of equality and representation types using an
equality-type-like mechanism
The technical contribution of this paper is in formalizing a multi-stage
language, and proving its safety under a sophisticated dependent
type system. We do this by capitalizing on the recent work
by Shao, Saha, Trifonov and Papaspyrou's on the system [44],
which in turn builds on a number of recent works on typed intermediate
languages [20, 7, 59, 43, 9, 57, 44].
1.6 Organization of this Paper
Section 2 shows how to take our motivating example and turn it
into a tagless staged interpreter in a dependently typed setting. First,
we present the syntax and semantics of a simple typed language and
show how these can be implemented in a direct fashion in Meta-D.
The first part of this (writing the unstaged interpreter) is similar to
what has been done in Cayenne [2], but is simplified by the presence
of dependent datatypes in Meta-D (see Related Work). The key observation
here is that the interpreter needs to be defined over typing
derivations rather than expressions. Dependently typed datatypes
are needed to represent such typing derivations accurately. Next,
we show how this interpreter can be easily staged. This step is exactly
the same as in the untyped and in the Hindley-Milner setting.
In Section 3 we point out and address some basic practical problems
that arise in the implementation of interpreters in a dependently
typed programming language. First, we show how to construct
the typing judgments that are consumed by the tagless inter-
preter. Then, we review why it is important to have a clear separation
between the computational language and the type language.
This motivates the need for representation types, and has an effect
on the code for the tagless staged interpreter.
Section 4 presents a formalization of a core subset of Meta-D,
and a formal proof of its type safety. The original work on used
this system to type a computational language that includes basic
effects, such as non-termination [44]. In this paper, we develop
a multi-stage computational language, and show how essentially
the same techniques can be used to verify its soundness. The key
technical modifications needed are the addition of levels to typing
judgments, and addressing evaluation under type binders.
Section 5 discusses related work, and Section 6 outlines directions
for future work and concludes.
An extended version of the paper is available on-line as a technical
report [36].
Staged Interpreter
In this section we show how the example discussed in the introduction
can be redeveloped in a dependently typed setting. We
begin by considering a definition of the syntax and semantics (of a
simply typed version) of the subject language.
2.1 Subject-Language Syntax and Semantics

Figure

1 defines the syntax, type system, and semantics of an
example subject language we shall call SL. For simplicity of the
development, we use de Bruijn indices for variables and binders.
The semantics defines how the types of SL are mapped to their intended
meaning. For example, the meaning of the type N is the set
of natural numbers, while the meaning of the arrow type
the function space Furthermore, we map the meaning of
type assignments G, into a product of the sets denoting the finite
number of types in the assignment. Note that the semantics of programs
is defined on typing judgments, and maps to elements of the
meanings of their types. This is the standard way of defining the
semantics of typed languages [56, 18, 39], and the implementation
in the next section will be a direct codification of this definition.
2.2 Interpreters in Meta-D
An interpreter for SL can be simply an implementation of the
definition in Figure 1. We begin by defining the datatypes that will
be used to interpret the basic types (and typing environments) of
SL. To define datatypes Meta-D uses an alternative notation to SML
or Haskell datatype definitions. For example, to define the set of
natural numbers, instead of writing
datatype
we write
inductive
The inductive notation is more convenient when we are defining
dependent datatypes and when we wish to define not only new types
but new kinds (meaning "types of types"). Now type expression and
type assignments are represented as follows:
inductive
inductive
inductive
The *1 in these definitions means that we are defining a new type.
To implement the type judgment of SL we need a dependently typed
datatype indexed by three parameters: a type assignment Env, an
expression Exp, and a type Typ. We can define such a datatype as
shown in Figure 2. 3 Each constructor in this datatype corresponds
to one of the rules in the type system for our object language. For
example, consider the rule for lambda abstraction (Lam) from Figure
1. The basic idea is to use the "judgments as types principle"
[19], and so we can view the type rule as a constant combinator on
judgments. This combinator takes hypothesis judgments (and their
returns the conclusion judgment. In this case the
rule requires an environment G, two types t and t 0 , a body e of the
lambda abstraction, a judgment that G;t returns a judgment
This rule is codified directly by the following
constructor
J(e1, EL t1 s2, ArrowT t1 t2).
In the definition of J we see differences between the traditional
datatype definitions and inductive datatypes: each of the constructors
can have dependently typed arguments and a range type J indexed
by different indices. It is through this variability in the return
3 For practical reasons that we will discuss in the next section,
this datatype is not legal in Meta-D. We will use it in this section
to explain the basic ideas before we discuss the need for so-called
representation types.

Figure

1. Semantics of SL
inductive

Figure

2. The typing judgment J (without representation types)
type of the constructors that dependent datatypes can provide more
information about their values.
2.2.1 Interpreters of Types and Judgments
After defining judgments, we are ready to implement the in-
terpretations. Note, however, that the type of the result of the
interpretation of judgments, depends on the interpretation of SL
types. This dependency is captured in the interpretation function
typEval. Figure 3 presents the implementation of the interpretation
of types typEval; the mapping of type assignments into Meta-
D types envEval; and the interpretation of judgments eval.
The function eval is defined by case analysis on typing judg-
ments. Computationally, this function is not significantly different
from the one presented in Section 1.2. Differences include additional
typing annotations, and the case analysis over typing judg-
ments. Most importantly, writing it does not require that we use
tags on the result values, because the type system allows us to specify
that the return type of this function is typEval t. Tags are no
longer needed to help us discriminate what type of value we are
getting back at runtime: the type system now tells us, statically.
2.3 Staged Interpreters in Meta-D

Figure

4 shows a staged version of eval. As with Hindley-Milner
types, staging is not complicated by dependent types. The
staged interpreter evalS, returns a value of type (code (typEval
t)). Note that the type of value assignments is also changed (see
envEvalS in Figure 4): Rather than carrying runtime values for
SL, it carries pieces of code representing the values in the variable
assignment. Executing this program produces the tagless code fragments
that we are interested in.
Even though the eval function never performs tagging and un-
tagging, the interpretative overhead from traversing its input is still
considerable. Judgements must be deconstructed by eval at run-
time. This may require even more work than deconstructing tagged
values. With staging, all these overheads are performed in the first
stage, and an overhead-free term is generated for execution in a later
stage.
Staging violations are prevented in a standard way by Meta-D's
type system (See technical report [36]). The staging constructs are
those of Davies [10] with the addition of cross-stage persistence
[55]. We refer the reader to these references for further details on
the nature of staging violations. Adding a run construct along the
lines of previous works [51, 30] was not considered here.
Now we turn to addressing some practical questions that are
unique to the dependent typing setting, including how the above-mentioned
judgements are constructed.
3 Practical Concerns
Building type judgments amounts to implementing either type-checking
or type inference for the language we are interpreting.
Another practical concern is that types that depend on values can
lead to either undecidable or unsound type checking. This happens
when values contain diverging or side-effecting computations. In
this section we discuss how both of these concerns are addressed in
the context of Meta-D.
3.1 Constructing Typing Judgments
Requiring the user of a DSL to supply a typing judgment for each
program to be interpreted is not likely to be acceptable (although it
can depend on the situation). The user should be able to use the
implementation by supplying only the plain text of the subject pro-
gram. Therefore, the implementation needs to include at least a type
checking function. This function takes a representation of a type-
annotated program and produces the appropriate typing judgment,
if it exists. We might even want to implement type inference, which
does not require type annotations on the input. Figure 4 presents a
function typeCheck. This function is useful for illustrating a number
of features of Meta-D:
The type of the result 4 of typeCheck is a dependent sum,
J(e,s,t). This means that the result
of typeCheck consists of an SL type, and a typing judgment
that proves that the argument expression has that particular
type under a given type assignment.
Since judgments are built from sub-judgments, a case (strong
dependent sum elimination) construct is need to deconstruct
4 In a pure (that is with no computational effects whatsoever)
setting the result of typeCheck should be option ([t : Typ]
(J (e,s,t))), since a particular term given to typeCheck may
not be well-typed. In the function given in this paper, we omit the
option, to save on space (and rely on incomplete case expressions
instead).
case t of NatT => Nat | ArrowT t1 t1 => (typEval t1) -> (typEval t2)
case e of EmptyE => unit | ExtE e2 t => (envEval e2, typEval t)
case j of
JN e1 n1 => n1
| JV e1 t1 => #2(rho)
| JW e1 t1 t2 i j1 => eval e1 (#1(rho)) (EV i) t1 j1
| JL ee1 et1 et2 es2 ej1 => fn
| JA e s1 s2 t1 t2 j1 j2 => (eval e rho s1 (ArrowT t1 t2) j1) (eval e rho s2 t1 j2)

Figure

3. Dependently typed tagless interpreter (without representation types)
case e of EmptyE => unit | ExtE e2 t =>
(envEvalS e2, code (typEval t))
case j of
JN e1 n1 => . .
| JV e1 t1 => #2(rho)
| JW e1 t1 t2 i j1 => evalS e1 (#1(rho)) (EV i) t1 j1
| JL ee1 et1 et2 es2 ej1 => .<fn v:(typEval et1) => (.-(evalS (ExtE ee1 et1) (rho,. .) es2 et2 ej1))>.
| JA e s1 s2 t1 t2 j1 j2 => .-(evalS e rho s1 (ArrowT t1 t2) j1)) (.-(evalS e rho s2 t1 j2))>.
case s of
| EV nn => (case nn of Z => (case e of ExtE ee t2 =>
| S n => (case e of ExtE e2 t2 =>
case x of [rx : Typ]j2 =>
(typeCheck e2 (EV n)))))
| EL targ s2 =>
case x of [rt : Typ] j2 =>
(typeCheck (ExtE e targ) s2))
| EA s1 s2 =>
case x1 of [rt1 : Typ]j1 => case x2 of [rt2 : Typ]j2 =>
(case rt1 of ArrowT tdom tcod =>
(cast [assert rt2=tdom,J(e,s,tdom), j2])) end)))
(typeCheck e s1) (typeCheck e s2))
case x of
(case t1 of NatT => eval EmptyE () s NatT j
| ArrowT t2 t3 => Z
(typeCheck EmptyE s))

Figure

4. Staged tagless interpreter and the function typeCheck (without representation types)
the results of recursive calls to typeCheck.
The case for constructing application judgments illustrates
an interesting point. Building a judgment for the expression
(EA s1 s2) involves first computing the judgments for
the sub-terms s1 and s2. These judgments assign types
(ArrowT tdom tcod) and rt2 to their respective expres-
sions. However, by definition of the inductive family J, in
order to build the larger application judgment, tdom and rt2
must be the same SL type (i.e., their Typ values must be
equal).
We introduce two language constructs to Meta-D to express
this sort of constraints between values. First, the expression of
the form assert introduces an equality judgment,
ID e1 e2 between values of equality types. 5
An elimination construct
is used to cast the expression e2 from some type T[v1]
to T[v2], where e1 is an equality judgment of the type
ID v1 v2. The type checker is allowed to use the Leibniz-
style equality to prove the cast correct, since e1 is an equality
judgment stating that v1 and v2 are equal.
Operationally, the expression assert e1=e2 evaluates its two
subexpressions and compares them for equality. If they are indeed
equal, computation proceeds If, however, the two values
are not equal, the program raises an exception and terminates.
The cast construct makes sure that its equality judgment introduced
by assert is evaluated at runtime, and if the equality
check succeeds, simply proceeds to evaluate its argument expression

An alternative to using assert/cast is to include equality
judgments between types as part of typing judgments, and
build equality proofs as a part of the typeCheck function. 6
This approach, while possible, proves to be verbose, and will
be omitted in this paper. The assert/cast, however, can
serve as a convenient programming shortcut and relieves the
user from the effort formalizing equality at the type level and
manipulating equality types.
3.2 Representation Types
Combining effects with dependent types requires care. For ex-
ample, the typeCheck function is partial, because there are many
input terms which are just not well typed in SL. Such inputs
to typeCheck would cause runtime pattern match failures, or an
equality assertion exception. We would like Meta-D to continue
to have side-effects such as non-termination and exceptions. At
the same time, dependently typed languages perform computations
during type checking (to determine the equality of types). If we
allow effectful computations to leak into the computations that are
done during type checking, then we risk non-termination, or even
unsoundness, at type-checking time. This goal is often described as
"preserving the phase distinction" between compile time and run-time
[5].
The basic approach to dealing with this problem is to allow types
to only depend on other types, and not values. Disallowing any kind
of such dependency, however, would not allow us to express our
type checking function, as it produces a term whose type depends
5 This feature is restricted to ground types whose value can be
shown equal at runtime.
6 Due to space limitation we omit this approach here, but define
an alternative type-checking function in the accompanying technical
report [36].
on the value of its argument. A standard solution to is to introduce a
mechanism that allows only a limited kind of dependency between
values and types. This limited dependency uses so-called singleton
or representation types [60, 7, 9, 57]. The basic idea is to allow
bijections on ground terms between the value and type world.
Now, we can rewrite our interpreter so that its type does not depend
on runtime values, which may introduce effects into the type-checking
phase. Any computation in the type checking phase can
now be guaranteed to be completely effect-free. The run-time values
are now forced to have representation types that reflect, in the
world of values, the values of inductive kinds. In Meta-D, a special
type constructor R is used to express this kind of dependency. For
example, we can define an inductive kind Nat
inductive
Note that this definition is exactly the same as the one we had for
the type Nat, except it is not classified by *2 instead of *1. Once
this definition is encountered, we have introduced not only the constructors
for this type, but also the possibility of using the special
type constructor R. Now we can write R(S(S Z)) to refer to a type
that has a unique inhabitant, which we also call rep (S(S Z)).

Figure

5 presents the implementation with representation types.
Introducing this restriction on the type system requires us to turn the
definition of Exp, Env, and Typ into definitions of kinds (again this
is just a change of one character in each definition). Because these
terms are now kinds, we cannot use general recursion in defining
their interpretation. Therefore, we use special primitive recursion
constructs provided by the type language to define these interpreta-
tions. Judgments, however, remain a type. But now, they are a type
indexed by other types, not by values.
For the most part, the definition of judgments and the interpretation
function do not change. We need to change judgments in the
case of natural numbers by augmenting them with a representation
for the value of that number. The constructor JN now becomes
and the definition of eval is changed accordingly. The modified
eval uses a helper function to convert a representation of a natural
type to a natural number. 7
The definition of the typeCheck function requires more substantial
changes (Figure 5). In particular, this function now requires carrying
out case analysis on types [20, 7, 59, 43, 9]. For this purpose
Meta-D provides a special case construct
tycase x by y of C_n x_n => e_n.
A pattern (C_n x_n) matches against a value x of type K, where
K is some inductive kind, only if we have provided a representation
value y of type R(x). Pattern matching over inductive kinds cannot
be performed without the presence of a corresponding runtime
value of the appropriate representation type. Inside the body of the
case (e_n), the expression rep x_n provides a representation value
for the part of the inductive constructor that x_n is bound to.
4 Formal Development
In this section we report our main technical result, which is type
safety for a formalized core subset of Meta-D. This result shows
that multi-stage programming constructs can be safely used, even
when integrated with a sophisticated dependent type system such
as that of We follow the same approach used by the developers
of TL, and build a computation language l H
that uses
as its type language. Integrating our formalization into the
7 In practice, we see no fundamental reason to distinguish the
two. Identifying them, however, requires the addition of some special
support for syntactic sugar for this particular representation
type.
inductive
inductive
inductive
inductive
inductive
inductive
|
|
|
|
primrec Typ nat (fn c : *1 => fn d : *1 => c -> d)
fun cast (n : by rn of Z => zero
| S (cast
case j of
JN e1 n1 rn1 => cast n1 rn1
| JV e1 t1 => #2(rho)
| JW e1 t1 t2 i j1 => eval e1 (#1(rho)) (EV i) t1 j1
| JL ee1 et1 et2 es2 ej1 =>fn
| JA e s1 s2 t1 t2 j1 j2 => (eval e rho s1 (ArrowT t1 t2) j1) (eval e rho s2 t1 j2)
tycase s by rs of
| EV n =>
(tycase n by (rep n) of Z => (tycase e by re of ExtE ee t2 =>
| S n => (tycase e by re of ExtE (e2) (t2) =>
case x of [rx : Typ]j2 =>
(#1 j2, JW e2 rx t2 n (#2 j2)))
(typeCheck e2 (rep e2) (EV n) (rep (EV n)))))))
| EL targ s2 =>
case x of
(typeCheck (ExtE e targ) (rep (ExtE e targ)) s2 (rep s2)))
| EA s1 s2 =>
case x1 of [t1 : Typ]j1 => case x2 of [t2 : Typ]j2 =>
(tycase t1 by (#1 (j1)) of
ArrowT tdom tcod =>
(cast [assert t2=tdom,J(e,s,tdom),j2]))) end)))
(typeCheck e (rep e) s1 (rep s1)) (typeCheck e (rep e) s2 (rep s2)))

Figure

5. Tagless interpreter with representation types in MetaD
inductive W

Figure

6. The definition of the types of l H
A  type expressions of
cast (e 0

Figure

7. Syntax of l H
A
A
cast

Figure

8. Type system of l H
framework gave us significant practical advantages in formal development
of l H
Important meta-theoretic properties of the type language we
use, TL, have already been proven [44]. Since we do not
change anything about the type language itself, all these results
(e.g., the Church-Rosser property of the type language,
decidable equality on type terms) are easily reused in our
proofs.
is based on the computational language lH [44]. We
have tried to make the difference between these two languages
as small as possible. As a result, the proof of type safety of
l H
is very similar to the type safety proof for lH . Again, we
were able to reuse certain lemmata and techniques developed
for lH to our own proof.
A detailed proof of the type safety of l H
is presented in an extended
technical report [36].

Figure

6 defines l H
computational types, and is the first step
needed to integrate l H
into the framework. The syntax of
the computational language l H
is given in Figure 7. The language
l H
contains recursion and staging constructs. It contains
two predefined representation types: naturals and booleans. The
if construct, as in lH , provides for propagating proof information
into branches (analogous to the tycase construct of MetaD); full
implementation of inductive datatypes in the style of MetaD is left
for future work. Since arbitrary dependent types are prohibited in
l H
, we use universal and existential quantification to express dependencies
of values on types and kinds. For example, the identity
function on naturals is expressed in l H
as follows:
In l H
, we also formalize the assert/cast construct, which
requires extending the language of computational types with equality
judgment types. Similarly, we add the appropriate constructs to
the syntax of l H
.
To be able to define the small-step semantics for a staged lan-
guage, we had to define the syntax of l H
in terms of level-indexed
families of expressions and values [48]. The typing judgment (Fig-
ure 8), as well as the type assignments, of l H
has also been appropriately
extended with level annotations [55]. A level-annotation
erasure function ( j n ) is used to convert l H
typing assignments
into a form required by the typing judgment of TL[44]. This interface
then allows us to reuse the original typing judgment.
Due to lack of space we do not show all the definitions for the
small-step semantics of l H
. These, together with proofs of the
relevant theorems, are included in a companion technical report
[36]. Here, we list the most important theorems.
Proof is by structural induction on e n 2E n , and then by examination
of cases of the typing judgment.
Proof is by cases of possible reductions e ! e 0 .
7!
Proof uses subject reduction (Lemma 2) and progress (Lemma 1)
lemmas and follows Wright and Felleisen's syntactic technique
[58].
5 Related Work
Barendregt [3] is a good high-level introduction to the theory of
dependent type systems. There are a number of other references
to (strictly terminating) functional programming in dependent type
theory literature [32, 31, 6].
Cayenne is a dependently typed programming language [1]. In
essence, it is a direct combination of a dependent type theory with
(potentially) non-terminating recursion. It has in fact been used to
implement an (unstaged) interpreter similar to the one discussed
in this paper [2]. The work presented here extends the work done
in Cayenne in three respects: First, Cayenne allows types to depend
on values, and thus, does not ensure that type checking termi-
nates. Second, Cayenne does not support dependent datatypes (like
J(e,s,t)), and so, writing an interpreter involves the use of a separate
proof object to encode the information carried by J(e,s,t)),
which is mostly just threaded through the program. The number of
parameters passed to both the Meta-D and Cayenne implementation
of the eval function is the same, but using dependent datatypes in
Meta-D allows direct analogy with the standard definition of the
semantics over typing judgments rather than raw terms. Third,
Cayenne does not provide explicit support for staging, an essential
component for achieving the performance results that can be
achieved using tagless staged interpreters.
Xi and Pfenning study a number of different practical approaches
to introducing dependent types into programming languages [59,
60]. Their work concentrates on limiting the expressivity of the
dependent types, and thus limiting the constraints that need to be
solved to Presburger arithmetic problems. Singleton types seem to
have been first used by Xi in the context of DML [60]. The idea
was later used in a number of works that further developed the idea
of representation types and intensional type analysis.
Logical frameworks [19, 37] use dependent types as a basis for
proof systems. While this is related to our work, logical frameworks
alone are not sufficient for our purposes, as we are interested
in computational programming languages that have effects
such as non-termination. It is only with the recent work of Shao,
Saha, Trifonov and Papaspyrou that we have a generic framework
for safely integrating a computation base language, with a rich dependent
type system, without losing decidability (or soundness) of
type-checking.
Dybjer extensively studies the semantics of inductive sets and
families [11, 12, 13, 14, 16] and simultaneous inductive- recursive
definitions [15]. uses only the former (in the type level), and
we also use them at the value level (J(e,s,t)). The Coq proof
assistant provides fairly extensive support for both kinds of definitions
[17, 34, 35]. In the future, it will be interesting to explore
the integration of the second of these techniques into programming
languages.
One interesting problem is whether self-interpretation is possible
in a given programming language. This is possible with simply-typed
languages [54]. It is not clear, however, that it can be done
in a dependently typed language [38]. Exploring this problem is
interesting future work.
Finally, staged type inference [46] can also be used as a means
of obtaining programs without tags. Of the techniques discussed
in this paper, it is probably closest in spirit to tag elimination. In
fact, in a multi-stage setting tag elimination is applied at runtime
and is nothing but a non-standard type analysis. Key differences
are that in the staged type inference system the code type that is
used does not reflect any type information, and type information
can only be determined by dynamic type checking. More impor-
tantly, the success and failure of staged type inference can depend
on whether the value in the code type has undergone simplifica-
tion, and it is easy to return a value that tells us (at runtime, in the
language) whether this dynamic inference succeeded or not. Tag
elimination, on the other hand, works on code that has an explicit
static type. Additionally, by using carefully crafted "fall-back plan"
projection/embedding pairs, runtime tag elimination is guaranteed
to always have the same denotational semantics (but certainly not
operational semantics) independently of the test of the code being
analyzed and any simplifications that may be done to the subject
program [54].
6 Conclusions and Future Work
In this paper we have shown how a dependently typed programming
language can be used to express a staged interpreter that completely
circumvents the need for runtime tagging and untagging operations
associated with universal datatypes. In doing so we have
highlighted two key practical issues that arise when trying to develop
staged interpreters in a dependently typed language. First,
the need for functions that build the representations of typing judgments
that the interpretation function should be defined over. And
second, the need for representation types to avoid polluting the type
language with the impure terms of the computational language. To
demonstrate that staging constructs and dependent types can be
safely combined, we formalize our language as a multi-stage computational
language typed by Shao, Saha, Trifonov, and Papaspy-
rou's system. This allows us to prove type safety in a fairly
straightforward manner, and without having to duplicate the work
done for the system.
A practical concern about using dependent types for writing interpreters
is that such systems do not have decidable type inference,
which some view as a highly-valued feature for any typed language.
We did not find that the annotations were a burden, and some simple
tricks in the implementation were enough to avoid the need for
redundant annotations.
In carrying out this work we developed a deeper appreciation
for the subtleties involved in both dependently typed programming
and in the implementation of type checkers for dependently typed
languages. Our current implementation is a prototype system that
we have made available online [27]. Our next step is to study the
integration of such a dependently typed language into a practical
implementation of multi-stage programming, such as MetaOCaml
[28]. We have also found that there a lot of opportunities in the context
of dependently typed languages that we would like to explore
in the future. Examples include syntactically lighter-support for
representation types, formalizing some simple tricks that we have
used in our implementation to help alleviate the need for redundant
type annotations. We are also interested in exploring the use of dependent
types to reflect the resource needs of generated programs
[8, 24, 52].



--R


An exercise in dependent types: A well-typed inter- preter
Lambda calculi with types.
Little languages.
Phase distinctions in type theory.
Type theory and programming.
Flexible type analysis.
Resource bound certifica- tion
Intensional polymorphism in type-erasure semantics
A modal analysis of staged computation.
Inductively defined sets in Martin-L-of's set theory
Inductive sets and families in Martin- L-of's type theory and their set-theoretic semantics
Inductive sets and families in Martin-L-of's type theory and their set-theoretic semantics
Inductive families.
A general formulation of simultaneous inductive-recursive definitions in type theory
Finite axiomatizations of inductive and inductive-recursive definitions
A tutorial on recursive types in Coq.
Semantics of Programming Languages.
A frame-work for defining logics
Compiling polymorphism using intentional type analysis.
A practical implementation of tag elimination.
Building domain specific embedded languages.
Modular domain specific languages and tools.
Proving the correctness of reactive systems using sized types.
Partial Evaluation and Automatic Program Generation.
On Jones-optimal specialization for strongly typed languages

MetaOCaml: A compiled
Inherited limits.
An idealized MetaML: Simpler
Programming in constructive set the- ory: Some examples
Programming in Martin-Lof's Type Theory
Oregon Graduate Institute Technical Reports.
Inductive definitions in the system Coq: Rules and properties.
Inductive definitions in the system Coq: Rules and properties.
Emir Pa-sali-c
Logic programming in the LF logical frame- work
LEAP: A language with eval and polymorphism.
Basic Category Theory for Computer Scientists.
Microlanguages for operating system specializa- tion
Definitional interpreters for higher-order programming languages
Definitional interpreters for higher-order programming languages

Nikolaos Pa- paspyrou
Benaissa, and Emir Pa-sali-c
Peyton Jones.
A transformation library for data structures.


A sound reduction semantics for untyped CBN multi-stage computation

Directions in functional programming for real(-time) applications
Tag elimination - or - type specialisation is a type-indexed effect
Tag elimination and Jones-optimality

Semantics of Programming Languages.
Fully reflexive intensional type analysis.
A syntactic approach to type soundness.
Eliminating array bound checking through dependent types.
Dependent types in practical programming.
--TR
Basic category theory for computer scientists
Logic programming in the LF logical framework
Inductive sets and families in Martin-LoMYAMPERSANDuml;f''s type theory and their set-theoretic semantics
Semantics of programming languages
Partial evaluation and automatic program generation
A syntactic approach to type soundness
Compiling polymorphism using intensional type analysis
A type-based compiler for standard ML
A modal analysis of staged computation
Proving the correctness of reactive systems using sized types
Building domain-specific embedded languages
Multi-stage programming with explicit annotations
Dynamic typing as staged type inference
Eliminating array bound checking through dependent types
Intensional polymorphism in type-erasure semantics
Dependent types in practical programming
Flexible type analysis
Resource bound certification
A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract)
DSL implementation using staging and monads
Fully reflexive intensional type analysis
A type system for certified binaries
Principles of Programming Languages
Semantics, Applications, and Implementation of Program Generation
Tag Elimination and Jones-Optimality
On Jones-Optimal Specialization for Strongly Typed Languages
Inductive Definitions in the system Coq - Rules and Properties
Multi-Stage Programming
Directions in Functional Programming for Real(-Time) Applications
An Idealized MetaML
Inherited Limits
Definitional interpreters for higher-order programming languages
Programming in Constructive Set Theory
Modular Domain Specific Languages and Tools
Multistage programming

--CTR
Chiyan Chen , Hongwei Xi, Implementing typeful program transformations, ACM SIGPLAN Notices, v.38 n.10, p.20-28, October
Jason Eckhardt , Roumen Kaiabachev , Emir Pasalic , Kedar Swadi , Walid Taha, Implicitly heterogeneous multi-stage programming, New Generation Computing, v.25 n.3, p.305-336, January 2007
Manuel Fhndrich , Michael Carbin , James R. Larus, Reflective program generation with patterns, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
Adam Chlipala, A certified type-preserving compiler from lambda calculus to assembly language, ACM SIGPLAN Notices, v.42 n.6, June 2007
Seth Fogarty , Emir Pasalic , Jeremy Siek , Walid Taha, Concoqtion: indexed types now!, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France
Oleg Kiselyov , Chung-chieh Shan, Lightweight Static Capabilities, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.79-104, June, 2007
Chiyan Chen , Rui Shi , Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, v.69 n.1-2, p.103-121, January 2006
Oleg Kiselyov , Kedar N. Swadi , Walid Taha, A methodology for generating verified combinatorial circuits, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy
Sheard, Languages of the future, ACM SIGPLAN Notices, v.39 n.12, December 2004
Edwin Brady , Kevin Hammond, A verified staged interpreter is a verified compiler, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
Jim Grundy , Tom Melham , John O'leary, A reflective functional language for hardware design and theorem proving, Journal of Functional Programming, v.16 n.2, p.157-196, March 2006
Walid Taha , Michael Florentin Nielsen, Environment classifiers, ACM SIGPLAN Notices, v.38 n.1, p.26-37, January
calculus of constructions;definitional interpreters;multi-stage programming;domain-specific languages