BRICS RS-95-33 Palsberg et al.: Type Inference with Non-structural Subtyping

BRICS

Basic Research in Computer Science

Type Inference with Non-structural Subtyping

Jens Palsberg Mitchell Wand Patrick O’Keefe

BRICS Report Series RS-95-33 ISSN 0909-0878 June 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Type Inference with Non-structural Subtyping

Jens Palsberg^{∗} Mitchell Wand^{†}^{‡} Patrick O’Keefe^{§}

Abstract

We present an O(n^{3}) time type inference algorithm for a type system with a largest type ⊤, a smallest type ⊥, and the usual ordering between function types. The algorithm infers type annotations of minimal size, and it works equally well for recursive types. For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference without ⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful.

∗BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Computer Science, University of Aarhus, Ny Munkegade, DK–8000 Aarhus C, Denmark. E-mail: palsberg@daimi.aau.dk.

†Work supported by the National Science Foundation under grants CCR-9304144 and CCR-9404646.

‡College of Computer Science, Northeastern University, 360 Huntington Avenue, 161CN, Boston, MA 02115, USA. E-mail: wand@ccs.neu.edu.

§151 Coolidge Avenue #211, Watertown, MA 02172, USA. E-mail:

pmo@world.std.com.

1 Introduction

This paper concerns types for the λ-calculus that can be generated from the grammar:

t ::= ⊥ | ⊤ | t_{1} → t_{2} .

Intuitively, ⊥ is a least type containing only the divergent computation; ⊤ is a maximal or universal type containing all values; and t_{1} → t_{2} is the usual function space.

Types are partially ordered by ≤ which is the smallest binary relation on types such that

1. ⊥ ≤ t ≤ ⊤ for all types t; and

2. s → t ≤ s′ → t′ if and only if s′ ≤ s and t ≤ t′.

Following [9], we denote this type system by PTB (PTB indicates Partial Types with Bottom). Thatte’s system of partial types [7] did not include ⊥; the fragment of PTB without ⊥ will be denoted PT [9].

The type system PTB can be extended with recursive types, yielding Amadio and Cardelli’s system [1], here denoted PTB_{μ}. The further extension of PTB_{μ} with the type Int of integers will be denoted PTB_{μ} ∪ {Int}.

We have earlier shown that PTB is strictly more powerful than PT [9], and recursive types add further power.

It is known that type inference for PT is computable in O(n^{3}) time [3]. It is also known that type inference for PTB_{μ} ∪ {Int} is computable in O(n^{3}) time, by reduction to a flow analysis problem [5].

In this paper we show that type inference for PTB and PTB_{μ} is also computable in O(n^{3}) time, by an algorithm similar to that in [3]. The algorithm infers type annotations of minimal size. A type is a tree, so its size is can be measured by the size of the set of paths from the root. In general, there can be several types of minimal size. For example, the λ-term λx.λy.(λf.f(fx))(λv.vy) can be typed such that

x : ⊥
y : ⊥
f : ⊥ → ⊥
v : ⊥ .

These type annotations are of minimal size. If we replace the type of y by ⊤, then we obtain another type annotation of minimal size.

In the type system PT, every typable λ-term has exactly one type annotation of minimal size. The algorithm by Kozen, Palsberg, and Schwartzbach [3] infers this minimal-size type annotation.

The type inference algorithm by Palsberg and O’Keefe [5] for PTB_{μ}∪{Int} does in general not infer type annotations of minimal size. It remains open if our result can be extended to PTB_{μ} ∪ {Int}.

For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference without ⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful. In our view, the simpler algorithm motivates having ⊤ and ⊥ together in a type system.

In the following Section we define the type inference problem and summarize some known results that will be helpful in the later sections. In Section 3 we define an automaton that will be used when defining possible solutions to the type inference problem, and in Section 4 we define a useful notion of upper bound. In Section 5 we prove our main theorem that characterizes a minimal-size solution, and in Section 6 we present our type inference algorithm. Finally, in Section 7 we give an example of how our type inference algorithm works.

2 The type system

2.1 Types

Let Σ = {→, ⊥, ⊤} be the ranked alphabet where → is binary and ⊥, ⊤ are nullary. A type is a finite tree over Σ. A path from the root of such a tree is a string over {0, 1}, where 0 indicates “left subtree” and 1 indicates “right subtree”. This set of types is the same as the one defined by the grammar in Section 1. We represent a type by a term, which is a function mapping each path from the root of the type to the symbol at the end of the path, as follows.

Definition 1 A term is a partial function

t : {0, 1}⋆ → Σ

with domain D(t) such that D(t) is non-empty and prefix-closed, and such that if t(α) =→, then {i | αi ∈ D(t)} = {0, 1}; and if t(α) ∈ {⊥, ⊤}, then {i | αi ∈ D(t)} = ∅. The set of all such terms is denoted T_{Σ}. The set of terms with finite domain is denoted F_{Σ}. They represent finite trees, by König’s Lemma. In our application, F_{Σ} is the set of types.

For s, t ∈ T_{Σ}, define →^{T_{Σ}}: T_{Σ} × T_{Σ} → T_{Σ} and ⊥^{T_{Σ}}, ⊤^{T_{Σ}} ∈ T_{Σ} by

(s →^{T_{Σ}} t)(0α) = s(α)
(s →^{T_{Σ}} t)(1α) = t(α)
(s →^{T_{Σ}} t)(ϵ) = →
⊥^{T_{Σ}}(ϵ) = ⊥
⊤^{T_{Σ}}(ϵ) = ⊤ .

