Selective Tail Call Elimination
Yasuhiko Minamide
Institute of Information Sciences and Electronics
University of Tsukuba
and
PRESTO, JSTminamide@is.tsukuba.ac.jp

Abstract. Tail calls are expected not to consume stack space in mostfunctional languages. However, there is no support for tail calls in someenvironments. Even in such environments, proper tail calls can be implemented with a technique called a trampoline. To reduce the overheadof trampolining while preserving stack space asymptotically we propose
selective tail call elimination based on an eﬀect system. The eﬀect system infers the number of successive tail calls generated by the executionof an expression, and trampolines are introduced only when they arenecessary.

1

Introduction

Tail calls are expected not to consume stack space in most functional languages.
Implementation of proper tail calls requires some support from a target environment, but some environments including C and Java Virtual Machine (JVM) [10]do not provide such support. Even in such environments, proper tail calls canbe implemented with a technique called a trampoline. However, the trampoline
technique is based on a non-standard calling convention and is considered to
introduce too much overhead. Thus, most compilers for such environments do
not adopt trampolining and abandon proper tail calls [2, 17, 3].
To solve this problem we selectively introduce trampolines based on an eﬀect
system. We consider a typed call-by-value language as a source language of
selective tail call elimination. Eﬀect systems were originally proposed to inferside-eﬀects of a program by Giﬀord and Lucassen [8, 11], and an extension wasapplied to estimate the execution time of a program [6, 15]. Our eﬀect system
infers the number of successive tail calls that can be generated by the executionof an expression. Based on eﬀects, functions are divided into two kinds: thosethat lead to a ﬁnite number of successive tail calls and those that may leadto an inﬁnite number of successive tail calls. Then, it is necessary to adopt
trampolines only for the latter kind. In this manner we can reduce the overheadof trampolining while preserving stack space asymptotically.
Our eﬀect system includes the rule of subtyping, and some applications may
call both kinds of functions. To support subtyping on functions and enable selective elimination of tail calls, we introduce a transformation that translates

a function into a record containing two functions supporting diﬀerent calling
conventions. We prove that the increase of stack space usage caused by thistransformation is bounded by a factor determined by the eﬀect system.
We have incorporated selective tail call elimination into the MLj compiler [2],which complies Standard ML into Java bytecodes. Results for benchmark programs show that our eﬀect system is strong enough to indicate that most functions are safe without tail call elimination. We show that there is little degradation of performance for most benchmark programs. We also measure impact oftail call elimination on stack space usage. It shows that general tail call elimination sometimes greatly reduces stack space usage.
This paper is organized as follows. In Section 2, we review the trampolining
transformation and clarify its problem. In Section 3, we introduce our selective
tail call elimination and prove its soundness. In Section 4, the eﬀect system isextended with a wider class of eﬀects. In Section 5 we outline eﬀect inference
for our eﬀect system. Section 6 shows some examples where our eﬀect systemshows that a function is unsafe without tail call elimination. In Section 7 we
describe our implementation and discuss the results of our experiments. Finally,
we review related work and present our conclusions.

2

Tail Call Elimination with Trampolines

In functional languages, loops are often expressed with tail calls and thus they
are expected not to consume stack space. Let us consider the following program
written in Standard ML. The application sum (x-1, a+x) in this program iscalled a tail call because there is nothing to do in the function sum after theapplication.
let fun sum (x, a) = if x = 0 then a else sum (x-1, a+x)insum (y, 0)
end
If the tail call is properly implemented, the program above requires only constant
stack space. On the other hand, if it is not properly implemented, it requires
stack space proportional to y. Loops are often expressed in this way in functional
languages and thus it is important to implement proper tail calls.
However, it is not straightforward to implement proper tail calls in environments without direct support of tail calls, such as in C and JVM. In suchenvironments it is possible to implement proper tail calls with a non-standard
calling convention called a trampoline [1]. We will explain the trampoline technique as a source-to-source transformation. The example above is transformed
into the following program.
datatype ’a ret = Thunk (unit -> ’a ret) | Val ’a
fun loop (Val x) = x

| loop (Thunk f) = loop (f ())
let fun sum (x, a) =if x=0 then Val a else Thunk (fn () => sum (x-1, a+x))
inloop (sum (y, 0))end
The tail call in the program is translated into the creation of a closure. Then theclosure is called from the loop.1 This technique was used in a Standard ML to
C compiler [18] and is also useful to implement various features of programming
languages [7]. However, it is clear that this technique introduces a lot of overhead.
Thus, most compilers into C and JVM do not adopt trampolining and abandon
proper tail calls.

3

Selective Tail Call Elimination

To reduce the overhead introduced by implementation of proper tail calls bytechniques such as trampolining, we propose selective elimination of tail callsthat preserves the asymptotic complexity of the stack space.
The basic idea is that if the number of successive tail calls generated bya function call is bounded by some constant, it is not necessary to adopt a
trampoline for the function. Let us consider the following program.
let fun f x = x
fun g x = f x
in
g 0
end
There are two tail calls in this program: f x and g 0. However, it is not necessary
to introduce a trampoline for this program. The execution of the function f leads
to no tail call and thus f x generates only one successive tail call. The function
g calls f at a tail-call position and thus the function call g 0 generates two
successive tail calls. Since the number of successive tail calls is bounded in thisprogram, it is safe to execute this program without tail call elimination.
On the other hand, in the following program the number of successive tailcalls that the application h y leads to cannot be bounded. Thus it is necessary
to introduce a trampoline for the program.
let fun h x = if x > 0 then h (x - 1) else 0
in
h y
end
1

