A Functional Representation of Data Structures with a Hole
Yasuhiko Minamide
Research Institute for Mathematical Sciences
Kyoto University
Kyoto 606-01, JAPANnan@kurims.kyoto-u.ac.jp

Abstract
Data structures with a hole, in other words data structures with anuninitialized field, are useful to write efficient programs: they enable us to construct functional data structures flexibly and write
functions such as append and map as tail recursive functions. In
this paper we present an approach to introducing data structureswith a hole into call-by-value functional programming languages
like ML. Data structures with a hole are formalized as a new formof λ-abstraction called hole abstraction. The novel features of holeabstraction are that expressions inside hole abstraction are evaluated and application is implemented by destructive update of a hole.
We present a simply typed call-by-value λ-calculus extended withhole abstractions. Then we show a compilation method of hole abstraction and prove correctness of the compilation.

1

Introduction

Functional data types such as list are distinguished from imperative
data types such as ref and array in ML, and no destructive operation
is provided for functional data types. This distinction ensures that
there is no side effect for functional data types in ML and makes understanding of ML programs easier. However, the way functional
data structures are built is very restrictive: they can be built onlyin the bottom-up manner. This limitation often prevents us fromwriting efficient programs.
In order to construct functional data structures more flexibly wewill introduce data structures with a hole into call-by-value functional languages like ML. By data structures with a hole we meandata structures with an uninitialized field such as a cons cell whose
tail is not yet given. Data structures with a hole enable us to build
functional data structures more flexibly: functional data structures
can be built in the top-down manner. For example, a list can bebuilt from the head to the tail.
Theoretically, data structures with a hole can be represented
by usual λ-abstraction: for example, λx.cons(1, x) can be considered as a cons cell whose tail is a hole. However, this does
not have the intended operational behaviour in call-by-value functional programming languages. It is because an expression inside
λ-abstraction is not evaluated and thus the data structure is not constructed at the time of the evaluation of abstraction, but at the timeof the evaluation of application.
Thus in order to represent data structures with a hole we introduce a new form of λ-abstraction λ̂x.M called hole abstraction.
A hole abstraction is evaluated to a pair of a data structure and thepointer to its hole at runtime. The application of a hole abstraction
fills its hole destructively. In order to create a data structure at thetime of the evaluation of hole abstraction, an expression inside λ̂abstraction is evaluated. This implementation of hole abstraction
imposes several restrictions on the usage of hole abstraction.
In order to formalize the idea of hole abstractions, we propose a
simply typed call-by-value λ-calculus extended with hole abstractions. The type system of the calculus is designed so that the implementation of hole abstraction and application introduces no side
effect and preserves desirable properties of the simply typed callby-value λ-calculus. We hide side effects by restricting the use ofhole abstraction to the single-threaded manner [6]. The restriction
is imposed by considering the types of hole abstractions as linear
types [21, 22, 16]. Then we give the operational semantics of thecalculus and prove the soundness of the type system.
By using hole abstractions we have more flexibility on construction of functional data structures than in the conventional callby-value functional languages. This enables us to apply some programming techniques used for imperative data types to functional
data types. The most significant application is to implement functions such as append and map as tail recursive functions. Furthermore, this tail recursive implementation can be considered ascontinuation-passing style transformation of the standard implementation of these functions: continuations for recursive calls are
represented by hole abstractions.
The next step is to establish a compilation method of hole abstractions. We propose a compilation method which can be incorporated into standard compilers with only minimal changes. It isbased on a transformation that converts a general hole abstraction
into a composition of primitive hole abstractions. After this transformation we need only the evaluation of primitive hole abstractions and do not require the evaluation of an expression inside holeabstraction. Thus programs can be compiled by a standard compilation method after the transformation. For this transformation, we
prove the correctness by the method of logical relations.
We incorporated some ideas of hole abstractions into an experimental ML compiler developed by the author. The results ofpreliminary benchmarks show about 15 - 40% improvement in execution time.
The rest of this paper is organized as follows. In Section 2 weintroduce hole abstraction informally and show how to use hole abstraction to write efficient programs, especially tail recursive functions. In Section 3 we present a simply typed call-by-value λcalculus extended with hole abstractions and prove the soundness

X

Y

p

happ(X,V)qhcomp(X,Y)

q

V

Figure 1: Application and Composition of Hole Abstractionsof the calculus. Then we show a compilation method of hole abstractions in Section 4. In Section 5 we discuss implementation andshow how much improvement we can obtain by using hole abstractions. We discuss related work in Section 6, and suggest directions
for future work in Section 7.

2

