Compilation Based on a Calculus for Explicit Type Passing
Yasuhiko Minamide
Research Institute for Mathematical Sciences, Kyoto University
Kyoto, 606-01, JAPANE-mail: nan@kurims.kyoto-u.ac.jp

ABSTRACT
We propose several calculi for explicit type passing that enable us to formalize
compilation of polymorphic programming languages like ML as phases of typepreserving translations. In our calculi various manipulations for type parameters
can be expressed without typing problems|this is impossible in the polymorphic-calculi. Furthermore, we develop the translation from an explicit typed source
calculus similar to Core-XML to one of the proposed calculi which completely
eliminates runtime construction type parameters. We propose an intermediate
language based on this calculus, and discuss an implementation of a compiler
for Core Standard ML.

1. Introduction
One of the advantages of typed programming languages is that type information
can be productively used to obtain ecient executable programs. However, in thepresence of polymorphism, a type in a program may contain type variables and cannot
be determined as a ground type at compile time. This has been one of the main diculties in developing implementations of ML which eectively utilize type information
obtained from type inference. In order to overcome this problem two approaches toutilizing type information for compilation have been proposed recently.
The rst approach is representation analysis proposed by Leroy 13], which is basedon coercions between monomorphic and polymorphic types. Although the polymorphic parts of a program must use uniform representation, the monomorphic parts canbe compiled eciently by using type information. It was reported that the compilers
based on this approach improved the performance of executable programs 13, 21].
More aggressive approach is to use type information by passing types as actual
parameters 17, 9, 4, 26, 25] as in the second order -calculus. The advantage ofthis approach is that even for a polymorphic type the actual type is known as an
instance at runtime and can be used for several purposes. For example, Tolmach
implemented tag-free garbage collection by passing type parameters 26]. Harper andMorrisett proposed a general mechanism for using types at runtime called intensional
type analysis 9]. In Tolmach's implementation it is shown that explicit type passing
is not so expensive as one might think.
In this paper, we propose several calculi for explicit type passing that enable us
to formalize compilation of polymorphic programming languages like ML as phasesof type-preserving translations. In our calculi, various manipulations for type parameters can be expressed without typing problems, which is impossible in standard1

polymorphic -calculi. Furthermore, we propose the translation from a source calculus similar to Core-XML to one of the proposed calculi which completely eliminatesruntime construction of type parameters. Based on the calculus, we propose an intermediate language and discuss an implementation of an experimental compiler forCore Standard ML 15].
There are many advantages of compilers which are constructed as phases of typepreserving translations. Complete type information can be used for optimizationsuch as instantiating polymorphic equality to monomorphic equality and choosingecient representation of data types. It is also useful to prove correctness of compilation through such a method as logical relations 24, 6, 20, 22, 23]. Furthermore,constructing compilers as phases of type-preserving translations has a practical advantage for development of compilers as mentioned in 16, 25]. When we debug acompiler itself, a code of an intermediate language can be type-checked. This has
greatly helped to nd bugs in our compiler.
Type parameter passing is sometimes considered expensive. For example, Tolmach reported that the memory allocated for type parameters sometimes exceeded
the memory saved by tag-free garbage collection. Thus, it is desirable to consider
optimization of manipulation of type parameters. We propose the transformationthat eliminates runtime construction of type parameters. However, it is found thatthe transformation cannot be formulated as a type-preserving translation in standard polymorphic -calculi. Thus, we develop a more suitable calculus to express
manipulations of type parameters.
There have been many studies that considered passing some kind of type information to implement various aspects of programming languages such as polymorphic
record operations and overloading 27, 18, 11]. For the theoretical basis of these approaches, various typed languages have been proposed. The calculus  ) we propose inthis paper can be considered as an extension of the implementation calculus for compilation of polymorphic records of Ohori 18, 19] and qualied types of Jones 12, 11].
Runtime type parameters are distinguished from the usual types and new abstraction
and application for runtime type parameters are introduced. In our calculus, various
manipulations of types are more naturally expressed.
The next step is to develop the translation from the source language to the calculus ) where type parameter passing is made explicit. There are many ways toachieve this depending on what type information is to be passed to each polymorphic
function. The simplest choice is to pass the type information for type variables as Tolmach's. This strategy gives complete type information and enables tag-free garbage
collection. However, if we only want the type information for some non-parametric
operations, only the type information for relevant type variables need to be passed.
Conversely, to avoid runtime construction of type parameters, more complicated type
information is passed to a type function. Thus, we formulate a deductive system that
non-deterministically chooses what type information is passed to each polymorphic
2