The function loop should be implemented so as not to consume stack space.

If we can statically analyze the number of successive tail calls generated byexecution of each function, we can avoid introducing trampolines for functions
satisfying some safety condition and selectively eliminate tail calls with trampolines. In the next section we introduce an eﬀect system to eliminate tail calls
selectively.
3.1

Eﬀect System

We introduce sized eﬀects to check the number of successive tail calls generated
by the execution of an expression. The following are the eﬀects we consider.
ρ ::= ω | 0 | 1 | . . .
We consider an order relation ρ ≤ ρ between eﬀects: the usual order relation
between natural numbers and i ≤ ω for any natural number i. For a ﬁnite eﬀect
i, the eﬀect i+ is deﬁned as i+ = i + 1. Then we consider the following types
where a function type is annotated with an eﬀect.
τ ::= nat | τ →ρ τ
We include nat as a base type for natural numbers and we also use other basetypes in examples. The functions we discussed above have the following types.
f : int →1 int
g : int →2 int
h : int →ω int
Application of f at a tail-call position leads to one tail call. Since the applicationof g leads to a subsequent application of f, the type of g is annotated with 2.
On the other hand, the number of successive tail calls generated by h cannot bebounded. Thus its type is annotated with ω.
We consider the subtyping relation deﬁned by the following rules.
τ ≤τ

τ1 ≤ τ1 τ2 ≤ τ2 ρ ≤ ρτ1 →ρ τ2 ≤ τ1 →ρ τ2

We formalize our eﬀect system for the following language, where abstractions
and applications are annotated with eﬀects.
V ::= x | 0 | suc(V ) | fix x.λρ y.M
M ::= V | @ρ M M | case V of 0 ⇒ M, suc(x) ⇒ M
We will discuss how to annotate the language without eﬀect annotations in
Section 5. The values 0 and suc(V ) are of natural numbers. Judgments of theeﬀect system have the following forms:
EV :τ
E  M : τ !ρx:τ ∈EEx:τ

E  V : nat
E  suc(V ) : nat

E  0 : nat+

E, x : τ1 →i τ2 , y : τ1  M : τ2 ! ii+i+

E  fix x.λ y.M : τ1 →

τ2EV :τ
E  V : τ !0

E, x : τ1 →ω τ2 , y : τ1  M : τ2 ! ωE  fix x.λω y.M : τ1 →ω τ2

E  M1 : τ1 →ρ τ2 ! ρ1 E  M2 : τ1 ! ρ2
E  @ρ M1 M2 : τ2 ! ρE  M : τ  ! ρ ρ ≤ ρE  M : τ !ρτ ≤ τ

E  V : nat E  M1 : τ ! ρ E, x : nat  M2 : τ ! ρE  case V of 0 ⇒ M1 , suc(x) ⇒ M2 : τ ! ρ
Fig. 1. Type system

where ρ represents the maximum number of successive tail calls generated byevaluation of M . The rules of the eﬀect system are deﬁned in Figure 1. The rulesof abstraction and application are explained as follows.
– If the body of a function leads to i successive tail calls, application of thefunction at a tail-call position leads to i+ successive tail calls.
– If the body of a function has eﬀect ω, the function has eﬀect ω. Thatmeans successive tail calls generated by application of the function cannot
be bounded.
– The eﬀects of M1 and M2 are ignored in the rule of application because
they correspond to evaluation at non-tail-call positions. Thus, the eﬀect of
the application @ρ M1 M2 is determined only by the eﬀect annotation of thefunction type.
To discuss the soundness of selective tail elimination we introduce an operational semantics that proﬁles stack space and models evaluation with proper
implementation of tail calls. We deﬁne a big-step operational semantics with thefollowing judgments:
T M ↓i V
N M ↓i V
with the meanings that M is evaluated to V with i stack frames at a tail-callposition or a non-tail-call position, respectively. A whole program is considered
to be evaluated at a tail-call position. The rules are given in Figure 2 whereα M ↓n V means the rule holds both for α = N and α = T . At a tail-callposition, the evaluation of the body of a function requires no new stack frame.
Thus, the stack space required for evaluation of the application is max(l, m, n).
On the other hand, at a non-tail-call position, it requires a new stack frame: thestack space is max(l, m, n + 1). This semantics models stack space usage whena program is executed after compilation. Correspondence to a semantics thatmodels execution based on an interpreter is discussed in [12].

T V ↓0 V

N M1 ↓l fix x.λρ y.M0

N M2 ↓m V2

N V ↓0 V

T M0 [fix x.λρ y.M0 /x][V2 /y] ↓n V

T @ρM1 M2 ↓max(l,m,n) VN M1 ↓l fix x.λρ y.M0