Data Structures with a HoleIn the λ-calculus data structures with a hole can be represented by
λ-abstraction. For example, λx.cons(1, x) can be considered asa cons cell whose tail is a hole. In this representation, the operation for filling the hole can be done by application: for example,(λx.cons(1, x)) nil fills the hole with nil.
However, this does not have the intended operational behaviourin call-by-value functional programming languages. It is because
an expression inside λ-abstraction is not evaluated. Thus a data
structure with a hole is not constructed at the time of the evaluation of λ-abstraction, but at the time of the evaluation of application. Furthermore, it is not a desirable representation for efficiency
because creation and application of a closure are not inexpensive
operations.
Thus in order to represent data structures with a hole we introduce a new form of λ-abstraction λ̂x.M called hole abstraction.
We also sometimes consider hole abstractions as a class of functions and say hole functions. For example, the previous example isrepresented by λ̂x.cons(1, x). For hole abstractions, we give type(τ1 , τ2 ) hfun where τ1 is the type of a hole and τ2 is the type of a
resulting data structure.
For efficient implementation of hole abstractions, at run timehole abstractions are represented by a pair of pointers to a data
structure and its hole as shown in Figure 1: X and Y are holeabstractions where data structures are represented by triangles, andp and q are the pointers to the holes.
The primitives for hole abstractions are illustrated in Figure 1. The primitive happ destructively fills the hole and corresponds to function applications as we saw before. The primitive hcomp fills the hole of the first argument with another data
structure with a hole and corresponds to function compositionsof the λ-calculus. It is because in the λ-calculus the composition of λ̂x.M and λ̂y.N can be reduced to λ̂y.M [N/x] which
represents the composed data structure with a hole. For example, hcomp(λ̂x.cons(1, x), λ̂y.cons(2, y)) should be evaluated toλ̂y.cons(1, x)[cons(2, y)/x] ≡ λ̂y.cons(1, cons(2, y)).
In this representation, the identity hole abstraction, λ̂x.x, cannot be treated because its body does not construct any data structure, but it is just a hole. However, the identity hole abstraction

is useful to write programs as we see later in examples. Thus we
represent the identity hole abstraction, λ̂x.x, by a pair of special
values which can be distinguished from other hole abstractions. 1
This implementation of hole abstractions and primitives forthem imposes several restrictions on the usage of hole abstractions.
First, the destructive implementation of happ and hcomp mustbe hidden so that no side effect can be seen. This is solved by
restricting operations on hole abstractions to the single-threadedmanner as proposed for introducing imperative operations in purefunctional languages [6, 21]. We impose single-threadedness byconsidering (τ1 , τ2 ) hfun as linear types. This makes efficient implementation through destructive update possible without introducing side effects.
Secondly, an expression inside λ̂-abstraction must be restricted
so that the expression can be evaluated to a data structure without using the value of a variable introduced by λ̂-abstraction. If
we impose no restriction on an expression inside λ̂-abstraction, we
cannot obtain a data structure as a result of the evaluation of theexpression. Let us consider the following program:
λ̂x.case x of nil ⇒ 0 | cons(y, z) ⇒ 1
In this program, x is used in the test of case-expression. However,the value of x is not yet determined at the time of the evaluation.
Thus we cannot evaluate this expression to a data structure. We also
prohibit application and λ-abstraction containing free variables introduced by hole abstractions. For example, expressions λ̂x.yx andλ̂x.λy.x are not permitted. This restriction is necessary for our implementation strategy.
Thirdly, hole abstractions must contain exactly one hole. It
is because a hole abstraction is implemented as a pair of pointers to a data structure and a single hole. Thus a data structurewith no hole or multiple holes cannot be represented. For example, the following programs are not permitted: λ̂x.nil andλ̂x.cons(x, cons(x, nil)).

2.1 Using Hole Abstractions
In this section we will explain how to use hole abstractions to improve programs. For example programs we use the syntax of Standard ML and hfn x => M instead of λ̂x.M .
By using hole abstractions we can build functional data structures more flexibly than in the conventional call-by-value functional languages. Functional data structures can be built in the topdown manner. For example, the following program creates a list
containing 1 and 2 from the head.
let val y1 = hfn x => 1::x
val y2 = hcomp (y1, hfn x => 2::x)inhapp (y2, nil)endThis example starts to create the list from a cons cell where its headis 1 and its tail is a hole. Another way is to create a list from theidentity hole abstraction as follows:
let val y0 = hfn x => x
val y1 = hcomp (y0, hfn x => 1::x)
val y2 = hcomp (y1, hfn x => 2::x)inhapp (y2, nil)end
1
By including the identity hole abstraction, the implementation of happ and hcomp
must check whether arguments are the identity hole abstraction.

fun append ([],ys) = ys
| append (x::xs,ys) = x :: append (xs, ys)
fun hfun_append (xs, ys) =let fun append_rec ([], k) = happ (k, ys)| append_rec (x::xs, k) = append_rec (xs, hcomp (k, hfn z => x::z))inappend_rec (xs, hfn x => x)
end
fun flatten [] = []| flatten (x::xs) = append (x, flatten xs)
fun append’ (k, []) = k| append’ (k, x::xs) = append’ (hcomp (k, hfn y => x::y), xs)
fun hfun_flatten xs =let fun flatten_rec (k, []) = happ (k, [])| flatten_rec (k, x::xs) = flatten_rec (append’ (k, x), xs)
inflatten_rec (hfn x => x, xs)
end
Figure 2: Using Hole Abstractions for Lists

