On-Demand Refinement of Dependent Types
Hiroshi Unno1 and Naoki Kobayashi2
1

University of Tokyo, uhiro@yl.is.s.u-tokyo.ac.jp
2
Tohoku University, koba@ecei.tohoku.ac.jp

Abstract. Dependent types are useful for statically checking detailed
specifications of programs and detecting pattern match or array bounds
errors. We propose a novel approach to applications of dependent types
to practical programming languages: Instead of requiring programmers’
declaration of dependent function types (as in Dependent ML) or trying
to infer them from function definitions only (as in size inference), we mine
the output specification of a dependent function from the function’s callsites, and then propagate that specification backward to infer the input
specification. We have implemented a prototype type inference system
which supports higher-order functions, parametric polymorphism, andalgebraic data types based on our approach, and obtained promisingexperimental results.

1

Introduction

Dependent types are useful for statically verifying that programs satisfy detailed
specifications and for detecting data-dependent errors such as pattern matchor array bounds errors. For example, the function λx.x + 1 is given a type
int → int in the simple type system, but with dependent types, it is given atype Πx : int.{y : int | y = x + 1}, so that we can conclude that the array
access a[(λx.x + 1) 0] is safe (if the size of array a is more than 1).
There are several approaches to introducing dependent types into programming languages. Size inference [1–3] fixes the shape of dependent types a priori(e.g., a list type is of the form τ listn where n is the length of a list), andtries to infer a dependent type of a function automatically from the function’s
definition. Shortcomings of that approach are inflexibility and inefficiency; forexample, it would be hard to infer that a sorting function indeed returns a sorted
list. Dependent ML (DML) [4, 5] lets users declare the dependent type of eachfunction manually, and checks whether the declaration is correct. A shortcomingof that approach is that it is often cumbersome for users to declare types for all
functions. For example, consider the following function isort for insertion sort,and suppose that one wants to verify that isort returns a sorted list.
fun insert (x, xs) = match xs with
Nil _ -> Cons(x, Nil ())| Cons(y, ys) -> if x <= y then Cons(x, xs) else Cons(y, insert (x, ys))
fun isort xs = match xs with
Nil _ -> Nil ()| Cons(x, xs’) -> insert (x, isort xs’)
Copyright(C) 2008 by Springer-Verlag. The original version is available at www.springerlink.com.

It would be fine to declare that isort returns a sorted list (because that is indeed
the property to be verified). It is, however, cumbersome to declare a dependent
type of the auxiliary function insert as well. Knowles and Flanagan [6] proposed
a complete type reconstruction algorithm for a certain dependent type system,
but the inferred types include fixed-point operators on predicates, so that theinferred types alone cannot be used for actual verification or bug finding (withouta reasonable algorithm for computing fixed-points).
We propose an alternative, complementary approach to the previous approaches discussed above. Instead of requiring programmers’ declaration of dependent function types or trying to infer them from function definitions only, we
infer a function’s type using information about not only the function’s definition
but also the function’s call sites. Another related, distinguishing feature of ourapproach is that types are refined on-demand ; we start with the simplest typefor each function, and refine the type gradually, when it turns out that more
precise type information is required by a call site of the function. For example,4
the function f = λx.x + 1 is first given a type int → int, but if a calling context
a[f y] is encountered, the type is refined to Πx : int.{y : int | y = x + 1} (sincefrom the calling context, we know that the actual return value of f is important
for the whole program to be typed). For another example, consider the sorting function isort above. The auxiliary function insert is first given a type
int list → int list. If the type of isort is declared as int list → ordlist(where ordlist denotes the type of sorted lists), however, we can find from thecall site insert (x, isort xs0 ) that the type of the output of insert should be
ordlist. We can then propagate that information backward to infer the typeof an argument of insert (see Section 5 for a more detailed description of thisrefinement step). In this manner, we expect that our approach can deal withmore flexible dependent types (without losing efficiency) than the size inference. Indeed, we have already implemented the prototype inference system andsucceeded in verifying the sorting function above.
The idea of on-demand type refinement mentioned above, so called type-errorguided type refinement, has been inspired from that of counter-example-guided
abstraction refinement (CEGAR) in abstract model checking [7]. In CEGAR,
the coarsest abstraction is first used for model checking; the predicates used for
abstraction are gradually refined when a false counter-example is encountered. In
our approach, simple types are first used for type-checking. If the type-checking
fails, types are gradually refined by inspecting a fragment of the program whichcauses the failure (until no further refinement is possible, when a type error isreported).
To formalize the idea mentioned above, Section 2 introduces a simple firstorder functional language with assert expressions and a dependent type system
for it. The assert expressions are used to model array bound checks and usersupplied specifications. Section 3 formalizes our type inference algorithm, andproves its soundness. In Section 4, we briefly discuss extension of the type inference algorithm to deal with higher-order functions, parametric polymorphism,
and algebraic data types. Section 5 reports on a prototype implementation ofour algorithm (for the full language, including higher-order functions, parametricpolymorphism, and algebraic data types) and experiments. Section 6 discusses
related work and Section 7 concludes.

2

Language and Dependent Type System