N M2 ↓m V2



T M0 [fix x.λρ y.M0 /x][V2 /y] ↓n V

N @ρM1 M2 ↓max(l,m,n+1) Vα M1 ↓n V
α case 0 of 0 ⇒ M1 , suc(x) ⇒ M2 ↓n V
α M2 [V0 /x] ↓n V
α case suc(V0 ) of 0 ⇒ M1 , suc(x) ⇒ M2 ↓n V
Fig. 2. Operational semantics

With respect to the operational semantics, the soundness of the type systemin the usual sense is proved. However, the following lemma says nothing about
eﬀects inferred by the eﬀect system.
Lemma 1 (Soundness).
1. If ∅  M : τ !ρ and N M ↓m V then ∅  V : τ .
2. If ∅  M : τ !ρ and T M ↓m V then ∅  V : τ .
3.2

Transformation

We introduce a program transformation that selectively eliminates tail calls
based on eﬀect annotations. The idea is to eliminate tail calls of the form @ω M M
with trampolining and to adopt the standard calling convention for @i M M .2
However, implementation based on this idea is not so simple because τ1 →i τ2
can be considered as τ1 →ω τ2 by subtyping. Let us consider the following
program.
let fun f x = x
fun g x = if ... then x else g (x - 1)
in
(if ... then f else g) 0
end
The functions f and g have types int →1 int and int →ω int, respectively. It is notpossible to determine the kinds of functions that are called by the applicationin the body of the let-expression. Thus, it is not straightforward to compile theapplication in the body.
2

We assume that the standard calling convention does not support tail call elimination.

To solve this problem, we represents τ1 →i τ2 as a record that contains twofunctions: one for a trampoline and one for the standard calling convention. Then
subtyping on function types is translated into record (object) subtyping.
For the target language of the transformation we consider the following types.
σ ::= nat | σ → σ | σ →t σ | {fun : σ, tfun : σ} | {tfun : σ}There are two kinds of function types: σ → σ uses the standard calling convention
without proper tail calls, and σ →t σ uses the non-standard calling convention
with tail call elimination. There is no subtyping relation between σ1 → σ2 andσ1 →t σ2 . Two kinds of record types, {tfun : σ} and {fun : σ, tfun : σ}, areincluded to translate function types and we consider the following subtyping
relation between them.
{fun : σ1 , tfun : σ2 } ≤ {tfun : σ2 }Then our transformation translates function types into record types so thatthe subtyping relation is preserved. The translation of types |τ | is deﬁned asfollows:|τ1 →ω τ2 | = {tfun : |τ1 | →t |τ2 |}|τ1 →i τ2 | = {fun : |τ1 | → |τ2 |, tfun : |τ1 | →t |τ2 |}We therefore have the following translation of subtyping.
|τ1 →i τ2 | ≤ |τ1 →ω τ2 |This translation of subtyping is natural for compilation to Java bytecodes because JVM has subtyping on objects through inheritance of classes.
The syntax of the target language is deﬁned as follows. It includes two kindsof abstraction and application, and syntax for records and ﬁeld selection.
N ::= W | @N N | @t N N | N.fun | N.tfun | case W of 0 ⇒ N, suc(x) ⇒ N
W ::= x | 0 | suc(W ) | λx.N | λt x.N | fix x.{fun = W, tfun = W } |fix x.{tfun = W }The ﬁelds of a record expression are restricted to values: this restriction is suﬃcient for our transformation. The type system of the target language is standard
and does not include eﬀects. The deﬁnition of the type system is shown in Appendix A.
We deﬁne an operational semantics of the target language in the same manneras that of the source language: we deﬁne a big-step operational semantics withfollowing judgments.
T N ↓i W
N N ↓i W
The main rules are deﬁned as follows. It should be noted that tail calls are notproperly implemented for application @N1 N2 and thus the evaluation of thebody of the function requires a new stack frame: the stack space required is not
max(l, m, n), but max(l, m, n + 1).
N N1 ↓l λt x.N

N N2 ↓m W2

T N [W2 /x] ↓n W

T @t N1 N2 ↓max(l,m,n) W
N N1 ↓ λx.N N N2 ↓m W2 T N [W2 /x] ↓n Wl

