A Type System Equivalent to Flow Analysis^{∗}

Jens Palsberg^{†} Patrick O’Keefe^{‡}

Abstract

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis.

In this paper we prove that Amadio and Cardelli’s type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

1 Introduction

1.1 Background

Many program analyses for higher-order languages are based on flow analysis, also known as closure analysis. Examples include various analyses in the Standard ML of New Jersey compiler [3], and the binding-time analyses for Scheme in the partial evaluators Schism [5] and Similix [4]. Such analyses have the advantage that they can be applied to untyped languages. This is in contrast to more traditional abstract interpretations which use types when defining the abstract domains.

Recently, it has become popular to define program analyses for typed languages by annotating the types with information about program behavior [8, 2]. This has lead to clear specifications of a range of analyses, and often such an analysis can be efficiently computed by a straightforward extension of a known type inference algorithm.

∗Extended abstract of a paper in Proc. POPL’95, 22nd Annual SIGPLAN–SIGACT Symposium on Principles of Programming Languages.

†Computer Science Department, Aarhus University, DK-8000 Aarhus C, Denmark. E-mail:

palsberg@daimi.aau.dk.

‡151 Coolidge Avenue #211, Watertown, MA 02172, USA. E-mail: pmo@world.std.com.

The precision of a type-based analysis depends on the expressiveness of the underlying type system. Similarly, the precision of a flow-based analysis depends on the expressiveness of the underlying flow analysis. In this paper we address an instance of the following fundamental question:

Fundamental question. What type-based analysis computes the same information as a given flow-based analysis?

We consider the case of flow-based safety analysis, that is, an analysis which collects type information from for example constants and applications of primitive operations. Such an analysis was first presented in 1991 by Shivers [13] who called it type recovery. Later, Palsberg and Schwartzbach [11, 10] proved that on the basis of the collected information, one can define a predicate which accepts only programs which cannot go wrong. They called this safety analysis. They also proved that their safety analysis accepts more programs than simple type inference.

In this paper, we consider the following instance of the above question:

Which type system accepts the same programs as safety analysis?

The particular safety analysis we consider is defined in Section 3.

Our thesis is that the type system that answers this specific question will in many cases also be the answer to the fundamental question.

1.2 Our result

We prove that a natural type system with subtyping and recursive types accepts the same programs as safety analysis. The proof involves mappings from types to flow information and back.

The type system has been studied by Amadio and Cardelli [1], and an O(n^{2}) algorithm for deciding the subtyping relation has been presented by Kozen, Palsberg, Schwartzbach, [6]. Open until now is the question of type inference. As a corollary of our result we get a type inference algorithm which works by first doing safety analysis and then mapping the flow information to types.

The set of types can be presented by the following grammar:

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

The type system contains the following components: the binary function type constructor →, the constant type Int, the possibility for creating recursive types, and two more constant types ⊤, and ⊥. Moreover, there is a subtype relation, written ≤. In contrast, safety analysis uses an abstract domain containing sets of syntactic occurrences of abstractions and the constant Int.

In slogan-form, our result reads:

Flow analysis + Safety checks = Simple types + Recursive types + ⊤ + ⊥ + Subtyping

Each component of the type system captures a facet of flow analysis:

• The function type constructor → corresponds to a set of abstractions. Intuitively, a function type is less concrete than a set of abstractions. Indeed, the other components of the type system are essential to make it accept the same programs as the safety analysis.

• The constant Int is used for the same purpose in both systems. For simplicity, we do not consider other base types, or product and sum constructors, etc. Such constructs can be handled by techniques that are similar to the ones we will present.

• Recursive types are needed in order that safety analysis accepts all programs that do not contain constants.

• The constant ⊤ corresponds to the largest possible set of flow information. This type is needed for variables which can hold both a function and a base value. Intuitively, a program with such a variable should be type incorrect. However, the flow-based analysis may detect that this variable is only passed around but never actually used. For the type system to have that capability, ⊤ is required.