Then

D(s →^{T_{Σ}} t) = {ϵ} ∪ {0α | α ∈ D(s)} ∪ {1α | α ∈ D(t)}
D(⊥^{T_{Σ}}) = {ϵ}
D(⊤^{T_{Σ}}) = {ϵ} .

For t ∈ T_{Σ} and α ∈ {0, 1}⋆, define the partial function t↓α : {0, 1}⋆ → Σ by

t↓α(β) = t(αβ) .

If t ↓ α has non-empty domain, then it is a term, and is called the subterm of t at position α.

For x ⊆ {0, 1}⋆ and α ∈ {0, 1}⋆, define x↓α = {β | αβ ∈ x}. □

The following properties are immediate from the definitions:

(i) (s →^{T_{Σ}} t)↓0 = s

(ii) (s →^{T_{Σ}} t)↓1 = t

(iii) (t↓α)↓β = t↓αβ

Following [2], we omit the superscript T_{Σ} on the operators →^{T_{Σ}}, ⊥^{T_{Σ}}, ⊤^{T_{Σ}}.

We will say that a term s has smaller size than a term t if D(s) ⊆ D(t). Our type inference algorithm will infer types that are of minimal size.

Terms are ordered by the subtype relation ≤, as follows.

Definition 2 The parity of α ∈ {0, 1}⋆ is the number mod 2 of 0’s in α. The parity of α is denoted πα. A string α is said to be even if πα = 0 and odd if πα = 1. Let ≤_{0} be the partial order on Σ given by

⊥ ≤_{0} → and → ≤_{0} ⊤

and let ≤_{1} be its reverse

⊤ ≤_{1} → and → ≤_{1} ⊥ .

For s, t ∈ T_{Σ}, define s ≤ t if s(α) ≤_{πα} t(α) for all α ∈ D(s) ∩ D(t). □

Kozen, Palsberg, and Schwartzbach [2] showed that the relation ≤ is equivalent to the order defined by Amadio and Cardelli [1]. The relation ≤ is a partial order with ⊥ ≤ t ≤ ⊤ for all t ∈ T_{Σ}, and s → t ≤ s′ → t′ if and only if s′ ≤ s and t ≤ t′ [1, 2]. Moreover, on F_{Σ}, ≤ coincides with the type ordering defined in Section 1 [2].

2.2 Type rules

If E is a λ-term, t is a type, and A is a type environment, i.e. a partial function assigning types to variables, then the judgement

A ⊢ E : t

means that E has the type t in the environment A. Formally, this holds when the judgement is derivable using the following four rules:

A ⊢ x : t (provided A(x) = t)  (1)
\frac{A[x ← s] ⊢ E : t}{A ⊢ λx.E : s → t}  (2)
\frac{A ⊢ E : s → t A ⊢ F : s}{A ⊢ EF : t}  (3)
\frac{A ⊢ E : s s ≤ t}{A ⊢ E : t}  (4)

The first three rules are the usual rules for simple types and the last rule is the rule of subsumption.

The type system has the subject reduction property, that is, if A ⊢ E : t is derivable and E β-reduces to E′, then A ⊢ E′ : t is derivable. This is proved by straightforward induction on the structure of the derivation of A ⊢ E : t [4].

This system types terms which are not typable in the simply-typed λcalculus. For example, consider λf.(fK(fI)), where K and I are the usual combinators. This is not typable in the ordinary calculus, since K and I have different types, but it is typable under partial typing: assign f the type ⊤ → ⊤ → ⊤. Both the K and I can be coerced to type ⊤, and the result (fI), of type ⊤ → ⊤, can be coerced to ⊤ to form the second argument of the first f. Therefore the entire term has type (⊤ → ⊤ → ⊤) → ⊤.

Similarly, some self-application is possible: (λx.xx) has type (⊤ → t) → t for all t, since the final x can be coerced to ⊤.

However, not all terms are typable in this system. Any λ-term typable in PTB is strongly normalizing [9]. To indicate the flavor of those strongly normalizing λ-terms which are not typable in this system, we have earlier [9] showed that (λx.xxx)(λy.y) is not typable in PTB. We also showed that (λf.f(fx))(λv.vy) is typable in PTB but not in PT. This demonstrates that ⊥ adds power to a type system.

2.3 Constraints

Given a λ-term E, the type inference problem can be rephrased in terms of solving a system of type constraints. Assume that E has been α-converted so that all bound variables are distinct. Let X_{E} be the set of λ-variables x occurring in E, and let Y_{E} be a set of variables disjoint from X_{E} consisting of one variable [[F]] for each occurrence of a subterm F of E. (The notation [[F]] is ambiguous because there may be more than one occurrence of F in E. However, it will always be clear from context which occurrence is meant.) We generate the following system of inequalities over X_{E} ∪ Y_{E}:

• for every occurrence in E of a subterm of the form λx.F, the inequality

x → [[F]] ≤ [[λx.F]] ;

• for every occurrence in E of a subterm of the form GH, the inequality

[[G]] ≤ [[H]] → [[GH]] ;

• for every occurrence in E of a λ-variable x, the inequality

x ≤ [[x]] .