T @N1 N2 ↓max(l,m,n+1) W
The other rules are shown in Appendix B.
The transformation of selective tail call elimination is deﬁned as follows:[[x]] = x[[0]] = 0[[suc(V )]] = suc([[V ]])[[fix x.λω y.M ]] = fix x.{tfun = λt y.[[M ]]}[[fix x.λi y.M ]] = fix x.{fun = λy.[[M ]], tfun = λt y.[[M ]]}[[@i M1 M2 ]] = @([[M1 ]].fun) [[M2 ]][[@ω M1 M2 ]] = @t ([[M1 ]].tfun) [[M2 ]][[case V of 0 ⇒ M1 , suc(x) ⇒ M2 ]] = case [[V ]] of 0 ⇒ [[M1 ]], suc(x) ⇒ [[M2 ]]We extend the translation of types to type environments as |E|(x) = |E(x)|.
Then the type correctness of this transformation is formulated as the following
lemma and proved by induction on the derivation of E  M : τ !ρ.
Lemma 2 (Type soundness). If E  M : τ !ρ then |E|  [[M ]] : |τ |.
To formalize the soundness of the transformation we introduce the following
notation: T M ↓≤k V if T M ↓k V for some k  ≤ k. The factor of increase of
stack space usage by selective tail call elimination is determined by the maximumof the eﬀect annotations in M , denoted by max(M ).
Theorem 1 (Soundness). Let C = max(M ) + 1.
1. If ∅  M : τ ! i and T M ↓k V then T [[M ]] ↓≤Ck+i [[V ]].
2. If ∅  M : τ ! ω and T M ↓k V then T [[M ]] ↓≤Ck+C−1 [[V ]].
3. If ∅  M : τ ! ρ and N M ↓k V then N [[M ]] ↓≤Ck [[V ]].
This theorem ensures that the stack space usage of a program is preserved asymptotically.
For example, @ω (fix f.λω x.@1 (fix g.λ1 y.y)x)0 and its translation are evaluated as follows:N @ω (fix f.λω x.@1 (fix g.λ1 y.y)x)0 ↓1 0
N @t (fix f.{tfun = λt x.@(fix g.{fun = λy.y, tfun = λt y.y}.fun)x}.tfun)0 ↓2 0This example corresponds to the worst case: k = 1 and C = 2. The proof of thetheorem appears in Appendix C.

4Extension of the Eﬀect SystemTh eﬀect system we have presented has one unnatural limitation: ω must always
be assigned to a function which calls a function with eﬀect ω at tail call position,even if the function is safe without tail call elimination. In this section, we extend
our eﬀect system to overcome this limitation by considering a wider class ofeﬀects.
We ﬁrst show an example where the limitation of our eﬀect system appears.
Let us consider the following program.
fun f x = f x
fun g x = f x
fun h (0,x) = g x| h (n,x) = h (n-1,x)
The function g is safe without tail call elimination: the stack space usage isincreased by 1 even if it is implemented with the standard calling convention.
However, in our eﬀect system the function is assigned the eﬀect ω to because it
calls the function f of the eﬀect ω at a tail call position.
We solve this limitation by extending the eﬀects in our type system into thefollowing form.
ρ ::= ω · i + j
where i and j are natural numbers. The intuition is that the function with eﬀect
ω · i + j such that j > 0 is safe without tail call elimination. We identiﬁes ω · i + 0
and ω · 0 +j with ω · i and j, respectively. The eﬀect ρ+ and the subeﬀect relationρ ≤ ρ are deﬁned as follows:+(ω · i + j) = ω · i + (j + 1)
ω · i + j ≤ ω · i + j iﬀ

i < i , or i = i and j ≤ j 

The typing rules of abstraction in the eﬀect system are extended as follows:+

E, x : τ1 →ρ τ2 , y : τ1  M : τ2 ! ρ++E  fix x.λρ y.M : τ1 →ρ τ2

E, x : τ1 →ω·i τ2 , y : τ1  M : τ2 ! ω · i
E  fix x.λω·i y.M : τ1 →ω·i τ2

Then we can assign the following types and thus g can be safely implemented
with the standard calling convention.
f : int →ω int
g : int →ω+1 int
h : int × int →ω·2 int
We also need to modify the transformation to implement selective tail callelimination. Since a function with eﬀect ω · i can be considered to have eﬀectω · i + 1 in this system, a function with eﬀect ω · i must support both calling
conventions. The transformation is modiﬁed as follows:[[fix x.λρ y.M ]] = fix x.{fun = λy.[[M ]], tfun = λt y.[[M ]]}[[@ω·i+j M1 M2 ]] = @([[M1 ]].fun) [[M2 ]][[@ω·i M1 M2 ]] = @t ([[M1 ]].tfun) [[M2 ]]where j > 0. The intuitive meaning of extended eﬀects can be explained withthis transformation.
– A tail call with eﬀect ω generates successive tail calls of @t and then successive tail calls of @. The successive tail calls of @ may be generated by
subeﬀect relation i ≤ ω.
– A tail call with eﬀect ω · i may repeat i times the pattern of tail calls for ω– A tail call with eﬀect ω · i + j may generate j successive tail calls of @ andthen generates tail calls of the pattern for ω · i.
The soundness theorem is extended in the following form. We write maxi (M )for the maximum j of ω · i + j appearing in M .
Theorem 2 (Soundness).
j−1
∞Let C = i=0 maxi (M ) + 1 and D(j) = i=0 maxi (M ).
1. If ∅  M : τ ! (ω · i + j) and T M ↓k V then T [[M ]] ↓≤Ck+D(i)+j [[V ]].
2. If ∅  M : τ ! ρ and N M ↓k V then N [[M ]] ↓≤Ck [[V ]].

5

Eﬀect Inference