function. It is proved that this general translation preserves the type and operational
behaviour of a program. As a special case of the deductive system we propose atranslation called aggressive lifting, where the program obtained through the translation requires no runtime construction of type parameters. Furthermore, we formulate
deterministic deductive systems for Tolmach's and aggressive lifting. These systems
naturally give rise to the algorithms of both types of lifting.
We propose another calculus ) which identies type parameters with values. It
is shown that ) has greater expressiveness on manipulations of type parameters andis more suited to an actual intermediate language of compilers. Since type parameters
can be considered as values, they can be components of tuples. By using this facility,
closures can be implemented more eciently. Furthermore, optimization such as
uncurrying of type parameter and usual abstractions is more simply formulated thanin the previous calculus.
We have implemented an experimental compiler by using Kit compiler 2] as front
end. The compiler translates Core Standard ML programs to C. Non-parametric operations such as polymorphic equality and tag-free garbage collection are implemented
by using runtime type parameters. As the intermediate language of the compiler, we
adopted the language based on calculus ) proposed in this paper. Our implementation of the compiler is such that Tolmach's and aggressive type lifting can be chosen
at compile time. The eect of this choice is measured on the simple benchmarks likepolymorphic equality and standard benchmarks such as life and knuth-bendix. The
results for simple benchmarks show that aggressive type lifting is more than 15 %faster at execution time than Tolmach's. For standard benchmarks, the advantage
of aggressive lifting varies from the minimal to 10 % at execution time and 35 % atheap allocation depending on benchmark programs.
Recently, there have been several attempts to utilize type information of ML
programs by passing type information. There are two compilers of ML that passtype information at runtime: Tolmach's compiler 26] and TIL 25]. The intermediate
language of Tolmach's compiler seems basically untyped. On the other hand, similarly
as our compiler TIL compiler is organized as phases of type-preserving translations.
However, TIL compiler does not consider optimizations of type parameter passing
and their typing problems. The intermediate language of the compiler is based on
the second order -calculus and intensional type analysis.

2. Explicit Type Parameters
There are no explicit type abstractions and applications in ML. However, as proposed in 8], ML programs can be translated to the language with explicit type abstractions and applications like the second order -calculus. Milner's type inference
algorithm nds a typing derivation for a well-typed program in the type system.
Based on the derivation, we can translate ML programs to the explicitly typed lan3

guage as described in 8]. For example, the following program is translated into theexplicitly-typed program below.
let fun f x =let fun g y = (x,y)
in(g 2, g true)endinf 3 f 3.14
end

let val f = t. x:t.
let val g = s. y:s. (x,y)
in(g int 2, g bool true)endinf int 3 f real 3.14
end

f g

f g

f

f

g

g

However, in order to preserve the operational behavior of a program we have torestrict generalization of types in let for values. Such restriction was studied in 28]
to avoid imperative types and reported to work well in practice.
Thus, as the source language of compilation of ML we consider the restricted
polymorphic -calculus similar to the Core-XML 8] that captures typing properties
of Core Standard ML. The source language is dened as follows:
Monotypes  ::= b j t j  ! 
Polytypes  ::=  j 8t1  : : :  tn:Expressions e ::= c j x j x::e j e1e2 j t1  : : :  tn:e j ef1  : : :  n g j p j
let x: = e1 in e2

We call this calculus 8 . For the illustration of compilation of non-parametric operations, the primitive p of type 8t:p is included in this calculus. We assume thatprimitive p requires some type information at runtime. We often write a sequenceof types as  . For example, we sometimes write a type application as ef g. For
this calculus, we consider the standard type system and call-by-value operationalsemantics.
4

As source programs of compilation, we consider only the type normalized expressions 10] that satisfy the following two conditions. Type abstractions occur only as
the bound expression of let-expressions i.e., let x: = t 1  : : :  tn:e1 in e2 . Typeapplications are only allowed for variables i.e, xf1  : : :  ng. The type normalized
expression corresponding to an expression can be obtained by some simple transformations without changing behaviour of the expression.
2.1. Tolmach's Lifting Transformation

There are several possibilities on how type information can be passed in programs.
The simplest way is to treat each type variable as a variable for values and implement
type substitution as substitution for values. However, such implementation seems tointroduce a lot of cost.
Thus, Tolmach proposed passing several type parameters as one parameter that
he called a type environment and performing type substitution lazily. To pass typeparameters as one parameter, a program is transformed so that every type function
is closed with respect to type variables. In the above example, we have type function
g with free type variable t. (Although type variable t does not occur in function g, itshould be considered free because variable x of type t occurs in function g.) To makeg closed with respect to type variables, free type variable t is lifted and t is abstractedwith s in an uncurried abstraction as below.
let val g = ts. x:t. y:s. (x,y)
val f = t. x:t.(g t,int x 2, gin
f int 3 f real 3.14
end

f g

f

f
g

g

ft,boolg x true)