This kind of the usage of the identity hole abstraction is often usefulto write programs as we see later.
By using data structures with a hole we can write functions
which usually need to construct a data structure by using the return
value of a recursive call as tail recursive functions.
Let us consider the function append in Figure 2. This function is not tail recursive because consing must be performed after the recursive call of append. By using hole abstractions thesame function can be implemented as the tail recursive function
hfun_append in Figure 2. For the argument k of append_rec, we
use hole abstractions representing lists whose tail is a hole. The
expression hcomp (k, hfn z => x::z) updates the tail of k by
the new cons cell consisting of x and a hole. That is to say, it adds x
to the right of k. Finally, the result is obtained by updating the tailof k by ys, i.e., happ(k,ys). The identity hole abstraction is used
for the initial argument. To sum up, hfun_append creates an appended list from the head. In our measurement this transformation
reduces execution time about 40% as we see later in Section 5.
Another view of this transformation is continuation passing
transformation [17]. If we think k as a continuation and replace
hole functions by usual functions, we obtain append in continuation passing style. Thus it can be considered that continuations
are represented by hole functions. However, if we use usual functions for continuations, the performance of the function is usually
not improved. It is because the function for the continuation grows
through recursive calls as stack grows for the original recursive version.
There are many functions producing a list which can be transformed to tail recursive functions. For example, there are 12 functions producing lists in the structure for lists in the proposal of Standard ML Basis Library. Among them, the following 6 functions canbe converted to tail recursive functions in this way: @, take, map,
mapPartial, filter, tabulate.
Furthermore, the transformation can be implemented as optimization that transforms a class of functions into tail recursivefunctions automatically. We can check whether the transformation

can be applicable syntactically by checking whether the continuations for recursive calls can be represented by hole abstractions.
This is a significant advantage of our transformation over the conventional optimization which transforms a function into tail recursive one [2, 7]. The conventional transformation usually needs theknowledge of properties such as associativity of functions for thetransformation.
The previous improvement of programs can be obtained by acompiler optimization without explicitly introducing hole abstractions into source languages. However, there are other kinds of usages of hole abstractions. The function flatten in Figure 2 flattens a list of lists to a list by using append. The function flatten
is not tail recursive because append must be performed after therecursive call of flatten. For better implementation of flatten,
we first prepare the function append’ which has type (’a list,’a list) hfun -> (’a list, ’a list) hfun and appends
a list to a list whose tail is a hole. Then we can implement
flatten as the tail recursive function hfun_flatten. This function hfun_flatten can be compiled to efficient code with nested
loops by inlining the definition of append’. However, this definition of hfun_flatten can be obtained only by using associativity of append and the following fact: if happ(k, []) = l thenhapp(append’(k, x),[]) = append (l,x). Without knowing these properties it is not possible to obtain hfun_flatten by
the compiler optimization.
Hole abstractions are useful for other data types than lists. In
Figure 3, hole abstractions are used for the type tree that is thetype for binary trees whose nodes are associated to integers. The
function binsert inserts an integer into a tree and is not tail recursive. As append, the function can be transformed to the tail recursive function hfun_binsert below by using hole abstractions.
However, for data types like trees there are many functions thatcannot be transformed to tail recursive form. For such functions,although we cannot obtain tail recursive functions, we can often
improve functions by converting the last recursive call to a tail recursive call. For example, addone which adds 1 to the integer as-datatype tree = Lf
| Br of int *tree * tree

fun binsert (Lf, y) = Br (y, Lf, Lf)| binsert (Br (x, t1, t2), y) =if y < x then Br (x, binsert (t1, y), t2)else if x < y then Br (x, t1, binsert (t2, y)) else raise Bsearch
fun hfun_binsert (t, y) =let fun binsert’ (Lf, y, k) = happ (k, Br (y, Lf, Lf))
| binsert’ (Br (x, t1, t2), y, k) =if y < x then binsert’ (t1, y, hcomp (k, hfn t => Br (x, t, t2)))else
if x < y then binsert’ (t2, y, hcomp (k, hfn t => Br (x, t1, t)))else raise Bsearchinbinsert’ (t, y, hfn t => t)
end
fun addone Lf = Lf
| addone (Br (x, t1, t2)) = Br (x + 1, addone t1, addone t2)
fun hfun_addone Lf = Lf
| hfun_addone (Br (x, t1, t2)) =let fun addone’ (Lf, k) = happ (k, Lf)| addone’ (Br (x, t1, t2), k) =addone’ (t2, hcomp (k, hfn t2 => Br (x + 1, hfun_addone t1, t2)))inaddone’ (t2, hfn t2 => Br (x + 1, hfun_addone t1, t2))
end

Figure 3: Using Hole Abstractions for Trees

sociated to each node includes two recursive calls as shown in Figure 3. Thus it cannot be converted to a tail recursive function by our
method. However, the function can be converted to hfun_addonethat requires one recursive call of hfun_addone and another tail recursive call of addone’. It should be remarked that the expressions
x + 1 and hfun_addone t1 are evaluated at the time of evaluation of hfn t2 => ..., because an expression inside hfn is evaluated. It is possible because they do not contain the variable t2
introduced by hole abstraction.

3

Calculus

In this section we present a simply typed call-by-value λ-calculus
extended with hole abstractions. We design the type system of thecalculus so that the restrictions discussed in the previous section
are imposed. Then we will show some properties of the calculus
including the soundness of the type system. The syntax of the calculus is defined as follows:types
τ ::= b | τ1 → τ2 | τ list | (τ1 , τ2 ) hfun
exp’s M ::= x | c | M1 M2 | λx : τ.M |nil | cons(M1 , M2 ) |λ̂x : τ.M | happ(M1 , M2 ) |case M1 of cons(x1 , x2 ) ⇒ M2 | nil ⇒ M3
We include τ list as a type constructor, and nil and cons(M1 , M2 )as expressions for illustration of usage of the calculus and its compilation. The hole composition hcomp(M1 , M2 ) is not includedin the calculus because it can be defined by hole abstractions andapplications as we will see later.
We consider types containing hfun as linear types, thoughτ1 → τ2 is always considered a nonlinear type. Thus linear types
are defined as follows:
σ ::= (τ1 , τ2 ) hfun | σ list
The treatment of linear types is based on steadfast types of
Wadler [21, 22]. The type system is designed so that a variablewith a linear type contains the sole pointer [23] and thus we canperform destructive operations on values of linear types. However,since linearity is used only for destructive update, values of linear types are permitted to be abandoned implicitly. In this sense
they are considered as affine types of Jacobs [8] or unique types ofClean [16].
For the type system of the calculus we use two kinds of contexts:
type assignements Γhole contexts
H