Denote by T (E) the system of constraints generated from E in this fashion. For every λ-term E, let Tmap(E) be the set of total functions from X_{E} ∪ Y_{E} to T_{Σ}. The function ψ ∈ Tmap(E) is a solution of T (E) if and only if it is a solution of each constraint in T (E). Specifically, for V, V′, V′′ ∈ X_{E} ∪ Y_{E}:

The constraint:  has solution ψ if:
V → V′ ≤ V′′ ψ(V) → ψ(V′) ≤ ψ(V′′)
V ≤ V′ → V′′ ψ(V) ≤ ψ(V′) → ψ(V′′)
V ≤ V′  ψ(V) ≤ ψ(V′)

The solutions of T (E) correspond to the possible type annotations of E in a sense made precise by Theorem 3.

Let A be a type environment assigning a type to each λ-variable occurring freely in E. If ψ is a function assigning a type to each variable in X_{E} ∪ Y_{E}, we say that ψ extends A if A and ψ agree on the domain of A.

Theorem 3 The judgement A ⊢ E : t is derivable if and only if there exists a solution ψ of T (E) extending A such that ψ([[E]]) = t. In particular, if E is closed, then E is typable with type t if and only if there exists a solution ψ of T (E) such that ψ([[E]]) = t.

Proof. Similar to the proof of Theorem 2.1 in the journal version of [3], in outline as follows. Given a solution of the constraint system, it is straightforward to construct a derivation of A ⊢ E: t. Conversely, observe that if A ⊢ E: t is derivable, then there exists a derivation of A ⊢ E: t such that each use of one of the ordinary rules is followed by exactly one use of the subsumption rule. The approach in for example [8, 6] then gives a set of inequalities of the desired form. □

2.4 Graphs

In this section we reduce the problem of solving constraint systems to a problem of solving a certain kind of constraint graphs. The graphs yield a convenient setting for applying algorithms like transitive closure.

Definition 4 A constraint graph is a directed graph G = (S, L, R, ≤) consisting of a set of nodes S and three sets of directed edges L, R, ≤. We write s →^{0} t to indicate that the pair (s, t) is in the edge set L, we write s →^{1} t to indicate that the pair (s, t) is in the edge set R, and we write s →^{≤} t to indicate that the pair (s, t) is in the edge set ≤. A constraint graph must satisfy the properties:

• any node has at most one outgoing L edge and at most one outgoing R edge;

• a node has an outgoing L edge if and only if it has an outgoing R edge.

A solution for G is any map h : S → T_{Σ} such that

(i) if u →^{0} v and u →^{1} w, then h(u) = h(v) → h(w);

(ii) if u →^{≤} v, then h(u) ≤ h(v).

Notice that we consider solutions in S → T_{Σ}, not just in S → F_{Σ}. The solution h is finite if h(s) is a finite set for all s.

Define finally

N = {u ∈ S | u has outgoing L and R edges in G}
□

A system of type constraints as described above gives rise to a constraint graph by associating a unique node with every subexpression occurring in the system of constraints, defining L and R edges from an occurrence of an expression to its left and right subexpressions, and defining ≤ edges for the inequalities.

Definition 5 A constraint graph is closed if the edge relation ≤ is reflexive, transitive, and closed under the following rule which says that the dashed edges exist whenever the solid ones do:

[figure: ≥; ≤; ≤; 1; 0; 1; 0]

The closure of a constraint graph G is the smallest closed graph containing G as a subgraph. □

Lemma 6 A constraint graph and its closure have the same set of solutions.

Proof. Any solution of the closure of G is also a solution of G, since G has fewer constraints. Conversely, the closure of G can be constructed from G by iterating the closure rules, and it follows inductively that any solution of G satisfies the additional constraints added by this process. □

3 An automaton

In this section we define an automaton M. It will be used to characterize a minimal-size assignment of types to nodes of a given constraint graph. An intuitive account follows the formal definition.

Definition 7 Let a constraint graph G = (S, L, R, ≤) be given. The automaton M is defined as follows. The input alphabet of M is {0, 1}. The set of states of M is S × S. A state is written (s, t). The transitions are defined as follows.

(u, v) →^{ϵ} (u, v′) if v →^{≤} v′ in G
(u, v) →^{ϵ} (u′, v) if u′ →^{≤} u in G
(u, v) →^{1} (u′, v′) if u →^{1} u′ and v →^{1} v′ in G
(u, v) →^{0} (v′, u′) if u →^{0} u′ and v →^{0} v′ in G

If p and q are states of M and α ∈ {0, 1}⋆, we write p →^{α} q if the automaton can move from state p to state q under input α, including possible ϵ-transitions.

The automaton M_{s} is the automaton M with start state (s, s). All states are accept states; thus the language accepted by M_{s} is the set of strings α for which there exists a state (u, v) such that (s, s) →^{α} (u, v). We denote this language by L(s). □

Informally, we can think of the automaton M_{s} as follows. We start with two pebbles, one green and one red, on the node s of the constraint graph G. We can move the green pebble forward along a ≤ edge at any time, and we can move the red pebble backward along a ≤ edge at any time. We can move both pebbles simultaneously along R edges leading out of the nodes they occupy. We can also move them simultaneously along outgoing L edges, but in the latter case we switch their colors. The sequence of 0’s and 1’s that were seen gives a string in L(s), and all strings in L(s) are obtained in this way.

For comparison, the automaton that was defined in [3] for doing type inference without ⊥ had eight rather than four rules for generating transitions.