We call this transformation Tolmach's lifting. This transformation is always possible
in 8 because all the application sites of a type function can be determined syntactically in this language. Then type arguments for an uncurried type abstraction are
passed as one parameter. Thus, only one parameter is necessary for type information
in a type function after applying this transformation.
It should be remarked that variable x is also lifted in function g, because thetype of x is t that is lifted. Without such lifting, the transformation may result in
an ill-typed program. Thus, the transfromation depends on which variables should
be considered free in a type function. This information is usually determined during
closure conversion to avoid closures for known functions 1]. Thus, this lifting transformation and closure conversion must be performed at the same time. That makes
the implementation of a compiler based on this transformation compilicated.
It is still expensive to construct a type environment every time a type function
is called. Thus, Tolmach used the method performing type substitution lazily. In
5his implementation, almost all parts of a type enviornment are created statically andeach construction of type environment consumes only 2 words.
2.2. Aggressive Lifting and Typing Problems

In this subsection we consider optimized type parameter passing and show that
it is impossible to express such type parameter passing in standard polymorphic calculi. The following example is taken from 26]. At runtime of the program, thetype environment fs  sg for pair is created every time the function repair is called.
let pair = t. x:t.(x,x)
repair = s. y:s. pairinrepair int n
end

f g

fs  sg (y,y)

To overcome this ineciency, Tolmach suggested lifting the type parameter for thefunction pair out of repair as below.
let pair = t. x:t.(x,x)
repair = s.t. y:s. pairinrepair int
int int n
end

f gf  g

ftg (y,y)

Now that the type paramter fintintg is closed, that can be constructed staticallyand there are no need of runtime construction of types. If a calling site of repair is in
another type function, the lifted type argument may be still open. Thus, in order toeliminate runtime construction of type parameters we must apply this transformationfrom the inner-most type functions repeatedly. Thus, if there are nested calls to type
fucntions, the number of type arguments may increase exponentially.
Furthermore, this program is not well-typed in the second order -calculus because
t is not equal to s  s in the function repair. One solution of this problem is to use
translucent types (or manifest types ) proposed for modules of Standard ML 7, 14]
and recently used to solve the typing problem of closure conversion of the second
order -calculus in 16]. For the program above, we can add the constraint t = s  s
at abstraction of t in repair and such modication makes the program well-typed
in the extended calculus. However, this solution is not satisfactory when we consider
other kinds of manipluation of types as we see below.
In order to avoid the increase of the number of type parameters, the transformation
is modied so that two type absractions are uncurried as below.
6let pair = t. x:t.(x,x)
repair = s. y:1 (s). pairinrepairint,int int
n
end

fh

 ig

f (s)g.(y,y)
2where uncurrying is made explicit by using type abstraction that takes a pair oftypes h1  2i instead of uncurried form of type abstraction t1 t2 :e. We call thistransformation aggressive lifting in this paper. In this transformation, the numberof the type arguments does not increase and the runtime construction of types are
replaced by projections of type parameters. However, even if we use translucent
types for this transformation, it is impossible to make this program well-typed. The
constraint that the type argument s of repair must hold is  2 (s) = 1 (s)  1 (s)and we cannot express this constraint by translucent types. So, we propose a calculus
more suitable to express manupulations of type parameters in the next section.

3. A Calculus for Explicit Type Passing
In this section, we propose the explicitly typed calculus that is suitable to express
wide range of manipulations of type parameters and thus the base of the intermediate language of compilers of ML. There have been many studies that proposed
passing some kind of type information to implement various aspects of programming
languages such as polymorphic record operations and overloading 27, 18, 11]. For
the theoretical basis of these approaches, various calculi have been proposed. The
calculus we propose can be considered as an extension of the implementation calculus for compilation of polymorphic records of Ohori 18, 19] and qualied types ofJones 12, 11]. We mainly use terminology of qualied types in this section. The
language of our calculus is dened as follows:
Monotypes  ::= b j t j  !  j  ) Predicates  ::=  j h1  : : :  ni
Polytypes  ::=  j 8t1  : : :  tn:Evidences ! ::= b j u j ! ! ! j i (! ) j h!1 : : :  !ni
Expressions e ::= c j x j x::e j e1 e2 j t1  : : :  tn:e j ef1  : : :  n g ju::e j e!] j p j let x: = e1 in e2

