Type specialisation for imperative languages.
We extend type specialisation to a computational lambda calculus with first-class references. The resulting specialiser has been used to specialise a self-interpreter for this typed computational lambda calculus optimally. Furthermore, this specialiser can perform operations on references at specialisation time, when possible.
Introduction
By far the most important program specialisation technique
is partial evaluation [?]. Partial evaluation is a program
transformation, in which a program and parts of its input
(the static part) is transformed into a new program. The
partial evaluator performs the operations for which enough
data is available and reconstructs the rest. Where an interpreter
only operates on values, a partial evaluator operates
on both values and symbolic values (code or values or a combination
of code and values). Partial evaluators appear in
two variants, online and offline. In online partial evaluators
all specialisation decisions are taken by inspecting the symbolic
values, whereas in the offline variants all specialisation
decisions are taken before actually running the specialiser.
The decisions are communicated to the specialiser by means
of two-level annotated programs [?]. These annotations can
be introduced by hand or by means of a binding-time anal-
ysis. The specialiser, in this case, is an interpreter for two-level
programs.
Type specialisation [?] is an extension of offline partial
evaluation, where the specialiser is expressed as a collection
of non-standard typing rules. Each type inference rule specifies
a transformation on an expression e and a type - via
specialisation judgements: \Gamma is the code
part or dynamic part of the result of applying the transfor-
mation, and - 0 plays the same r-ole as the symbolic values
in partial evaluation, and may contain values. The static
Supported by the Belgian National Fund for Scientific Research
(N.F.W.O. This work was done while visiting Chalmers.
y This work was done while visiting Chalmers
To appear in the proceedings of ICFP'97.
parts can be used in static computations and the dynamic
parts are treated as black-boxes. In this setting, specialisation
corresponds to building a proof of a specialisation
judgement. The advantage over partial evaluation is that
symbolic values, the residual types, are propagated via type
unification 1 . The combination of a rich language of residual
types and the superior value propagation strategy, type
unification, has enabled Hughes to achieve optimal specialisation
of a self-interpreter for a typed lambda calculus [?], a
feat that has not been achieved with standard partial eval-
uation. Optimal specialisation in this context means that
specialising the interpreter with respect to some term yields
the same term up to ff-conversion. The problem here is the
presence of a universal type in the self-interpreter. Standard
partial evaluation is not able to get rid of the tagging and
untagging operations of the universal type [?].
This work serves two purposes. First, we show that type
specialisation is modular with respect to the addition of new
type constructors (here: references and computations). Sec-
ond, we show that type specialisation is not restricted to
purely functional languages, but that it also applies to specialising
operations with computational effects, such as performing
operations on references at specialisation time for
a language like ML. More formally, we extend type specialisation
to an extension of Moggi's computational metalanguage
ml with first-class references. We demonstrate the
usefulness of this extension by instantiating it with the store
monad. The result is a type specialiser for   oe
ml , that is   ml
extended with ML-style operations on references. A distinguishing
feature of our specialiser is the fact that it can
perform some operations on references statically. This specializer
achieves optimal specialisation for a self-interpreter
for   oe
ml and it also yields satisfactory results on other interesting
problems (to be described below).

Overview

For the reader unfamiliar with type speciali-
sation, we start with a short type specialisation primer.
Further information can be found in Hughes' original paper
[?]. Then we introduce the language   oe
ml , an extension
of Moggi's computational lambda calculus with first-class
references. As a first step towards the full specialiser, we
state the specialisation rules for the treatment of dynamic
reference operations. We apply this specialiser to a self-
interpreter for   oe
ml and achieve optimal specialisation. In a
second step we add specialisation rules for static references
and apply this specialiser to an interpreter for a lazy functional
language that implements laziness using updatable
More information can be found in Section ??
closures. Next, we discuss the extension to state threads
and state the new postprocessing rules. Finally, we assess
our work with respect to partial evaluation, consider related
work, and conclude.
Type Specialisation Primer
Type specialisation is a form of program specialisation in
which types play a central r-ole. Rather than saying that
one term specialises to another term, we say that a source
term and type specialise to a residual term and type: e : - ,!
carry information to control specialisa-
tion, in particular binding-times: most type formers come in
static and dynamic variants, and we mark the dynamic ones
by underlining as usual. Residual types are sufficiently refined
to carry all static information, which means that static
values need not appear at all in residual terms. For exam-
ple, static integer constants are specialised to dummy val-
where the residual type records which
integer the dummy value represents. The residual type information
is enough to specialise expressions that use static
values appropriately: for example, the lift operation, which
converts a static integer to a dynamic one, specialises to the
constant value given by the residual type of its argument:
Well-typedness of the source term can be checked once
and for all before specialisation, but well-typedness of the
residual term can be checked only as it is constructed, during
specialisation. Thus the specialiser embodies a residual
type-checker, and it is the unifications in this type-checker
that propagate static information during specialisation. For
example, specialising
(where @ is dynamic function application) yields
where unification assigns x the residual type 3, and this
is sufficient information to perform the static addition and
specialise the lift to 4.
Type specialisation can propagate static information
more effectively than partial evaluation can. Modifying the
example slightly, we can specialise
to
since unification assigns x the residual type 3, which enables
the static addition to be performed, allowing f to be
assigned residual type 3 ! 4, which enables the lift to be
specialised to a constant. This can be done even though
f is a dynamic function, whose calls may not be unfolded.
Conventional partial evaluators do not allow dynamic functions
to return static results, since they derive static values
by reducing expressions to their normal form, and dynamic
function applications must not be reduced.
Type specialisation is inherently monovariant ; if we
modify our example to
then it can no longer be specialised, because f would need to
be assigned both 3 ! int and 4 ! int as residual types. But
polyvariance is easily added via a new source type poly - ,
with constructor poly and selector spec. An expression
poly e specialises to a tuple of specialisations of e, while
spec e specialises to a selection from the tuple. If we rewrite
our example as
poly -x:lift (x+1) in spec f @ 3 +spec f @ 4 : int
then it specialises to
where f has residual type (3 int). The residual
type information is enough to enable spec to choose the
right version at each call, and conversely the type information
at each spec is enough to enable poly to decide which
versions to create.
Alternatively, we could change f in the example into a
static function:
(note that the - and the applications are no longer under-
lined). Static functions are unfolded during specialisation,
so in this example each call of f is replaced by a specialisation
of its body, and of course the two specialisations can
be different. In order to unfold static function applications,
the specialiser represents a static function as a closure. The
static parts of the closure (bound variable name, body, and
residual types of the free variables) make up the residual
type of a static -, while the dynamic part (a tuple of the
becomes the residual term. The residual
type of a static function says nothing about the type
of its argument or result, and so such a function can be
freely applied to different static arguments at different calls.
In this example f has no free variables, and so its residual
term is the empty tuple (or dummy value). The result of
specialisation is
As these examples reveal, static computations leave an
undesirable 'residue' of dummy values in the specialised pro-
grams. But an optimal specialiser must remove static computations
completely. Fortunately, most dummy values can
be removed by a post-processing phase we call void erasure.
Completely static expressions yield residual types with only
a single element, for example 3, 4, 3 ! 4, or 3 \Theta 4. All such
expressions can safely be replaced by the dummy value ffl,
and all such types by void. Now using the isomorphisms
we can eliminate void components, void parameters, and of
course let-bound variables of void type. Void erasure often
simplifies residual programs drastically; for example, the last
two specialisations above become just
and
Optimal specialisation of typed interpreters demands
that we specialise the universal type that such interpreters
poly e j spec e terms
poly - types
poly -
poly -

Figure

1: The Two-level Source Language
1 in e 0

Figure

2: Basic Specialisation Rules
use to represent values appropriately. For example, an interpreter
for -calculus with integers might use the type
data
to represent values. This is an example of a static sum type:
the constructors encode the type of interpreted values, and
must be known statically. We therefore embed such static
constructors into residual types, rather than residual terms.
For example
The residual type records the fact that a Num constructor
was applied, and so it need not appear at all in the residual
term. Case expressions over static sums can be simplified
to one branch, given the residual type of the inspected ex-
pression, and so neither run-time type tags, nor run-time
tag checks, need appear in the residual programs. An interpreter
for   oe
ml that can be specialised optimally will be
given below.
Of course, partial evaluators can also implement static
sum types, and keep track of constructors statically. But
to specialise interpreters optimally, we need to be able to
return values of a static sum type from a dynamic function.
For the type specialiser which is deriving static information
by type inference, this is no problem. For a partial evaluator
which is using reduction, it is impossible.
In

Figure

?? we give the syntax and two-level type system
for a large fragment of our meta-language. It is essentially
a two-level version of the simply-typed -calculus.
The full language also includes sums and products, which we
have omitted here. We allow types to be recursive with no
special syntax. The point we wish to emphasise here is that
types can be freely formed according to the syntax given;
there are no 'well-formedness' conditions, such as that the
argument and result of a dynamic function type must themselves
be dynamic. Neither are there side conditions in the
typing rules, requiring for example that the variable bound
in a dynamic let itself be of a dynamic type. Such extra
conditions are an essential part of other two-level -calculi;
they are needed to make partial evaluation possible. The
key advantage of type specialisation is that these conditions
can be dropped.
The standard semantics of the meta-language is just the
usual semantics for the (call-by-name) -calculus: static and
dynamic constructs are not distinguished, and both poly e
and spec e have the same semantics as e. These are annotations
to control specialisation, and as such do not affect
the meaning of the original program.
Type specialisation can be specified quite simply via specialisation
rules that let us infer judgements of the form
where the context \Gamma tells us how to specialise variables, via
a sequence of entries of the selection

Figure

3: The Computational Metalanguage
of specialisation rules appears in Figure ??; we have omitted
the rules for static functions, which are a little more complicated
to express. Compare the rules for static and dynamic
let expressions: the only difference is that a static let is un-
folded, while a dynamic one is not. Precisely the same static
information about the bound variable x is available in both
cases. Again, this is in contrast to partial evaluation, where
a variable bound by a dynamic let must itself be dynamic.
The specialisation rules are more complicated to implement
than the usual type inference rules, because they are
not all syntax-directed. A description of the implementation
is beyond the scope of this paper, but can be found in [?].
3 A Metalanguage with Effects
Languages with effects are invariably harder to treat formally
than purely functional languages. One reason is that
evaluation order suddenly becomes important, even for constructs
in the 'pure' subset. Adding references and unrestricted
assignment to our metalanguage would therefore
change the semantics of every construct, and potentially invalidate
all the specialisation rules presented above.
To avoid this, we have chosen to work with Moggi's computational
metalanguage   ml [?], which explicitly distinguishes
between a value of type - , and a computation (with
effects) delivering a result of type - . The latter is assigned
a computation type M - . Trivial computations (with no ef-
fects) can be created by the unit operator j, and the results
of computations can be inspected using mlet x ( e1 in e2 ,
which combines the computations e1 and e2 in sequence, and
binds x to the value that e1 delivers in the evaluation of e2 .
The extensions to the syntax and type-system of our meta-language
are shown in Figure ??.
If e1 and e2 are computations with effects, then it is a
type error to write e1 + e2 . Instead, we must write
mlet x1 ( e1 in mlet x2 ( e2 in j (x1
making the evaluation order explicit. Similarly, to
pass the result of e1 to a function f , we must write
mlet x ( e1 in f x, making it explicit that e1 is evaluated
before the call. To write f e1 instead would not compute e1
first: it would pass the entire computation as a parameter
to f , to be invoked later (or not) at f 's pleasure. Think of
a value of type M - as a suspended computation, that can
be invoked by mlet.
Many different kinds of effects can be represented in
Moggi's framework, depending on how the types M - and
operators j and mlet are interpreted. To represent side effects
on a store for example, we can interpet a computation
as a function from the store beforehand to a result and the
store afterwards:
mlet x ( e1 in
Note that the translation passes the store that e1 produces
to e2 , and that x is in scope in e2 . Operations to create and
assign to references are interpreted as suitable functions with
a computation type. An interpretation for M , j and mlet
is called a monad, provided it satisfies the so-called monad
laws:
mlet x ( e in
mlet x ( (mlet y ( e1 in e2 ) in
mlet y ( e1 in mlet x ( e2 in e3
where in the third law, y must not occur free in e3 .
Haskell provides imperative operations in exactly this
way, but of course other imperative languages do not distinguish
computations explicitly. However, it is well known
that a -calculus with implicit effects can be simply translated
(in several different ways) into   ml , each translation
making a different evaluation order explicit [?]. By extending
the call-by-value translation we can map, say, ML or
Algol programs into our metalanguage. Thus we claim that
type specialisation is also applicable to such languages; they
simply have to mapped into an intermediate form which
makes evaluation order explicit first.
Moggi's language is a conservative extension of the -
calculus; the meaning of the pure subset remains unchanged.
Isomorphisms such as void ! - remain true - if a
function with this type has effects, then - must be a computation
type, and both sides represent a suspended com-
putation. This is its big advantage for us: the type specialisation
and void erasure rules for the pure metalanguage
remain valid when effects are added. We need only define
new rules for the new constructs.
The specialisation rules for j and mlet cannot be given
yet: they depend on which kind of effects we are interested
in. But we can note that these operations do not come in
static and dynamic versions. We will indeed be interested in
both static and dynamic effects, but since both kinds may
be used in one and the same computation, we need only
one computation type, and therefore only one version of the
monad operators.
Specialising Operations on State
We approach the specialisation of imperative operations
in three steps. First, we consider the situation when all
these operations are deferred until run time. This is already
enough to achieve optimal specialisation for a self-
interpreter. Then in Sec. ??, we move on to consider static
effects. Finally in section ?? we show how to combine the

Figure

4: Operations on Dynamic References
residual types
1 in e 0

Figure

5: Specialisation Rules for Dynamic State
two. This requires us to factorise the monad M into a
static state transformer and a second monad, so that the
specialiser can manipulate the static state.
4.1 Specialising a Dynamic State
We shall extend the metalanguage with operations to cre-
ate, inspect, and update dynamic references. The additional
syntax and typing rules are given in Figure ??; ref creates
a reference, ! reads its contents, and := assigns to it. Of
course, all three operations have a computation type.
Under the assumption that all monadic operations are
dynamic the specialisation rules turn out to be rather
straightforward (see Fig. The monadic operations simply
specialise their subexpressions and reconstruct them-
selves. In spite of this simplicity it is still possible to achieve
interesting results, since dynamic references can contain
static information in their residual type, which is propagated
to the rest of the computation via unification. For
example, specialising
mlet r ( ref 2
in mlet x
in j (lift
yields
mlet r ( ref ffl
in mlet x
in j 3
int.
The static value 2 is not present at run-time, but is preserved
in the residual type of r (which is ref 2). When r
is dereferenced we know statically that the result is 2, even
though r itself is dynamic.
We can see from the specialised expression that the reference
r still exists in the residual program, but it is useless
because its contents are of void type. The final phase
of type specialisation, void erasure, is extended to remove
such references and operations on them. It will thus transform
the above term to j 3. (We assume here that reading
and writing are the only operations on references; if testing
references for equality were also available then erasing void
references would not be correct.)
Since the residual type of a dynamic reference includes
the residual type of the value it contains, all the values we
assign to it must have the same static part. In the example
above, the only value we can assign to r is 2! When
a dynamic reference contains a partially static value, then
the static part must be the same at each assignment, but
the dynamic part can vary. For example, a reference of type
ref Univ (where Univ was defined in Sec. ??) created by
mlet r ( ref (Num (lift 2)) in
could later be assigned Num (lift 3) or Num (lift 4), because
all these values have residual type Num int. It could not be
assigned a value of the form Fun f . The residual program
would just contain a reference to an int, which would be
assigned the (untagged) values 2, 3 and 4.
When we want a reference to contain many different
static values, we are obliged to use a static reference. The
situation is comparable to the difference between static and
dynamic functions: a dynamic function can be specialised to
only one static argument, whereas a static function (which
is unfolded) can be applied to any number.
data
data
case e of
case eval env e 1 of
case eval env e of
case eval env e1 of
case eval (upd env i v) e2 of
case eval env e of
As e 1 case eval env e1 of
in eval (-i:Wrong)

Figure

Self-Interpreter for Optimal Specialisation
4.2 Optimal Specialisation
This specialiser is already capable of optimal specialisation.
To show this, we give a self-interpreter for the meta-language
in

Figure

??. (The interpreter is recursive: see [?] for specialisation
rules for recursion). Since the interpreted language
is typed, we represent values by a static sum type
When an expression of type Univ is specialised, its
residual type (for example Num int or Fun (Num int !
us what type of value it represents. All
type tags are known at specialisation time, and so both they
and the corresponding tag tests are simplified away by the
specialiser. As a consequence, this interpreter can only be
specialised to well-typed programs - supplying an ill-typed
input will lead to a failure during residual type inference.
references are needed to write the self-
interpreter, because the only use of references in the interpreter
is to model references in the interpreted program.
Such references can only be assigned values of one type (be-
cause the interpreted language is well-typed), and so during
specialisation all the values assigned will have the same
static part.
When we specialise this interpreter to a term, we obtain
essentially the same term as the result, up to ff-conversion.
The only operations in the interpreter which give rise to
residual code are those marked dynamic, the lift in the interpretation
of constants, and the monadic operations mlet
and j. By inspection, it is clear in most cases that eval
specialises to a copy of its second argument, provided the
same is true for the recursive calls. For example, the case
for constants contains one lift, which generates a residual
constant; the case for -expressions contains one dynamic
-, which generates a residual -expression, and so on. Only
two cases break this pattern: those for Rf and As each generate
an additional mlet and j. However, these can always
be removed by a post-processor which applies the monad
laws. In the case of Rf , the residual code is always of the
mlet r ( ref e in j r, which by the second monad
law is equal to ref e. In the case of As , the residual code is
of the form mlet z ( e1 := e2 in j ffl. Since z is of type
void this is equivalent to mlet z ( e1 := e2 in j z, which
is equal to e1 := e2 by the second monad law. The postprocessor
performs both these simplifications. Specialisation of
the interpreter is therefore optimal.
(In fact the post-processor may simplify additional re-
dexes, so to be more accurate: when we specialise this interpreter
to a term we obtain a reduct of the original term.
We claim that this specialisation should still be considered
optimal - it would be unreasonable to refuse to do so because
our specialiser sometimes performs more simplifications
than optimality requires!)
4.3 Specialising a Static State
Dynamic references are created and updated at run-time.
Consequently we cannot know their contents during special-
isation, and so we insist that all their contents have the same
static part, which we do know at specialisation time. So for
example, the expression
mlet r ( ref 2 in mlet z ( r := 3 in ! r
would cause a specialisation error, since r is used with both
ref 2 and ref 3 as residual types. We could avoid the error
by making the reference contents dynamic:
mlet r ( ref lift 2 in mlet z ( r := lift 3 in ! r
Now specialisation succeeds since r has residual type ref int,
but on the other hand no useful simplification is performed.
In constrast, static references are created and updated
during specialisation; the specialiser keeps track of their contents
in a static state, and so they may freely be assigned
residual types
1 s0 in e 0

Figure

7: Specialisation Rules for Static State
values with different residual types at different times. If our
example is rewritten using static references
mlet r ( ref 2 in mlet z ( r := 3 in ! r
then specialisation succeeds and produces
In this section we shall consider specialisation of a language
with only static references. The new operations and
their types are analogous to those for dynamic references
in

Figure

??, the only difference being that we omit the
underlines.
When we specialised a dynamic state above, we were
able to treat the monad and its operations as a black box:
because all effects were deferred to run-time, the specialiser
did not need to know anything about them. But now that we
are treating static effects that is no longer the case. Let us
therefore say explicitly that the computation type is State !
computations are represented as functions.
The static state itself is a tuple of the contents of the
existing static references. We actually build tuples up out
of pairs, so let us define a little syntactic sugar for values
and types:
We will also should be obvious how to
translate such pattern matching into combinations of projections

In source programs the static state is implicit, but in
residual programs we will represent it explicitly as a tuple,
and pass it explicitly to and from residual computations.
But now we encounter a problem. The residual type of the
static state is a tuple type, whose components are the residual
types of the contents of references. But a computation
may modify those residual types! Thus, in the residual pro-
gram, a computation may modify not only the contents of
the state, but its type! Residual computations have types of
the form
where oe is the residual type of the state beforehand, and oe 0
its type afterwards. This type is not a monad, which means
that we cannot express the residual program in terms of the
monad operators. However, ST has much in common with
a monad - we can for example give sensible definitions of
and mlet, for which the monad laws hold - and so we
call it a quasimonad 2 .
The specialisation rules for static references are given in

Figure

??. The rules for j and mlet just generate code to
pass the state around explicitly. Notice in the rule for mlet
that the residual types propagate static information about
the store from e1 to e2 (via the shared variable oe 1 ).
Creating a static reference (the third rule) enlarges the
static store by one element. The static reference may very
well have dynamic contents, which become part of the residual
static store. The only static information we need about
the new reference itself is the location to which it refers,
so we introduce a new form of residual type loc i to represent
the ith location. The dereferencing and assignment
operations just generate functions that access or modify the
residual store appropriately. Notice how the residual types
record precisely the static contents of every reference before
and after each operation.
The last three rules cannot be applied unless the shape
of the static store is known; the last two cannot either be
applied unless the address of the static location i is also
known. During specialisation this information should be
propagated from the context by unification. It is considered
a specialisation error if it is not possible to determine the
size of the static store during specialisation.
For example, suppose we specialise the term
mlet x ( ref (lift 2)
in mlet y ( ref 3
in mlet z ( x := lift 4 in j (x; y)
in an initially empty static store. The result of applying the
2 This is quite different from Steele's pseudomonads [?].
1 s0 in e 0

Figure

8: Specialisation Rules for Mixed State
specialisation rules is
in
in
in (-s3 :((x; y); s3))
Now s0 , x, y and z have void types and can so be removed
by the void eraser, which also deletes void components from
tuples. The result of void erasure in this case is
in
in
in (-s3 :s3
We use a post-processor which contracts trivial fi-redexes
(in which the actual parameter is just a variable), since the
specialisation rules introduce many of these. The final result
after post-processing is
All static operations on the store have been removed, and
the resulting program just passes around the dynamic values
which it held.
The residual programs we generate with this approach
are purely functional, and pass around any dynamic components
of the static store explicitly. An alternative approach
which we considered was to store such dynamic components
in the dynamic store instead. Thus every static reference
(with dynamic contents) would be associated with a reference
in the residual program, holding the dynamic part of its
contents. But remember that a static reference can hold values
with different residual types at different times - for ex-
ample, a reference of type ref Univ could hold both Num n
and Fun f on different occasions. No single residual reference
can hold both dynamic parts, n and f , because they
have different types. We could perhaps associate each static
reference with a tuple of references in the residual program,
one for each type of value it is assigned. At any dereference
operation, we would of course know statically which of the
associated residual references held the current dynamic part
of the contents. But reference creation would be awkward,
because all but one of the corresponding residual references
would be uninitialised. The problems are probably soluble,
but we feel that the approach we presented above is considerably
simpler.
4.4 Specialising a Mixed State
Now that we know how to specialise a static and a dynamic
state separately, it is relatively straightforward to specialise
them together. The trick is to separate the monad into
two parts: a static part which we manipulate explicitly in
the specialiser, and a dynamic part which we treat as a
black box. We therefore interpret the monad type M - as
is the monad type used
in residual programs. As in the previous section, residual
computations may change the type of the static state; they
will have types of the form
The specification rules have to be modified to produce
terms of this type. We modify the rules for dynamic reference
operations to pass the static store on unchanged, and
we modify the rules for static reference operations to construct
trivial M 0 computations using j. The modified rules
are given in Figure ??.
4.5 Specialisation of a Lazy Interpreter
We demonstrate the capabilities of the specialiser by specialising
a lazy interpreter to a term. Laziness is implemented
by using updatable closures. At application an abstraction
is passed a reference to a closure, which when evaluated
reduces the argument to weak-head normal form, and
performs an update on the reference cell. Provided only a
bounded number of closures are created, the reference operations
can be performed statically. Figure ?? shows the
interpreter.
Specialising the interpreter to the term (-x:x+x)(1+ 2)
yields the residual type ST hi hVl (Num int)i (Num int).
Here the output store contains the Vl (Num int). The
constructor Vl tells us that the corresponding closure was
evaluated at specialisation time. The constructor Num is
also manipulated at specialisation time, which means that
we can eliminate tagging and untagging from residual pro-
grams. What remains to be stored at run time is the integer.
The residual term after simplication (see section ??) is
in let
in f b
The resulting program, although a bit awkward, has the
expected structure. f corresponds to the abstraction, and b
to the argument 1 2, for which we have to build a closure.
The closure b takes a store s, and returns the result of the
addition. f takes this closure-dereference has taken place
at specialisation time - and applies the closure to itself-the
closure is the sole element in the store. The result of this
application is a computation taken apart by the monadic
let. We then perform the addition a + a, and tuple it with
a, the result of updating the store. The application s s of
the store to itself may seem strange, but it has a perfectly
admissible recursive type int. It is the result of
void erasure.
Delimiting Effects
The type specialiser is able, among other things, to derive
static information about the result of a dynamic conditional.
For example,
if b then Num (lift
which tells us statically that the result is tagged Num. Of
course, for this to be possible and for the residual program to
be well typed, the two branches must have the same residual
type. When the arms of the conditional are computations,
this implies that they must leave the static store in the same
state.
It is very awkward to meet this restriction. It means
that if any references are created in one branch, then exactly
corresponding references must be created in the other,
and assigned contents with the same static part! Most partial
evaluators for imperative languages handle the problem
by forbidding modifications to the static store in the arms of
a dynamic conditional, but this makes the static store much
less useful. Our solution to the problem is to support a stack
discipline for the static store. We introduce a 'store prompt'
# e, which causes the specialiser to deallocate static references
created by e after its specialisation is complete (see
Fig. If we use store prompts in the arms of a dynamic
conditional, then each arm can refer to the previous static
store, and create and use its own local references, without
causing a residual type mismatch. Of course store prompts
should only be used when local references do not escape from
the enclosed expression.
As we have explained, operations on the static store can
only be specialised once the size of the store is known. The
specialisation rules propagate the static store from operation
to operation, so if the initial size of the store is known, then
its size will be derivable at all subsequent operations. Of
course we intend the initial store to be empty, but so far we
have glossed over how we specify this.
In fact, there can be other reasons for wanting to specify
the size of the store. Consider the function
-t:mlet r ( ref 1 in mlet v liftv).
which uses the static store internally to compute t + 1. This
function's type is int!M int, and it cannot be specialised
without knowing the size of the static store at the point
where it is called. That seems unfortunate since it doesn't
refer to any non-local references. Moreover, if the function
were called from two points with different static stores, then
we would need to make it polyvariant and construct two different
specialisations - even though it doesn't access those
different stores. This would be the case even if we inserted
a store prompt into the function's definition.
The solution is to run the computation in the function's
body in a new, empty static store. We define two new operators
to do so, which differ only in their treatment of the
dynamic store (see Fig. runM e turns a computation
with effects into one without, from a computational
perspective. It runs e in a completely new (static and dy-
namic) store, so that e can neither access nor modify the
enclosing store - it is a state thread. The residual type
does not involve the monad, and so the residual code must
itself include the effect delimiter runM . runM e runs e
of type M- in a new and empty static store, but threads
the dynamic store through, so that e can access and modify
non-local dynamic references. The residual type is still
because of the dynamic store. We should ensure that
references neither escape from runM e nor can they be imported
from the outside (and analogously for runM e and
static references). We gloss over this problem here because
we can apply Launchbury and Peyton Jones's solution to a
related problem [?, ?].
The specialisation rule for runM e (see Fig. ??) applies
the residual quasimonad of e to an empty initial static state,
runs the resulting dynamic computation, and discards the
final static state. The result is a value with residual type - 0 .
The rule for runM e also applies the residual quasimonad
to an empty static state, and the final state oe 0 is again dis-
carded. In contrast with runM , the resulting expression
might still induce effects at run-time. For this reason we
thread the resulting computation into the dynamic computation
thread.
Now we can specialise our initial example in two ways:
in mlet v
in
or
in mlet v
in
data
data
data
case e of
case v of
mlet
case b of
Ap
mlet a ( ref Bl 0 in
mlet b ( a := Cl (mlet c ( eval env e2 in a := Vl c) in
case f of
Pl eval env e1 in
mlet b ( eval env e2 in
case a of
case b of
in eval (-i:Wrong)

Figure

9: Lazy Interpreter

Figure

10: Typing and Specialisation Rules for Store Prompts
The only other specialiser to combine first-class functions
with static references is due to Dussart and Thiemann [?]. It
is a more conventional partial evaluator, in which dynamic
functions cannot have static arguments. Consequently it
always specialises the bodies of dynamic -expressions in an
empty static store. Our runM essentially simulates this
behaviour.
Our effect delimiters runM and runM are rather blunt
instruments. Ideally we would like to be able to specialise a
computation knowing only the contents of static references
that it actually refers to. Likewise we would like to be able
to invoke such a specialisation in different static stores, provided
the references actually used have the same contents.
To do so requires polymorphism in residual programs -
we want to invoke the same residual function on stores with
different residual types. The generation of polymorphic programs
by type specialisation is so far an open problem, which
must be solved before a better treatment of static stores is
possible.
6 Postprocessing
As we remarked above,   oe
ml is a pure language in the sense
that isomorphisms like void ! - are still valid. Therefore
the all techniques for void erasure in the lambda calculus
[?] are still valid.
6.1 Void Erasure
The void eraser follows one simple principle: Replace every
expression whose type denotes a singleton set by ffl. Apart
from the standard situations involving products, sums, and
function types described by Hughes [?], we now have two
additional type constructors to consider: ref - and M - .
Keeping references of type ref void makes no sense unless
there is an equality operation on references. They can be
erased in the absence of such an operation. However, the
type M void denotes a computation returning void, but
the computation may very well affect the (dynamic) state.
It cannot be erased.
Since we regard ref void as useless we can replace all

Figure

11: Type Rules for Store Delimiters

Figure

12: Specialisation Rules for Store Delimiters
operations processing them by appropriate monadic units:
This process removes operations on the dynamic state. The
residual operations on the static state are expressed by explicit
store passing. The simplification rules for the standard
types suffice to simplify them.
6.2 Monadic Simplifications
The residual programs are written in monadic style and
contain a lot of redundant monadic let and unit expres-
sions. This is partly due to the actions of the preceding
void erasure. These expressions present ideal targets for
applying the three monad laws. Moggi [?] has proved that
ml is sound and complete with respect to all monadic mod-
els, specifically for our model that uses state transformers.
Therefore, the application of the monad laws is very safe
in the sense that it does not duplicate, discard, or reorder
computations.
If the type of x is void then after application of the rule
we can drop the let and e 0 entirely if the type of x is void.
In this case let . The post-processor does
not unfold lets in general, but we do use the simplication
because terms of this form appear quite
often after applying the preceding transformations.
Finally, simplification discards trivial computations
wrapped in runM :
runM (j e) ,! e.
6.3 Further Simplifications
Due to the explicit store-passing style, the residual program
contains many trivial fi-redexes like (-x:e) x. We convert
them to let-expressions and apply the same simplifications
as outlined above. No other (serious) fi reductions are performed

The explicit representation of the store as tuples introduces
a lot of extraneous tupling and tuple operations.
These are eliminated via an arity raising phase [?].
Finally, explicit store-passing introduces many j-redexes
on top of computations that do not affect the static store.
Therefore, the void eraser also performs j-reductions.
Assessment
Type specialisation enhances partial evaluation with information
propagation by unification. This enables side-ways
information exchange in the source program's execution tree
whereas partial evaluation is restricted to paths in the execution
tree. A consequence is that residual programs cannot
be constructed in a bottom-up manner, but rather program
fragments are constructed in a demand-driven order prescribed
by the flow of information.
Much of the power of type specialisaton stems from the
refined type language used. The type language is able to
express single element types that play the r-ole of symbolic
values and partially static values of standard partial evaluation

In contrast to partial evaluation, the two-level type discipline
of type specialisation does not impose well-formedness
conditions like "if an abstraction is dynamic then its argument
and result must also be dynamic." Another instance
is the fact that dynamic references may hold static values.
This liberality is unique to type specialisation. It is the key
to the optimal specialisation results for typed functional languages
reported here and in Hughes initial work [?], because
it allows information (such as static tags) to be communicated
out of dynamic functions.
However, the well-formedness conditions are at the heart
of traditional binding-time analysis. A binding-time analyser
constructs the least (most static) assignment of well-formed
types to terms; dynamic inputs force other computations
to be dynamic also via the well-formedness conditions.
The most static type assignment is always 'best' - it leads
to the strongest specialisation. The type specialiser in contrast
can check that a two-level program is well-typed, but
cannot infer a 'best' assignment of two-level types to a one-level
program. In the absence of well-formedness constraints
many more operations can be made static, but this does not
mean that they should be. For example, in the interpreters
in this paper we chose to make Univ a static sum type,
so that type tags would be removed during specialisation.
In consequence these interpreters can only be specialised
to well-typed programs - they interpret a typed language.
Had we chosen to make Univ a dynamic sum instead, then
type tags would have remained in residual programs, but
we would be able to specialise the interpreters to arbitrary
programs - such interpreters accept an untyped language.
Neither alternative is obviously better than the other, and
we do not believe the choice can be made by an automated
analysis. The assignment of binding-times in an interpreter
is essentially a way to specify the static semantics of the
interpreted language, and this is a creative activity.
Furthermore, type specialisation also performs program
analysis of the residual program while it constructs the residual
program. An example for this is shown in Hughes work
[?] where he constructs a firstifying two-level interpreter for
a type lambda calculus. Here the type specializer performs
closure analysis and the construction of recursive residual
types on the fly.
8 Related Work
8.1 Type and Constructor Specialisation
Hughes [?] introduces type specialisation for a simply-typed
lambda calculus with products and sums. The current work
is an conservative extension to Moggi's computational meta-language
[?]. The type specialiser embodies constructor specialisation
[?, ?] and extends it to higher-order languages.
Hagiya and Iino [?] consider a weaker variant of constructor
specialisation that they call "data type specialisation"
for a Lisp-like language. They have set up an extension
of the standard partial evaluation framework consisting of
an extended binding-time analysis and a specialiser which
is expressed as a non-standard interpreter and constructs
the residual program in a compositional manner. Bechet [?]
gives an account of a very similiar technique geared towards
typed languages. The other constructor specialisers and the
type specialiser construct the residual program out of order.
8.2 Partial Evaluation
Partial evaluators for traditional imperative languages like
FORTRAN, C, Pascal, or Modula-2 [?, ?, ?, ?, ?] all perform
side effects at specialization time. However, none of them
incurs the problems inherent in higher-order control flow
and only some of them face the problems of dealing with
pointers which are similar to the problems with first-class
references. In the present work, type specialisation deals
satisfactorily with a language with higher-order control flow
and first-class references.
Partial evaluators for higher-order functional languages
are quite common [?, ?, ?, ?, ?, ?]. Only some of them
attempt to handle side effects [?, ?, ?] but all of them follow
the approach of Bondorf and Danvy [?] in deferring all side
effects like operations on references, assignments to global
variables, and I/O to run time.
Recently, there have been approaches to perform partial
evaluation of imperative programs with static operations on
references. Moura, Consel, and Lawall [?] show how to use
Schism [?]-a partial evaluator for pure Scheme with a poy-
variant binding-time analysis-to specialise programs in the
C language by transforming them to a sophisticated variant
of store-passing style. This approach avoids the construction
of new program analyses and new partial evaluation
techniques for imperative programs.
Dussart and Thiemann [?] have constructed an offline
partial evaluator for a simply-typed lambda calculus with
first-class references. Their system is traditional in that its
monovariant binding-time analysis ensures that there are no
errors at specialization time. The binding-time analysis is
based on an effect system. The system is automatic, in contrast
to the type specialiser which only works on manually
annotated programs.
9 Conclusion
Type specialisation adapts seamlessly to the specialisation
of imperative languages. Unification again gives us the necessary
power to achieve optimal specialisation for a version
of Moggi's computational metalanguage with first-class references

Our use of the computational metalanguage   oe
ml turned
out to be a big win. First, we only had to add rules for the
new constructs of the language to the type specializer. No
existing rule was changed. Contrast this with the specializer
of Dussart and Thiemann [?] where every specialization
rule had to be changed in order to thread the state through
the computation. Second, our specialiser is completely independent
of the evaluation order. Only the sequence of the
monadic operations is fixed; the remaining parts of a program
can be specialized without committing to a specific
evaluation order. Third, we conjecture that the monadic
approach allows further modular extensions to cater for ex-
ceptions, non-determinism, etc.

Acknowledgement

We thank the anonymous reviewers and Mads Tofte for their
valuable comments.



--R

Program Analysis and Specialization for the C Programming Language.
Partial evaluation of numerical programs in Fortran.
Removing value encoding using alternative values in partial evaluation of strongly-typed languages

Automatic autoprojection of higher order recursive equations.
Automatic autoprojection of recursive equations with global variables and abstract data types.
Efficient analysis for realistic off-line partial evaluation
Practical aspects of specialization of Algol-like programs
A tour of Schism.
A general approach for run-time specialization and its application to C
Partial Evaluation
Polyvariant constructor specialization.
Partial evaluation for higher-order languages with state
Building interpreters by transforming stratified monads.
Binding time analysis for data type specialization.
Functional Programming Languages and Computer Architecture
Type specialisation for the
Partial Evaluation and Automatic Program Generation.
A strongly-typed self-applicable partial evaluator


Modular denotational semantics for compiler construction.
ML partial evaluation using set-based analysis

Techniques for partial evaluation of imperative languages.
Constructor specialization.
Computational lambda-calculus and mon- ads
Bridging the gap between functional and imperative languages.




Automatic online partial evaluation.
--TR
Computational lambda-calculus and monads
Arity raiser and use in program specialization
Techniques for partial evaluation of imperative languages
Automatic autoprojection of recursive equations with global variable and abstract data types
A strongly-typed self-applicable partial evaluator
Automatic online partial evaluation
Two-level functional languages
Automatic autoprojection of higher order recursive equations
Partial evaluation and automatic program generation
Partial evaluation and semantics-based program manipulation
Constructor specialization
A generic account of continuation-passing styles
Building interpreters by composing monads
Lazy functional state threads
Polyvariant constructor specialisation
State in Haskell
A general approach for run-time specialization and its application to C
Functional Programming Languages and Computer Architecture
Partial Evaluation
Removing Value Encoding Using Alternative Values in Partial Evaluation of Strongly-Typed Languages
Hand-Writing Program Generator Generators
Practical Aspects of Specialization of Algol-like Programs
Type Specialisation for the lambda-Calculus; or, A New Paradigm for Partial Evaluation Based on Type Inference

--CTR
John Hughes, Type specialization, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
John Hatcliff, Foundations for partial evaluation of functional programs with computational effects, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
Kedar Swadi , Walid Taha , Oleg Kiselyov , Emir Pasalic, A monadic approach for avoiding code duplication when staging memoized functions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
Gilles Barthe , John Hatcliff , Morten Heine B. Srensen, CPS Translations and Applications: The Cube and Beyond, Higher-Order and Symbolic Computation, v.12 n.2, p.125-170, September 1999
type systems;specialisation;monads;program transformation