::=
::=

x1 :τ1 , . . . , xn :τn∅ | x:τ

Type assignments are used for variables introduced by usual λabstraction and hole contexts are used for variables introduced by
λ̂-abstraction. Here we should remark that hole contexts containat most one binding. By this restriction we prohibit data structureswith multiple holes represented by nested hole abstractions. For example, λ̂x : τ.λ̂y : τ list.cons(x, y) is prohibited. This restriction

(hole)Γ; x:τ  x : τ(var)

x:τ ∈ ΓΓ; ∅  x : τ(hfn)

Γ; x:τ1  M : τ2
Γ; ∅  λ̂x:τ1 .M : (τ1 , τ2 ) hfun

(happ)

Γ1 ; ∅  M1 : (τ1 , τ2 ) hfun Γ2 ; H  M2 : τ1
Γ1  Γ2 ; H  happ(M1 , M2 ) : τ2(nil)

Γ; ∅  nil : τ list

(cons)

Γ1 ; H1  M1 : τ Γ2 ; H2  M2 : τ list
Γ1  Γ2 ; H1 ⊕ H2  cons(M1 , M2 ) : τ list(abs)

Γ|N  {x : τ1 }; ∅  M : τ2
Γ; ∅  λx : τ1 .M : τ1 → τ2(app)

Γ1 ; ∅  M1 : τ1 → τ2 Γ2 ; ∅  M2 : τ1
Γ1  Γ2 ; ∅  M1 M2 : τ2(case)

Γ1 ; ∅  M : τ  list Γ2 , x:τ  , y:τ  list; ∅  M1 : τ Γ2 ; ∅  M2 : τΓ1  Γ2 ; ∅  case M of cons(x, y) ⇒ M1 | nil ⇒ M2 : τ
Figure 4: Type System

is not essential for the definition of the calculus, but it is required
for the simple compilation method presented in the next section.
We say that Γ1 and Γ2 are compatible if for x:τ ∈ Γ1 andx:τ  ∈ Γ2 , τ and τ  are identical and nonlinear. For compatible Γ1and Γ2 , we define Γ1 Γ2 by the union of the two type assignments.
For type assignments we define Γ|N that is the restriction of Γ tox:τ for nonlinear τ . We say that H1 and H2 are compatible ifeither H1 or H2 is empty. For compatible hole contexts we define
H1 ⊕ H2 by the union of H1 and H2 .
The judgement of the type system has the following form:
Γ; H  M : τ . The type system of the calculus is shown in Figure 4. We summarize the key features of the type system below.

Then evaluation M −→ M  is defined by E[M ] −→ E[M  ] if
M M  . We write M ↓ M  if M −→∗ M  and M  is in normal
form with respect to −→.
The composition hcomp(M1 , M2 ) can be defined in this calculus as λ̂x:τ.happ(M1 , happ(M2 , x)) and the reductions inside
λ̂-abstractions result in the intended simplified hole abstraction as
follows:• Variables introduced by λ-abstractions can be abandoned by
the rule (var). However, even for nonlinear types a variable
introduced by λ̂-abstraction is used linearly in a strict senseand cannot be abandoned implicitly. For example, λ̂x:b.nil
is ill-typed.

The reduction of hcomp should be compared to that of the usualfunction composition:• λ-abstractions, applications, and case-expressions can be
typed only with the empty hole context. However, they can be
still used inside λ̂-abstraction if the evaluation of them is not
related to the hole. For example, λ̂x:blist.cons((λx:b.x)c, x)
is well-typed.
• In the rule (happ), M1 of happ(M1 , M2 ) must be typed
with the empty hole context.
This restriction is imposed because we cannot evaluate expressions such as
λ̂x:(b, τ ) hfun.happ(x, c).
• In the rule (abs), only the nonlinear part of Γ, Γ|N , is used
for the typing of the body of a λ-abstraction. It is because
τ1 → τ2 is considered as a nonlinear type.
We define the operational semantics of the calculus in the styleof [25] and prove the soundness of the type system. The operationalsemantics of the calculus is defined in Figure 5. We consider a λ̂abstraction as a value only if the body of the abstraction is a value.
Evaluation contexts are defined so that evaluation does not occur
inside usual λ-abstraction, but inside λ̂-abstraction. Similar evaluation order is used for the implementation calculus of polymorphic
records of Ohori [13] where evaluation occurs within index abstraction to preserve the operational semantics of ML. The definition of
reductions is standard and is also shown in Figure 5.