Compared to 8 , the language is extended by predicates and evidences. Evidences
are corresponding to runtime type parameters for our purpose and are classied by
predicates. Monotypes are extended by type  )  which is the type for the functionthat takes a type parameter classied by . Evidences (or runtime type parameters)
have the denition similar to that of monotypes to express corresponding type information. However, a type variable is replaced by an evidence variable u and it isextended by tuple h!1 : : :  !ni and projection i(!), which are used to pass multiple7 ` !2:2(base)   ` b:b (var) u: `2 u: (arrow) ` `!1!:1! !2 :1 ! 2
1
 ` !i:i (1  i  n)  ` !:h1 : : :  ni(tuple)   ` h!1 : : :  !ni:h1 : : :  ni (proj)  ` i (!):i
Figure 1: Rules for Evidences
types as one parameter. The abstraction u::e represents the function which takes
type information corresponding to . The runtime type information ! is given to anevidence abstraction by evidence application e!]. We call this calculus  ) , where is evidence abstraction and ) is the type of evidence abstraction.
Now we will give the type system for the calculus. First, we need the following
three kinds of contexts.
Type contexts
 ::= t1  : : :  tn
Predicate assignments  ::= u1 :1  : : :  un:nType assignments; ::= x1 :1  : : :  xn:n
We extend the usage of type contexts to general sequence of type variables. For
example, we sometimes write polytypes and type abstractions as 8: and :e.
There are two kinds of judgments as follows:  ` !: evidence ! satises predicate   ; ` e: expression e has type 

where we assume that all free type variables in  and ; are included in . The rules
for judgment   ` !: are shown in Figure 1. Intuitively,  u 1:1 : : :  un:n ` !:
means that evidence ! is the type information corresponding to predicate  if we
assume each ui is the type information corresponding to predicate i. According
to our specic purpose, these rules are simplied compared to the rules of qualied
types. However, they are extended for tuples and projections of evidences.
The typing rules for the calculus are similar to the rules of qualied types and areshown in Figure 2. Only the rules for type abstraction and application, and evidence
abstraction and application are shown. Other rules are standard. For primitive p oftype 8t:p in 8 , we assume that the corresponding primitive p in  ) requires theevidence (or type parameter) which satises predicate  p and thus has type 8t:p ) pin ) .
For this calculus, we consider the standard call-by-value operational semantics:
8  u: ; ` e :   ; ` u::e :  )   ; ` e :  )    ` ! :   ; ` e!] :  0  ; ` e :   ; ` 0:e : 80 :  ; ` e : 8t1  : : :  tn:  ; ` ef1 : : :  ng :  1  : : :  n=t1 : : :  tn]  ; ` p : 8t:p ) p
Figure 2: Typing Rules(u::e)!] is reduced to e!=u].
3.1. Representing Type Passing in )

In this subsection, we consider how various ways of type lifting we have considered
can be represented in this calculus without causing typing problems. The formal
account of the translation from the source language 8 to the calculus ) is given in
Section 4.
The following program is the translation of the rst example corresponding toTolmach's lifting.

hi

let val f = t.u: t . x:t.
let val g = s.u: t s . y:s. (x,y)
in(g int  t int ] 2, g bool  t bool ] true)endinf int  int ] 3 f real  real ] 3.14
end

h i
f g h if g h i

f

f

g h

i

g h i

For the function f and g, the evidence abstractions are added after the type abstractions. The evidence parameter u for g takes an evidence corresponding type variables
t and s. Thus, all the necessary type information can be obtained from one parameteru in the function g. It can be easily checked that this program is well-typed in  ) .
Furthermore, as the example shows, we do not have to lift type and value abstractions. Thus we can separate the lifting transformation from closure conversion andthe design of compilers can be simplied. Furthermore, this representation is moreclosely reecting Tolmach's implementation since it is explicitly expressed that all
runtime type arguments to a type function are passed as one argument.
9Furthermore, we can express various manipulations of type parameters withoutcausing the typing problems we described in Section 2.2. In the following example,
the type parameter for the function pair is lifted from the function repair as typeparameter u2 .
let pair = t.u:hti. x:t.(x,x)
repair = s.u1 :hsi.u2 :hs  si. y:s. pair fs  sg u 2 ] (y,y)
inrepairend

fintg hinti] hint  inti] 1

The function pair has type 8t:hti ) t ! t  t and pair fs  sg has type hs  si )(s  s) ! (s  s)  (s  s). Since u2 satises predicate hs  si and (y,y) has types  s, pair fs  sg u2 ] (y,y) is well-typed.
In the same way, uncurrying of type parameters can be done while preserving
well-typedness of the program as the following. The type parameter consiting of sand hs  si is passed as one parameter to repair and its second component is usedas the type parameter to the funciton pair.
let pair = t.u:hti. x:t.(x,x)
repair = s.u:hs hs  sii. y:s. pair fs  sg  2 (u)] (y,y)
inrepairend

fintg hint hint  intii] 1

4. Type Lifting Translation

In this section, we will give the translation from source calculus 8 to calculus) . First, we consider a general translation that is non-deterministic and involves
not only Tolmach's lifting but also aggressive lifting. The translation is given as  ; ` e e0 where , , and ; are a type context, a predicate assignment, and atype assignment of ) respectively. The closed expressions are translated under theempty contexts.
The rules for the translation are shown in Figure 3. In rule (let), the body ofthe type abstraction, e1, is translated by assuming that type information is passed
by fresh evidence variable u. This variable u is assumed to hold the evidence thatsatises predicate . However, no condition is given for the predicate  in this rule.
That makes the translation non-deterministic and gives the ability to express various
ways of lifting. As we see later, several restrictions are imposed in this rule dependingon the strategies of lifting. After the translation of e1 , e2 is translated by assumingthat x takes an evidence that satises predicate .
A type application is translated into the combination of type and evidence applications by rule (tapp). The applied type parameter is determined from the type10