The intuition motivating the definition of M is that we want to identify the conditions that require a path to exist in the domain of any solution. Thus L(s) is the set of α that must be there; this intuition is made manifest in Lemma 8. It turns out that once we identify this set, we can construct a solution with domain L(s).

Lemma 8 If h : S → T_{Σ} is any solution and (s, s) →^{α} (u, v), then α ∈ D(h(s)). Moreover, h(u) ≤ h(s)↓α ≤ h(v).

Proof. We proceed by induction on the number of transitions. If this is zero, then (u, v) = (s, s) and α = ϵ, and the result is immediate. Otherwise, assume that (s, s) →^{α} (u, v) and the lemma holds for this sequence of transitions. We argue by cases, depending on the form of the next transition out of (u, v).

If (u, v) →^{ϵ} (u′, v′), then u′ →^{≤} u and v →^{≤} v′, so αϵ = α ∈ D(h(s)) and

h(u′) ≤ h(u) ≤ h(s)↓α ≤ h(v) ≤ h(v′) .

If (u, v) →^{1} (u′, v′), then u →^{1} u′ and v →^{1} v′, so h(u′) = h(u) ↓ 1 and

h(v′) = h(v)↓1. Then 1 ∈ D(h(u)) and 1 ∈ D(h(v)), so 1 ∈ D(h(s)↓α) and α1 ∈ D(h(s)), and

h(u′) = h(u)↓1 ≤ h(s)↓α1 ≤ h(v)↓1 = h(v′) .

If (u, v) →^{0} (v′, u′), then u →^{0} u′ and v →^{0} v′, so h(u′) = h(u) ↓ 0 and

h(v′) = h(v)↓0. Then 0 ∈ D(h(u)) and 0 ∈ D(h(v)), so 0 ∈ D(h(s)↓α) and α0 ∈ D(h(s)), and

h(u′) = h(u)↓0 ≥ h(s)↓α0 ≥ h(v)↓0 = h(v′) .
□

When certain paths in M exist, others must exist too, as expressed in Lemmas 9 and 10.

Lemma 9 If (u, v) →^{ϵ} (u′, v′), then for any w ∈ S, (w, v) →^{ϵ} (w, v′) and

(u, w) →^{ϵ} (u′, w).

Proof. We proceed by induction on the number of transitions in (u, v) →^{ϵ} (u′, v′). If it is zero, then (u, v) = (u′, v′) and the result is immediate. Otherwise, assume that (u, v) →^{ϵ} (u′, v′) and that the lemma holds for this sequence of transitions. We argue by cases, depending on the form of the next transition out of (u′, v′). Clearly, the next transition need be an ϵ-transition.

If (u′, v′) →^{ϵ} (u′, v′′) and v′ →^{≤} v′′ in G, then, by the induction hypothesis,

(w, v) →^{ϵ} (w, v′) →^{ϵ} (w, v′′) .

If (u′, v′) →^{ϵ} (u′′, v′) and u′′ →^{≤} u′ in G, then, by the induction hypothesis,

(u, w) →^{ϵ} (u′, w) →^{ϵ} (u′′, w) .

□

Lemma 10 If (u_{1}, v_{1}) →^{α} (u′_{1}, v′_{1}) and (u_{2}, v_{2}) →^{α} (u′_{2}, v′_{2}), then (u_{1}, v_{2}) →^{α}

(u′_{1}, v′_{2}).

Proof. We proceed by induction on the length of α. In the base case, consider |α| = 0. We then have α = ϵ, so by Lemma 9,

(u_{1}, v_{2}) →^{ϵ} (u′_{1}, v_{2}) →^{ϵ} (u′_{1}, v′_{2}) .

In the induction step, consider first

(u_{1}, v_{1}) →^{α1} (u′_{1}, v′_{1})

(u_{2}, v_{2}) →^{α1} (u′_{2}, v′_{2}) .

Choose x_{1}, y_{1}, x_{2}, y_{2} ∈ N and x′_{1}, y′_{1}, x′_{2}, y′_{2} ∈ S such that

(u_{1}, v_{1}) →^{α} (x_{1}, y_{1}) →^{1} (x′_{1}, y′_{1}) →^{ϵ} (u′_{1}, v′_{1})

(u_{2}, v_{2}) →^{α} (x_{2}, y_{2}) →^{1} (x′_{2}, y′_{2}) →^{ϵ} (u′_{2}, v′_{2})

and x_{1} →^{1} x′_{1}, y_{1} →^{1} y′_{1}, x_{2} →^{1} x′_{2}, y_{2} →^{1} y′_{2}. From the induction hypothesis and Lemma 9 we get

(u_{1}, v_{2}) →^{α} (x_{1}, y_{2}) →^{1} (x′_{1}, y′_{2}) →^{ϵ} (u′_{1}, y′_{2}) →^{ϵ} (u′_{1}, v′_{2}) .

Consider then

(u_{1}, v_{1}) →^{α0} (u′_{1}, v′_{1})

(u_{2}, v_{2}) →^{α0} (u′_{2}, v′_{2}) .

Choose x_{1}, y_{1}, x_{2}, y_{2} ∈ N and x′_{1}, y′_{1}, x′_{2}, y′_{2} ∈ S such that

(u_{1}, v_{1}) →^{α} (x_{1}, y_{1}) →^{0} (y′_{1}, x′_{1}) →^{ϵ} (u′_{1}, v′_{1})