Ihcomp(λ̂y1 :τ  .V1 , λ̂y2 :τ.V2 ) −→∗λ̂x:τ.happ(λ̂y1 :τ  .V1 , V2 [x/y2 ]) −→λ̂x:τ.V1 [V2 [x/y2 ]/y1 ](λx:τ  .M ) ◦ (λy:τ.N ) −→∗ λz:τ.(λx:τ  .M )((λy:τ.N )z)
Here the original two lambda abstractions still remain even after
reduction.
The following two lemmas show that the evaluation preserves
the type of an expression.
Lemma 1 (Substitution) 1. If Γ  x:τ0 ; H  M : τ and ∅; ∅ V : τ0 , then Γ; H  M [V /x] : τ .
2. If ∅; x:τ0  V1 : τ and ∅; H  V2 : τ0 , then ∅; H 
V1 [V2 /x] : τ .
Lemma 2 (Subject Reduction) If ∅; H  M :τ and M −→ M  ,then ∅; H  M  :τ .
The most important lemma is the following: it claims that theevaluation of a program cannot get stuck [25].
Lemma 3 If ∅; H  M :τ , then M is a value or M −→ M  forsome M  .
By combining the previous two lemmas, we obtain the soundness of the type system.
Theorem 1 (Soundness) If ∅; ∅  M :τ , then M is a value or
M −→ M  and ∅; ∅  M  :τ .
Although the calculus we have considered does not include recursion, we think that it is easy to extend the calculus by adding
recursion.

Values:V ::= c | x | λx:τ.M | nil | cons(V1 , V2 ) | λ̂x:τ.V
Evaluation Contexts:
E::=[] | E M | V E |cons(E, M ) | cons(V, E) | case E of cons(x, y) ⇒ M1 | nil ⇒ M2 |λ̂x:τ.E | happ(E, M ) | happ(V, E)

Reduction Rules:(λx:τ.M )Vhapp(λ̂x:τ.V1 , V2 )case cons(V1 , V2 ) of cons(x, y) ⇒ M1 | nil ⇒ M2
case nil of cons(x, y) ⇒ M1 | nil ⇒ M2

I M [V /x]
I V1[V2 /x]
I M1[V1 /x, V2/y]
I M2

Figure 5: Operational Semantics

4

Compilation

In this section we will show a compilation method of hole abstractions. It is based on a transformation that converts a general holeabstraction into a composition of primitive hole abstractions. Thistransformation is analogous to the translation from the λ-calculus
to combinatory logic found in the standard text [1]. After this transformation we need only the evaluation of primitive hole abstractions and do not require the evaluation of expressions inside holeabstractions. Thus programs can be compiled by a standard compilation method after the transformation. We prove the correctnessof the transformation by the method of logical relations.
In this section, we consider hcomp as a primitive that is implemented as we described in Section 2. The reduction rule for hcomp
is defined as follows:
hcomp(λ̂y1 :τ  .V1 , λ̂y2 :τ.V2 )I λ̂y2 :τ.V1 [V2/y1 ]Furthermore, we consider three more hole functions as primitives:
idhfunτ , consheadτ (M ), and constailτ (M ). They correspondto λ̂x:τ.x, λ̂x:τ.cons(x, M ), and λ̂x:τ list.cons(M, x) respectively. The reduction rules for them are defined as follows:
idhfunτconsheadτ (V )constailτ (V )I λ̂x:τ.x
I λ̂x:τ.cons(x, V )I λ̂x:τ list.cons(V, x)

The typing rules for the primitives are derived from the definitionand shown in Figure 6. We also extend evaluation contexts as follows:E::=. . . | hcomp(E, M ) | hcomp(V, E) |consheadτ (E) | constailτ (E)The compilation is defined as a deductive system with judgements of the following form:
Γ; H  M : τ

M .

The rules of the deductive system are shown in Figure 7. The rules
can be considered as refinements of the typing rules. Thus it is clear
M  for some M  .
that if Γ; H  M : τ , then Γ; H  M : τConversely, if Γ; H  M : τ
M , then Γ; H  M : τ .

There are three rules for cons: (cons) is used if the hole context
is empty, (conshead) and (constail) are used if the hole context is
not empty. There are two rules for happ depending on whether thehole context is empty or not.
For example, λ̂x:int list.cons((λy:int.y)1, x) is translated to
the following expression.
hcomp(constailint ((λy:int.y)1), idhfunint list )This expression has type (int list, int list) hfun as we expect. Furthermore, it is evaluated as follows:
−→
−→
−→
−→

hcomp(constailint ((λy:int.y)1), idhfunint list )hcomp(constailint (1), idhfunint list )hcomp(λ̂x:int list.cons(1, x), idhfunint list )hcomp(λ̂x:int list.cons(1, x), λ̂x:int list.x)λ̂x:int list.cons(1, x)This evaluation does not require reductions inside λ̂-abstractions.
Let us check that the derived definition of hole composition in
the previous section is actually compiled to the primitive hole composition by this translation. The derived definition of hole composition of M1 and M2 is λ̂x:τ.happ(M1 , happ(M2 , x)). This expression is translated to hcomp(M1 , hcomp(M2 , idhfunτ )). Then it iseasily shown that this expression is equivalent to hcomp(M1 , M2 ).
The translation rules often introduce redundant identity
hole abstractions. For example, λ̂x.cons(1, x) is translated
to hcomp(constail(1), idhfunint list ) and it is clearly equivalent to constail(1).
In general it is easily shown that
hcomp(M, idhfunτ ) is equivalent to M . By considering that we
obtain the following derived rules. They can be added for removing
redundant identity hole abstractions.
Γ; ∅  M2 : τ list
Γ; x : τ  cons(x, M2 ) : τ list