• The constant ⊥ corresponds to the empty set of flow information. This type is needed for variables which are used both as a function and as a base value. Intuitively, a program that uses a variable in both these ways should be type incorrect. However, the flow-based analysis may detect that this part of the program will never be executed. For the type system to have that capability, ⊥ is required.

• Subtyping is needed to capture flow of information. Intuitively, if information flows from A to B, then the type of A will be a subtype of the type of B.

Palsberg and Schwartzbach [10, 11] proved that the system without ⊥ accepts at most as many programs as safety analysis. In this paper we present the type system which accepts exactly the same programs as safety analysis. This may be seen as a natural culmination of the previous results.

1.3 Examples

Our example language is a λ-calculus, generated by the following grammar:

E ::= x | λx.E | E_{1}E_{2} | 0 | succ E

Programs that yield a run-time error include (0 x), succ(λx.x), and (succ 0)(x), because 0 is not a function, succ cannot be applied to functions, and (succ 0) is not a function. These programs are not typable and they are rejected by safety analysis. Some programs can be typed in the type system without the use of ⊥ and ⊤, for example

λx.xx : μα.α → α ,

where E : t means “E has type t”. Some programs require the use of ⊤, for example

(λf.(λx.fI)(f0))I : ⊤ ,

where I = λx.x. Note that ⊤ is the only type of (λf.(λx.fI)(f0))I. Some programs require the use of ⊥, for example

λx.x(succ x) : ⊥ → t for any t.

Both type inference and safety analysis can be phrased as solving a system of constraints, derived from the program text. We will now present the constraint systems for the last of the above examples. For notational convenience, we give each of the two occurrences of x a label so that the λ-term reads λx.x_{1}(succ x_{2}). For brevity, let E = λx.x_{1}(succ x_{2}). The constraint system for type inference looks as follows:

x → [[x_{1}(succ x_{2})]] ≤ [[E]]
[[x_{1}]] ≤ [[succ x_{2}]] → [[x_{1}(succ x_{2})]]
x ≤ [[x_{1}]]
x ≤ [[x_{2}]]
Int ≤ [[succ x_{2}]]
[[x_{2}]] ≤ Int

Here, the symbols x, [[x_{1}]], [[x_{2}]], [[succ x_{2}]], [[x_{1}(succ x_{2})]], [[E]] are type variables. Solving this constraint system yields that the possible types for the λ-term λx.x(succ x) are ⊤ and ⊥ → t for any type t. Among these, ⊥ → ⊥ is a least type. In general, however, such a constraint system need not have a least solution.

The constraint system for safety analysis looks as follows:

{E} ⊆ [[E]]
[[x_{1}]] ⊆ {E}
x ⊆ [[x_{1}]]
x ⊆ [[x_{2}]]
{E} ⊆ [[x_{1}]] ⇒ [[succ x_{2}]] ⊆ x
{E} ⊆ [[x_{1}]] ⇒ [[x_{1}(succ x_{2})]] ⊆ [[x_{1}(succ x_{2})]]
{Int} ⊆ [[succ x_{2}]]
[[x_{2}]] ⊆ {Int}

If such a constraint system is solvable, then it has a least solution. This particular constraint system is indeed solvable, and the least solution is the mapping φ, where

φ([[E]]) = {E}
φ([[succ x_{2}]]) = {Int}
φ([[x_{1}(succ x_{2})]]) = φ(x) = φ([[x_{1}]]) = φ([[x_{2}]]) = ∅

In the following two sections we present the type system and the safety analysis, and in Section 4 we prove that they accept the same programs.

2 The type system

2.1 Types

Definition 1 Let Σ = {→, Int, ⊥, ⊤} be the ranked alphabet where → is binary and Int, ⊥, ⊤ are nullary. A type is a regular 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”. □

Definition 2 We represent a type by a term, that is, a partial function

t : {0, 1}∗ → Σ

with domain D(t) where t maps each path from the root of the type to the symbol at the end of the path. The set of all such terms is denoted T_{Σ}. □