We show how to infer eﬀects in this section. Th eﬀect inference can be formalized
as a type system with constraints, where a constraint generated by the typesystem is solved with a simple graph-based algorithm. We assume that types
are already inferred with the standard type inference and consider the following
explicitly-typed language for eﬀect inference.
τ ::= nat | τ →α τ
V ::= 0 | suc(V ) | x | fix x : τ.λy.M
M ::= V | @α M M | case V of 0 ⇒ M, suc(x) ⇒ M
where α denotes an eﬀect variable. The eﬀect annotation of a lambda abstraction
can be determined from the type annotation of the fix-expression. We assume
eﬀect variables appearing in a program are distinct.
Judgments of the eﬀect system have the following forms: E; C  V : τ andE; C  M : τ !α where C is a set of subeﬀect relations: α < α and α ≤ α . A
constraint α < α holds if α ≤ α and α = α , or α = α = ω · i for some i. The
main rules of the eﬀect system are given as follows:
E; C  V : τ α is fresh
E; C  V : τ !αE, x : τ1 →α τ2 , y : τ1 ; C  M : τ2 ! αE; C ∪ {α < α}  fix x : τ1 →α τ2 .λy.M : τ1 →α τ2

E; C1  M1 : τ1 →α τ2 ! α1 E; C2  M2 : τ1 ! α2
E; C1 ∪ C2 ∪ {α ≤ α} ∪ C≤ (τ1 , τ1 )  @α M1 M2 : τ2 ! α
where C≤(τ1 , τ1 ) is the constraint to obtain the subtyping τ1 ≤ τ1 .
C≤(nat, nat) = ∅αC≤(τ1 → τ2 , τ1 →α τ2 ) = C≤ (τ1 , τ1 ) ∪ C≤ (τ2 , τ2 ) ∪ {α ≤ α }The constraint obtained by the rules above can be solved in the following
manner. We consider the graph of the relations α < α and α ≤ α , and compute the strongly connected components of the graph. If a strongly connectedcomponent contains a relation of the form α < α , the eﬀect of the form ω · imust be assigned to the eﬀect variables appearing in the component. It is clearthat an eﬀect ω · i + j (j > 0) can be assigned to an eﬀect variable not belonging
to such components.

6

ExamplesThere are several situations where an eﬀect of the form ω · i is assigned to afunction. Although some of them are actually unsafe without tail call elimination, our eﬀect system sometimes assigns ω · i to functions safe without tail callelimination. In this section we show some examples of both the situations.
In our eﬀect system, ω · i must be assigned to tail recursive functions ingeneral. However, tail recursive calls in a single recursive function can be implemented as a loop and thus trampolining can be avoided for such tail calls. Oureﬀect system can be extended to be consistent with this implementation andthen such functions are not assigned ω · i to. Then there are two common examples where recursive functions are unsafe without tail call elimination: mutually
tail recursive functions and higher order recursive functions.
In the following example, the functions f and g contains mutually recursive
tail calls and thus must be assigned ω to.
fun f 0 = 0| f n = g (n-1)
and g n = f (n-1)
However, it is possible to implement the tail calls as a loop if only one of f andg are used from the other part of a program or the functions are copied into two
deﬁnitions.
The following is an example with a higher order function.
fun h 0 y = y| h x y = h (x-1) (x+y)
The function h has type int → int → int. The tail recursive call of h (x-1)(x+y) cannot be implemented as a loop. However, if the function is uncurried,the tail call in the function can be implemented as a loop and thus the function
can be safely implemented without tail call elimination.
As the third example, we show a program that is safe without tail call elimination, but is assigned ω to with our eﬀect system.
let fun f (g:int -> int) = g 0
in
f (fn x => f (fn y => y))end
You can check this program is safe without tail call elimination. Let us infer thetype of f. By assuming that f has type (int →α1 int) →α2 int, the constraints
α1 < α2 and α2 < α1 must be satisﬁed where the ﬁrst constraint is obtained
from the deﬁnition of f and the second constraint is obtained from the body ofthe let-expression. Then the eﬀects α1 and α2 must be ω · i for some i. Thisweakness of our eﬀect system appears in the benchmark “logic” we will discussin the next section: many functions similar to the function above appear in the
program.

7

Implementation and Measurements

We have incorporated our selective tail call elimination into the MLj compiler [2],which translates Standard ML into Java bytecodes. In MLj, tail calls are compiled into Java method invocations except recursive calls which are implemented
as loops. MLj uses an intermediate language based on monads to represent effects such as IO operations, exception, and non-termination. We extended theeﬀects of the intermediate language with our eﬀect. The eﬀects for selective tailcall elimination are inferred in a late stage of compilation and the transformationis merged into the code generation phase of the compiler.
The translation of a function presented in Section 3.2 and 4 has one problem:the body of λi x.M is copied into two functions and thus the translation may
increase the code size. This problem can be solved by the following translation.
λi y.M = let y = λx.[[M ]] in {fun = y, tfun = λt x.@yx}
However, we do not adopt this translation because it makes it diﬃcult to compare stack space usage. The worst case increase of code size observed for thebenchmark programs we will discuss later is about 35 %.3
We measured the eﬀectiveness of our selective tail call elimination for themost benchmark programs obtained from the following URL.4
ftp://ftp.research.bell-labs.com/dist/smlnj/benchmarks/
3

The pair representation is not used for the known function that are safe without tailcall elimination.
4
We excluded two programs count-graphs and mlyacc that are diﬃcult to compile
with MLj because of the limitation of MLj.