We use a call-by-value, first-order functional language to present our type inference algorithm. We extend the language with higher-order functions in Section 4.
The language is essentially an “implicitly-typed” version of a subset of DML [4, 5]
extended with assert expressions.
The syntax of the language is defined as follows:(expressions) e ::= x | n | (e1 , e2 ) | fun f x = e1 in e2 | f e| let x = e1 in e2 | let (x1 , x2 ) = e1 in e2| if e1 then e2 else e3 | assert e1 in e2(values) v ::= n | (v1 , v2 ) | fun f x = e
Here, x, n, and f are meta-variables ranging over a set of variables, integer
constants, and function names respectively. We write FV(e) for the set of freevariables in e. We assume given primitive operators such as +, ×, = and ≤ on
integers, and ¬, ∧, and ⇒ on booleans. Actually, booleans are represented byintegers (the truth > by a non-zero integer, and the false ⊥ by zero). Thus,
e1 ≤ e2 returns 1 if the value of e1 is less than or equal to that of e2 , and returns
0 otherwise. In the function definition fun f x = e1 in e2 , f may appear in e1
for recursive calls. However, we do not allow mutually recursive functions in thelanguage for the sake of simplicity. Our framework can be easily extended to deal
with mutually recursive functions. An assertion assert e1 in e2 evaluates to e2
only if the conditional e1 holds. Otherwise, it gets stuck. Assertions are used formodeling array bounds errors and user-supplied specifications. For example, thearray access a[x] is modeled as assert 0 ≤ x < h in · · ·, where h is the size ofa. See the full paper [8] for the operational semantics.
We introduce a dependent type system, which ensures that well-typed programs never get stuck. In particular, an assertion assert e1 in e2 is accepted
only if e1 is statically guaranteed to be non-zero. The type system is used tostate properties of our type inference algorithm in Section 3. The type system
is undecidable, since the constraint language includes integer addition and multiplication.
The syntax of types is defined as follows:(base types) t ::= intρ | t1 × t2
(expression types) τ ::= {t | φ}(function types) σ ::= ∀eρ.hφ | t → τ ie | ∀ρ.φ | ∃ρ.φ(constraints) φ ::= ρ | n | op(φ)(type environments) Γ ::= ∅ | Γ, x : t | Γ, f : σ
A constraint, denoted by φ, is an index variable ρ, a constant n, an operator
e or a quantifier expression. oe signifies a list of objects o1 , . . . , om
expression op(φ),

for some m ≥ 0. We often write > for 1 and ⊥ for 0. Note that the set of operators
contains standard logical operators like ∧ and ¬.
The base type intρ is the type of an integer whose value is denoted by ρ.
The base type t1 × t2 is the type of pairs consisting of values with the types t1
and t2 . The expression type {t | φ} is a subtype of t whose index variables areconstrained by φ. For example, {intρ1 × intρ2 | ρ1 > ρ2 } is the type of integer
pairs whose first element is greater than the second element. The index variables
in t are bound in {t | φ}. The function type ∀eρ.hφ | t → τ i is the type of functions
that take an argument of the type {t | φ} and return a value of the type τ . For
example, hρ1 > 0 ∧ ρ2 > 0 | intρ1 × intρ2 → {intρ3 | ρ3 = ρ1 + ρ2 }i is the typeof functions that take a pair of positive integers as an argument, and return thesum of the integers. The index variables in t and ρe are bound in ∀eρ.hφ | t → τ i.
We often abbreviate ∀eρ.hφ | t → τ i as ∀eρ.{t | φ} → τ if the index variables int do not occur in τ and as ∀e
ρ.t → τ if φ ≡ >. We assume that α-conversion is
implicitly performed so that bound variables are different from each other andfree variables.
A typing judgment is of the form φ; Γ ` e : τ . It reads that on the assumptionthat index variables satisfy φ, the expression has the type τ under the type0
environment Γ . For example, ρ > 0; x : intρ ` x + 1 : {intρ | ρ0 > 1}.

x:t∈Γρe0 = FIV(t)ρe ∩ FIV(φ, Γ ) = ∅φ; Γ ` x : {[eρ/eρ0 ]t | ρe = ρe0 }φ; Γ ` n : {intρ | ρ = n}

(T-Var)(T-Int)φ; Γ ` e1 : {t1 | φ1 }φ; Γ ` e2 : {t2 | φ2 }φ; Γ ` (e1 , e2 ) : {t1 × t2 | φ1 ∧ φ2 }(T-Pair)φ ∧ φ1 ; Γ, f : σ, x : t1 ` e1 : τ1
ρe ∩ FIV(Γ, φ) = ∅σ = ∀eρ.hφ1 | t1 → τ1 iφ; Γ, f : σ ` e2 : τ2φ; Γ ` fun f x = e1 in e2 : τ2
(T-Let-Fun)f :σ∈Γ

φ ` σ 6 τ1 → τ2
φ; Γ ` e : τ1φ; Γ ` f e : τ2

(T-App)φ; Γ ` e1 : {t | φ0 }φ ∧ φ0 ; Γ, x : t ` e2 : τ
FIV(t) ∩ FIV(τ ) = ∅φ; Γ ` let x = e1 in e2 : τ(T-Let)φ; Γ ` e1 : {t1 × t2 | φ0 }φ ∧ φ0 ; Γ, x1 : t1 , x2 : t2 ` e2 : τ
FIV(t1 , t2 ) ∩ FIV(τ ) = ∅φ; Γ ` let (x1 , x2 ) = e1 in e2 : τ(T-Let-Pair)φ; Γ ` e1 : {intρ | φ0 }φ ∧ ∃ρ.(φ0 ∧ ρ 6= 0); Γ ` e2 : τφ ∧ ∃ρ.(φ0 ∧ ρ = 0); Γ ` e3 : τ
φ; Γ ` if e1 then e2 else e3 : τ
φ; Γ ` e1 : {intρ | ρ 6= 0}
φ; Γ ` e2 : τ
φ; Γ ` assert e1 in e2 : τ(T-Assert)

φ01 ; Γ ` e : {t | φ02 }|= φ1 ⇒ (φ01 ∧ (φ02 ⇒ φ2 ))φ1 ; Γ ` e : {t | φ2 }Fig. 1. Typing Rules(T-If)(T-Sub)