(let)

 0   u: ; ` e1 e01   ; x:80 : )  ` e2 e02  ; ` let x:80 : = 0:e1 in e2 let x:80 : )  = 0:u::e01 in e02(tapp)

  ` ! : 1=0 ]  ; x:80 :1 ) 2 ` xf g xf g!](prim)

  ` ! : p =t]  ; ` pf g pf g!]Figure 3: Translation from 8 to )
assignment of the variable. If the variable with type 8t 1  : : :  tn:1 ) 2 is applied to the type 1  : : :  n then it requires the type parameter corresponding to1 1  : : :  n =t1  : : :  tn ]. So the evidence ! that satises  1 1  : : :  n =t1  : : :  tn ] under  is applied. For primitive p, pf g is applied to the evidence ! which satisesp =t].
For this deductive system, we proved that the translation preserves the type andoperational behaviour of a program. Operational correctness is proved by the methodof logical relations.
4.1. Tolmach's Lifting

Tolmach's lifting is formulated by restricting the rule (let) as follows: 0  u:h 0i ; ` e1 e01   ; x:80 :h 0 i )  ` e2 e02  ; ` let x:80 : = 0:e1 in e2
let x:80 :h 0 i )  = 0 :u:h 0 i:e01 in e02
where the predicate  is restricted to   0. This choice of predicate  0 for u isalways enough to translate e1 . By this restriction the translation is almost deterministic. However, the deduction of ` is still non-deterministic and may give redundanttranslation such as ` 1(hbi) : b. Thus, Tolmach's algorithm is obtained by restricting
the (var) and (proj) rules as follows:  u:ht1 : : :  tni ` i(u):ti:

4.2. Aggressive Lifting

In order to avoid runtime construction of types, we restrict evidence ! as follows:! ::= ! 0j u j i(!)
11where ! 0 is a closed evidence that does not contain projection  i. A translation obtained with this restriction does not have to construct type parameters at runtime,since there is no evidence variable within h: : :i and !. However, the restricted deductive system does not provide the algorithm for the translation because it is notknown at the translation of let what open evidences are necessary to translate e 1 andthus what predicate  should be used for translation of e1. Thus, we will dene thedeterministic version of the deductive system that provides a translation algorithm.
The deterministic version of the deductive system is obtained by collecting necessary types during translation. The relation has the following form:  u ; `e h1  : : :  m i
e0  h1  : : :  m  : : :  m+k i , where u is the current evidence variable for obtaining type information. The predicates which u must satisfy are createdduring the translation of e. First we assume that u must hold the evidences for1  : : :  m . Then, the predicates necessary to translate e,  m+1 : : : m+k , are appended to the list. The rules of the translation are given below.
=0 ] is open.
x   1  : : :  n
x  n+1 (u)] 1 : : :  n =0 ] u ; x:80 : ) 2 ` f g h

i

fg
h
i
=0 ] is closed.  ` ! : =0 ]  ; x : 80 : )  ` xf g  xf g!]  0  u ; ` e  h 0i e0   u0 ; x:80 : )  ` e  0 e0  00
 u0 ; ` let x:80 : = 0:e in e  0
let x:80 : )  = 0 :u::e0 in e0  00
2

1

1

0

1

0

2

2

2

1

2

In case of the rst rule, since predicate = 0] is open, if we create the evidence
here, the runtime construction of the evidence is necessary. Instead, we add predicate
=0 ] to the list of the predicates and apply xf g to the projection of current
evidence variable u. However, since in the second rule = 0] is closed the evidence
to corresponding to it can be created statically. In the rule for let, expression e 1
is translated with h 0 i. That guarantees that the type information for every free
type variable can be obtained from u and tag-free garbage collection can be performedby using type information obtained from u.
The following lemma ensures that there is a deduction in the original systemcorresponding to a deduction of the algorithmic version of the deductive system.
Lemma 1 If  u ; ` e  e0  0, then  u:0 ; ` e e0.
Polytype 80 : )  in ) is called a translation of 80 : under  if F T V () 0 . This relation is naturally extended to type assignments.
Lemma 2 Let ;0 be a translation of ; under . If  ; ` e : 0 , then for all  there
exist e0 and 0 such that  u ;0 ` e  e0  0 .
12

It is clear from this lemma that for  ` e :  there exists a deduction of  u `e hi e0  hi. This ensures the existence of a translation for an arbitrary well-typed
closed program.