total (A) (B) (C) (D)barnes-hut

25

0

0

0

total (A) (B) (C) (D)2mandelbrot

6

0

0

0

1

boyer

24

0

0

0

2

nucleic

38

0

0

0

3

ﬀt

28

0

0

0

3

ratio-regions

51

0

0

0

2

knuth-bendix

83

5

5

5

3

ray

82

2

2

0

3

lexgen

110

13 11

2

3

simple

175

0

0

0

4

life

30

1

0

2

tsp

20

0

0

0

2

logic

58

51 36 36

2

vliw

463

19 18 16

4

1

Table 1. Results of eﬀect inference

MLj TCE STCE
knuth-bendix 3895 3373

3485

1259

94

life

298

49

49

logic

3814 236

260

lexgen94

Table 2. Maximum stack size: (in number of frames)

Table 1 summarizes the results of our eﬀect analysis. The column total shows
the number of the functions generated for each benchmark program. The columns(A), (B) and (C) are the numbers of functions the analysis assigns an eﬀect of
the form ω · i: (A), (B) and (C) are the numbers for selective tail call elimination
without extension, with extension and with extension
and an extra phase of
optimization, respectively. The column (D) shows ∞max(P) for each program
i=0
P , which determines the theoretical upper bound of increase of stack space usage.
– Eight programs out of 13 are shown safe without tail call elimination. Evenfor the other programs except for the program logic, the ratio of the functionof eﬀect ω · i is small.
– The most functions of the program logic have eﬀect ω · i by the reason we
described in Section 6. The extension reduces the number, but more thanhalf of the functions still have ω · i.
– Since the maximum of the numbers in column (D) is 4, the theoretical upperbound of stack space increase for selective tail call elimination compared totail call elimination is 5.
– The eﬀectiveness of our selective tail call elimination depends on other phasesof compilation. An extra phase of optimization including uncurrying decreased the number of functions of eﬀect ω · i for three programs.
Table 2 shows the maximum stack size during execution measured by the
number of frames. The table shows the results for the benchmark programs whereInterpreted-mode
MLj

TCE

STCE

HotSpot Client VM
MLj

TCE

STCE

barnes-hut

5.77

6.30(109.2) 5.83(101.0)

1.22

1.21(99.2) 1.23(100.8)

boyer

1.41

1.65(117.0) 1.41(100.0)

0.81

0.58(71.6) 0.82(101.2)

ﬀt

1.71

2.12(124.0) 1.71(100.0)

0.57 0.60(105.3) 0.64(112.3)

knuth-bendix

11.09

10.80(97.4)

2.00 2.12(106.0)

8.19(73.9)

1.61(80.5)

lexgen3.50

3.40(97.1)

3.49(99.7)

0.61 0.75(123.0) 0.63(103.3)

life

1.24

1.24(100.0)

1.15(92.7)

0.36 0.37(102.8)

0.35(97.2)

logic

17.40 18.90(108.6) 16.49(94.8)

4.51

2.70(59.9)

2.79(61.9)

mandelbrot

4.18

6.45(154.3) 4.22(101.0)

0.52 1.49(286.5) 0.55(105.8)

nucleic

0.68

0.73(107.4)

0.34 0.44(129.4) 0.34(100.0)

0.67(98.5)

ratio-regions 212.93 216.38(101.6) 209.11(98.2) 33.62 42.34(125.9) 33.67(100.1)
ray

5.77

6.20(107.5)

5.68(98.4)

1.88

1.13(60.1) 2.12(112.8)

simple6.61

7.35(111.2)

6.38(96.5)

1.49 1.63(109.4) 1.54(103.4)

tsp

4.78

5.13(107.3)

4.75(99.4)

0.88 0.96(109.1)

vliw

6.26

7.32(116.9) 6.42(102.6)

0.84(95.5)

1.34 2.37(176.9) 1.46(109.0)

Table 3. Execution time (in seconds)

tail call elimination has some impact on the results. For all the other program, thenumbers are between 33 and 103. The results supports that tail call elimination isdesirable: stack sizes are greatly reduced for several programs. Selective tail callelimination may increase stack size compared to tail call elimination. However,
the increase is relatively small, compared to the theoretical upper bound.
Table 3 shows execution times. The columns TCE and STCE are the results
for tail call elimination and selective tail call elimination, respectively. The numbers in the parenthesis are the ratios to those of MLj. Even for TCE, all the
non-tail-calls are implemented with the standard calling convention based on
the pair representation of functions. Measurements were done using Sun JDK
1.4.0, Java HotSpot Client VM on a Linux PC. We measured execution time on
the interpreted-mode with the -Xint option, and on the mode where HotSpot
compilation is enabled because it is sometimes diﬃcult to interpret results on
the HotSpot VM. Each benchmark was run ﬁve times and we chose the fastestrun.
– TCE sometimes degrades the performance a lot. The worst case overhead
is 54.3 % and 186.5 % for the interpreted-mode and the HotSpot VM, respectively. Compared to TCE, STCE causes little overhead: the worst caseoverhead is 2.6 % and 12.8 %, respectively.
– For benchmark programs where stack size is reduced by tail call elimination,
execution times are sometimes reduced for both TCE and STCE: knuthbendix and logic. This can be explained as a reduction of garbage collection