M2conshead(M2 )M1
Γ; ∅  M1 : τΓ; x : τ list  cons(M1 , x) : τ list
constail(M1 )M1
Γ; ∅  M1 : (τ1 , τ2 ) hfun
Γ; x : τ1  happ(M1 , x) : τ2
M1Γ; ∅  idhfunτ : (τ, τ ) hfun

Γ; ∅  M1 : (τ1 , τ2 ) hfun Γ; ∅  M2 : (τ3 , τ1 ) hfun
Γ; ∅  hcomp(M1 , M2 ) : (τ3 , τ2 ) hfun

Γ; ∅  M : τ list
Γ; ∅  consheadτ (M ) : (τ, τ list) hfun

Γ; ∅  M : τΓ; ∅  constailτ (M ) : (τ list, τ list) hfun

Figure 6: Typing Rules for Primitives(var)

x:τ ∈ ΓΓ; ∅  x : τ

(hfn)

M
Γ; x : τ1  M : τ2
Γ; ∅  λ̂x : τ1 .M : (τ1 , τ2 ) hfun

(nil)

x
M

Γ; ∅  nil : τ list

(hole) Γ; x : τ  x : τnilidhfunτ(conshead)Γ1 ; x : τ  M1 : τ 
M1 Γ2 ; ∅  M2 : τ  listM2
Γ1  Γ2 ; x : τ  cons(M1 , M2 ) : τ  list
hcomp(consheadτ  (M2 ), M1 )(constail)M1 Γ2 ; x : τ  M2 : τ  listM2
Γ1 ; ∅  M1 : τ Γ1  Γ2 ; x : τ  cons(M1 , M2 ) : τ list
hcomp(constailτ  (M1 ), M2 )(cons)

M1 Γ2 ; ∅  M2 : τ  listM2
Γ1 ; ∅  M1 : τ Γ1  Γ2 ; ∅  cons(M1 , M2 ) : τ list
cons(M1 , M2 )(happ)

M1 Γ2 ; ∅  M2 : τ1
M2Γ1 ; ∅  M1 : (τ1 , τ2 ) hfun
Γ1  Γ2 ; ∅  happ(M1 , M2 ) : τ2happ(M1 , M2 )(hcomp)M1 Γ2 ; x:τ  M2 : τ1
M2Γ1 ; ∅  M1 : (τ1 , τ2 ) hfun
Γ1  Γ2 ; x:τ  happ(M1 , M2 ) : τ2
hcomp(M1 , M2 )

(abs)

M
Γ|N  {x : τ1 }; ∅  M : τ2
Γ; ∅  λx : τ1 .M : τ1 → τ2
λx : τ1 .M 

(app)

M1 Γ2 ; ∅  M2 : τ1
Γ1 ; ∅  M1 : τ1 → τ2
Γ1  Γ2 ; ∅  M1 M2 : τ2
M1 M2

(case)

M2

M  Γ2 , x:τ  , y:τ  list; ∅  M1 : τ
M1 Γ2 ; ∅  M2 : τM2Γ1 ; ∅  M : τ  list
Γ1  Γ2 ; ∅  case M of cons(x, y) ⇒ M1 | nil ⇒ M2 : τcase M  of cons(x, y) ⇒ M1 | nil ⇒ M2
Figure 7: Rules of Compilation

M ∼τ M 

M ↓ V and M  ↓ V  and V ≈τ V c ≈b cnil ≈τ list nilcons(V1 , V2 ) ≈τ list cons(V1 , V2 )V ≈τ1 →τ2 V 
V ≈(τ1 ,τ2 ) hfun V 

V1 ≈τ V1 and V2 ≈τ list V2
for V1 ≈τ1 V1 it holds V V1 ∼τ2 V  V1
for V1 ≈τ1 V1 it holds happ(V, V1 ) ∼τ2 happ(V  , V1 )Figure 8: Logical Relations

For example, by using these rules the derived definition of holecomposition λ̂x:τ.happ(M1 , happ(M2 , x)) can be compiled tohcomp(M1 , M2 ) directly.

We define type τ H as follows: τ ∅ ≡ τ and τ x:τ ≡(τ , τ ) hfun. Then the following lemma is proved easily by induction of the derivation of compilation.
Lemma 4 (Type Correctness) If Γ; H  M : τΓ; ∅  M  : τ H .

M  , thenThis lemma implies that the transformation preserves the type of aprogram.
To prove the operational correctness of the transformation, we
use the method of logical relations as many studies on compilation [14, 12]. First, the type-indexed relations ∼τ between closed
expressions of type τ and relations ≈τ between closed values oftype τ are defined in Figure 8. We define the relations on list types,≈τ list , by the smallest relations satisfying the condition in Figure 8.
Then the relations are well-defined by induction on the structure oftypes. Informally, M ∼τ M  means that M and M  have the same
operational behaviour. The relations ≈τ are extended to the relations ≈Γ between substitutions. The following lemma states the
key properties of hole functions.
Lemma 5 1. If ∅; x:τ3
happ(V1 , V2 ):τ and∅; ∅  V : τ3 , then happ(λ̂x:τ3 .happ(V1 , V2 ), V ) ∼τhapp(V1 , happ(λ̂x:τ3 .V2 , V )).
2. If ∅; ∅  hcomp(V1 , V2 ) : (τ3 , τ2 ) hfun and ∅; ∅  V : τ3 ,then happ(hcomp(V1 , V2 ), V ) ∼τ2 happ(V1 , happ(V2 , V )).
3. If ∅; x:τ   cons(V1 , V2 ) : τ list and x ∈ F V (V1 ) and∅; ∅  V : τ  , then happ(λ̂x:τ  .cons(V1 , V2 ), V ) ∼τ list
cons(happ(λ̂x:τ  .V1 , V ), V2 ).
4. If ∅; x:τ   cons(V1 , V2 ) : τ list and x ∈ F V (V2 ) and∅; ∅  V : τ  , then happ(λ̂x:τ  .cons(V1 , V2 ), V ) ∼τ list
cons(V1 , happ(λ̂x:τ  .V2 , V )).
Now we will show that an expression of type τ and its translation are related by ∼τ . We use the previous lemma for the proofsof translations under non-empty hole contexts.
Lemma 6 1. If Γ; ∅  M : τγ(M ) ∼τ γ  (M  ).