5. Identifying Evidences with Values
In this section, we propose a calculus which is more expressive for manipulation ofevidences and is more suitable for an intermediate language of a compiler. In calculus) , there are three kinds of abstractions and applications for types, evidences, andvalues. Abstractions and applications for types are completely ignored at runtime,
though enable type checking of programs. However, the latter two are implemented in
the similar way. Thus, by identifying the latter two we obtain the following calculus:
Monotypes  ::= b j t j  !  j T () j h1  : : :  ni
Predicate  ::=  j h1 : : :  ni
Polytypes  ::=  j 8:
Evidence! ::= b j E (e) j ! ! ! j i (! ) j h!1 : : :  !n i
Expressions e ::= c j x j x::e j e1 e2 j :e j ef1  : : :  n g j p jR(!) j he1  : : :  en i j i (e) j let x: = e1 in e2
where T () is the type for the evidences satisfying predicate , E (e) coerces expressions to evidences, and R(!) coerces evidences to expressions. Since evidences
are abstracted by usual we call this calculus ) . In order to illustrate advantages of ) over the previous calculus, the tuple of expressions he 1 : : :  eni and its
type h1  : : :  n i are included in the calculus. As the evidences may contain freevariables the judgments of the calculus has the following forms: ; ` ! :  evidence ! satises predicate  ; ` e :  expression e has type 
The rules to identify evidences with values are dened as follows: ; ` e : T () ; ` ! :  ; ` E (e) :   ; ` R(!) : T ()Other rules are analogous to those of ) .
This calculus is more expressive in manipulation of evidences (or type parameters).
For example, since type parameters can now be considered as values they can becomponents of tuples. Furthermore, it is possible to express a function that returns
a type parameter as bellow.
x:T (t):R(E (x)! E(x)) : T (t) ! T (t ! t)

This function takes the evidence corresponding to type t and returns the evidence
corresponding to t ! t. Optimization such as uncurrying abstractions for a type13

parameter and a value is formulated more simply than in the previous calculus. Thus,
we think that this calculus is more suitable for an intermediate language of a compiler.
Now we consider the representation of closures in both calculi. Since evidences
are distinguished from usual values in  ) , an evidence cannot be a component ofa usual record. Thus, the evidence and value environments of a closure cannot bemerged into a single environment. For example, the closure of x:t:y for y = 1 andt = int is represented in  ) as follows:h(t:u:t: y:t: x:t:y)fintg int 1i

In order to keep uniform representation for closures we cannot eliminate the evidence
abstraction in the code and evidence component of a closure even if there are no freeevidence variables. Thus the closure of x:int:x + y for y = 1 is represented as follows:hu:h i: y:int: x:int:x + y h i 1iwhere the evidence environment is empty h i. Furthermore, we need a special con-structor for closures since it has an evidence as a component.
However, in ) an evidence can be a component of a record of expressions. Hence,the evidence and value environments can be merged into a single environment. The
closures of x:t:y and x:int:x + y are represented as follows:h(t: z:hT (t)  ti: x:t: (z))fintg hR(int) 1ii
h y:int: x:int:x + y 1i
2

As we see in the example above, this representation saves space for empty evidence
environments in closures.
Even if we use ) , we need a special constructor for closures to hide the typeof the environment of a closure. However, as described in 16], we can represent a
closure of ) by a standard tuple and a package expression of existential types. A
closure of type 1 ! 2 can be represented as a value of type 9t:(t !  1 ! 2 )  t
where t is the type of the environment.

6. Implementation
An experimental compiler is implemented as a translator from Core SML to C byusing Kit Compiler as front end. An executable program produced by the compiler
uses type parameters for tag-free garbage collection and non-parametric operations
such as polymorphic equality.
The compiler is organized as in Figure 4. The Kit Compiler translates Core SML
to the explicitly typed intermediate language Lambda that is similar to 8 . We havedesigned another intermediate language called IL. It is based on calculus ) proposed
14

Core SML#
Lambda
#
IL
#
IL
#
IL
#
IL
#
IL
#

Kit Compiler
A-normalize
Optimization
Type lifting
Record attening, Uncurrying
Closure conversion

Translation to CC
Figure 4: The organization of the compiler
in this paper and on A-normal forms 5, 25]. Since 8 can be considered as a subset of) , IL is used not only after type lifting but before type lifting. Then, all the stages
except the last translation to C are implemented as type-preserving translations.
The type-checker for IL is implemented so that the intermediate code producedby each translation can be type-checked during debugging of the compiler. Typechecking of intermediate code has greatly helped development of our compiler.
We implemented the type lifting translation so that Tolmach's and aggressive
lifting can be chosen when we compile a program. Evidences (or runtime type parameters) are implemented by the data structures similar to Tolmach's. For aggressive
lifting, the representation of evidences is simplied because only projections of evidences are necessary at runtime. Type parameters are passed to functions as usual
C arguments.
Uncurrying optimization is performed after type lifting to eliminate the abstractions and applications introduced by type lifting if possible. Closures are represented
by a special constructor as the abstract closures described in 16]. However, closures
do not consists of code, type environment, and value environment but just code andenvironment as described in Section 5.
The polymorphic equality function of SML is implemented as C function whichuses runtime type information. In Tolmach's representation, the function must perform computation corresponding to reductions of projections of evidences. However,for aggressive lifting the type arguments to the polymorphic equality function are
also lifted and then such reductions are not necessary at all. That simplies the implementation of polymorphic equality in aggressive lifting and makes the use of type15