(GC) time. For example, the GC times for logic are 2.43, 0.49 and 0.49 for
MLj, TCE and STCE, respectively. The same phenomenon was observed by
Schinz and Odersky in their tail call elimination for JVM [16].
– There are unexpected results on boyer and ray: the big improvement ofexecution time over MLj and STCE is observed for TCE. We checked the
proﬁling data of executions and found that better decisions on compilation
are made by the HotSpot VM for TCE and the programs compiled by MLj
and STCE spent more time on interpreted methods.

8

Related Work

Dornic, Jouvelot and Giﬀord proposed an eﬀect system to estimate execution
time of a program [6], and their work was extended by Reistad and Giﬀord [15]with sized types [9]. By adapting the eﬀect system extended with sized types wemay obtain more information about the stack usage of a program. However, oursimple eﬀect system gives enough information for selective tail call elimination.
Implementation of proper tail calls and space safety are discussed by Clinger [5].
He considered that an implementation is safe with respect to space if it does notincrease the asymptotic space complexity of programs. Our selective tail callelimination satisﬁes the criterion on stack space, but the factor of increase of
stack space depends on the program and is determined by the eﬀect system.
Schinz and Odersky proposed tail call elimination for the Java virtual machine [16] that preserves complexity on stack space. Their method is dynamic:
it keeps track of the number of successive tail calls and execution is returned toa trampoline if some predeﬁned limit is exceeded. We think that it is possible
to reduce the overhead of their method with selective elimination of tail calls.
We have translated a function in the source language into a record with twofunctions supporting diﬀerent calling conventions. Similar translation was used
to support multiple calling conventions in type-directed unboxing by Minamide
and Garrigue [14], and the vectorized functions of Chakravarty and Keller [4].

9Conclusion and Future Work

We have presented an eﬀect system and a program transformation to eliminate
tail calls selectively. The transformation translates a function into a record with
two functions supporting diﬀerent calling conventions. The transformation preserves stack space asymptotically.
Our eﬀect system will be useful even for target environments that directly
supports tail calls. Various program transformations sometimes translate tailcalls into non-tail calls. With our eﬀect system, it is possible to check if suchtranslation is safe for each tail call.
We incorporated our eﬀect system into the MLj compiler and measured the
proportion of functions that are unsafe without tail call elimination. The results
indicated that selective tail call elimination is very eﬀective for most programs
and most functions can be implemented with the standard calling convention.

However, there is a limitation that our eﬀect system is monovariant. This limitation may be solved if we extend our eﬀect system with eﬀect polymorphism
or intersection types.
By selective tail call elimination, the asymptotic complexity of stack space
is preserved. The factor of the increase is determined by eﬀect analysis anddepends on a program. However, it is also possible to guarantee the factor of
stack space increase by translating applications with annotations greater thanthe predeﬁned factor as applications with annotation ω.

Acknowledgments
This work is partially supported by Grant-in-Aid for Encouragement of Young
Scientists, No. 13780193.

References
1. H. Baker. Cons should not cons its arguments, part II: Cheney on the M.T.A.
SIGPLAN Notices, 30(9):17–20, 1995.
2. N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In Proceedings of the Third ACM SIGPLAN International Conference on
Functional Programming (ICFP ’98), pages 129–140, 1998.
3. P. Bothner. Kawa - compiling dynamic languages to the Java VM. In Proceedingsof the USENIX 1998 Technical Conference, 1998.
4. M. M. T. Chakravarty and G. Keller. More types for nested data parallel programming. In Proceedings of the Fifth ACM SIGPLAN International Conference
on Functional Programming, pages 94–105, 1999.
5. W. D. Clinger. Proper tail recursion and space eﬃciency. In Proceedings of the
ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation, pages 174–185. ACM Press, 1998.
6. V. Dornic, P. Jouvelot, and D. K. Giﬀord. Polymorphic time systems for estimating program complexity. ACM Letters on Programming Languages and Systems(LOPLAS), 1(1):33–45, 1992.
7. S. D. Ganz, D. P. Friedman, and M. Wand. Trampolined style. In Proceedingsof the 4th ACM SIGPLAN International Conference on Functional Programming(ICFP ’99), pages 18–22, 1999.
8. D. K. Giﬀord and J. M. Lucassen. Integrating functional and imperative programming. In Proceedings of the ACM Conference on Lisp and Functional Programming,
pages 28–38, 1986.
9. J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems.
In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, pages 410–423, 1996.
10. T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison
Wesley, 1999.
11. J. M. Lucassen and D. K. Giﬀord. Polymorphic eﬀect systems. In Proceedings ofthe Fifteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages, pages 47–57, 1988.