Following [6], we finitely represent a term by a so-called term automaton, as follows.

Definition 3 A term automaton over Σ is a tuple

M = (Q, Σ, q_{0}, δ, ℓ)

where:

• Q is a finite set of states,

• q_{0} ∈ Q is the start state,

• δ : Q × {0, 1} → Q is a partial function called the transition function, and

• ℓ : Q → Σ is a (total) labeling function, such that for any state q ∈ Q, if ℓ(q) ∈ {→} then

{i | δ(q, i) is defined} = {0, 1}

and if ℓ(q) ∈ {Int, ⊥, ⊤} then

{i | δ(q, i) is defined} = ∅ .

The partial function δ extends naturally to a partial function

δ̂: Q × {0, 1}∗ → Q

inductively as follows:

δ̂(q, ϵ) = q
δ̂(q, αi) = δ(δ̂(q, α), i) , for i ∈ {0, 1}.

The term represented by M is the term

t_{M} = λα.ℓ(δ̂(q_{0}, α)) .
□

Intuitively, t_{M}(α) is determined by starting in the start state q_{0} and scanning the input α, following transitions of M as far as possible. If it is not possible to scan all of α because some i-transition along the way does not exist, then t_{M}(α) is undefined. If on the other hand M scans the entire input α and ends up in state q, then t_{M}(α) = ℓ(q).

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

Definition 4 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
⊥ ≤_{0} Int and Int ≤_{0} ⊤

and let ≤_{1} be its reverse

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

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

Kozen, Palsberg, and Schwartzbach [6] showed that the relation ≤ is equivalent to the order defined by Amadio and Cardelli [1]. The relation ≤ is a partial order, and if s → t ≤ s′ → t′, then s′ ≤ s and t ≤ t′ [1, 6].

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 six rules:

A ⊢ 0 : Int (1)

\frac{A ⊢ E : Int}{A ⊢ succ E : Int} (2)

A ⊢ x : t (provided A(x) = t) (3)

\frac{A[x ← s] ⊢ E : t}{A ⊢ λx.E : s → t} (4)

\frac{A ⊢ E : s → t A ⊢ F : s}{A ⊢ EF : t} (5)

\frac{A ⊢ E : s s ≤ t}{A ⊢ E : t} (6)

The first five 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.

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 0, the inequality

Int ≤ [[0]] ;

• for every occurrence in E of a subterm of the form succ F, the two inequalities

Int ≤ [[succ F]]
[[F]] ≤ Int ;

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

(x → [[F]])_{λx.F} ≤ [[λx.F]] ;

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

[[G]] ≤ ([[H]] → [[GH]])_{GH} ;

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

x ≤ [[x]] .

The subscripts are present to ease notation in Section 4.1; they have no semantic impact and will be explicitly written only in Section 4.1.

Denote by T (E) the system of constraints generated from E in this fashion. The solutions of T (E) over T_{Σ} correspond to the possible type annotations of E in a sense made precise by Theorem 5.

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 5 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 [7], in outline as follows. Given a solution of the constraint system, it is straightforward to construct a derivation of A ⊢ M: t. Conversely, observe that if A ⊢ M: t is derivable, then there exists a derivation of A ⊢ M: 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 [14, 11] then gives a set of inequalities of the desired form. □

3 The safety analysis

Following [10, 11], we will use a flow analysis as a basis for a safety analysis. Given a λ-term E, assume that E has been α-converted so that all bound variables are distinct. The set Abs(E) is the set of subterms of E of the form λx.F. The set Cl(E) is the powerset of Abs(E) ∪ {Int}. Safety analysis of a λ-term E can be phrased as solving the following system of constraints over X_{E} ∪ Y_{E} where type variables range over Cl(E).

• For every occurrence in E of a subterm of the form 0, the constraint

{Int} ⊆ [[0]] ;

• for every occurrence in E of a subterm of the form succ F, the two constraints

{Int} ⊆ [[succ F]]
[[F]] ⊆ {Int}

where the latter provides a safety check;

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