M  and γ ≈Γ γ  , then

2. If Γ; x : τ   M : τM  and γ ≈Γ γ  , thenγ(λ̂x:τ  .M ) ∼(τ  ,τ ) hfun γ  (M  ).
By restricting the previous lemma, we obtain the correctness ofcompilation stated as follows.
Theorem 2 (Correctness) Let ∅; ∅  M : b
only if M  ↓ c.

5

M  . M ↓ c if and

Implementation and Measurement

In this section we will discuss some issues on implementation ofhole abstractions and then show results of some simple benchmarks. We have implemented some ideas described in this paper
in an experimental ML compiler being developed by the author.
The compiler was originally developed for the study of a ML compiler based on explicit type parameter passing in [11] and now produces assembly code for the core language of Standard ML extended with structure definitions. All measurements are done on

a ALPHA STATION 500/500 with 8 Mbyte cache memory under
Digital Unix 4.0A.
So far we have not yet implemented general hole abstractions
and the compilation method described in this paper. However,in order to measure how much improvement we can obtain byusing hole functions we implemented happ, hcomp, and several
other primitive hole abstractions including idhfun, constail, andconshead. Furthermore, as a phase of the compiler we also implemented the transformation that converts a class of functions producing lists into tail recursive functions as described in Section 2.1.
The elaboration phase of the compiler is modified so that(τ1 , τ2 ) hfun is treated as a linear type. However, for simplicity werestrict the type system so that polymorphic types are not instantiated by linear types. Although this restriction is not a problem
to write examples in this paper, for greater flexibility we should
consider a type system which keeps track of use of variables moreaccurately such as the type system studied by Turner et al. [20].
In the intermediate language of the compiler, we represent holeabstractions by a usual record of two pointers to a data structure
and a hole. Thus in the intermediate language (’a, ’b) hfun isrepresented as follows:
type (’a, ’b) hfun = (’a, ’b) prehfun * ’a hole
The type (’a, ’b) prehfun is the type for pointers to values oftype ’b with a hole of type ’a. The type ’a hole is the type forholes of type ’a. In our implementation, idhfun is represented bya pair of null pointers which can be distinguished from the pointersto heap memory. By using this representation, the standard optimization of flattening records can optimize manipulations on holefunctions. However, by this representation the type system does notprevent using the hole and the data structure part of a hole function
independently. Thus it is possible to write a program with side effects on functional data types in the intermediate language.
Our compiler uses tag-free copying garbage collection [19, 11].
There is one problem in implementation of garbage collection in
the presence of hole functions: holes point to middle of objects inheap memory. Thus we have to treat holes carefully in implementation of garbage collection. Our strategy is updating the pointers toholes after usual garbage collection is finished. This works because
if a hole is live, then there is a live object containing the hole.
We measured the effect of using hole abstractions for several
simple programs. The results are shown in Table 1. The columns
stand and hfun show execution time for the standard implementation and the implementation using hole abstractions for each program respectively. For append and msort, we used the automatic transformation converting functions into tail recursive ones
described in Section 2.1. In merge sort, the function for merging two lists is converted to a tail recursive function. For flatten
we compared the standard implementation using the tail recursive
append and hfun_flatten in Section 2.1. For these functions onlists, the execution time is reduced more than 20%.
To measure effects on programs producing other data types, weused the programs binsert and addone in Section 2.1. Improvement obtained for binsert and addone is smaller, but still about
15%. The result for addone indicates that optimization by using
hole abstractions is useful even if a function cannot be converted totail recursive one.

6

Related Work

6.1 Linear Types
The calculus we introduced utilizes linearity for efficient implementation of hole application and composition through destructive

appendflattenmsort
binsertaddone

stand
5.46
2.80
10.03
19.24
3.85

hfun
3.26
2.22
7.33
15.90
3.26

hfun/stand
0.60
0.79
0.73
0.83
0.85

Description
append lists of length 500, 100000 times
flatten a list of length 500 of lists of length 5, 10000 times
sort a list of length 500 by merge sort, 10000 times
insert 5000 integers into a binary tree, 1000 times
add 1 to each node of a tree of depth 8, 100000 times

Table 1: Execution time (sec)operations. The linearity we used does not directly correspond tothat of linear logic [5], but that for destructive updates used in [21].
However the linearity itself is not sufficient to express data structures with a hole and associated operations. It is because we haveto maintain two pointers to a data structure: one is to the top of thedata structure and the other is to the hole.

6.2