(u_{2}, v_{2}) →^{α} (x_{2}, y_{2}) →^{0} (y′_{2}, x′_{2}) →^{ϵ} (u′_{2}, v′_{2})

and x_{1} →^{0} x′_{1}, y_{1} →^{0} y′_{1}, x_{2} →^{0} x′_{2}, y_{2} →^{0} y′_{2}. From the induction hypothesis and Lemma 9 we get

(u_{1}, v_{2}) →^{α} (x_{2}, y_{1}) →^{0} (y′_{1}, x′_{2}) →^{ϵ} (u′_{1}, x′_{2}) →^{ϵ} (u′_{1}, v′_{2}) .

□

The fundamental relation between a closed constraint graph G and the automaton M is expressed by Lemma 11.

Lemma 11 Suppose G is a closed constraint graph. If u →^{≤} v and (u, v) →^{α}

(u′, v′), then u′ →^{≤} v′.

Proof. We proceed by induction on the number of transitions in (u, v) →^{ϵ} (u′, v′). If it is zero, then (u, v) = (u′, v′) and the result is immediate. Otherwise, assume that (u, v) →^{α} (u′, v′) and that the lemma holds for this sequence of transitions. We argue by cases, depending on the form of the next transition out of (u′, v′).

If (u′, v′) →^{ϵ} (u′, v′′) and v′ →^{≤} v′′ in G, then, by the induction hypothesis, u′ →^{≤} v′, so since ≤ is transitive we have u′ →^{≤} v′′.

If (u′, v′) →^{ϵ} (u′′, v′) and u′′ →^{≤} u′ in G, then, by the induction hypothesis, u′ →^{≤} v′, so since ≤ is transitive we have u′′ →^{≤} v′.

If (u′, v′) →^{1} (u′′, v′′) and both u′ →^{1} u′′ and v′ →^{1} v′′, then, by the induction hypothesis, u′ →^{≤} v′, so since G is closed we have u′′ →^{≤} v′′.

If (u′, v′) →^{0} (v′′, u′′) and both u′ →^{0} u′′ and v′ →^{0} v′′, then, by the induction hypothesis, u′ →^{≤} v′, so since G is closed we have v′′ →^{≤} u′′. □

4 Upper bounds

We want to construct a solution ψ : S → T_{Σ} such that D(ψ(s)) = L(s) for all s ∈ S. Suppose L(u) ↓ α = {ϵ} for some u ∈ S. Then we want (ψ(u))(α) ∈ {⊥, ⊤}. The question is: should we pick ⊥ or ⊤? To answer this question, we consider Up(u, α), which intuitively is the set of upper bounds of u at level α, and is defined as follows.

Definition 12 Define Up : S × {0, 1}^{∗} → 2^{N} as follows:

Up(s, α) = {w ∈ N | (s, s) →^{α} (u, w) for some u ∈ S}

□

Lemma 13 Suppose u →^{≤} v and α ∈ L(u) ∩ L(v).

1. If Up(u, α) = ∅, then Up(v, α) = ∅.

2. If Up(v, α) = ∅ and πα = 1, then Up(u, α) = ∅.

3. If L(u)↓α ≠ {ϵ}, L(v)↓α = {ϵ}, then Up(v, α) = ∅.

4. If L(v)↓α ≠ {ϵ}, L(u)↓α = {ϵ}, and πα = 1, then Up(u, α) = ∅.

Proof. To prove (1), suppose Up(v, α) ≠ ∅. Choose w ∈ N and u′ ∈ S such that (v, v) →^{α} (u′, w). Choose also u_{1}, v_{1} ∈ S such that (u, u) →^{α} (u_{1}, v_{1}). From u →^{≤} v and Lemma 10 we then get

(u, u) →^{ϵ} (u, v) →^{α} (u_{1}, w) ,

contradicting Up(u, α) = ∅.

To prove (2), suppose Up(u, α) ≠ ∅. Since πα = 1, we can write α = β0γ where β ∈ {0, 1}⋆ and γ ∈ {1}⋆. Choose x_{1}, y_{1}, w ∈ N and x_{2}, y_{2}, u′ ∈ S such that

(u, u) →^{β} (x_{1}, y_{1}) →^{0} (y_{2}, x_{2}) →^{γ} (u′, w)

and x_{1} →^{0} x_{2} and y_{1} →^{0} y_{2}. Choose p_{1}, q_{1} ∈ N and p_{2}, q_{2}, u′′, v′′ ∈ S such that

(v, v) →^{β} (p_{1}, q_{1}) →^{0} (q_{2}, p_{2}) →^{γ} (u′′, v′′)

and p_{1} →^{0} p_{2} and q_{1} →^{0} q_{2}. From u →^{≤} v and Lemma 10 we then get

(v, v) →^{ϵ} (u, v) →^{β} (x_{1}, q_{1}) →^{0} (q_{2}, x_{2}) →^{γ} (u′′, w) ,

contradicting Up(v, α) = ∅.

To prove (3), suppose Up(v, α) ≠ ∅. Choose w ∈ N and u′ ∈ S such that (v, v) →^{α} (u′, w). Choose also x, y ∈ N such that (u, u) →^{α} (x, y). From u →^{≤} v and Lemma 10 we get

(v, v) →^{ϵ} (u, v) →^{α} (x, w) ,

contradicting L(v)↓α = {ϵ}.