information in aggressive lifting cheaper than in Tolmach's as described in the next
section.

7. Measurements
We measured the cost of passing and using type parameters in aggressive andTolmach's lifting. In general, when a type parameter corresponding to an open typeis passed, Tolmach's lifting constructs a new type environment and allocates 2 words
and aggressive lifting has to perform a projection on a type parameter. We rst
compared the cost of these operations.
Function repair in Section 2.2 allocates 4 words for usual pairs. Thus, if wecompile this program by instantiating pair and repair to monomorphic functions,this program consumes 4 words for usual data structures for pairs. This is same foraggressive lifting. However, Tolmach's lifting allocates 2 words for type parameters
and thus allocates 1.5 times memory in the whole. An even worse situation for
Tolmach's lifting is the following program.

let proj = t1 t2 . x:t1 t2 .1 (x)pair-proj = s. y:s. proj s,sinpair-proj int n
end

f g

f g (y,y)Record attening optimization of our compiler converts the function proj from thefunction that takes a pair into the function with two arguments. So if we compile
this program by instantiating proj and pair-proj to monomorphic functions or
aggressive lifting, this program allocates no words. However, the executable program
compiled by Tolmach's lifting allocates 2 words for each call of pair-proj. So, evenif we considered heap allocation of programs asymptotically, the program compiled
by Tolmach's lifting may show unexpected behaviour.
Execution time of these programs are shown in Figure 5. The column Mono shows
the results when the programs are compiled by instantiating polymorphic functions
to monomorphic functions. The numbers in the parentheses are the ratio to the casesof aggressive lifting. It shows that aggressive lifting is more than 15 % faster thanTolmach's. If we compare aggressive lifting to the monomorphic cases, we cannot see
any signicant dierence in performance.
In order to measure the cost using type information, we measured the execution
time of programs using the polymorphic equality function. In Tolmach's representation, the computation corresponding normalizing type parameters must be performed
because of lazy reduction of types. The test programs polyeq1 and polyeq2 repeatedly applies polymorphic equality to integers, polyeq2pair to pairs of integers. Before calling polymorphic equality, there are one nested call of polymorphic function
16

repairpair-proj
polyeq1
polyeq2
polyeq2pair

Aggressive
TolmachMono
10.40 12.33 (1.19) 10.36 (1.00)
5.31 7.70 (1.45) 5.30 (1.00)
6.43 9.23 (1.44)
6.43 10.91 (1.70)
16.53 21.85 (1.32)-

Figure 5: Basic benchmarks: execution time excluding garbage collection time (sec)in polyeq1 and two netsted calls in polyeq2 and polyeq2pair. The results are also
shown in Figure 5. In both cases aggressive lifting is faster than Tolmach's. In caseof aggressive lifting, the type argument to the polymorphic equality is identical forpolyeq1 and polyeq2 and their execution time are almost the same. On the other
hand, if compiled by Tolmach's lifting, there are one more nesting of type environment in case of polyeq2 and the dierence in Tolmach's and our representation inpolyeq2 is bigger than that of polyeq1. However, since checking equality is much
expensive for polyeq2pair, the relative dierence of the two is smaller.
We measured the allocation and execution time of standard benchmarks for bothaggressive and Tolmach's lifting. The rusults are shown in Figure 6. The resultsfor SML/NJ 0.93 are also shown to show the excutable programs are fast enough toconsider the eect of the strategies of type lifting. a
The excutable programs compiled by aggressive lifting are always faster than thoseby Tolmach's except for mandelbrot, which is compiled to a completely monomporhic
program. The biggest dierence about 10 % in execution time is seen for life. As
reported in 21], life spends almost all the execution time for polymorphic equality.
(We did not implement minimal typing 3].) Thus, the dierence comes from thetime spent for polymorphic equality. This seems also true for boyer since there is nodierence in allocation.
As for allocation the dierences between Tolmach's and aggressive lifting are minimal except for simple. For simple, the executable program compiled by Tolmach's
lifting allocates 35 % more memory. This seems to happen because most polymorphic
functions are inlined in the other programs. Thus, much bigger dierence might beseen when we consider separate compilation.

8. Conclusion
We have proposed several calculi for explicit type passing that enable us to formalize compilation of polymorphic programming languages like ML as phases of typea It is not fair to compare allocation of excutable programs of our compiler to that of SML/NJ

because ours uses stack for frames of functions, but SML/NJ uses heap.

17

life
knuth-bendix
simpleboyer
mandelbrot

Aggressive
Tolmach's
SML/NJ 0.93
Time Allocation
Time Allocation Time Allocation
7.78
3.79 8.55 (1.10) 3.92 (1.03) 12.04
39.63
8.63
16.78 8.82 (1.02) 16.81 (1.00) 11.72
62.88
21.75
20.43 22.71 (1.04) 27.61 (1.35) 31.45
153.85
2.48
3.42 2.58 (1.04) 3.42 (1.00) 1.70
9.52
7.83
0.00 7.82 (1.00) 0.00 (1.00) 10.65
46.48