This work is partially supported by Grant-in-Aid for Encouragement of Young Scientists of Japan No. 09780271. We would liketo thank Jacques Garrigue, Masahito Hasegawa, Koji Kagawa, Atsushi Ohori, and the anonymous reviewers for their many helpfulcomments and suggestions.

Tail Recursion Modulo Cons

Several researchers have studied transformation to convert functions which require construction of a data structure using the valueof the recursive call into tail recursive functions [9, 24, 3]. Thiskind of recursion is called tail recursion modulo cons in [24]. In
those studies the transformation similar to that in Section 2.1 is formulated as a translation to an imperative language with destructive
operations on functional data types. In contrast we can formulate
the transformation without introducing explicit destructive operations.
Recently Cheng and Okasaki implemented this optimization for
the TIL compiler [3, 18]. They discuss issues related to garbage
collection and report similar improvement in their benchmarks.

6.3

Acknowledgements

Logical Variable

References[1] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Horth-Holland, 1984.
[2] R. M. Burstall and J. Darlington. A transformation system fordeveloping recursive programs. Journal of ACM, 24(1):44–
67, 1977.
[3] P. Cheng and C. Okasaki. Destination-passing style and generational garbage collection. Unpublished, 1996.
[4] J. Chirimar, C. A. Gunter, and J. G. Riecke. Proving memory management invariants for a language based on linear
logic. In Proc. ACM Conf. Lisp and Functional Programming, pages 139–147, 1992.
[5] J.-Y. Girard. Linear logic. Theoretical Computer Science,50(1), 1987.

Logical variables are introduced in pure functional programming
languages to use programming techniques developed for logic programming languages such as difference-list [10, 15]. Values forlogical variables are determined by giving constraints as for variables of logic programming languages. Thus an unconstrained logical variable can be used to represent a hole. Logical variables areusually implemented by using graph reduction. Thus it is not clearthat it can be incorporated with call-by-value functional programming languages without significant changes of implementation.

[6] J. C. Guzmán and P. Hudak. Single-threaded polymorphic
lambda calculus. In IEEE Symp. on Logic in Computer Science, 1990.

7[8] B. Jacobs. Semantics of weakening and contraction. Annalsof Pure and Applied Logic, 69:73–106, 1994.

Future Work

It is natural to consider data structures with multiple holes: for example, a cons cell where both car and cdr are holes. We thinkthat the extension is possible just by extending hole contexts to theform x1 :τ1 , . . . , xn :τn , though we have not yet checked the details.
However, it does not seem easy to develop an efficient method ofcompilation for the extended calculus.
Another topic for future work is to prove the correctness ofcompilation based on a low level operational semantics. The semantics we used does not capture sharing of objects and destructive
implementation of hole application. We are working on the correctness proof based on a low level semantics similar to the semantics
used to prove properties of a language based on linear logic [4].

[7] G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11, 1978.

[9] J. R. Larus. Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. PhD thesis, Computer
Science Division, University of California at Berkeley, 1989.
USB/CSD 89/502.
[10] G. Lindstrom. Functional programming and the logical variable. In Proc. ACM Symp. on Principles of Prog. Languages,
pages 266 – 280, 1985.
[11] Y. Minamide. Compilation based on a calculus for explicit
type passing. In Second Fuji International Workshop on
Functional and Logic Programming, pages 301–320. World
Scientific, 1996.
[12] Y. Minamide, G. Morrisett, and R. Harper. Typed closure
conversion. In Proc. ACM Symp. on Principles of Prog. Languages, pages 271 – 283, 1996.

[13] A. Ohori. A compilation method for ML-style polymorphic
record calculi. In Proc. ACM Symp. on Principles of Prog.
Languages, 1992.
[14] A. Ohori. A polymorphic record calculus and its compilation.
ACM Transaction on Programming Languages and Systems,
17(6), 1995.
[15] K. K. Pingali. Lazy evaluation and the logic variable. In D. A.
Turner, editor, Research Topics in Functional Programming,
pages 171–198. Addison-Wesley, 1987.
[16] R. Plasmeijer and M. van Eekelen. Language Report CONCURRENT Clean Version 1.1. 1996.
[17] G. D. Plotkin. Call-by-name, call-by-value and the λcalculus. Theoretical Computer Science, 1(2), December
1975.
[18] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, andP. Lee. TIL: A type-directed optimizing compiler for ML.
In Proc. ACM SIGPLAN Conf. on Programming Language
Design and Implementation, 1996.
[19] A. Tolmach. Tag-free garbage collection using explicit typeparameters. In Proc. ACM Conf. Lisp and Functional Programming, pages 1–11, 1994.
[20] D. N. Turner, P. Wadler, and C. Mossin. Once upon a type.
In Functional Programming Languages and Computer Architecture, 1995.
[21] P. Wadler. Linear types can change the world! In Programming Concepts and Methods, 1990.
[22] P. Wadler. Is there a use for linear logic? In Partial Evaluationand Semantics Based Program Manipulation, 1991.
[23] P. Wadler. A taste of linear logic. In Mathematical Foundations of Computing Science, 1993. LNCS 711.
[24] P. L. Wadler. Listlessness is Better than Laziness. PhD thesis,
Computer Science Department, Carnegie-Mellon University,
1985. CMU-CS-85-171.
[25] A. K. Wright and M. Felleisen. A syntactic approach totype soundness. Information and Computation, 115(1):38–
94, 1994.