An Approach to Completing Variable Names
for Implicitly Typed Functional Languages
Takumi Goto

Isao Sasano

Shibaura Institute of Technology
Tokyo, Japan{m110057, sasano}@sic.shibaura-it.ac.jp

Abstract

cially IDEs for statically typed functional languages are expected
to utilize the feature of being statically typed. Reflecting typing information on variable name completion reduces the number of candidates for completion, as well as decreases type errors and spelling
errors. Actually IDEs for Java, including Java IDE on Eclipse, provide member variable or method name completion, after typing
dot, with type information (class definition) reflected. In explicitly
typed languages like Java, type information can be directly computed from the program text. In implicitly typed languages, i.e.,
those which allow either annotating or not annotating types to variable declarations, it is not so obvious how to design variable completion mechanism with type information reflected, since we need
Categories and Subject Descriptors D.3.2 [Programming Lanto do type inference in some way when completing variable names.
guages]: Language Classifications—Applicative (functional) lanIn developing small programs, purely syntactic variable comguages; D.2.3 [Software Engineering]: Coding Tools and Techniques—pletion may work well without using type information. Our intenProgram editors
tion is to complete variable names that are defined in some libraries
General Terms Reliability, Theory, Languages
or some other program modules. For example, let us consider thecase where a programmer is writing a program fragment that prints
Keywords polymorphic language, type inference, Emacs-mode,
some integer value. In Standard ML she might write the fragment
variable name completionas follows1 .
print (Int.
1. Introduction
Here
let
us
supposethat
shedoes not recall the function name that
Integrated development environments (IDE) play an important role
converts an integer to the corresponding string but remembers thein developing large software. IDEs provide functionalities includstructure name Int inside which the function is declared. In thising automatic indentation, keyword highlighting, variable namesituation there are 29 candidates since the structure Int has 29
completion, and so on. Among them one of the most basic and condeclarations. By using type information, the candidates are reduced
venient functionalities is variable name completion: when inputting
to two since the function print takes a value of string type as its
a variable name, candidates for the variable names that start withargument and the structure Int has only two functions that may
the string which has been input are shown on a pop-up window
return a value of string type: fmt and toString.
for example. In developing large programs, we tend to use longIn this paper we present a basic mechanism of variable namenames especially for variables with long scopes for enhancing thecompletion for an implicitly typed ML-like core functional lanprogram readability, and in such cases variable name completion
guage. In order to filter candidates by type information, we need
substantially decreases the time for recalling the variable names as
to do type inference for incomplete programs. While various setwell as the amount of keyboard typing or spelling errors. Up to now
tings can be considered, we consider a simple case: up to the curIDEs for commonly-used languages like Java, C, C++ have beensor position, the program text is given completely. More precisely,
well developed while not so much for functional programming lanwe assume that the input programs before the cursor position doguages. Functional languages are now getting to be used widely so
not have any syntax error or type error. When computing candithat IDEs for them are strongly expected.
dates for variable names to be completed we only use the program
IDEs should be designed and implemented reliably as well astext before the cursor position and ignore the text after the cursor
compilers, since otherwise people may not want to use them. Espeposition. This simple approach works well for ML-like languages
since all the variables are declared syntactically before their use in
ML-like languages except for (mutually) recursive declarations. In
the future we may extend the approach to use the program text after the cursor position for supporting Haskell-like languages where
variables may appear syntactically before their declarations.
c ACM, 2012. This is the author’s version of the work. It is posted here
Copyright °This paper presents an approach to completing variable names
when writing programs in implicitly typed functional languages.
As a first step toward developing practical systems, we considereda simple case: up to the cursor position the program text is given
completely. With this assumption we specify a variable completion
problem for an implicitly typed core functional language with letpolymorphism and show an algorithm for solving the problem.
Based on the algorithm we have implemented a variable namecompletion system for the language as an Emacs-mode.

by permission of ACM for your personal use. Not for redistribution. The definitive
version was published in ACM SIGPLAN 2012 Workshop on Partial Evaluation and
Program Manipulation (PEPM’12), January 23-24, 2012, Philadelphia, Pennsylvania,
USA, http://doi.acm.org/10.1145/2103746.2103771.

1 Although our current system does not deal with programs with structures(or modules), here we use this example since it is a typical case where
filtering with types effectively reduces the number of candidates.

If the system might sometimes eliminate valid candidates, itwould be confusing since the programmer would have to consider
whether or not some valid candidates may exist other than thecandidates in the pop-up window. So it is strongly desired for thevariable name completion system to have the property that all thepossible variables are shown as candidates. On the other hand,variable name completion system is expected to eliminate all thevariables that cause type error for whatever program text is input
after the cursor position. In Section 7 we state as conjectures that
our solution presented in this paper satisfies these two properties.
As for the cost of inferring types for partial programs, we construct an efficient partial type inference algorithm while retaining
the above two properties. It is sufficient to do type inference foreach variable that is within its scope at the cursor position, but it
includes many redundant computation. As will be presented in Section 5, our partial type inference algorithm appropriately abstracts
types of variables that are within their scope at the cursor position,
which results in an efficient algorithm suitable for practical use.
Based on the mechanism we present, we have implemented
variable name completion as an Emacs mode for the ML-like corelanguage. Our experiment shows that our mechanism works wellat least for the core language. Currently we apply the algorithm
for computing candidates every time when some character is input
on Emacs. We expect that the algorithm can be incrementalized byreusing the previous computation, which we leave as future work.
The rest of the paper is organized as follows. Section 2 specifies
the variable completion problem we solve. Section 3 shows our basic ideas and outline of our solution. Section 4 describes the termcompletion phase by introducing two abstractions, dummy nodes
and marked nodes. Section 5 describes the type inference algorithm. Section 6 describes the phase for filtering by type constraint
and the (partial) spelling of the variable name being input at the
cursor position. Section 7 summarizes the algorithm and gives theproperties of our algorithm. Section 8 describes our implementation as an Emacs mode for a small subset of Standard ML. Section
9 describes some experimental results. Section 10 discusses about
related work. Section 11 describes future work and concludes thepaper.

2.

Specification of variable completion problem

In this section we specify the problem that we solve in this paper.
We use the following core language on which we specify the problem.
M

::=
|

x | c | λx.M | M M | (M )let x = M in M end | ﬁx x.M

Here x represents a variable, c represents a constant, λx.M represents a function abstraction, M M represents a function application, let x = M in M end represents a let expression, andﬁx x.M represents a fix expression. For simplicity we suppose
constants are + and - of type int → int → int and natural numbers of type int. We have explicitly included the parentheses in thecore language in order to express situations where there are open
parentheses not yet closed. For simplicity we only consider the program without type annotations.
We consider the following types for the core language.
σ := ∀α1 . . . αn .τ

τ := int | α | τ → τ

The types consist of the integer type int, type variables, function
types, and polymorphic types. Here we used σ as a meta variable
for representing a polymorphic type and τ as a meta variable forrepresenting a monomorphic type. When σ = ∀α1 . . . αn .τ0 andthere exists some τ1 , . . . , τn such that τ = [τ1 /α1 . . . τn /αn ]τ0 ,we call τ as an instance of the polymorphic type σ and write τ < σ.

(const) Γ . c : τ (c : τ ∈ Const)(var) Γ{x : σ} . x : τ if τ < σ
Γ . M1 : τ 1 → τ 2 Γ . M2 : τ 1(app)
Γ . M1 M2 : τ2
Γ{x : τ1 } . M : τ2(abs)
Γ . λx.M : τ1 → τ2
Γ . M1 : τ1 Γ{x1 : Cls(Γ, τ1 )} . M2 : τ2
(let)
Γ . let x1 = M1 in M2 end : τ2
Γ{x : τ } . M : τ(fix)
Γ . ﬁx x.M : τ
Figure 1. Type system for the core language

pre : M → {(P, x)}
pre c = {}pre x = {( s , x) | s is a preﬁx of x}
pre (M1 M2 ) = {(M1 P2 , x2 ) | (P2 , x2 ) ∈ pre M2 } ∪{(P1 , x1 ) | (P1 , x1 ) ∈ pre M1 }pre (λx.M ) = {(λx.P, x1 ) | (P, x1 ) ∈ pre M }pre (let x = M1 in M2 end) ={(let x = M1 in P2 , x2 ) | (P2 , x2 ) ∈ pre M2 } ∪{(let x = P1 , x1 ) | (P1 , x1 ) ∈ pre M1 }pre (ﬁx x.M ) = {(ﬁx x.P, x1 ) | (P, x1 ) ∈ pre M }pre ((M )) = {((P, x1 ) | (P, x1 ) ∈ pre M }Figure 2. Function pre for prefix relation
We use a usual ML-style type system with let-polymorphism
given in Figure 1, where we omit the case for (M ). As usual wewrite Γ . M : τ for a type judgment that a term M has a type τunder a type environment Γ. A type environment is a mapping fromvariables to types. When we add a mapping from a variable x to a
type τ to a type environment Γ, we write Γ{x : τ }. We can obtainthe type of a variable x under a type environment Γ by Γ(x). Cls isa function that takes a type environment Γ and a type τ and returns∀α1 · · · αn . τ when F T V (τ ) \ F T V (Γ) = {α1 , . . . , αn }, where
F T V takes a type τ or a type environment Γ and returns a set offree type variables in it. Const is a set of types of constants.
As we mentioned in Section 1, we only use the program text
before the cursor position. In order to represent such an incomplete program text we introduce the following prefix of the corelanguage.
P::=|| λx.P | M P | (P
let x = M in P | let x = P | ﬁx x.P

Here we introduced a cursor node , which corresponds to thecursor position in the program being written. For simplicity weonly complete variable names and do not complete keywords orconstants, so the cursor node corresponds to a variable and does
not correspond to constants or any other constructs. Each of theprefix terms defined above ends with the cursor node . The cursor
node has as its attribute the (partial) spelling of a variable now
being input. The spelling may be an empty spelling, which we write². We may write the spelling as the subscript of the cursor node likef and ² when necessary.
Here we formally specify the prefix relation between P and M ,with the variable name being input at the cursor position, by thefunction pre in Figure 2. The function pre takes a term M andreturns all the prefix terms of M , each of which is paired with avariable name being focused on. Note that pre returns the empty
set for the case of constant c since we do not complete constants.
Note also that we do not complete the identifiers bound at function
abstractions or declarations, which is reflected in the definition

of pre. We show an example for pre. By applying pre to a term
(λabc. abc) 1, we obtain the following set.
{((λabc. ² , abc), ((λabc. a , abc),((λabc. ab , abc), ((λabc. abc , abc)}
The constant 1 is not included in this result since pre returns anempty set in the case of constant.
Now we are ready to specify the problem.
P ROBLEM 1 (Variable completion). Given a prefix term P and atype environment Γ, find a set V of variables such that ∀v ∈V, ∃M, ∃τ , Γ . M : τ, (P, v) ∈ pre M.
The set V of variables are the candidates to be popped up. Most
desirable answer to the problem is the largest set V of variables.
Actually our algorithm for solving the problem presented in thispaper gives the largest one. Note that in practical situations Γ
includes types of variables declared in libraries.
Let us see a simple example, where the following prefix term(partial program) P is given.
let xx = 1 in let xy = λx.λy.x y in let xz = λx.x in xyx

The above term corresponds to the situation where we are typing acharacter x at the cursor position. Suppose the type environment Γis ∅. Then candidates to be popped up have to be within their scope,so they must be some of the variables xx, xy, and xz. Among thesevariables, xy and xz satisfy the condition while xx does not. So
the largest set is {xy, xz}. To be concrete, the types of these threevariables are int, ∀αβ. (α → β) → α → β, and ∀α. α → α,
respectively. The cursor node x is immediately after the variable
xy, so every candidate becomes the argument of the function xy.
By typing constraint the variable xx is excluded.
Here let us see another example, where the following prefix term
P is given.
ﬁx xf.λxx.+ (xf (- xx 1)) (xfxThis term P corresponds to the situation where we are in the middleof writing the definition of a recursive function. We suppose again
the type environment Γ is ∅. There are two variables, xf and xx,
which are in the scope at the cursor position. The types of xf andxx are int → int and int respectively. In this case the type of thecandidates must be int since the function xf takes as its argument
an expression (- xx 1) of type int. So the largest set is {xx}.

the term. Then we do type inference for each of the terms. In type
inference we assign a fresh type variable for the cursor node andfresh type variables for dummy nodes. For each term for which type
inference succeeds, we enumerate the variables that are within theirscope and then unify each of them with the type of the cursor node.
We filter all variables for which the unification succeeds, and obtain
those variables whose prefixes match the characters currently being
typed.
Here we illustrate the naive solution by using the following
simple term P .
let ff = λx.+ x 1 in ff ( fFirstly we generate the terms each of which has the above term as
its prefix, using dummy nodes. The above term with completing aclosing parenthesis is one of the generated terms. In type checking
we assign some fresh type variable α for the cursor node f . As aresult we obtain α = int. In this case ff is the only variable thatis within its scope. Since ff has type of int → int, there is no
candidate in this case.
There is another possible term, which is the above term withff ( f replaced by ff ( f [ ]). Here [ ] indicates a dummy node,
which represents an arbitrary term that can be an argument of
the function application. In type checking we assign fresh typevariables α and β for f and [ ] respectively, and obtain α = β →int. In this case the type of ff matches against the type of f , so
ff remains to be a candidate, which finally becomes a candidate to
be popped up by checking ff has f as its prefix.
There are many other possible terms by adding function applications. One of such examples is the above term with ff ( f replaced
by ff ( f [ ] [ ]). In this case the type of the cursor node becomesα → β → int, which does not match with the type of ff.
There are actually infinitely many possible terms even by using
dummy nodes since the programmer can write infinitely many
expressions as arguments of function applications after the cursor
position. So we used some threshold with respect to the depth of theterms and thus we may not necessarily obtain all the candidates.
We actually have implemented a system based on this naive
solution, but it took much time (e.g., 100 seconds) in some casesand does not even necessarily generate all the candidates. So we
considered how to overcome these two points. We show the outlineof the solution we have reached in Section 3.2.
3.2

3.

Basic ideas

Here we show basic ideas for solving the variable completion problem. Following the problem specification, if we could generate all
the terms of M having P as their prefix, then by type inference we
could solve the problem. But obviously there are infinitely many
terms M . In order to reduce the number of terms generated, we
introduce the notion of dummy node. We then give a naive preliminary solution based on this notion, which may take much timeand does not necessarily produce all the candidates. By introducing
another notion of marked node, we reached our current solution,
which produces all the candidates in time short enough to be usedpractically (see Section 9 for results of measuring time for completion).
3.1

A preliminary solution

Here we introduce the notion of dummy node. In other words, we
generate terms of M that additionally have as its constructs thedummy node and cursor node. A dummy node is a placeholder for
an arbitrary term. If we could generate all the terms using dummy
nodes, we could solve the problem. But even by using dummy
nodes there are still infinitely many terms to generate. So we had touse some threshold with respect to some criteria, e.g. the depth of

Our solution

By introducing another notion of marked node, which represents
conceptually zero or more function applications with dummy nodes
given as its arguments, we developed a solution that generates all
the candidates without generating infinitely many terms. In thefollowing, we illustrate our solution by the example above.
Since any expression can take an argument syntactically, thepreliminary solution complemented a dummy node for each subterm. As a result there appeared a sequence of function applications
with dummy nodes. Our idea is that this sequence can be abstracted
by marking such nodes. For the above example our new algorithm
constructs the following term by marking the nodes that can takean argument syntactically.
(let ff = λx.+ x 1 in (ff ( f ∗ ))∗ end)∗
Nodes with asterisk ∗ are marked nodes. For example, f ∗ represents f , f [ ], f [ ] [ ], f [ ] [ ] [ ], and so on, and (ff ( f ∗ ))∗represents ff f , ff ( f [ ]), ff f [ ], ff ( f [ ]) [ ], and so on.
The type of the variable ff is int → int, which is not influenced
by whatever the nodes with the asterisk ∗ represent. Since the variable ff is the only variable that is within the scope at the cursor
position, the possible types of f ∗ should be the possible types offf∗ . Since the type of ff is int → int, possible terms represented

cmp : P → D
cmp
cmp (λx.P )cmp (M P )cmp (let x = M in P )cmp (let x = P )cmp (ﬁx x.P )cmp ((P )

=
=
=
=
=
=
=

λx.(cmp P )∗(M (cmp2 P ))∗(let x = M in cmp P end)∗(let x = cmp P in [ ] end)∗
ﬁx x.(cmp P )∗(cmp P )∗cmp2 : P → D
cmp2
cmp2 (let x = M in P )cmp2 (let x = P )cmp2 ((P )

=
=
=
=

(let x = M in cmp P end)(let x = cmp P in [ ] end)
cmp P

∗

Figure 3. Term completion function cmp
by ff∗ are either ff or ff [ ] in order for the term to be well typed.
The type of f ∗ must be int since f ∗ is in the argument positionof the variable ff. So f ∗ can only take the form of ff [ ]. The typeof (ff ( f ∗ ))∗ must be int since the type of ff ( f ∗ ) is int. As aresult, ff becomes the candidate in this example.
Based on this idea we develop an algorithm for the variable
completion in the following sections. The algorithm generates all
the candidates and runs substantially faster than the preliminary
naive solution.

The algorithm V takes a pair of a term D and a type environment
Γ and returns a set of tuples of a substitution, a type, and a pair oftype environment and type of the cursor position. A substitution is afunction from type variables to types. A substitution may be applied
to types or type environments by natural extension. We use C as ameta variable for representing a pair of type environment and typeof the cursor position and S as a meta variable for representing asubstitution.
Our algorithm uses Milner’s W as a subroutine in the cases offunction application M D and let expression let x = M in D end.
The algorithm W takes a type environment Γ and a term M as its
arguments and returns a substitution S and a type τ . When W succeeds the judgment S(Γ) . M : τ holds. We omit the definition of
W. The algorithm V uses the unification algorithm U [22] in thecase of function application and fix expression, as is also the casefor W. The algorithm U takes a set of pairs of type expressions andreturns one of the most general unifiers when they are unifiable andfails when they are not.
V is different from W in the following points.
• The terms given as the argument include the mark, dummy, andcursor node.
• The algorithm W returns a pair of a substitution and a typewhile the algorithm V returns a set of tuples of a substitution, atype, and a pair of the type environment at the cursor position
and a type of the cursor position.

• We have not written explicitly in the algorithm V the cases

4.

Term completion with dummy nodes andmarked nodes

As the first phase of the algorithm, we generate terms that have as
their prefix the given partial term P by using dummy nodes andmarked nodes. We call this generation phase as term completion.
We define terms that include dummy nodes and marked nodes asfollows.
| D∗ | λx.D | M D | let x = D in [ ] end
D ::=| let x = M in D end | ﬁx x.D
We omit the parentheses here since terms of D are already completed by dummy nodes [ ].
We define a term completion function cmp from P to D in
Figure 3. Although we are manipulating abstract syntax we would
like to treat it in a way consistent with the concrete syntax. So we
introduce the function cmp2 to exclude the outer most mark in theargument part of the function applications, since otherwise function
applications would become right associative, which violates theconvention of lambda notations. Note that cmp2 does not take
λx.P or M P since such cases do not occur according to theconvention in describing lambda terms. Also note that the result ofcmp (λx.P ) is not (λx.(cmp P ))∗ since an expression input after
P becomes part of the body of the lambda abstraction according to
the convention in describing lambda terms.
We illustrate the function cmp by using an example. Suppose
the following term P is given.
let xa = λx.x 2 in let yy = λx.x in let xc = 3 in xa ( xBy applying cmp to this, we obtain the following term D.
(let xa = λx.x 2 in (let yy = λx.x in(let xc = 3 in (xa ( x ∗ ))∗ end)∗ end)∗ end)∗

5. Type inference
In this phase we do type inference to obtain types of the variables
and the cursor node. Our type inference algorithm V, defined in
Figure 4, is based on Milner’s type inference algorithm W [18].

where some unification fails, as is usual in the description of
the algorithm W. Unlike W, when some unification fails, theentire algorithm V does not fail but just eliminates the casewhen taking union of the results.
A term D that includes marked nodes, dummy nodes, or a cursor
node conceptually represents multiple terms of M . The type inference algorithm V instantiates each occurrence of the three constructs in an appropriate way to cover all the cases, so that V returns
multiple results. The cursor node conceptually represents all thevariables that are within their scope with the types constrained by
the contexts. So for the case of the cursor node , V enumerates all
the variables in the domain of Γ. As for arity and g, we explain later.
A marked node D∗ conceptually represents zero or more function
applications with dummy nodes given as its arguments. So for thecase of D∗ , V computes all the types taken from the right spine of
the types of D, that is, at(τ ) where τ is a type of D. The dummy
node [ ] conceptually represents all the terms and can thus have any
type depending on the context, so fresh type variables are generated
for the dummy node in the case of let x = D in [ ] end.
In order to reduce the number of elements in the result of type
inference, the algorithm V abstracts their types τ1 → · · · → τk ,where τk is int or a type variable, into α1 → · · · → αk where
α1 , . . . , αk are fresh type variables. This is done by the functions
arity and g. The function arity takes a type τ and counts the numberof arguments, or arity, in τ . For example, arity (int → int → int)
results in 2. The function g takes n as its argument and generates atype that consists of n + 1 fresh type variables connected by thearrows. For example, g(2) results in a type α0 → α1 → α2 ,where α0 , α1 , and α2 are distinct fresh type variables. Using thefunctions arity and g the algorithm V groups types of variables thatare within their scope at the cursor position into equivalence classes
with respect to the arity. This makes computations about functions
that have the same arity be performed at once. Since in typical cases
functions take a few arguments, this abstraction effectively works
for reducing redundant computations. The precise computation isdelayed until the filtering phase in Section 6.

V(Γ, D) = case D of
⇒ let T = {g(arity(Γ(x))) | x ∈ dom(Γ)} in {(∅, τ, (Γ, τ )) | τ ∈ T }| D∗ ⇒ {(S, τ 0 , C) | (S, τ, C) ∈ V(Γ, D), τ 0 ∈ at(τ )}| λx.D ⇒ let {(S0 , τ0 , C0 ), . . . , (Si , τi , Ci )} = V(Γ{x : α}, D) (α fresh)in {(S0 , S0 (α) → τ0 , C0 ), . . . , (Si , Si (α) → τi , Ci )}| M D ⇒ let (S1 , τ1 ) = W(Γ, M ){(S2,0 , τ2,0 , C2,0 ), . . . , (S2,i , τ2,i , C2,i )} = V(S1 (Γ), D)
S3,j = U{(S2,j (τ1 ), τ2,j → αj )} (αj fresh) (j ∈ {0, . . . , i})in {(S3,j ◦ S2,j ◦ S1 , S3,j (αj ), C2,j ) | j ∈ {0, . . . , i}}| let x = D in [ ] end ⇒ let {(S0 , τ0 , C0 ), . . . , (Si , τi , Ci )} = V(Γ, D)
in {(S0 , α0 , C0 ), . . . , (Si , αi , Ci )} (α0 , . . . , αi fresh)| let x = M in D end ⇒ let (S1 , τ1 ) = W(Γ, M ){(S2,0 , τ2,0 , C2,0 ), . . . , (S2,i , τ2,i , C2,i )} = V(S1 (Γ){x : Cls(S1 (Γ), τ1 )}, D)in {(S2,j ◦ S1 , τ2,j , C2,j ) | j ∈ {0, . . . , i}}| ﬁx x.D ⇒ let {(S1,0 , τ0 , C0 ), . . . , (S1,i , τi , Ci )} = V(Γ{x : α}, D) (α fresh){S2,0 , . . . , S2,i } = U(τj , S1,j (α)) (j ∈ {0, . . . , i})in {(S2,j ◦ S1,j , τj , Cj ) | j ∈ {0, . . . , i}}arity(∀α1 . . . αn .τ )arity(τ1 → τ2 )arity(α)
arity(int)

=
=
=
=

at(τ1 → τ2 ) = {τ1 → τ2 } ∪ at(τ2 )
at(α)
= {α}
at(int)= {int}g(n + 1) = α → g(n) (α fresh)g(0)= α (α fresh)arity(τ )arity(τ2 ) + 1
0
0

Figure 4. Type inference algorithm V
The second element of the result for the case of D∗ is the set of
all types that are taken from the right spine of the type of D. This
reflects the situation where the production M := M1 M2 could
be applied arbitrarily many times in the term completion phasewithout using the notion of marking.
In the algorithm V we do not apply substitution to the environments and types of the cursor position while traversing the term,
but apply it to the result of the algorithm V. The environments andtypes at the cursor position are obtained as follows: in each tuple(S, τ, (Γ , τ )) in the results of V(Γ, D), apply the substitution S
to Γ and τ , respectively.
Let us see an example. Let D be the result of term completionin Section 4. In the following we show the process of computingV(∅, D). The type environment given to V can be empty since theterm D does not have free variables. When V encounters the cursor
expression f , the type environment Γ for the cursor position has
been obtained as follows.
Γ={xa : ∀α.(int → α) → α, yy : ∀α.α → α, xc : int}

The algorithm V returns the following set of two tuples when it
encounters the cursor expression x .
{(∅, β1 → β2 , (Γ , β1 → β2 )), (∅, β3 , (Γ , β3 ))}By taking all the types from the right spine of each of the above two
types β1 → β2 and β3 , V returns the following set of three tuples
for x ∗ .
{(∅, β1 → β2 , (Γ , β1 → β2 )), (∅, β2 , (Γ , β1 → β2 )),(∅, β3 , (Γ , β3 ))}Next, when V processes xa ( x ∗ ) the following unifications aretried:
S1 = U{(int → α0 ) → α0 , (β1 → β2 ) → γ1 )}S2 = U{(int → α1 ) → α1 , β2 → γ2 )}S3 = U{(int → α2 ) → α2 , β3 → γ3 )}where the types (int → αi ) → αi (i = 0, 1, 2) are instantiatedtypes of the function xa. These instantiations are done in the function W. All the unifications succeed and V returns the following

set of three tuples for xa ( x ∗ ).
{(S1 , α0 , (Γ , β1 → β2 )), (S2 , α1 , (Γ , β1 → β2 )),(S3 , α2 , (Γ , β3 ))}Eventually these three tuples become the results of V(∅, D). Asa final step, we apply S1 , S2 and S3 to β1 → β2 , β1 → β2 andβ3 and obtain types int → α0 , β1 → int → α1 , and int → α2
respectively, for the cursor. Similarly by applying S1 , S2 and S3 toΓ we obtain Γ as the type environment for the cursor position.
Note that all the first elements of the third elements in the tuplesof the result of the algorithm V are the same. We show filtering forthis example in the next section.

6. Filtering candidates
In this phase we make the candidates to be shown in pop-up window. The initial candidates are taken from the variables in the domain of the type environment Γ obtained in the type inference
phase. They are filtered by unifying their types with the types of
the cursor. Variables that failed to unify with any of the types of the
cursor are deleted from candidates. When a candidate has a type ofτ , we unify τ with each of the types of the cursor. When a candidate has a polymorphic type of ∀α1 . . . αk .τ , we unify the type of[β1 /α1 ] . . . [βk /αk ]τ (β1 , . . . , βk fresh) with each of the types of
the cursor. Note that all of the types of the cursor are monomorphic. We finally filter the candidates by matching the spellings ofthe candidates with the (partial) spelling of the variable name being
input.
We show an example for filtering candidates by using the resultof type inference in Section 5. Candidates must have a type that is
unifiable with int → α0 , β1 → int → α1 , or int → α2 . There
are thus the following nine combinations.
U{(int → α0 , (int → α5 ) → α5 )}, (for xa)
U{(int → α0 , α6 → α6 )}, (for yy)
U{(int → α0 , int)}, (for xc)
U{(β1 → (int → α1 ), (int → α5 ) → α5 )}, (for xa)
U{(β1 → (int → α1 ), α6 → α6 )}, (for yy)
U{(β1 → (int → α1 ), int)}, (for xc)

U{(int → α2 , (int → α5 ) → α5 )}, (for xa)
U{(int → α2 , α6 → α6 )}, (for yy)
U{(int → α2 , int)} (for xc)

start
exp
appexpThe second, the fourth, the fifth and the eighth unifications succeed. As a result we get two candidates xa and yy. Among thesecandidates the variable xa matches with the (partial) spelling x ofthe variable name currently being input while yy does not. So we
obtain the singleton set {xa} as the final candidate set.
There is another alternative about when filtering the candidates
with the spelling of the variable name being input: to filter themin the first step. In the future we may incrementalize the variable
completion system by caching the intermediate results of the computation. When we accomplish this, matching in the last step may
effectively work in such cases where the programmer erases the last
character of a variable name being input.

atexp

dec
decseqvalbind

:=
:=
|
:=
|
:=
|
|
|
:=
:=
|
:=
|

exp
appexpfn id => exp
atexp
appexp atexp
id
const
(exp)
let decseq in exp endval valbinddec decseq²
id = exp
rec id = exp

(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
(12)
(13)
(14)

Figure 5. Concrete syntax for the core language

7.

Properties of the algorithm
startP
expP

Here we summarize the algorithm and give some statements about
the properties of the algorithm. The algorithm for solving Problem
1 can be summarized as follows.

appexpP

A LGORITHM 1. Let {(S0 , τ00 , (Γ , τ0 )), . . . , (Si , τi0 , (Γ , τi ))}= V(Γ, cmp P ) and s be the spelling of the cursor node s in P .
Then compute the set V of variables as follows.
V =[j∈{0,...,i}

n˘

atexp

x ∈ dom(Γ ),¯ox | s is a prefix of the spelling of x,
U{((Sj (Γ ))(x), Sj (τj ))} succeeds

decP
decseqP

We expect Algorithm 1 satisfies the following two properties.

valbindPP ROPERTY 1 (Soundness). The set V of variables obtained by
the algorithm satisfies the condition in Problem 1. That is, ∀v ∈V, ∃M, ∃τ , Γ . M : τ, (P, v) ∈ pre M.
P ROPERTY 2 (Completeness). Any variable that satisfies the condition in Problem 1 is included in the set V of variables obtainedby the algorithm. That is, if ∃M, ∃τ , Γ . M : τ, (P, v) ∈ pre M ,then v ∈ V .
Properties 1 and 2 are our conjectures. As far as we have tried
we have found no counterexample to the above two properties. The
soundness property assures that all the unnecessary candidates are
eliminated with respect to the typing constraint. By having thisproperty the length of the list of candidates substantially decreases
when there are many candidates without considering typing constraint. The completeness property is considered to be rather important in variable completion since programmers strongly expectthat the variable they are trying to recall should be shown in thecandidates. Having both properties makes the variable completion
system really suitable for practical use.

8. Implementation
Based on our approach we have developed an Emacs mode called
lambda-mode that provides variable name completion for a small
subset of the Standard ML on Emacs. Lambda-mode is available
on our web site http://www.cs.ise.shibaura-it.ac.jp/
lambda-mode/. In this section we describe our implementationof lambda-mode. The variable name completion consists of thephases of computing the candidates and interacting with users, forwhich we give details in the followings. As for the filtering phase,
it is implemented by following exactly what we have presented in
Section 6.

:=
:=
|
:=
|
:=
|
|
|
:=
:=
|
|
:=
|

expP
appexpP
fn id => expP
atexpPappexp atexpP(expP
let decseq in expP
let decseqPval valbindP
dec decseqP
decP²
id = expP
rec id = expP

Figure 6. Prefix syntax for the core language
8.1

Core language

We have implemented the lambda-mode for the core language
given in Figure 5, which is a subset of Standard ML. An expression
fn x => exp corresponds to a function abstraction λx.M for someM . A recursive function declaration val rec f = exp corresponds
to a declaration f = ﬁx f.M for some M .
The tokens for the core language are as follows.
let, id, val, rec, in, end, =, =>,fn, (, ), const, ws, EOF
The tokens in type writer font correspond to the string of their own
spellings. The token id is for variable names with the spelling as
its attribute, const is for constants with the value as its attribute,
ws is for whitespace, and EOF is for representing the end of thesequence of tokens input to the parsing phase. More concretely, thetoken id is for sequences of capital and small alphabets, const isfor sequences of numbers from 0 to 9 that start with numbers from
1 to 9 and for the operators + and -, and ws is for tabs, spaces, andnew line characters. The sequence of numbers have type of int, theoperators have type of int → int → int.
8.2

Lexical analysis

The lexer reads all the program text until the character being justtyped. We have implemented it by moving the cursor to the position
immediately before the token being input and restoring the cursor
position after the parsing. We do not move the cursor in the casethe programmer input tabs, spaces, and new line characters. Whenthe lexer reaches the cursor position, the lexer returns an id token

with the information being in the cursor position and memorizes
the next token to return is EOF. We memorize the spelling of thetoken in the middle of typing and use it in the final filtering phase.
In the following we write the token as id .
8.3

Parsing

After lexical analysis, we do parsing to make a partial term P .
In order to parse programs up to the cursor position, we made a
concrete syntax for the prefix programs of the core language. We
give the syntax for the prefix programs in Figure 6. Currently, we
manually make the syntax for the prefix programs from the concrete
syntax for the core language in Figure 5. The parser produces aprefix term P as a result of parsing. After obtaining a prefix term
P , we proceed with exactly following the method we described in
the previous sections.
We wrote the parser for the prefix programs fully in Emacs Lisp
with the state transition table produced by applying a parser generator kmyacc [7], which is compatible with yacc, to a description of
the syntax in Figure 6 with actions to construct a prefix term P .
We illustrate the parsing phase by using the following example.
let val ff = fn x => + x 1 in ff (f_By parsing the above prefix program, we obtain the following prefix
term P .
(let ff = λx.+ x 1 in (ff ( ∗f ))∗ )∗There is one thing to note about the syntax of Standard ML.
In Standard ML the right hand side of val rec declaration must
be a function abstraction by the definition of the language [19].
When parsing val rec declaration, we check whether or not theright hand side of val rec declaration is a function abstraction. By
the definition, it is allowed to (meaninglessly) parenthesize the righthand side of the val rec declaration like the following example.
let val rec f = (((fn x => f x))) in f 2 end
Although the parentheses are ignored in parse trees in general,
we have to take into account the parentheses not yet closed. For
example, let us consider the situation where we are inputting theargument x in the above example.

Generally the complexity of the type inference algorithm V is
exponential with respect to the number of mark nodes. But actually
the mark nodes introduced by the nested let expressions obtainedby the transformation do not increase the complexity exponentiallybecause the computation corresponding to each of the mark nodes
produces the same tuples as the input ones. Here the computation
for the case of D∗ once divides the types into their right spines andthen makes the set union operations on them, producing the same
set as the input one.
The former approach has the same approximate complexity as
the latter approach, but the former approach unnecessarily divides
the types and makes the set union operations. In order to avoid theredundant computation, we take the latter approach. We replace
the cases for let expressions in the algorithm V in Figure 7. We
modified V by replacing the cases for let expressions with thecases let x1 = M1 , . . . , xn = Mn , xn+1 = D in [ ] end andlet x1 = M1 , . . . , xn = Mn in D end. We convert the completed
concrete syntax trees to a term D with the above modification
before entering the type inference phase.
There is one thing to note about the type inference. Standard
ML has value restriction [24], which we need to take into accountin the future. The core language does not have side effect, so we do
not check value restriction in the current implementation.
8.5

User interaction

We utilize an Emacs mode called auto-complete mode [5] forinteracting with users. The auto-complete mode calls some function
for computing candidates to pop up each time the programmer
types a character. If there are some candidates then the mode
displays them in a pop-up window. In this case the programmer
either select a candidate or proceed on inputting next characterswithout selecting any candidate. If there are no candidates thenthe mode does nothing. Our implementation of the lambda-mode
utilizes the auto-complete mode with providing a function that iscalled every time a character is typed to return the candidates. We
show a screen shot of the lambda-mode in Figure 8, which is taken
when the programmer has just typed the character x.

let val rec f = (((fn x => f _In order to allow this kind of cases, the parser checks the constructed prefix term for the right hand side of the val rec declaration to allow arbitrarily many open parentheses before the function
abstraction.
8.4

Type inference

The concrete syntax of the subset is almost same as the core language M , except for that let expressions may have one or more declarations decseq. There are two alternative approaches to handle let
expressions having decseq. One is to convert them into nested let
expressions and use the type inference the algorithm V. The otheris to replace the cases for the let expressions in the algorithm V. We
take the latter approach.
In the former approach, a let expression
let val ff = fn x => + x 1
val yy = 3 in f y_
is transformed into a nested let expression. By parsing and termcompletion on the obtained prefix term P , we obtain the following
term D.
(let val ff = λx.+ x 1 in(let val yy = 3 in(f ( y ∗ ))∗ end)∗ end)∗
As seen in the above, the term completion introduces a mark nodefor each partial let expression in the input partial expression P .

Figure 8. A snap shot of the lambda-mode

9. Experimental results
In usual cases the lambda-mode shows the candidates immediately
after the programmer types a character. Since we do not have reallarge programs of the core language, we measured the time forextreme programs automatically generated.
The time is measured from when the programmer typed a key
until when candidates are displayed. The environment in measuring
the time is as follows: CPU is Intel Core i7 920, the size of memory
is 6GB, OS is Windows 7 Home Premium 64bit, and emacs isV(Γ, D) = case D of...
| let x1 = M1 , . . . , xn = Mn , xn+1 = D in [ ] end ⇒let (S1 , τ1 ) = W(Γ, M1 )(S2 , τ2 ) = W(S1 (Γ){x1 : Cls(S1 (Γ), τ1 )}, M1 )...
(Sn , τn ) = W(Sn−1 ◦ · · · ◦ S1 (Γ){x1 : Cls(S1 (Γ), τ1 ), . . . ,xn−1 : Cls(Sn−1 ◦ · · · ◦ S1 (Γ), τn−1 )}, Mn ){(Sn+1,0 , τn+1,0 , C0 ), . . . , (Sn+1,i , τn+1,i , Ci )} = V(Sn ◦ · · · ◦ S1 (Γ), D)
in {(Sn+1,0 , α0 , C0 ), . . . , (Sn+1,i , αi , Ci )} (α0 , . . . , αi fresh)| let x1 = M1 , . . . , xn = Mn in D end ⇒let (S1 , τ1 ) = W(Γ, M1 )(S2 , τ2 ) = W(S1 (Γ){x1 : Cls(S1 (Γ), τ1 )}, M1 )...
(Sn , τn ) = W(Sn−1 ◦ · · · ◦ S1 (Γ){x1 : Cls(S1 (Γ), τ1 ), . . . ,xn−1 : Cls(Sn−1 ◦ · · · ◦ S1 (Γ), τn−1 )}, Mn )in V(Sn ◦ · · · ◦ S1 (Γ){x1 : Cls(S1 (Γ), τ1 ), . . . ,xn : Cls(Sn ◦ · · · ◦ S1 (Γ), τn )}, D)
Figure 7. The cases for the let expressions having the sequence of the declarations in the modified type inference algorithm V
Meadow (GNU Emacs 22.2.1), although this kind of rather highspec machine is not necessarily required.
We tested for the extreme cases where let expressions havevarious numbers of declarations and some constructs such as let
expressions, function abstractions, and parentheses have various
depth of nesting. We show the case for let expressions with various
numbers of declarations in Table 1, which is typical in functional
languages. We typically write a sequence of many declarations, say
30 declarations, in one let expression.
The time complexity of our algorithm increases exponentiallywith respect to the depth of the nesting of let expressions, function
abstractions, and function applications including the cursor node.
The depth of the nesting of function abstractions, function applications, and let expressions is usually small and it is practicallyregarded as constant. Let expressions typically have a sequence of
declarations, in which case the time complexity does not increase
exponentially as mentioned in Section 8. In Table 1 we show thetime for computing candidates for let expressions having 10, 30,
and 50 declarations. In Table 1, the column “Constant” shows thecases where all declarations have different names in the left handside and constant 1 in the right hand side. “Various” shows the cases
where all declarations have different names in the left hand side andvarious expressions of various types in the right hand side. We haveincluded the programs used in the experiment in the archive file oflambda-mode.
One thing to note is that there are many declarations in external
libraries but ordinary type inference can be applied to them inadvance. In the future we are planning to extend our variable namecompletion system to deal with external libraries.

Table 1. Comparison of completion time for let expressions withvarious numbers of declarations

The number ofdeclarations

10
30
50

Time(millisec)
Constant Various
12
28
30
93
54
218

10.

Related work and discussions

Variable name completion, more generally identifier completion,
has naturally arised from practically used IDEs such as Eclipse.
Currently many IDEs support identifier completion. We begin bysummarising the current status of major IDEs supporting identifiercompletion in Section 10.1. We then discuss two aspects of ourwork, type inference and term generation, in Section 10.2 and 10.3
respectively, in comparison with several other studies. There is few
academic research directly concerning identifier completion andactually as far as we know there is just one such work [21], about
which we discuss in Section 10.4. Finally we make a remark about
identifier completion for object oriented languages in Section 10.5.
10.1

Identifier completion in major IDEs

Here we summarize the current status of major IDEs that provide
the functionality of identifier completion. They use various engines
for identifier completion. Some of them simply compute candidates
based on words that have been input in the current file. Some ofthem compute candidates based on identifiers that have been defined in some other modules or classes which were already compiled. Some of them are more intelligent: Intellisense in Visual
Studio, omni completion in vim, and content assist [2] in Eclipse
plugins for various languages. They try to give the candidates that
fit in the context of editing program. For example intellisense andcontent assist take into account the scope of the variables. Although
they are becoming more convenient, as far as we know, none ofthem filter the candidates by their types in languages with type inference.
In the following we describe individual IDEs with respect tothe intelligence of engines for completion. First of all, there aremany IDEs with no support for identifier completion. Such IDEs
for functional languages include OCaml Development Tools [9],which is an Eclipse plugin for OCaml, and Caml mode [1] andtuareg mode [11], which are Emacs modes for editing Caml andOCaml code.
Some IDEs use engines that compute the candidates only frompackages. Such IDEs include Java Development Environment for
Emacs (JDEE) [6] which is an Emacs mode for Java, Eclipse FP[4] which is an Eclipse plugin for Haskell, and Leksah [8] which
is an IDE for Haskell. JDEE complete the member names only incompiled classes, and Leksah and Eclipse FP complete the function
and type names in packages. These IDEs do not complete names

declared in the current buffer not yet compiled, and hense cannot
complete local variable names without compilation. JDEE partiallytakes into account the syntactic context of the cursor position suchas the cases where the cursor is following dot, while Leksah does
not.
More intelligent identifier completion engines are used in Visual
F#, Visual C++, Visual C#, and Eclipse plugins for C++ and Java.
They take into account the syntactic context of the cursor position
to some extent. They show the candidates only when an expression
can appear in the cursor position. They also consider the scope ofvariables.
The IDEs listed above which have variable completion functionality allow completion of identifiers that do not satisfy the typing
constraint. In contrast, our completion fully utilizes the types whenfiltering candidates and excludes the candidates that do not satisfy
the typing constraint.
As for typing information, Caml mode can show the type ofthe variable pointed by the cursor and show the location of its
declaration, provided that OCamlSpotter [10], a tool for generating
types and locations of the variables, processes the file including thedeclaration of the variable in advance.
10.2

Type inference

tried to handle a case where there is nothing unifiable in the library
but there may be some identifier that yields the desired type by taking an extra argument. Cosmo studied the problem of valid isomorphisms in ML-like languages with let polymorphism and provided
a complete and decidable characterization for it [13]. Our problem
is more general than the problems in their work in the sense thatin their problem a type is given as its input to find identifiers having its equivalent types while in our problem a context, i.e., partial
program text up to the cursor position, is given as its input to findidentifiers that fit in the cursor position with some (not yet input)
program text after the cursor position. Under the assumption that
Property 2 holds, our work covers all of these cases in this sense.
10.4

Variable name completion

Here we discuss a study directly concerning variable name completion. Robbes et al. [21] pointed out that finding the correct candidate from the pop-up window can be cumbersome or even slower
than typing the full name when using completion engines like content assist in Eclipse. In order to solve this problem they limit the
number of the candidates so that the programmer can select a candidate quickly. They made some assumptions that programmers arelikely to use methods they have just defined or modified and that
local methods are called more often than the ones in other packages. Based on these assumptions they developed an algorithm tocompute the candidates by using history of program editing. They
claim that the candidates computed by their algorithm include thecandidate the programmer is looking for with high probability. Ouralgorithm computes all the type-correct candidates while their algorithm may not.

There have been some studies concerning type inference for incomplete programs, some of which we discuss in the followings.
Haack et al. [14] presented an approach to identifying the setof program points (a slice) that causes a type error in implicitly
typed languages like Standard ML. They identified the criteria ofcompleteness and minimality for type error slices and presented
algorithms for finding complete and minimal type error slices. In
this paper we assume that the input programs before the cursor
position do not have any type error. When in the future we allow
programs to have some type errors we might utilize their work toeliminate variables related to the type error from the candidates.
Lerner et al. [17] presented an approach to producing bettertype-error messages for languages with type inference such as
OCaml and C++. They generate well-typed programs from an illtyped program by replacing a program fragment that causes thetype error with a “wildcard” expression, which plays the same role
as a dummy node in this paper. As well as the work by Haack et
al. [14], this work might be utilized to cope with programs with
type error by replacing the fragments that cause the type error withdummy nodes.

Let us remark about completion of identifiers in object oriented
languages. Let us suppose we have typed some identifier for some
object in object oriented languages like C++ and Java. When theobject has some member variables or member functions, the identifier can be followed by a dot and the names. This can be made intoa chain so that we can obtain various types of expressions. Alternatively speaking, functional and object oriented languages apply
functions in reverse order: in an object oriented language, we give aparameter like “this” firstly, and then name the function (method),where in functional languages it’s the other way around. So in object oriented languages filtering by types may not be effectively
applied.

10.3

11. Conclusions and future work

Term generation

There have been some studies concerning term generation, some ofwhich we discuss in the followings.
Hashimoto [15] constructed an ML-style programming language with first-class contexts, i.e., expressions with holes. Holes
correspond to dummy nodes in this paper, but his language has theoperation for filling holes as a language construct while ours does
not.
Some tools have been developed for generating terms undertype constraint. One is Djinn [3], which generates a term having
a given type, and another is to generate a minimum term having agiven type [16]. In these tools a type is given for generating terms
while in our variable name completion system, given a prefix term,
we generate a term having dummy and mark expressions without
being given a type.
Rittri [20] developed a method to search for an identifier in a
program library by using types as search keys, regarding isomorphic types under some equivalence relation, considering argument
permutation and the currying-uncurrying, as the same one. Runciman et al. [23] independently developed a method for the sameproblem by regarding types that are unifiable as the same. They also

10.5

Remark about object oriented languages

In this paper we have presented an approach to completing variablenames for implicitly typed functional languages. We have specified
the variable completion problem in the simplest form and given
a solution to the problem. The key ideas of our approach werethe use of cursor and dummy nodes and insertion of marks. By
using these ideas we have successfully developed basic mechanismof variable name completion system, based on which we plan todevelop systems for real languages like Haskell, Standard ML,
OCaml, and so on. In order to extend our solution to cover theselanguages there are several things to overcome, which we leave as
future work.
• Computation of candidates processes the program text from the

beginning of the text to the cursor position whenever a characteris input, so many redundant computation may be performed. In
real program development, a program is divided in many files
each of which is not so large. What really matters is the timeto process the program in the file currently edited. In particular
we can compute necessary information in advance about theidentifiers declared in libraries. Moreover in the future we mayincrementalize the completion algorithm, which decreases thetime to compute the candidates. There is much work about thereuse of computation, so we expect they might be used for thereuse of intermediate results of parsing and type inference. For
example, as for the reuse of type inference, Aditya et. al. [12]proposed an incremental algorithm for type inference. His work
is to enable type inference to be performed in units of the toplevel declarations.
• When there is an error in the beginning of a program, the vari-able name completion does not work for the entire program
since we assumed that the program text before the cursor isgiven completely without any syntax error or type error. This
assumption is too strict, so we are planning to extend the completion algorithm to handle the programs having syntax errors
in some way similar to error recovery in parsing. As for the
programs having type errors, we discussed in Section 10.
• In order for our approach to scale up to the level of real lan-

guages, the completion algorithm has to cope with many constructs including mutually recursive function declarations, infix operators, pattern matching, modules, and type annotations.
We expect that pattern matching, type annotations, and modules should be naturally handled. We believe our framework
works well with infix operators by extending the meaning ofmarked nodes to include the application of infix operators aswell as usual prefix function applications. Note that infix operators have to be used syntactically together with the operands,
so we have only to consider the infix operators already declared
before the cursor node, except for those declared after the cursor position, which may be the case in mutually-recursive declarations or in Haskell-like languages. In this case we may haveto explicitly require users that the infix operators should be defined before their use. As for mutually recursive function declarations, we expect the usual type inference works with natural modifications. To be concrete, when encountering some
unknown identifiers, which may appear in mutually recursivefunction declarations, we simply assign a fresh type variable tothe unknown identifiers.
• In Haskell variables can be used before their bindings. In ML

languages variables can be used before their bindings in mutually recursive function definitions. Our framework is not directly applied to these situations since currently we do not use
the program text after the cursor position according to the problem specification. In the future we intend to overcome the situation by enlarging the problem specification.

Acknowledgments
We would like to thank the anonymous referees for many helpfulcomments and for pointing out the paper in ASE 2008.

References[1] Caml mode. http://www.emacswiki.org/emacs/CamlMode.
[2] Content assist.
http://help.eclipse.org/help32/index.
jsp?topic=/org.eclipse.platform.doc.isv/guide/
editors contentassist.htm.
[3] Djinn.
http://permalink.gmane.org/gmane.comp.lang.
haskell.general/12747.
[4] Eclipse FP. http://eclipsefp.sourceforge.net/.
[5] EmacsWiki: Auto complete.
emacs/AutoComplete.

http://www.emacswiki.org/[6] Java development environment for Emacs.
sourceforge.net/.

http://jdee.

[7] KMyacc. http://www005.upp.so-net.ne.jp/kmori/kmyacc/.

[8] Leksah. http://leksah.org/.
[9] OCaml Development Tools. http://ocamldt.free.fr/.
[10] OCamlSpotter.
http://jun.furuse.info/hacks/
ocamlspotter/.
[11] Tuareg mode. http://www-rocq.inria.fr/∼acohen/tuareg/
index.html.en.
[12] Shail Aditya and Rishiyur S. Nikhil. Incremental polymorphism. In
Proceedings of the 5th ACM Conference on Functional Programming
Languages and Computer Architecture, pages 379–405, Cambridge,
USA, 1991.
[13] Roberto Di Cosmo. Type isomorphisms in a type-assignment framework. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposiumon Principles of programming languages, POPL ’92, pages 200–210,
New York, NY, USA, 1992. ACM.
[14] Christian Haack and J. B. Wells. Type error slicing in implicitly typed
higher-order languages. Science of Computer Programming, 50:189–
224, 2004.
[15] Masatomo Hashimoto. First-class contexts in ML. In Asian Computing Science Conference, volume 1538 of Lecture Notes in Computer
Science, pages 206–223. Springer, 1998.
[16] Susumu Katayama. Systematic search for lambda expressions. In
Trends in Functional Programming, pages 111–126, 2005.
[17] Benjamin Lerner, Matthew Flower, Dan Grossman, and Craig Chambers. Searching for type-error messages. In PLDI ’07: Proceedingsof the 2007 ACM SIGPLAN conference on Programming Language
Design and Implementation, New York, NY, USA, 2007. ACM Press.
[18] Robin Milner. A theory of type polymorphism in programming.
Journal of Computer and System Sciences, 17(3):348–375, 1978.
[19] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The
Definition of Standard ML (Revised). The MIT Press, 1997.
[20] Mikael Rittri. Using types as search keys in function libraries. In
Proceedings of the fourth international conference on Functional programming languages and computer architecture, FPCA ’89, pages
174–183, New York, NY, USA, 1989. ACM.
[21] Romain Robbes and Michele Lanza. How program history can improve code completion. In Proceedings of the 2008 23rd IEEE/ACM
International Conference on Automated Software Engineering, ASE’08, pages 317–326, Washington, DC, USA, 2008. IEEE Computer
Society.
[22] John A. Robinson. A machine-oriented logic based on the resolution
principle. Journal of the ACM, 12(1):23–41, 1965.
[23] Colin Runciman and Ian Toyn. Retrieving re-usable software components by polymorphic type. In Proceedings of the fourth international
conference on Functional programming languages and computer architecture, FPCA ’89, pages 166–173, New York, NY, USA, 1989.
ACM.
[24] Andrew Wright. Simple imperative polymorphism. LISP and Symbolic Computation, 8:343–355, 1995.