The typing rules are given in Figure 1. In the figure, FIV(o) is the set offree index variables in some object o. The relation η |= φ means that an index
environment η (a function from index variables to integers) satisfies a constraint
φ. We write |= φ if ∅ |= ∀eρ.φ, where {eρ} = FIV(φ).
The subtyping relation φ ` σ 6 σ 0 on function types is defined by:|= φ ⇒ ∀ρe0 , FIV(t1 ).(φ01 ⇒ ∃e
ρ.(φ1 ∧ ∀FIV(t2 ).(φ2 ⇒ φ02 )))φ ` ∀eρ.hφ1 | t1 → {t2 | φ2 }i 6 ∀ρe0 .hφ01 | t1 → {t2 | φ02 }i
The type system ensures that evaluation of a well-typed, closed expression(i.e., an expression e such that >; Γ0 ` e : τ , where Γ0 is the type environment
for primitive operators) never gets stuck: See [8] for a formal discussion.

3

Type Inference Algorithm

This section formalizes our type inference algorithm and proves its soundness.
First, we extend the syntax of constraints with predicate variables to denoteunknown predicates. We also introduce extended type environments to model anintermediate state for on-demand type refinement.
e(constraints) φ ::= · · · | P (φ)(constraint substitutions) S ::= ∅ | S, P 7→ λe
ρ.φe(extended function types) T ::= (σ; φ; S)(extended type environments) ∆ ::= ∅ | ∆, x : t | ∆, f : T
Here, P is a meta-variable ranging over the set of predicate variables, which areused to express unknown specifications of functions. We write FPV(o) for the setof free predicate variables in some object o. Constraint substitutions map predicate variables to predicates (i.e., functions from index variables to constraints).
An extended type environment ∆ maps a function name f to an extended funce Here, σ is a template for the typetion type which is a triple of the form (σ; φ; S).
of f , which may contain predicate variables. For example, a template for a function from integers to integers is ∀e
ρ.hP (eρ, ρx ) | intρx → {intρy | Q(eρ, ρx , ρy )}i,
where ρe denotes a sequence of index variables (whose length is unknown). The
second element φ is a constraint that records a sufficient condition on predicate
variables for the definition of f to be well-typed; this is used to avoid re-checking
the function’s definition when the function’s type needs to be refined. The third
element Se records solutions for φ (which are substitutions for predicate variables)
found so far.
The type inference algorithm is specified as inference rules for the 5-tuple
relation ∆ B e : τ a φ; ∆0 . Here, ∆, e, and τ should be regarded as inputsof the algorithm, and φ and ∆0 as outputs of the algorithm. Intuitively, φ is asufficient condition for e to have type τ , and ∆0 describes types refined during theinference. For example, let e, τ , and ∆ be f (z), {intρ | ρ > 1}, and z : intρz , f :(σ; φ1 ; {S}), where σ = ∀e
ρ.hP (eρ, ρx ) | intρx → {intρy | Q(eρ, ρx , ρy )}i, φ1 =∀eρ, ρx .P (eρ, ρx ) ⇒ ∀ρy .(ρy = ρx + 1 ⇒ Q(eρ, ρx , ρy )), and S = {P 7→ λρx .>, Q 7→
λ(ρx , ρy ).>}. Then, φ and ∆0 would be ρz > 0 and z : intρz , f : (σ; φ1 ; {S, S 0 }),where S 0 is {P 7→ λρx .ρx > 0, Q 7→ λ(ρx , ρy ).ρy > 1}.
The inference rules for the relation ∆ B e : τ a φ; ∆0 (which are a declarativedescription of our type inference algorithm) are given in Figures 2 and 3. Figure 3
shows the rules for function definitions and applications, and Figure 2 shows
the rules for other expressions. The sub-algorithm σ 6 σ 0 a φ for computing asufficient condition φ for σ to be a subtype of σ 0 is also defined in Figure 3. In the
figures, TypeOf(∆, o) is a template for the type of some object o, obtained fromthe simple type of o by decorating it with fresh index variables and predicate
variables. For example, if the simple type of o is int, then TypeOf(∆, o) returns
intρ ; if the simple type of o is int → int, TypeOf(∆, o) returns ∀eρ.hP (eρ, ρx ) |intρx → {intρy | Q(eρ, ρx , ρy )}i.
In the rules in Figure 2, type inference proceeds in a backward manner:
For example, in B-Var, given the required type {t | φ} of the variable x, if
x : t0 ∈ ∆, we check whether |t| = |t0 | (where |t| is the simple type obtained fromt by removing index variables). If the check succeeds, we produce the constraint[t0 /t]φ, which is the constraint obtained from φ by replacing each occurrence ofan index variable of t with the corresponding index variable of t0 .
In B-Pair, given the required type {t1 × t2 | φ} of the pair (e1 , e2 ), we
compute the constraint φ2 which is sufficient for e2 to have {t2 | φ}. Then,
we compute the constraint φ1 which is sufficient for e1 to have {t1 | φ2 }. The
remaining rules in Figure 2 can be read in a similar manner.
We now explain the rules for functions in Figure 3. In B-Let-Fun, a template
for the function’s type is first prepared (see the first line). We then check thefunction’s definition, and compute a sufficient condition ψ on predicate variables
for the definition to be well-typed (see the second line). Then, we find a solution
S for ψ (i.e., a substitution such that |= S(ψ)) by using an auxiliary algorithm
Solve(FPV(σ); ψ), which is explained later. As a result, we obtain the input
specification of f which is sufficient for no assertion violation to occur in f . At
this stage, there is no requirement for the output of f , so that the inferred return
type of f is of the form {t | >}. Finally, we check e2 and produce φ2 and ∆0 .
Note that f ’s type may be refined during the type inference for e2 .
B-App is the rule for applications. From the type τ of f e and the simple
type of e, we prepare a template of f ’s type: {t | P (eρ)} → τ . The value of thepredicate variable P is computed by a sub-algorithm, expressed by using therelation ∆ B f : σ a{P } S; ∆0 (which is defined using B-Reuse and B-Refine:see below). Finally, we check that the function’s argument e has the required
type {t | S(P (eρ))}.
We have two rules B-Reuse and B-Refine for the auxiliary judgment ∆Bf :σ aPe S; ∆0 . The rule B-Reuse supports the case where the type of f in ∆ isprecise enough to be a subtype of σ, while B-Refine supports the case where
the type of f needs to be refined. The rules are non-deterministic, in the sensethat both rules may be applied. In the actual implementation, B-Reuse is given

a higher priority, so that B-Refine is used only when applications of B-Reuse
fail. For recursive calls and primitive operators, B-Refine is not used.
In B-Reuse, we pick up an already inferred type Sk (σ 0 ), and match it withthe required type σ. (Since the argument type of σ is a predicate variable, we
actually match the return types of σ and σ 0 here.) The constraint ψ, computedby using B-Sub, is a sufficient condition for Sk (σ 0 ) to be a subtype of σ. We
then solve ψ by using Solve.
In B-Refine, we match the template σ 0 of the function’s type with therequired type σ, and compute a sufficient condition ψ for σ 0 to be a subtype of
σ. We then compute a solution for ψ ∧ φ by using Solve. The key point here isthat both information about the function’s definition (expressed by φ) and thatabout the call site (expressed by ψ) are used to compute the function’s type.
Solve can use predicates occurring in ψ as hints for computing a solution of ψ ∧φ.

x : t0 ∈ ∆|t| = |t0 |0∆ B x : {t | φ} a [t /t]φ; ∆∆ B n : {intρ | φ} a [n/ρ]φ; ∆(B-Var)t1 × t2 = TypeOf(∆, e1 )∆, x1 : t1 , x2 : t2 B e2 : τ a φ2 ; ∆2∆2 \ {x1 , x2 } B e1 : {t1 × t2 | φ2 } a φ1 ; ∆1

(B-Int) ∆ B let (x1 , x2 ) = e1 in e2 : τ a φ1 ; ∆1
(B-Let-Pair)∆ B e2 : {t2 | φ} a φ2 ; ∆2
∆2 B e1 : {t1 | φ2 } a φ1 ; ∆1
∆ B (e1 , e2 ) : {t1 × t2 | φ} a φ1 ; ∆1
(B-Pair)t = TypeOf(∆, e1 )∆, x : t B e2 : τ a φ2 ; ∆2∆2 \ x B e1 : {t | φ2 } a φ1 ; ∆1
∆ B let x = e1 in e2 : τ a φ1 ; ∆1
(B-Let)∆ B e2 : τ a φ2 ; ∆2
∆2 B e3 : τ a φ3 ; ∆3
ρ : freshφ = (ρ 6= 0 ∧ φ2 ) ∨ (ρ = 0 ∧ φ3 )∆3 B e1 : {intρ | φ} a φ1 ; ∆1
∆ B if e1 then e2 else e3 : τ a φ1 ; ∆1
(B-If)
ρ : fresh∆ B e1 : {intρ | ρ 6= 0} a φ1 ; ∆1
∆1 B e2 : τ a φ2 ; ∆2

∆ B assert e1 in e2 : τ a φ1 ∧ φ2 ; ∆2
(B-Assert)

Fig. 2. Type inference rules (for basic expressions)

Constraint Solving We now describe a heuristic algorithm Solve(Pe; ϕ) to obtaina solution for ϕ (i.e., a substitution for the predicate variables Pe that satisfy ϕ).
If ϕ contains a subformula of the form ∀eρ.(P (eρ) ⇒ ψ(eρ, P )), and ψ(eρ, P )
does not contain negative occurrences of P , then the algorithm tries to compute
the greatest fixed-point of F = λP.λeρ.ψ(eρ, P ) by iterations from λe
ρ.> (i.e.,
by computing F n (λeρ.>) for n = 1, 2, . . .). (As a special case, if ψ(eρ, P ) does
not contain P , then the iteration immediately converges with the solution P =λeρ.ψ(eρ, P ).) The algorithm also uses widening [9] to accelerate convergence.
If the above iteration does not converge, the algorithm chooses a new starting
point of iterations by extracting a sub-formula of ψ(eρ, P ) which does not contain
P and generalizing its constants. This phase roughly corresponds to predicate

σ = ∀eρ.hφ | t → τ1 i = TypeOf(∆, fun f x = e1 )∆, f : σ, x : t B e1 : τ1 a φ1 ; ∆1 , f : σ, x : tψ = ∀eρ, FIV(t).(φ ⇒ φ1 )S = Solve(FPV(σ); ψ)∆1 , f : (σ; ψ; {S}) B e2 : τ a φ2 ; ∆2
∆ B fun f x = e1 in e2 : τ a φ2 ; ∆2 \ f(B-Let-Fun)t = TypeOf(∆, e)
ρe = FIV(t)P : fresh∆ B f : {t | P (eρ)} → τ a{P } S; ∆1∆1 B e : {t | S(P (eρ))} a φ2 ; ∆2
∆ B f e : τ a φ2 ; ∆2f : (σ 0 ; φ; {Sj }mj=1 ) ∈ ∆1≤k≤m

Sk (σ 0 ) 6 σ a ψ(B-App)

S = Solve(Pe; ψ)∆ B f : σ aPe S; ∆(B-Reuse)0dom(S) = Pe

∆ = ∆b , f : (σ ; φ; {Sj }m
σ0 6 σ a ψj=1 ), ∆a0dom(Sm+1 ) = FPV(σ )S, Sm+1 = Solve(Pe ∪ FPV(σ 0 ); ψ ∧ φ)
∆ B f : σ aPe S; ∆b , f : (σ 0 ; φ; {Sj }m+1j=1 ), ∆a(B-Refine)φ = ∀ρe0 , FIV(t1 ).(φ01 ⇒ ∃e
ρ.(φ1 ∧ ∀FIV(t2 ).(φ2 ⇒ φ02 )))∀eρ.hφ1 | t1 → {t2 | φ2 }i 6 ∀ρe0 .hφ01 | t1 → {t2 | φ02 }i a φ(B-Sub)Fig. 3. Type inference rules (for functions)discovery in abstract model checking. Unlike model checking, however, we do notrepeat the whole verification process; we just redo the fixed-point computation.
We use the following examples to illustrate how type inference works.
Example 1. fun pred x = assert x > 0 in x − 1 in assert e1 = pred e2 in ()By B-Let-Fun, we first check the definition of pred. We prepare the template σ = ∀e
ρ.hP (eρ, ρx ) | intρx → {intρy | Q(eρ, ρx , ρy )}i for the type of pred.
Then we check ∆Bassert x > 0 in x−1 : {intρy | Q(eρ, ρx , ρy )} a φ0 ; ∆0 for ∆ =ρx0∆0 , pred:σ, x:int , and obtain φ = ρx > 0∧Q(eρ, ρx , ρx −1). Here, ∆0 = +:h> |intρ1 × intρ2 → {intρ3 | ρ3 = ρ1 + ρ2 }i, . . . , ≤ :h> | intρ1 × intρ2 → {intρ3 |ρ3 = ρ1 ≤ ρ2 }i, . . . is the extended type environment for primitive operators.
Thus, we obtain the constraint φ = ∀eρ, ρx .P (eρ, ρx ) ⇒ φ0 on P and Q. We thencheck assert e1 = pred e2 in () under ∆1 = ∆0 , pred : (σ; φ; {P 7→ λρx .ρx >0, Q 7→ λ(ρx , ρy ).>}). To check pred e2 against the type {intρy | ρ = ρy }, therule B-Refine is used. From σ 6 {intρx | R(ρx )} → {intρy | ρ = ρy } a ψ, we
get ψ = ∀ρx .R(ρx ) ⇒ ∃e
ρ.(P (eρ, ρx ) ∧ ∀ρy .(Q(eρ, ρx , ρy ) ⇒ ρ = ρy )). Then, ψ ∧ φ ispassed to Solve as an input. From the subformula Q(eρ, ρx , ρy ) ⇒ ρ = ρy , Solveinfers that Q(ρ, ρx , ρy ) ≡ ρ = ρy . From the subformula φ, P (ρ, ρx ) is inferred
to be ρx > 0 ∧ ρ = ρx − 1. Thus, we obtain the refined type ∀ρ.hρx > 0 ∧ ρ =ρx − 1 | intρx → {intρy | ρ = ρy }i of pred.
Example 2.
fun f act x = if x ≤ 0 then 1 else x ∗ f act (x − 1) in assert f act e > 0 in ()By B-Let-Fun, we first check the definition of fact. We prepare the template σ = ∀e
ρ.hP (eρ, ρx ) | intρx → {intρy | Q(eρ, ρx , ρy )}i for the type of fact.
Then we check ∆Bif x ≤ 0 then 1 else x∗f act (x−1) : {intρy | Q(eρ, ρx , ρy )} a
φ0 ; ∆0 for ∆ = ∆0 , fact:σ, x:intρx , and obtain φ0 = (ρx ≤ 0∧φ1 )∨(ρx > 0∧φ2 ).
Here, φ1 = Q(eρ, ρx , 1) and φ2 = ∃ρe0 .(P (ρe0 , ρx − 1) ∧ ∀ρy .(Q(ρe0 , ρx − 1, ρy ) ⇒Q(eρ, ρx , ρx ∗ ρy ))) are respectively obtained from the then- and else- branches.
Thus, we obtain the constraint φ = ∀eρ, ρx .P (eρ, ρx ) ⇒ φ0 on P and Q. We thencheck assert fact e > 0 in () under ∆1 = ∆0 , fact : (σ; φ; {P 7→ λρx .>, Q 7→
λ(ρx , ρy ).>}). To check fact e against the type {intρy | ρy > 0}, the rule
B-Refine is used. From σ 6 {intρx | R(ρx )} → {intρy | ρy > 0} a ψ, we
get ψ = ∀ρx .R(ρx ) ⇒ ∃e
ρ.(P (eρ, ρx ) ∧ ∀ρy .(Q(eρ, ρx , ρy ) ⇒ ρy > 0)). Then, ψ ∧ φis passed to Solve as an input. From the subformula Q(eρ, ρx , ρy ) ⇒ ρy > 0,
Solve infers that Q(ρx , ρy ) ≡ ρy > 0. From the subformula φ, P (ρx ) is inferred
to be > as the result of the greatest fixed-point computation of the function
F = λP.λρx .(ρx ≤ 0 ∧ 1 > 0) ∨ (ρx > 0 ∧ P (ρx − 1) ∧ ∀ρy .(ρy > 0 ⇒ ρx ∗ ρy >0)) ≡ λP.λρx .ρx ≤ 0 ∨ (ρx > 0 ∧ P (ρx − 1)) by iterations from λρx .>, whichconverge immediately since F (λρx .>) ≡ λρx .ρx ≤ 0 ∨ ρx > 0 ≡ λρx .>. Thus, we
obtain the refined type h> | intρx → {intρy | ρy > 0}i of fact.
3.1

Soundness

We say that ∆ is valid if and only if for any f : (σ; φ; {Sj }mj=1 ) ∈ ∆, |= Sk (φ)
holds for any k ∈ {1, . . . , m}.
Let us define the function (|∆|), which maps an extended type environment∆ to an ordinary type environment, as follows:(|∅|) = ∅(|∆, x : t|) = (|∆|), x : t(|∆, f : (σ; φ; {Sj }m)|)=(|∆|),
f : merge({Sj (σ)}m
j=1
j=1 ).
000Here, merge({σj }mj=1 ) = hφ1 ∨ · · · ∨ φm | t → {t | (φ1 ⇒ φ1 ) ∧ · · · ∧ (φm ⇒ φm )}i
if σj = hφj | t → {t0 | φ0j }i for any j ∈ {1, . . . , m}. The following theorem statesthat the type inference algorithm is sound with respect to the dependent typesystem presented in Section 2. (We assume the soundness of Solve here; see thefull paper [8] for the proof).

Theorem 1 (Soundness). If ∆ B e : τ a φ; ∆0 is derivable and ∆ is valid then,∆0 is valid, ` (|∆0 |) 6 (|∆|), and φ; (|∆0 |) ` e : τ is derivable.
Note that the type inference algorithm is not complete with respect to thetype system because of the incompleteness of Solve.

4

Extensions

In this section, we briefly discuss how to extend our type inference algorithm
formalized in Section 3 with higher-order functions, parametric polymorphism,
and algebraic data types. Interested readers are referred to the full paper [8] forthe formalization of the extended algorithm.

Higher-Order Functions A main new issue in handling higher-order functions iswhat kind of template is prepared for higher-order functions. For example, for afunction of type (int → int) → int, one may be tempted to consider a templateof the form: hR1 (P1 , Q1 ) | hP1 (ρ1 ) | intρ1 → {intρ2 | Q1 (ρ1 , ρ2 )}i → {intρ3 |R2 (P1 , Q1 , ρ3 )}i, which is the type of a function that takes a function whose
precondition P1 and postcondition Q1 satisfy R1 (P1 , Q1 ), and returns an integerthat satisfies R2 (P1 , Q1 , ρ3 ). This allows us to express a higher-order functionthat is polymorphic on the property of a function argument, but requires asignificant extension of the constraint solving algorithm due to the presence of
higher-order predicates.
Instead, we consider only first-order predicate variables, and use a templatehP1 (ρ1 ) | intρ1 → {intρ2 | Q1 (ρ1 , ρ2 )}i → {intρ3 | Q2 (ρ3 )} for (int → int) →int. This allows us to extend the algorithm in Section 3 in a fairly straightforward manner. A shortcoming of the approach is that a higher-order function ismonomorphic on the property of function arguments; we use parametric polymorphism to overcome that disadvantage to some extent.
Parametric Polymorphism The above treatment of higher-order functions sometimes results in too specific types. For example, the following type of map would
be inferred from the calling context (map (λx.x + 1) l) : {intw list | w ≥ 0}:({intx | x ≥ −1} → {inty | y ≥ 0}) → {intz list | z ≥ −1} → {intw list | w ≥ 0}.
This is too specific to be used in other calling contexts of map. To remedy the
problem, we use parametric polymorphism. In the case of map function, thepolymorphic type ∀α, β.(α → β) → α list → β list is assigned to map,
which can be instantiated to ({intx | P (x)} → {inty | Q(y)}) → {intz list |P (z)} → {intw list | Q(w)} for any P and Q.
Algebraic Data Types We require users to declare data type invariants and dependent types for constructors of each user-defined algebraic data type as in DML.
Then, our algorithm infers dependent types of functions automatically unlike in
DML. We allow users to declare multiple types for each data constructor; forexample, for lists, users may declare Nil as ∀α.unit → {α listρ | ρ = 0} and∀ρ.unit → {ordlistρ1 | ρ1 = ρ} (see Section 5.1). This allows users to specify
multiple properties like the list length and sortedness.
The main new difficulty in type inference is how to handle multiple types declared for each constructor as mentioned above. An extended type environment∆
now maps each function name to a set of extended function types, instead ofa single extended function type. For example, a list function may have the following four templates: { hP1 (ρx ) | int listρx → {int listρy | Q1 (ρx , ρy )}i,hP2 (ρx ) | int listρx → {ordlistρy | Q2 (ρx , ρy )}i, hP3 (ρx ) | ordlistρx →{int listρy | Q3 (ρx , ρy )}i, hP4 (ρx ) | ordlistρx → {ordlistρy | Q4 (ρx , ρy )}i},
which are generated on-demand (based on calling contexts), in order to avoid a
combinatorial explosion of the number of templates. Once an appropriate template is chosen, the rest of the algorithm is basically the same as the one describedin Section 3: constraints on predicate variables are generated and solved.

5

Implementation and Experiments

We have implemented a prototype type inference system (available from http://web.yl.is.s.u-tokyo.ac.jp/∼uhiro/depinf/) according to the formalization in Section 3. It supports higher-order functions, parametric polymorphism,
and algebraic data types as described in Section 4. We adopted Cooper’s algorithm for checking satisfiability of integer constraints. We report two kinds ofexperiments to show the effectiveness of our approach. All the experiments were
performed on Intel Xeon CPU 3GHz with 3GB RAM.
5.1

Verification of sorting algorithms

This experiment shows an application of our system to infer the specifications for
auxiliary functions from the specification of the top-level function. The programs
used in the experiment are the insertion sort defined in Section 1, and a merge
sort. We discuss below the experiment for the insertion sort. The experiment forthe merge sort is similar: The merge sort program consists of a main function
msort and two auxiliary functions merge and msplit. The types of merge andmsplit have been automatically inferred from the type specification that msort
should return a sorted list only.
In the experiment, Nil is defined as a constructor having two types: ∀α.unit →{α listρ | ρ = 0} and ∀ρ.unit → {ordlistρ1 | ρ1 = ρ}. Cons is defined as aconstructor having two types: ∀α.α × α listρ1 → {α listρ2 | ρ2 = ρ1 + 1} andhρ1 ≤ ρ2 | intρ1 × ordlistρ2 → {ordlistρ3 | ρ3 = ρ1 }i. Here, α listρ is thetype of lists of length ρ, whose elements have the type α. ordlistρ is the typeof ordered lists, whose elements are integers greater than or equal to ρ. As in
this example, multiple types can be declared for each constructor in our system,
and an appropriate type is chosen depending on each context. We also added atype declaration that isort should return a value of type {ordlistρ | >}. The
full paper [8] shows the whole code used in the experiment.
Our system succeeded in verifying the program, and inferred the following
types in 0.912 seconds:
insert : ∀ρ.hρ ≤ ρ1 ∧ ρ ≤ ρ2 | intρ1 × ordlistρ2 → {ordlistρ3 | ρ ≤ ρ3 }i,
isort : int list → ordlist.
The type of insert means that insert returns a sorted list whose head is greaterthan or equal to the first argument or the head of the second argument if a sorted
list is given as the second argument.
We describe below how the type of the auxiliary function insert is refined.
From the definition of insert, the initial type assigned to insert is int ×
int list → int list. When the call site insert (x, isort xs0 ) (on the lastline of the definition of isort) is checked (with the required output specification{ordlistρ | >}), the following new template for the type of insert is prepared:∀eρ.hP (eρ, ρ1 , ρ2 ) | intρ1 × ordlistρ2 → {ordlistρ3 | Q(eρ, ρ1 , ρ2 , ρ3 )}i,

Since the required type for insert (x, isort xs0 ) is {ordlistρ | >}, the system first infers that Q(ρ1 , ρ2 , ρ3 ) ≡ >, and checks the constraint extracted fromthe definition of isort. That type is, however, not precise enough to check therecursive call insert(x, ys) (on the last line of the definition of insert), which
requires that ∀ρret .Q(eρ0 , ρx , ρys , ρret ) ⇒ ρy ≤ ρret holds. Thus, Q(ρ, ρ1 , ρ2 , ρ3 )is strengthened to ρ ≤ ρ3 . Then, the system successfully infers the input specification P (ρ, ρ1 , ρ2 ) ≡ ρ ≤ ρ1 ∧ ρ ≤ ρ2 by propagating the output specification.
5.2

Experiment with functions from the OCaml list module

In this experiment, we demonstrate an application of our system to learn specifications of library functions. We use the list module of the OCaml programming
language (http://caml.inria.fr/) as the target of the experiment.
The experiment proceeded as follows.
1. We manually translated the source code of the list module into our language.
We have also added the definition of list constructors Nil : ∀α.unit →{α listρ | ρ = 0} and Cons : ∀α.α × α listρ1 → {α listρ2 | ρ2 = ρ1 + 1}.
2. We executed our system for the translated code above. No call site information was used in this phase (except for the calls inside libraries).
3. Let f be a function whose argument type constraint inferred in the previous
step is not >. (For example, the argument type of combine was inferred tobe {α listρ1 × β listρ2 | ρ1 = ρ2 } in Step 2.) Let g be another libraryfunction. Then, we searched for code fragments of the form f (. . . g (. . .) . . .)from various application programs. (Here, we have used Google Code Search,
http://code.google.com/.)
4. We executed our system on the code fragments collected in the above step,
to refine the types of library functions.
The first and third steps of the experiment have been conducted manually, but
automation of those steps would not be difficult.
The result of the experiment is summarized in Table 1. Table 2 shows someof the call sites used in the final step. The filed “time” indicates the time spentin the second and fourth steps.
For most of the library functions, the inferred types are the same as the
expected types (modulo simplification of some constraints). For some functions,the inferred types were less precise than expected: For example, the type of
rev map2 in Table 1 does not capture the property that the length of the returned
list is the same as that of the second argument. We expect that those types canbe refined by using more appropriate call sites.
As for the efficiency, our system was slow for length, map2, and combine.
We think that this is due to the present naive implementation of the fixed-pointcomputation algorithm, and that we can remedy the problem by using convexhull or selective hull operator [10] to keep the size of the constraints small.
As already mentioned, we have collected the call sites manually in step 3.
To confirm that our choice of call sites did not much affect the quality of theinferred types, we have tested our system also with call sites other than thoseshown in Table 2, and confirmed that similar types are inferred from them.

function inferred specificationtime(sec.)
namelength ∀α.∀ρ, ρ0 .{α listρ1 | ρ ≥ ρ1 ≥ ρ0 } → {intρ2 | ρ ≥ ρ2 ≥ ρ0 }27.7730.004
hd ∀α.{α listρ | ρ > 0} → αtl ∀α.∀ρ.{α listρ1 | ρ1 > 0 ∧ ρ1 = ρ + 1} → {α listρ2 | ρ2 = ρ}
0.064
nth ∀α.{α listρ1 × intρ2 | ρ1 > ρ2 ≥ 0} → α
0.268
0.540
rev ∀α.∀ρ.{α listρ1 | ρ1 = ρ} → {α listρ2 | ρ2 = ρ}append ∀α.∀ρ.{α listρ1 × α listρ2 | ρ1 + ρ2 = ρ} →2.892
{α listρ3 | ρ3 = ρ}map ∀α, β.(α → β) → ∀ρ.{α listρ1 | ρ1 = ρ} → {β listρ2 | ρ2 = ρ}
0.292
0.276
iter2 ∀α, β.(α × β → unit) →{α listρ1 × β listρ2 | ρ1 = ρ2 } → unit
map2 ∀α, β, γ.(α × β → γ) →14.236∀ρ.{α listρ1 × β listρ2 | ρ1 = ρ2 = ρ} → {γ listρ3 | ρ3 = ρ}
rev map2 ∀α, β, γ.(α × β → γ) →0.448
{α listρ1 × β listρ2 | ρ1 = ρ2 } → γ list
fold left2 ∀α, β, γ.(α × β × γ → α) →0.276
{α × (β listρ1 × γ listρ2 ) | ρ1 = ρ2 } → αfold right2 ∀α, β, γ.(α × β × γ → γ) →0.276{(α listρ1 × β listρ2 ) × γ | ρ1 = ρ2 } → γ
for all2 ∀α, β.(α × β → bool) →0.276{α listρ1 × β listρ2 | ρ1 = ρ2 } → bool
exists2 ∀α, β.(α × β → bool) →0.276{α listρ1 × β listρ2 | ρ1 = ρ2 } → bool
split ∀α, β.∀ρ.{(α × β) listρ1 | ρ1 = ρ} →0.340
{α listρ2 × β listρ3 | ρ2 = ρ3 = ρ}
combine ∀α, β.∀ρ.{α listρ1 × β listρ2 | ρ1 = ρ2 = ρ} →15.576{(α × β) listρ3 | ρ3 = ρ}Table 1. The specifications of the library functions from the OCaml list module. Our
system automatically inferred them from the call sites of the functions in Table 2.

6

Related WorkAs already mentioned in Section 1, closely related to ours is the work on DML [4,5] and size inference [1–3].
DML [4, 5] is an extension of ML with a restricted form of dependent types.
DML requires users to declare function types, and then automatically performs
implicit argument inference and type checking. An advantage of our approachis that users need not always declare function types, as demonstrated in theverification of sorting functions.
Size inference can automatically infer size relations between arguments andreturn values of functions [1–3]. A main difference is that the size inference tries
to infer as precise specification as possible from the definition of a function, while
our algorithm starts with simple types, and gradually refines the types based on
information about functions’ call sites. A main advantage of our approach isthat we can allow more flexible dependent types based on the user’s demandfile name call siterefinedfunctionspredabst.ml combine (a1, (tl a2))tl
lengthcompletion.ml nth (a3, (length a3 - 1))
xdr.ml let (a4, a5) = split a6 insplit,
combine (a4, map f1 a5)
map
rev
pmlize.ml combine (rev a7, a8)
ass.ml combine (append (fst (split a9), fst (split a10)), append,append (snd (split a9), snd (split a10))) split
printtyp.ml map2 f2 (a11, map2 f3 (a12, a13))
map2
combinectype.ml fold_left2 f4 (a14, a15, combine (a16, a17))
Table 2. The call sites used to infer the specifications of the functions in Table 1. Wecollected them from existing programs written in OCaml.

(as demonstrated in the verification of sorting functions, where two kinds oflist types were declared). Another possible advantage of our approach (that has
yet to be confirmed by more experiments) is that the on-demand inference canbe more efficient, especially when precise specification is not required for mostfunctions. On the other hand, an advantage of size inference is that it can findmore precise specification than ours, and that it needs to infer the specificationof a function just once.
Rich type systems which include dependent types with datasort and index
refinements [11, 12], and generalized algebraic data types [13–15] have been introduced to practical programming languages so that non-trivial program invariants
can be expressed as types [16, 17]. Partial type inference in the spirit of local
type inference [18] is employed in those type systems, to reduce type annotations. Type information can, however, be propagated locally, so that the typesof recursive functions cannot be inferred automatically.
Flanagan proposed hybrid type checking which allows users to refine datatypes with arbitrary program terms [19]. A type reconstruction algorithm forthat type system has been proposed by Knowles and Flanagan [6]. The result of
their type inference algorithm, however contains fixed-point operators on predicates, so that their algorithm alone can neither statically detect errors, nor produce useful documentations for the program. Their algorithm does not support
compound data structures and parametric polymorphism.
Theorem provers such as Coq [20] can also be used for writing dependently
typed programs [21, 22]. Epigram [23] and Cayenne [24] support interactive development of dependently typed programs: a program template and sub-goals
are automatically generated from a type. These systems greatly reduce users’burden of writing programs and types. However, these systems currently seemto be difficult to master for ordinary programmers without a knowledge of formal
logic.
As mentioned in Section 1, the idea of our approach has been inspired byautomatic predicate discovery and loop invariant inference in other verification techniques, such as predicate abstraction [7, 25–27], the induction-iteration

method [28], on-demand loop invariant refinement by Leino [29], and constraintbased invariant generation which solves unknown parameters in invariant templates [30, 31]. Our main contribution in this respect is to bring those techniques
into the context of dependently-typed functional languages; The advantage ofusing the type-based setting is that the verification technique can be smoothly
extended to support algebraic data types, higher-order functions, etc.

7

Conclusion

We have proposed a novel approach to applying dependent types to practicalprogramming languages: Our type inference system first assigns simple types
to functions, and refines them on demand, using information about both thefunctions’ definitions and call sites. A prototype type inference system has been
already implemented and tested for non-trivial programs.
Future work includes an extension of our system for producing better error
messages. With the current system, when type inference fails, it is difficult for
the user to judge whether the failure is due to a bug of the program, or theincompleteness of our type inference algorithm. Finding minimal unsatisfiable
constraints as in [16] would be useful for producing better error messages.
Our type inference algorithm presented in this paper assumes that all thefunction definitions are available. To support separate type inference for each
module, we have to let users declare module interface (i.e., dependent types ofthe exported functions). Some module interface may be, however, automaticallygenerated as shown in the experiments in Section 5.2.

Acknowledgments
We thank anonymous reviewers for their comments.

References
1. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using
sized types. In: POPL ’96, ACM Press (1996) 410–423
2. Chin, W.N., Khoo, S.C.: Calculating sized types. In: PEPM ’00, ACM Press (1999)
62–72
3. Chin, W.N., Khoo, S.C., Xu, D.N.: Extending sized type with collection analysis.
In: PEPM ’03, ACM Press (2003) 75–84
4. Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types.
In: PLDI ’98, ACM Press (1998) 249–257
5. Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL ’99,
ACM Press (1999) 214–227
6. Knowles, K., Flanagan, C.: Type reconstruction for general refinement types. In:
ESOP ’07. (2007)
7. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI ’01, ACM Press (2001) 203–213

8. Unno, H., Kobayashi, N.: On-demand refinement of dependent types (Full version)(January 2008) Available from http://web.yl.is.s.u-tokyo.ac.jp/∼uhiro/.
9. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variablesof a program. In: POPL ’78, ACM Press (1978) 84–96
10. Popeea, C., Chin, W.N.: Inferring disjunctive postconditions. In: ASIAN ’06.
LNCS, Springer-Verlag (December 2006)
11. Dunfield, J.: Combining two forms of type refinements. Technical Report CMUCS-02-182, Carnegie Mellon University (September 2002)
12. Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: POPL ’04, ACM Press(2004) 281–292
13. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL
’03, ACM Press (2003) 224–235
14. Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic
data types. In: POPL ’06, ACM Press (2006) 232–244
15. Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unificationbased type inference for GADTs. In: ICFP ’06, ACM Press (2006) 50–61
16. Sulzmann, M., Voicu, R.: Language-based program verification via expressive
types. Electronic Notes in Theoretical Computer Science 174(7) (2007) 129–147
17. Kiselyov, O., chieh Shan, C.: Lightweight static capabilities. Electronic Notes in
Theoretical Computer Science 174(7) (2007) 79–104
18. Pierce, B.C., Turner, D.N.: Local type inference. In: POPL ’98, ACM Press (1998)
252–265
19. Flanagan, C.: Hybrid type checking. In: POPL ’06, ACM Press (2006) 245–256
20. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development.
Springer-Verlag (2004)
21. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler
with a proof assistant. In: POPL ’06, ACM Press (2006) 42–54
22. Chlipala, A.: Modular development of certified program verifiers with a proof
assistant. In: ICFP ’06, ACM Press (2006) 160–171
23. Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter.
Manuscript, available online (April 2005)
24. Augustsson, L.: Cayenne – a language with dependent types. In: ICFP ’98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, ACM Press (1998) 239–250
25. Graf, S., Saı̈di, H.: Construction of abstract state graphs with PVS. In: CAV ’97,
Springer-Verlag (1997) 72–83
26. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL
’02, ACM Press (2002) 191–202
27. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL
’02, ACM Press (2002) 58–70
28. Suzuki, N., Ishihata, K.: Implementation of an array bound checker. In: POPL
’77, ACM Press (1977) 132–143
29. Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: APLAS ’05. Volume3780 of LNCS., Springer-Verlag (November 2005) 119–134
30. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations
analysis. In: SAS ’04. Volume 3148 of LNCS., Springer-Verlag (August 2004) 53–68
31. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In:
PLDI ’07, ACM Press (2007) 300–309