Figure 6: Results for standard benchmarks: time is the execution time (sec) excluding
garbage collection time and allocation is in M words.
preserving translations. Furthermore, we have formulated a translation from thesource language to the proposed calculus as a non-deterministic deductive systemand proved its correctness. The translation algorithm that avoids runtime construction of type parameters has been given as a special case of the deductive system.
Based on the calculus, we have designed an intermediate language and implemented a compiler of Core Standard ML. The results for simple benchmarks show
programs compiled by aggressive type lifting are more than 15 % faster at execution
time than those compiled by Tolmach's. For standard benchmarks, the advantage ismuch smaller in general. This seems to happen because most polymorphic functions
are inlined. Thus, we would like to extend our compiler to separate compilation andstudy various strategies of type passing in presence of separate compilation.

Acknowledgements
Some of the ideas presented in this paper were developed while the author was
visiting Carnegie Mellon University. We would like to thank Robert Harper and Greg
Morrisett for many interesting discussions on the subject of this paper. Irek Ulidowski
and the anonymous referees provided helpful comments to improve this paper.

References
1] Andrew W. Appel. Compiling with Continuation. Cambridge University Press,
1992.
2] Lars Birkedal, Nick Rothwell, Madds Tofte, and David N. Turner. The ML Kit
Version 1, 1993.
3] Nikolaj Skallerud Bjorner. Minimal typing derivations. In ACM SIGPLAN
Workshop on ML and its Application, 1994.
18

4] Ctherine Dubois and Pierre Weis. Generic polymorphism. In Proc. ACM Symp.
on Principles of Prog. Languages, 1995.
5] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The
essence of compiling with continuations. In Proc. ACM SIGPLAN Conf. on
Programming Language Design and Implementation, 1993.
6] H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium '75. North-Holland, 1975.
7] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-ordermodules. In Proc. ACM Symp. on Principles of Prog. Languages, pages 123{137,1994.
8] Robert Harper and John C. Mitchell. On the type structure of standard ML.
ACM Transaction on Programming Languages and Systems, 15(2), 1993.
9] Robert Harper and Greg Morrisett. Compiling polymorphism using intensional
type analysis. In Proc. ACM Symp. on Principles of Prog. Languages, pages
130{141, 1995.
10] Fritz Henglein and Jesper Jorgensen. Formally optimal boxing. In Proc. ACM
Symp. on Principles of Prog. Languages, 1994.
11] Mark P. Jones. A theory of qualied types. In ESOP '92: European Symposiumon Programming, LNCS 582, 1992.
12] Mark P. Jones. ML typing, explicit polymorphism and qualied types. In TACS
'94: Conference on theoretical aspects of computer software, LNCS 789, 1994.
13] Xavier Leroy. Unboxed objects and polymorphic typing. In Proc. ACM Symp.
on Principles of Prog. Languages, 1992.
14] Xavier Leroy. Manifest types, modules, and separate compilation. In Proc. ACM
Symp. on Principles of Prog. Languages, pages 109{122, 1994.
15] Robin Milner, Mads Tafte, and Robert Harper. The Denition of Standard ML.
MIT Press, 1990.
16] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Proc. ACM Symp. on Principles of Prog. Languages, 1996.
17] R. Morrison, A. Dearle, R.C.H. Connor, and A. L. Brown. An ad hoc approachto the implementation of polymorphism. ACM Transaction on Programming
Languages and Systems, 13(3), 1991.
19

18] Atsuhi Ohori. A compilation method for ML-style polymorphic record calculi.
In Proc. ACM Symp. on Principles of Prog. Languages, 1992.
19] Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transaction on Programming Languages and Systems, 17(6), 1995.
20] Gordon D. Plotkin. Lambda-denability in the full type hierarchy. In To
H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism.
Academic Press, 1980.
21] Zhong Shao and Andrew W. Appel. A type-based compiler for Standard ML. In
Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, 1995.
22] R. Statman. Completeness, invariance, and lambda-denability. Journal of Symbolic Logic, 47:17{26, 1982.
23] R. Statman. Logical relations and the typed -calculus. Information and Control,
65, 1985.
24] W. W. Tait. Intensional interpretation of functionals of nite type. Journal of
Symbolic Logic, 32(2), 1967.
25] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P Lee. TIL: A
type-directed optimizing compiler for ML. In Proc. ACM SIGPLAN Conf. on
Programming Language Design and Implementation, 1996.
26] Andrew Tolmach. Tag-free garbage collection using explicit type parameters. In
Proc. ACM Conf. Lisp and Functional Programming, pages 1{11, 1994.
27] Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad
hoc. In Proc. ACM Symp. on Principles of Prog. Languages, 1989.
28] Andrew K. Wright. Polymorphism for imperative languages without imperative
types. Technical report, Rice University, 1993. TR93-200.

20