To prove (4), suppose Up(u, α) ≠ ∅. Since πα = 1, we can write α = β0γ where β ∈ {0, 1}⋆ and γ ∈ {1}⋆. Choose x_{1}, y_{1}, w ∈ N and x_{2}, y_{2}, u′ ∈ S such that

(u, u) →^{β} (x_{1}, y_{1}) →^{0} (y_{2}, x_{2}) →^{γ} (u′, w)

and x_{1} →^{0} x_{2} and y_{1} →^{0} y_{2}. Since L(v) ↓ α ≠ {ϵ}, choose p_{1}, q_{1}, u′′, v′′ ∈ N

and p_{2}, q_{2} ∈ S such that

(v, v) →^{β} (p_{1}, q_{1}) →^{0} (q_{2}, p_{2}) →^{γ} (u′′, v′′)

and p_{1} →^{0} p_{2} and q_{1} →^{0} q_{2}. From u →^{≤} v and Lemma 10 we then get

(u, u) →^{ϵ} (u, v) →^{β} (x_{1}, q_{1}) →^{0} (q_{2}, x_{2}) →^{γ} (u′′, w) ,

contradicting L(u)↓α = ∅. □

Lemma 14 Suppose i ∈ {0, 1}, u →^{i} v, and α ∈ L(v).

1. If Up(u, iα) = ∅, then Up(v, α) = ∅.

2. Suppose G is closed. If Up(v, α) = ∅, then Up(u, iα) = ∅.

Proof. To prove (1), suppose Up(v, α) ≠ ∅. Choose w ∈ N and u′ ∈ S such that

(u, u) →^{i} (v, v) →^{α} (u′, w) ,

contradicting Up(u, iα) = ∅.

To prove (2), suppose Up(u, iα) ≠ ∅. Choose w ∈ N and u′, u_{1}, v_{1} ∈ S such that

(u, u) →^{i} (u_{1}, v_{1}) →^{α} (u′, w) .

From (u, u) →^{i} (v, v) and Lemma 10 we get

(u, u) →^{i} (u_{1}, v)

(u, u) →^{i} (v, v_{1}) .

From u →^{≤} u and Lemma 11 we get u_{1} →^{≤} v →^{≤} v_{1}, hence

(v, v) →^{ϵ} (u_{1}, v_{1}) →^{α} (u′, w) ,

contradicting Up(v, α) = ∅. □

Lemma 15 Suppose i ∈ {0, 1}, u →^{i} v, and α ∈ L(v). If G is closed and L(v)↓α = {ϵ}, then L(u)↓iα = {ϵ}.

Proof. Suppose L(u) ↓ iα ≠ {ϵ}. Choose x, y ∈ N and u_{1}, v_{1} ∈ S such that

(u, u) →^{i} (u_{1}, v_{1}) →^{α} (x, y) .

From (u, u) →^{i} (v, v) and Lemma 10 we get

(u, u) →^{i} (u_{1}, v)

(u, u) →^{i} (v, v_{1}) .

From u →^{≤} u and Lemma 11 we get u_{1} →^{≤} v →^{≤} v_{1}, hence

(v, v) →^{ϵ} (u_{1}, v_{1}) →^{α} (x, y) ,

contradicting L(v)↓α = {ϵ}. □

5 Main result

Definition 16 Let a closed constraint graph G = (S, L, R, ≤) be given. Define ψ : S → T_{Σ} as follows:

ψ(s) = λα. \{ \begin{matrix}⊤ & if α ∈ L(s) ∧ L(s)↓α = \{ϵ\} ∧ Up(s, α) = ∅ \\ ⊥ & if α ∈ L(s) ∧ L(s)↓α = \{ϵ\} ∧ Up(s, α) ≠ ∅ \\ → & if α ∈ L(s) ∧ L(s)↓α ≠ \{ϵ\} \\ undefined & if α ∉ L(s) \end{matrix}

□

Theorem 17 If G is a closed constraint graph, then the function ψ is a solution of G. Moreover, if h : S → T_{Σ} is any other solution of G, then D(ψ(s)) ⊆ D(h(s)) for any s.

Proof. For any s ∈ S, notice that ψ(s) is nonempty since (s, s) →^{ϵ} (s, s), that it is prefix-closed since all states of M_{s} are accept states, that if (ψ(s))(α) =→ then {i | αi ∈ D(ψ(s))} = {0, 1}, and that if (ψ(s))(α) ∈ {⊥, ⊤} then {i | αi ∈ D(ψ(s))} = ∅, so ψ(s) ∈ T_{Σ}. Notice also that D(ψ(s)) = L(s) for all s ∈ S.

We first prove that

If u →^{0} v_{0} and u →^{1} v_{1}, then ψ(u) = ψ(v_{0}) → ψ(v_{1}).

Notice that ψ(u) = ψ(v_{0}) → ψ(v_{1}) is equivalent to

(ψ(u))(α) = (ψ(v_{0}) → ψ(v_{1}))(α) for all α ∈ D(ψ(u)) ∩ D(ψ(v_{0}) → ψ(v_{1})).

(5)

To see this equivalence, notice that (5) implies both ψ(u) ≤ ψ(v_{0}) → ψ(v_{1}) and ψ(u) ≥ ψ(v_{0}) → ψ(v_{1}).

To prove (5), notice first that (ψ(u))(ϵ) = (ψ(v_{0}) → ψ(v_{1}))(ϵ) =→. Then, let i ∈ {0, 1} and iα ∈ D(ψ(u)) ∩ D(ψ(v_{0}) → ψ(v_{1})). It is sufficient to prove

(ψ(u))(iα) = (ψ(v_{i}))(α) .

There are three cases. Suppose (ψ(v_{i}))(α) =→. Then L(v_{i}) ↓ α ≠ {ϵ}. From (u, u) →^{i} (v_{i}, v_{i}) we get L(u) ↓ iα ≠ {ϵ}, so (ψ(u))(iα) =→. Suppose then (ψ(v_{i}))(α) = ⊥. Then L(v_{i}) ↓ α = {ϵ} and Up(v_{i}, α) ≠ ∅. From Lemma 14.1 we get Up(u, iα) ≠ ∅. From Lemma 15 we get L(u) ↓ iα = {ϵ}, so (ψ(u))(iα) = ⊥. Suppose finally (ψ(v_{i}))(α) = ⊤. Then L(v_{i}) ↓ α = {ϵ} and Up(v_{i}, α) = ∅. From Lemma 14.2 we get Up(u, iα) = ∅. From Lemma 15 we get L(u)↓iα = {ϵ}, so (ψ(u))(iα) = ⊤.

We then prove that

If u →^{≤} v, then ψ(u) ≤ ψ(v).

Suppose α ∈ D(ψ(u)) ∩ D(ψ(v)) = L(u) ∩ L(v). We then need to prove (ψ(u))(α) ≤_{πα} (ψ(v))(α). There are two cases.

Suppose first πα = 0. If (ψ(u))(α) = ⊥, then the result is immediate. If (ψ(u))(α) = ⊤, then L(u) ↓ α = {ϵ} and Up(u, α) = ∅. By Lemma 13.1, Up(v, α) = ∅. Hence, L(v) ↓ α = {ϵ}, so (ψ(v))(α) = ⊤, from which the result follows. If (ψ(u))(α) =→, then there are two cases. If L(v)↓α ≠ {ϵ}, then (ψ(v))(α) =→, from which the result follows. If L(v) ↓ α = {ϵ}, then it follows from Lemma 13.3 that Up(v, α) = ∅. Hence, (ψ(v))(α) = ⊤, from which the result follows.

Suppose then πα = 1. If (ψ(v))(α) = ⊥, then the result is immediate. If (ψ(v))(α) = ⊤, then L(v) ↓ α = {ϵ} and Up(v, α) = ∅. By Lemma 13.2, Up(u, α) = ∅. Hence, L(u) ↓ α = {ϵ}, so (ψ(u))(α) = ⊤, from which the result follows. If (ψ(v))(α) =→, then there are two cases. If L(u)↓α ≠ {ϵ}, then (ψ(u))(α) =→, from which the result follows. If L(u) ↓ α = {ϵ}, then it follows from Lemma 13.4 that Up(u, α) = ∅. Hence, (ψ(u))(α) = ⊤, from which the result follows.

To show that ψ is a solution of minimal size, we need to show that for any other solution h : S → T_{Σ} of G, D(ψ(s)) ⊆ D(h(s)) for any s. This follows directly from Lemma 8. □

6 An Algorithm

We have shown that the type inference problem for PTB can be reduced to solving constraint graphs. Using the characterization of Theorem 17, we get a straightforward type inference algorithm.

Theorem 18 One can decide in time O(n^{3}) whether a constraint graph of size n has a finite solution.

Proof. By Theorem 17, there exists a finite solution if and only if the domain of the constructed solution ψ is finite. To determine this, we need only check whether any L(s) contains an infinite path. We first form the constraint graph, then close it; this gives a graph with n vertices and O(n^{2}) edges. This can be done in time O(n^{3}). We then form the automaton M, which has n^{2} states but only O(n^{3}) transitions, at most O(n) from each state. We then check for a cycle with at least one non-ϵ transition reachable from some (s, s). This can be done in linear time in the size of the graph using depth-first search. The entire algorithm requires time O(n^{3}). □

A λ-term of size n yields a constraint graph with O(n) nodes and O(n) edges. Allowing types to be represented succinctly by the automata M_{s}, we get our main result.

Corollary 19 The type inference problem for PTB is solvable in O(n^{3}) time.

Recursive types are just regular trees [1]. The minimal-size solution we have constructed, although possibly infinite, is a regular tree for every node in the constraint graph. Thus, we get the following result.

Corollary 20 For PTB_{μ}, we can infer a minimal-size type annotation in O(n^{3}) time.

It remains to be seen how to extend this result to PTB_{μ} ∪ {Int}.

7 Example

We now give an example of how our type inference algorithm works. Consider the λ-term E = (λx.xx)(λy.y) which was also treated in [5]. We give each of the two occurrences of x a label so that the λ-term reads (λx.x_{1}x_{2})(λy.y). The constraint system T (E) looks as follows:

From λx.x_{1}x_{2} x → [[x_{1}x_{2}]] ≤ [[λx.x_{1}x_{2}]]
From λy.y  y → [[y]] ≤ [[λy.y]]
From E  [[λx.x_{1}x_{2}]] ≤ [[λy.y]] → [[E]]
From x_{1}x_{2}  [[x_{1}]] ≤ [[x_{2}]] → [[x_{1}x_{2}]]
From x_{1}  x ≤ [[x_{1}]]
From x_{2}  x ≤ [[x_{2}]]
From y  y ≤ [[y]]

To the left of the constraints, we have indicated from where they arise. We will use the following abbreviations:

The symbol: abbreviates:
→_{1}  x → [[x_{1}x_{2}]]
→_{2}  y → [[y]]
→_{3}  [[λy.y]] → [[E]]
→_{4}  [[x_{2}]] → [[x_{1}x_{2}]]

The constraint graph derived from T (E) looks as follows:

[figure: →_{1}; →_{2}; →_{3}; →_{4}; [[λx.x_{1}x_{2}]]; [[x_{1}x_{2}]]; [[λy.y]]; [[E]]; [[x_{1}]]; [[y]]; [[x_{2}]]; x; y; ≤; ≤; ≤; ≤; ≤; ≤; ≤; 0; 0; 0; 0; 1; 1; 1; 1]

To close the constraint graph, it is sufficient to first fill in the edges

[[x_{1}x_{2}]] →^{≤} [[E]]
[[λy.y]] →^{≤} x
[[y]] →^{≤} [[x_{1}x_{2}]]
[[x_{2}]] →^{≤} y ,

and then make ≤ transitive.

The constraint graph has 13 nodes, so the automaton M has 13^{2} = 169 states. The following picture shows some of the states reachable from the state (x, x).

[figure: (x, x); (x, [[x_{1}]]); (x, →_{4}); ([[λy.y]], x); ([[λy.y]], [[x_{1}]]); ([[λy.y]], →_{4}); (→_{2}, x); (→_{2}, [[x_{1}]]); (→_{2}, →_{4}); ([[y]], [[x_{1}x_{2}]]); ([[x_{2}]], y); ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; ϵ; 1; 0]

It turns out that

L(x) = {ϵ, 0, 1}
L(y) = {ϵ}
Up(x, 0) = ∅
Up(x, 1) = ∅
Up(y, ϵ) = ∅ .

We then get

ψ(x) = ⊤ → ⊤
ψ(y) = ⊤ ,

and it turns out that E is typable.

For comparison, we can apply the algorithm for type inference for PTB extended with recursive types [5] to E. The result is that both x and y get annotated by the infinite type μα.α → α [5].

References

[1] Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993. Also in Proc. POPL’91.

[2] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science. To appear. Also in Proc. POPL’93, Twentieth Annual SIGPLAN–SIGACT Symposium on Principles of Programming Languages, pages 419–428, Charleston, South Carolina, January 1993.

[3] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. Journal of Computer and System Sciences, 49(2):306–324, 1994. Also in Proc. FOCS’92, 33rd IEEE Symposium on Foundations of Computer Science, pages 363–371, Pittsburgh, Pennsylvania, October 1992.

[4] John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1:245–285, 1991.

[5] Jens Palsberg and Patrick M. O’Keefe. A type system equivalent to flow analysis. In Proc. POPL’95, 22nd Annual SIGPLAN–SIGACT Symposium on Principles of Programming Languages, pages 367–378, San Francisco, California, January 1995.

[6] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference for partial types. Information Processing Letters, 43:175–180, 1992.

[7] Satish Thatte. Type inference with partial types. In Proc. International Colloquium on Automata, Languages, and Programming 1988, pages 615– 629. Springer-Verlag (LNCS 317), 1988.

[8] Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1–15, 1991.

[9] Mitchell Wand, Patrick M. O’Keefe, and Jens Palsberg. Strong normalization with non-structural subtyping. Mathematical Structures in Computer Science. To appear.

Recent Publications in the BRICS Report Series

RS-95-33 Jens Palsberg, Mitchell Wand, and Patrick O’Keefe. Type Inference with Non-structural Subtyping. June 1995. 22 pp.

RS-95-32 Jens Palsberg. Ef�cient Inference of Object Types. June 1995. 32 pp. To appear in Information and Computation. Preliminary version appears in Ninth Annual IEEE Symposium on Logic in Computer Science, LICS ’94 Proceedings, pages 186�195.

RS-95-31 Jens Palsberg and Peter �rb�k. Trust in the λ-calculus. June 1995. 32 pp. To appear in Static Analysis: 2nd International Symposium, SAS ’95 Proceedings, 1995.

RS-95-30 Franck van Breugel. From Branching to Linear Metric Domains (and back). June 1995. 30 pp. Abstract appeared in Engberg, Larsen, and Mosses, editors, 6th Nordic Workshop on Programming Theory, NWPT ’6 Proceedings, 1994, pages 444-447.

RS-95-29 Nils Klarlund. An n log n Algorithm for Online BDD Re�nement. May 1995. 20 pp.

RS-95-28 Luca Aceto and Jan Friso Groote. A Complete Equational Axiomatization for MPA with String Iteration. May 1995. 39 pp.

RS-95-27 David Janin and Igor Walukiewicz. Automata for the μcalculus and Related Results. May 1995. 11 pp. To appear in Mathematical Foundations of Computer Science: 20th Int. Symposium, MFCS ’95 Proceedings, LNCS, 1995.

RS-95-26 Faith Fich and Peter Bro Miltersen. Tables should be sorted (on random access machines). May 1995. 11 pp. To appear in Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS, 1995.

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.

RS-95-24 Peter �rb�k. Can you Trust your Data? April 1995. 15 pp. Appears in Mosses, Nielsen, and Schwartzbach, editors, Theory and Practice of Software Development. 6th International Joint Conference CAAP/FASE, TAPSOFT ’95 Proceedings, LNCS 915, 1995, pages 575�590.