12. Y. Minamide. A new criterion for safe program transformations. In Proceedingsof the Forth International Workshop on Higher Order Operational Techniques in
Semantics (HOOTS), volume 41(3) of ENTCS, Montreal, 2000.
13. Y. Minamide. Selective tail call elimination. Technical Report ISE-TR-03-192,
Institute of Information Sciences and Electronics, University of Tsukuba, 2003.
14. Y. Minamide and J. Garrigue. On the runtime complexity of type-directed unboxing. In Proceedings of the Third ACM SIGPLAN International conference on
Functional Programming, pages 1–12, 1998.
15. B. Reistad and D. K. Giﬀord. Static dependent costs for estimating execution time.
In Proceedings of the 1994 ACM Conference on LISP and Functional Programming,
pages 65–78, 1994.
16. M. Schinz and M. Odersky. Tail call elimination on the Java virtual machine. In
Proceedings of the First International Workshop on Multi-Language Infrastructure
and Interoperability (BABEL), volume 59(1) of ENTCS, 2001.
17. B. Serpette and M. Serrano. Compiling Scheme to JVM bytecode: a performance
study. In Proceedings of the Seventh ACM SIGPLAN International Conference on
Functional Programming, pages 259–270, 2002.
18. D. Tarditi, A. Acharya, and P. Lee. No assembly required: Compiling standard ML
to C. ACM Letters on Programming Languages and Systems (LOPLAS), 1(2):161–
177, 1992.

A

Type System of the Target Language

The type system of the target language is deﬁned as a deductive system with
judgments of the form E  N : σ. We do not show the rules for 0, suc(W ), andcase-expressions that are the same as those for the source language.
x:σ∈E
Ex:σ
E, x : σ1  N : σ2E  λx.N : σ1 → σ2
E  N1 : σ1 → σ2 E  N2 : σ1
E  @N1 N2 : σ2

E  N : σ σ ≤ σEN :σE, x : σ1  N : σ2E  λt x.N : σ1 →t σ2
E  N1 : σ1 →t σ2 E  N2 : σ1
E  @t N1 N2 : σ2

E, x : {fun : σ1 , tfun : σ2 }  W1 : σ1 E, x : {fun : σ1 , tfun : σ2 }  W2 : σ2
E  fix x.{fun = W1 , tfun = W2 } : {fun : σ1 , tfun : σ2 }E, x : {tfun : σ}  W : σ
E  fix x.{tfun = W } : {tfun : σ}E  N : {fun : σ1 , tfun : σ2 } E  N : {tfun : σ}E  N.fun : σ1
E  N.tfun : σBOperational Semantics of the Target Language

The following are the rules of the operational semantics of the target language.
We write α N ↓n W if the rule holds for both N N ↓n W and T N ↓n W .
N N1 ↓l λx.N

N N2 ↓m W2

α N [W2 /x] ↓n W

α @N1 N2 ↓max(l,m,n+1) W
α W ↓0 W

N N ↓n fix x.{tfun = W }α N.tfun ↓n W [fix x.{tfun = W }/x]

N N ↓n fix x.{fun = W1 , tfun = W2 }
α N.tfun ↓n W2 [fix x.{fun = W1 , tfun = W2 }/x]
N N ↓n fix x.{fun = W1 , tfun = W2 }
α N.fun ↓n W1 [fix x.{fun = W1 , tfun = W2 }/x]C

Proof of Soundness

The following lemma is crucial to establish soundness of transformation.
Lemma 3. [[M [V /x]]] ≡ [[M ]][[[V ]]/x].
We prove the main theorem in the following form to simplify case-analysis.
Lemma 4. Let C = max(M ) + 1.
1. If ∅  M : τ ! ρ and T M ↓k V then T [[M ]] ↓≤Ck+D(ρ) [[V ]].
2. If ∅  M : τ ! ρ and N M ↓k V then N [[M ]] ↓≤Ck [[V ]].
where D(ρ) is a function such that D(i) = i and D(ω) = max(M ).
Proof. By mutual induction on the derivations of T M ↓k V and N M ↓k V .
Due to lack of space, we show only one case of application for the property 1.
The details of the proof can be found in the technical report [13].
Case: T @i M1 M2 ↓k V is derived from N M1 ↓l V1 and N M2 ↓m V2 and+T M [V1 /x][V2 /y] ↓n V where V1 ≡ fix x.λj y.M and k = max(l, m, n).
From the deﬁnition of the type system, j < i. From ∅  @i M1 M2 : τ !ρ,+i ≤ ρ. We also have x : τ  →j τ, y : τ   M : τ !j.
By the induction hypothesis, N [[M1 ]] ↓≤Cl [[V1 ]] and N [[M2 ]] ↓≤Cm [[V2 ]].
From ∅  M [V1 /x][V2/y] : τ !j, by the induction hypothesis,
T [[M ]][[[V1]]/x][[[V2]]/y] ↓≤Cn+j [[V ]]This case is proved by the following derivation.
N [[M1 ]].fun ↓≤Cl λy.[[M ]][[[V1]]/x] N [[M2 ]] ↓≤Cm [[V2 ]]T [[M ]][[[V1]]/x][[[V2]]/y] ↓≤Cn+j [[V ]]T @([[M1 ]].fun)[[M2 ]] ↓≤max(Cl,Cm,Cn+j+1) [[V ]]where max(Cl, Cm, Cn + j + 1) ≤ Ck + D(ρ).