({λx.F })_{λx.F} ⊆ [[λx.F]] ;

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

[[G]] ⊆ (Abs(E))_{GH} ;

which provides a safety check;

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

x ⊆ [[x]] ;

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

({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[H]] ⊆ x
({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[F]] ⊆ [[GH]] .

Again, the subscripts are present to ease notation in Section 4.1; they have no semantic impact and will be explicitly written only in Section 4.1.

Denote by C(E) the system of constraints generated from E in this fashion. A solution of C(E) assigns an element of Cl(E) to each type variable such that all constraints are satisfied. Solutions are ordered by variable-wise set inclusion. See [10, 12] for a cubic time algorithm that given E computes the least solution of C(E) or decides that none exists. See [9] for a proof of the following subject reduction property. If E β-reduces to E′, and C(E) has solution φ, then C(E′) also has solution φ.

4 Equivalence

4.1 Deductive Closures

We now introduce two auxiliary constraint systems called \overline{C}(E) and \overline{T} (E). They may be thought of as “deductive closures” of C(E) and T (E). We then show that they are isomorphic (Theorem 9).

Definition 6 For every λ-term E, define \overline{C}(E) to be the smallest set such that:

• The non-conditional constraints of C(E) are members of \overline{C}(E).

• If a constraint c ⇒ K is in C(E) and c is in \overline{C}(E), then K is in \overline{C}(E).

• For s ∈ X_{E} ∪ Y_{E}, if r ⊆ s and s ⊆ t both are in \overline{C}(E), then r ⊆ t is in \overline{C}(E).

Notice that every constraint in \overline{C}(E) is of the form W ⊆ W′, where W is of the forms V, {Int}, or ({λx.F })_{λx.F}, and where W′ is of the forms V, {Int}, or (Abs(E))_{GH}, for V ∈ X_{E} ∪ Y_{E}. □

Definition 7 For every λ-term E, define \overline{T} (E) to be the smallest set such that:

• T (E) ⊆ \overline{T} (E).

• If (s → t)_{λx.F} ≤ (s′ → t′)_{GH} is in \overline{T} (E), then s′ ≤ s and t ≤ t′ are in \overline{T} (E).

• For s ∈ X_{E} ∪ Y_{E}, if r ≤ s and s ≤ t both are in \overline{T} (E), then r ≤ t is in \overline{T} (E).

Notice that every constraint in \overline{T} (E) is of the form W ≤ W′ where W is of the forms V, Int, or (V → V′)_{λx.F}, and where W′ is of the form V, Int, or (V → V′)_{GH}, for V, V′ ∈ X_{E} ∪ Y_{E}. □

We will now present the definition of two functions I and J, one from \overline{C}(E) to \overline{T} (E) and one from \overline{T} (E) to \overline{C}(E). After the definition we prove that they are well-defined and each others inverses.

Definition 8 The functions

I : \overline{C}(E) → \overline{T} (E)
J : \overline{T} (E) → \overline{C}(E)

are defined as follows.

I(W ⊆ W′) = (L_{I}(W) ≤ L_{I}(W′))
J (W ≤ W′) = (L_{J} (W) ⊆ L_{J} (W′))

where the functions L_{I} and L_{J} are:

L_{I}(W) = \{ \begin{matrix}W & if W ∈ X_{E} ∪ Y_{E} \\ Int & if W = \{Int\} \\ (x → [[F]])_{λx.F} & if W = (\{λx.F \})_{λx.F} \\ ([[H]] → [[GH]])_{GH} & if W = (Abs(E))_{GH} \end{matrix}

L_{J} (W) = \{ \begin{matrix}W & if W ∈ X_{E} ∪ Y_{E} \\ \{Int\} & if W = Int \\ (\{λx.F \})_{λx.F} & if W = (x → [[F]])_{λx.F} \\ (Abs(E))_{GH} & if W = ([[H]] → [[GH]])_{GH} \end{matrix}

□

Theorem 9 The sets \overline{C}(E) and \overline{T} (E) are isomorphic, and I and J are bijections and each others inverses.

Proof. If I and J are well-defined, then clearly they are inverses of each other and thus bijections, so \overline{C}(E) and \overline{T} (E) are isomorphic.

First we show that I is well-defined. We proceed by induction on the construction of \overline{C}(E). In the base case, consider the non-conditional constraints of C(E) and observe that for those we have:

\overline{C}(E)  \overline{T} (E)
{Int} ⊆ [[0]]  Int ≤ [[0]]
{Int} ⊆ [[succ F]]  Int ≤ [[succ F]]
[[F]] ⊆ {Int}  [[F]] ≤ Int
({λx.F })_{λx.F} ⊆ [[λx.F]] (x → [[F]])_{λx.F} ≤ [[λx.F]]
[[G]] ⊆ (Abs(E))_{GH}  [[G]] ≤ ([[H]] → [[GH]])_{GH}
x ⊆ [[x]]  x ≤ [[x]]

It follows that the lemma holds in the base case.

In the induction step, consider first the constraints

({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[H]] ⊆ x
({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[F]] ⊆ [[GH]]

in C(E) and suppose (\{λx.F \})_{λx.F} ⊆ [[G]] is in \overline{C}(E). By the induction hypothesis, (x → [[F]])_{λx.F} ≤ [[G]] is in \overline{T} (E). Moreover, [[G]] ≤ ([[H]] → [[GH]])_{GH} is in T (E) and thus also in \overline{T} (E). Hence, (x → [[F]])_{λx.F} ≤ ([[H]] → [[GH]])_{GH} is in \overline{T} (E), so also [[H]] ≤ x and [[F]] ≤ [[GH]] are in \overline{T} (E).

Consider then r ⊆ s and s ⊆ t in \overline{C}(E), and suppose s ∈ X_{E} ∪ Y_{E}. By the induction hypothesis, L_{I}(r) ≤ L_{I}(s) and L_{I}(s) ≤ L_{I}(t) are in \overline{T} (E). From s ∈ X_{E} ∪ Y_{E} we get L_{I}(s) = s, so L_{I}(r) ≤ L_{I}(t) is in \overline{T} (E).

Then we show that J is well-defined. We proceed by induction on the construction of \overline{T} (E). In the base case, consider the constraints of T (E). Using the same table as above we observe that J is well-defined on all these constraints.

In the induction step, consider first (x → [[F]])_{λx.F} ≤ ([[H]] → [[GH]])_{GH} in \overline{T} (E). It is sufficient to prove that L_{J} ([[H]]) ⊆ L_{J} (x) and L_{J} ([[F]]) ⊆ L_{J} ([[GH]]) are in \overline{C}(E), or equivalently, that [[H]] ⊆ x and [[F]] ⊆ [[GH]] are in \overline{C}(E). In C(E) we have

({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[H]] ⊆ x
({λx.F })_{λx.F} ⊆ [[G]] ⇒ [[F]] ⊆ [[GH]] .

Moreover, (\{λx.F \})_{λx.F} ⊆ [[G]] is in \overline{C}(E). Hence, [[H]] ⊆ x and [[F]] ⊆ [[GH]] are in \overline{C}(E).

Consider then r ≤ s and s ≤ t in \overline{T} (E), and suppose s ∈ X_{E} ∪ Y_{E}. By the induction hypothesis, L_{J} (r) ⊆ L_{J} (s) and L_{J} (s) ⊆ L_{J} (t) are in \overline{C}(E). From s ∈ X_{E} ∪ Y_{E} we get L_{J} (s) = s, so L_{J} (r) ⊆ L_{J} (t) is in \overline{C}(E). □

4.2 The equivalence proof

Definition 10 For every λ-term E, let Tmap(E) be the set of total functions from X_{E} ∪ Y_{E} to T_{Σ} and let Cmap(E) be the set of total functions from X_{E} ∪ Y_{E} to Cl(E). □

The following construction is the key to mapping flow information to types.

Definition 11 For every λ-term E, φ ∈ Cmap(E), and q_{0} ∈ Cl(E), define the term automaton A(E, φ, q_{0}) as follows:

A(E, φ, q_{0}) = (Cl(E), Σ, q_{0}, δ, ℓ)

where:

• δ({λx_{1}.E_{1}, …, λx_{n}.E_{n}}, 0) = ⋂_{i=1}^{n} φ(x_{i})

for n > 0

• δ({λx_{1}.E_{1}, …, λx_{n}.E_{n}}, 1) = ⋃_{i=1}^{n} φ[[E_{i}]] for n > 0

•  ℓ(q) = \{ \begin{matrix}⊥ & if q = ∅ \\ Int & if q = \{Int\} \\ → & if q ⊆ Abs(E) ∧ q ≠ ∅ \\ ⊤ & otherwise \end{matrix}

□

Lemma 12 Suppose φ ∈ Cmap(E) and S_{1}, S_{2} ∈ Cl(E). If S_{1} ⊆ S_{2}, then t_{A(E,φ,S_{1})} ≤ t_{A(E,φ,S_{2})}.

Proof. Define the orderings ⊆_{0}, ⊆_{1} on Cl(E) such that ⊆_{0} equals ⊆ and ⊆_{1} equals ⊇. The desired conclusion follows immediately from the property that if α ∈ D(t_{A(E,φ,S_{1})}) ∩ D(t_{A(E,φ,S_{2})}), then δ̂(S_{1}, α) ⊆_{πα} δ̂(S_{2}, α). This property is proved by straightforward induction on the length of α. □

We can now prove that the type system and the safety analysis accept the same programs.

Theorem 13 For every λ-term E, the following seven conditions are equivalent:

1. C(E) is solvable.

2. T (E) is solvable.

3. \overline{T} (E) is solvable.

4. \overline{C}(E) is solvable.

5. \overline{C}(E) does not contain constraints of the forms \{Int\} ⊆ Abs(E) or \{λx.F \} ⊆ {Int}.

6. \overline{T} (E) does not contain constraints of the forms Int ≤ V → V′ or V → V′ ≤ Int, where V, V′ ∈ X_{E} ∪ Y_{E}.

7. The function

λV.\{ k | the constraint \{k\} ⊆ V is in \overline{C}(E) \}

is the least solution of C(E).

Proof. Given a λ-term E, notice that by the isomorphism of Theorem 9,

(5) ⇔ (6). To show the remaining equivalences, we proceed by proving the implications:

(1) ⇒ (2) ⇒ (3) ⇒ (4) ⇒ (5) ⇒ (7) ⇒ (1)

To prove (1) ⇒ (2), suppose C(E) has solution φ ∈ Cmap(E). Let f be the function λS.t_{A(E,φ,S)} and define ψ ∈ Tmap(E) by ψ = f ∘ φ. We will show that T (E) has solution ψ. We consider each of the constraints in turn. The cases of the constraints generated from subterms of the forms 0, succ E, x are immediate, by using Lemma 12. Consider then λx.F and the constraint x → [[F]] ≤ [[λx.F]]. By Lemma 12 we get

ψ(x) → ψ([[F]]) = f({λx.F }) ≤ ψ([[λx.F]]) .

Consider then GH and the constraint [[G]] ≤ [[H]] → [[GH]]. We know that φ([[G]]) ⊆ Abs(E) so there are two cases. Suppose first that φ([[G]]) = ∅. We then have ψ([[G]]) = ⊥ ≤ ψ([[H]]) → ψ([[GH]]). Consider then the case where φ([[G]]) = {λx_{1}.E_{1}, …, λx_{n}.E_{n}}, for n > 0. We then have that φ([[H]]) ⊆ φ([[x_{i}]]) and φ([[E_{i}]]) ⊆ φ([[GH]]) for i ∈ {1, …, n}. Thus, φ([[H]]) ⊆ ⋂_{i=1}^{n} φ([[x_{i}]]) and ⋃_{i=1}^{n} φ([[E_{i}]]) ⊆ φ([[GH]]). So, by Lemma 12,

ψ([[G]]) = f(φ([[G]]))
= f( ⋂_{i=1}^{n} φ([[x_{i}]])) → f( ⋃_{i=1}^{n} φ([[E_{i}]]))
≤ f(φ([[H]])) → f(φ([[GH]]))
= ψ([[H]]) → ψ([[GH]])

To prove (2) ⇒ (3), suppose T (E) has solution ψ ∈ Tmap(E). It is sufficient to show that \overline{T} (E) has solution ψ, and this can be proved by straightforward induction on the construction of \overline{T} (E).

To prove (3) ⇒ (4), suppose \overline{T} (E) has solution ψ ∈ Tmap(E). Define \overline{φ} ∈ Cmap(E) as follows:

\overline{φ}(V) = \{ \begin{matrix}∅ & if (ψ(V))(ϵ) = ⊥ \\ \{Int\} & if (ψ(V))(ϵ) = Int \\ Abs(E) & if (ψ(V))(ϵ) = → \\ Abs(E) ∪ \{Int\} & if (ψ(V))(ϵ) = ⊤ \end{matrix}

We will show that \overline{C}(E) has solution \overline{φ}. To see this, let W ⊆ Z be a constraint in \overline{C}(E). If it is of the forms \{Int\} ⊆ \{Int\} or \{λx.F \} ⊆ Abs(E), then it is solvable by all functions, including \overline{φ}. For the remaining cases, notice that by Theorem 9, L_{I}(W) ≤ L_{I}(Z) is in \overline{T} (E) and thus it has solution ψ. This means that W ⊆ Z cannot be of the forms {Int} ⊆ Abs(E) or {λx.F } ⊆ {Int}. Suppose then that W ⊆ Z is of one of the remaining forms, that is, {Int} ⊆ V, V ⊆ V′, V ⊆ {Int}, {λx.F } ⊆ V, V ⊆ Abs(E), where V, V′ ∈ X_{E} ∪ Y_{E}. We will treat just the first of them, the others are similar. For a constraint of the form {Int} ⊆ V, it follows that Int ≤ V is in \overline{T} (E). Since \overline{T} (E) has solution ψ we get that (ψ(V))(ϵ) ∈ \{Int, ⊤\}. Thus, \overline{φ}(V) is either \{Int\} or Abs(E) ∪ \{Int\}, and hence \{Int\} ⊆ V has solution \overline{φ}.

To prove (4) ⇒ (5), observe that constraints of the forms {Int} ⊆ Abs(E) or {λx.F } ⊆ {Int} are not solvable.

To prove (5) ⇒ (7), suppose \overline{C}(E) does not contain constraints of the forms {Int} ⊆ Abs(E) or {λx.F } ⊆ {Int}. Define

φ′ = λV.\{ k | the constraint \{k\} ⊆ V is in \overline{C}(E) \}

We proceed in four steps, as follows.

• First we show that φ′ is a solution of \overline{C}(E). We consider in turn each of the seven possible forms of constraints in \overline{C}(E). Constraints of the forms {Int} ⊆ {Int} and {λx.F } ⊆ Abs(E) have any solution, including φ′. We are thus left with constraints of the forms {Int} ⊆ V, V ⊆ V′, V ⊆ {Int}, {λx.F } ⊆ V, V ⊆ Abs(E), where V, V′ ∈ X_{E} ∪ Y_{E}. We will treat just the first three, since case four is similar to case one and since case five is similar to case three. For a constraint of the form {Int} ⊆ V, notice that Int ∈ φ′(V), so the constraint has solution φ′. For a constraint of the form V ⊆ V′, suppose k ∈ φ′(V). Then the constraint \{k\} ⊆ V is in \overline{C}(E), and hence the constraint \{k\} ⊆ V′ is also in \overline{C}(E). It follows that k ∈ φ′(V′). For a constraint of the form V ⊆ {Int}, suppose it does not have solution φ′. Hence, there exist k ∈ φ′(V) such that k ≠ Int. It follows that the constraint \{k\} ⊆ V is in \overline{C}(E), and hence the constraint \{k\} ⊆ \{Int\} is also in \overline{C}(E), a contradiction.

• Next we show that φ′ is the least solution of \overline{C}(E). To do this, let φ be any solution of \overline{C}(E) and suppose V ∈ X_{E} ∪ Y_{E}. It is sufficient to prove that φ′(V) ⊆ φ(V). Suppose k ∈ φ′(V). Then the constraint {k} ⊆ V is in \overline{C}(E). Since φ is a solution of \overline{C}(E), k ∈ φ(V).

• Next we show that φ′ is a solution of C(E). Consider first the nonconditional constraints of C(E). Since these constraints are also members of \overline{C}(E), they have solution φ′. Consider then \{λx.F \} ⊆ V ⇒ K in C(E) and suppose {λx.F } ⊆ V has solution φ′. Then by the definition of φ′, we have that \{λx.F \} ⊆ V is in \overline{C}(E), so also K is in \overline{C}(E), and hence K has solution φ′.

• Finally we show that φ′ is the least solution of C(E). To do this, let φ be any solution of C(E). Then φ is also a solution of \overline{C}(E), as can be proved by straightforward induction on the construction of \overline{C}(E). Since φ′ is the least solution of \overline{C}(E), φ′ is smaller than φ.

To prove (7) ⇒ (1), simply notice that since C(E) has a solution, it is solvable. □

Corollary 14 The type system accepts the same programs as the safety analysis.

4.3 Algorithms

As corollaries of Theorem 13 we get two cubic time algorithms. Given a λ-term E, first observe that both \overline{C}(E) and \overline{T} (E) can be computed in time O(n^{3}) where n is the size of E. We can then easily answer the following two questions:

• Question (safety): Is E accepted by safety analysis?

Algorithm: Check that \overline{C}(E) does not contain constraint of the forms {Int} ⊆ Abs(E) or {λx.F } ⊆ {Int}.

• Question (type inference): Is E typable? If so, what is an annotation of it? Algorithm: Use the safety checking algorithm. If E turns out to be typable, we get an annotation by first calculating the two functions

φ′ = λV.\{ k | the constraint \{k\} ⊆ V is in \overline{C}(E) \}

and

f = λS.t_{A(E,φ,S)}

and then forming the composition

ψ = f ∘ φ′ .

This function ψ is a solution of T (E).

The question of type inference has been open until now. In contrast, it is wellknown that flow analysis in the style discussed in this paper can be computed in time O(n^{3}).

Acknowledgements

The authors thank Mitchell Wand for encouragement and helpful discussions. The results of this paper were obtained while the first author was at Northeastern University, Boston; he is currently hosted by BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation.

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] Torben Amtoft. Minimal thunkification. In Proc. WSA’93, pages 218–229, 1993.

[3] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[4] Anders Bondorf. Automatic autoprojection of higher order recursive equations. Science of Computer Programming, 17(1–3):3–34, December 1991.

[5] Charles Consel. A tour of Schism: A partial evaluation system for higherorder applicative languages. In Proc. PEPM’93, Second ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 145–154, 1993.

[6] 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.

[7] 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.

[8] Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In Proc. Conference on Functional Programming Languages and Computer Architecture, pages 260–272, 1989.

[9] Jens Palsberg. Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems. To appear. Also in Proc. CAAP’94, Colloquium on Trees in Algebra and Programming, Springer-Verlag (LNCS 787), pages 276–290, Edinburgh, Scotland, April 1994.

[10] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation. To appear.

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

[12] Jens Palsberg and Michael I. Schwartzbach. Object-Oriented Type Systems. John Wiley & Sons, 1994.

[13] Olin Shivers. Data-flow analysis and type recovery in Scheme. In Peter Lee, editor, Topics in Advanced Language Implementation, pages 47–87. MIT Press, 1991.

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