BRICS RS-95-34 J. Palsberg: Type Inference with Selftype

BRICS

Basic Research in Computer Science

Type Inference with Selftype

Jens Palsberg

BRICS Report Series RS-95-34 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 Selftype

Jens Palsberg

BRICS^{∗} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract

The metavariable self is fundamental in object-oriented languages. Typing self in the presence of inheritance has been studied by Abadi and Cardelli, Bruce, and others. A key concept in these developments is the notion of selftype, which enables flexible type annotations that are impossible with recursive types and subtyping. Bruce et al. demonstrated that, for the language TOOPLE, type checking is decidable. Open until now is the problem of type inference with selftype.

In this paper we present a type inference algorithm for a type system with selftype, recursive types, and subtyping. The example language is the object calculus of Abadi and Cardelli, and the type inference algorithm runs in nondeterministic polynomial time.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation. E-mail: palsberg@daimi.aau.dk.

1 Introduction

1.1 Background

The metavariable self is fundamental in object-oriented languages. It may be used in a method to refer to the object executing the method. Since methods can be inherited, the meaning of self cannot be determined statically. For a denotational semantics of inheritance, see for example [7].

Typing self in the presence of inheritance has been studied by Abadi and Cardelli [3, 2, 1, 4], Bruce [5, 6], Palsberg and Schwartzbach [11, 12], and others. These developments all identify a need to give self a special treatment, as illustrated by the following standard example.

   object Point
     ...
     method move
       ...
       return self
     end
   end
   object ColorPoint extends Point
     ...
     method setcolor
       ...
     end
   end
   -- Main program:
   ColorPoint.move.setcolor

The object ColorPoint is defined by inheritance from Point: it extends Point with the method setcolor. The only significant aspect of the objects is that the move method returns self. Consider now the main program. It executes without errors, but is it typable? With most conventional type systems, the answer is: no! For example, suppose we use a C^{++} style of types such that we can annotate the method move with the return type Point. Then the expression ColorPoint.move has the type Point, and thus ColorPoint.move.setcolor is not type-correct, since Point does not have

a setcolor method.

One approach to giving self a special treatment is the use of selftype, “the type of self”, which enables flexible type annotations that are impossible with recursive types and subtyping. Selftype has been studied by Abadi and Cardelli [4], Bruce [5, 6], and others, and used in for example Eiffel [9] (Eiffel uses the syntax like Current for selftype). In the example with Point and ColorPoint, we can annotate the move method with selftype as the return type. This has the effect that the type of ColorPoint.move has the same

type as ColorPoint, and thus ColorPoint.move.setcolor is type-correct.

Although the object ColorPoint extends the object Point, this use of inheritance is not essential for creating examples that demonstrates the usefulness of selftype. In Section 1.3 we present an example where an object overrides a method in its parent object. That example is typable with selftype, but not with recursive types and subtyping.

There is no common agreement on the “right” type system with selftype. For example, when comparing the type rules of Abadi and Cardelli [4] with those of Bruce et al. [5, 6], we find both striking similarities, such as in the rules for message send, and significant differences, such as Bruce’s use of the ≤_{meth} relation on types. Both these type systems have been proved sound, and for Bruce’s language TOOPLE, type checking is decidable [6].

Open until now is the problem of type inference with selftype. Of course, the complexity of such a type inference problem depends on the exact details of the type system. In this paper, we address the following fundamental question:

Fundamental question. Can we design a useful type system with selftype such that type inference is decidable?

In other words: are selftype and type inference compatible?

1.2 Our Results

We present a type inference algorithm for a type system with selftype, recursive types, and subtyping. The example language is the object calculus of Abadi and Cardelli, and the type inference algorithm runs in nondeterministic polynomial time. Intuitively, our algorithm works by first guessing which methods should be annotated with selftype as the return type, and then solving the remaining type inference problem in polynomial time. It remains open if type inference is NP-complete or in polynomial time.

Type inference in the smaller type system without selftype is computable in O(n^{3}) time and it is P-complete [10]. In Section 1.3 we present a program which is typable with selftype but not without. Thus, selftype makes the type system more powerful and type inference remains decidable.

Our type system with selftype is essentially a subsystem of the one of Abadi and Cardelli in [4]. The key restriction is that a method cannot both have selftype as return type and also be overridable. It remains open if type inference in the full version of Abadi and Cardelli’s type system is decidable.

1.3 Example

We now present an example program which uses overriding of methods but not extension of objects.

   object Point            object Circle
     ...                     ...
     method move             method center
       ...                     return Point
       return self           end
     end                     ...
   end                     end
   object ColorPoint       object ColorCircle overrides Circle
     ...                     ...
     method move             method center
       ...                     return ColorPoint.move.setcolor
       return self           end
     end                   end
     method setcolor
       ...                 -- Main program:
       return self
     end                   ColorCircle.center.move
   end

The only significant aspect of the Point and ColorPoint objects is that their methods return self. The object Circle returns the Point object when asked for its center. The object ColorCircle is defined by inheritance from Circle: it overrides the center method. When asked for its center, the ColorCircle first slightly changes the coordinates and color of the ColorPoint, and then it returns the resulting object. This behavior may of course seem odd, but from a typing perspective, we would prefer that it does not make a difference if the center method returns ColorPoint or ColorPoint.move.setcolor. In both cases, the main program executes without errors.

The key aspects of the example can be directly represented in the object calculus of Abadi and Cardelli [3, 2, 1, 4], as follows.

P oint ≡ [move = ς(x)x]
ColorP oint ≡ [move = ς(y)y setcolor = ς(z)z]
Circle ≡ [center = ς(d)P oint]
ColorCircle ≡ Circle.center ⇐ ς(e)(ColorP oint.move.setcolor)
Main ≡ ColorCircle.center.move

We may then ask: can the program be typed in Abadi and Cardelli’s firstorder type system with recursive types and subtyping? The answer is, perhaps surprisingly: no! This answer can be obtained by running the type inference algorithm of Palsberg [10]. The key reason for the untypability is that the body of the ColorCircle’s center method forces ColorP oint to have a type which is not a subtype of the type of P oint, intuitively as follows.

P oint : μ(X)[move : X]
ColorP oint : μ(X)[move, setcolor : X]
μ(X)[move, setcolor : X] ≰ μ(X)[move : X]
Moreover : ColorCircle.center.move is not typable .

If we change the body of the ColorCircle’s center method to return simply ColorP oint, then the program is typable with recursive types and subtyping (actually with subtyping alone). This state of affairs is not satisfactory and calls for something to supplement or replace recursive types and subtyping.

This call is answered by our type system with selftype. With that type system the type of ColorP oint is a subtype of the type of P oint, and the program is typable:

P oint : [move : selftype]
ColorP oint : [move, setcolor : selftype]
[move, setcolor : selftype] ≤ [move : selftype]
Moreover : ColorCircle.center.move is typable .

Note that our type system can type this program even though it is strictly less powerful than the one suggested by Abadi and Cardelli in [4].

In the following section we briefly present Abadi and Cardelli’s calculus, and in Section 3 we present our new type system. In Section 4 we prove that the type inference problem is log-space reducible to a constraint problem, and in Section 5 we prove that the constraint problem is solvable in nondeterministic polynomial time. Finally, in Section 6 we give an example of how the algorithm works.

2 Abadi and Cardelli’s Calculus

Abadi and Cardelli has presented an untyped object calculus, called the ςcalculus. The ς-terms are generated by the following grammar:

a : := x variable [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] (l_{i} distinct) object a.l field selection / method invocation a.l ⇐ ς(x)b field update / method override

We use a, b, c to range over ς-terms. An object [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] has method names l_{i} and methods ς(x_{i})b_{i}. The order of the components does not matter. In a method ς(x)b, we have that x is the self variable and b is the body. Thus, in the body of a method we can refer to any enclosing object, like in the Beta language [8].

The reduction rules for ς-terms are as follows. If o ≡ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}], then, for j ∈ 1..n,

• o.l_{j} ⇝ b_{j}[o/x_{j}]

• o.l_{j} ⇐ ς(y)b ⇝ o[l_{j} ← ς(y)b]

Here, a[o/x] denotes the ς-term a with o substituted for free occurrences of x (after renaming bound variables if necessary); and o[l_{j} ← ς(y)b] denotes the ς-term o with the l_{j} field replaced by ς(y)b. An evaluation context is an expression with one hole. For an evaluation context a[.], if b ⇝ b′, then a[b] ⇝ a[b′].

A ς-term is said to be an error if it is irreducible and it contains either o.l_{j} or o.l_{j} ⇐ ς(y)b, where o ≡ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}], and o does not contain an l_{j} field.

For an example of a reduction, consider the object o ≡ [l = ς(x)x.l]. The expression o.l yields the infinite computation: o.l ⇝ x.l[o/x] ≡ o.l ⇝ …

3 The Type System

The following type system for the ς-calculus catches errors statically, that is, rejects all programs that may yield errors.

The concrete syntax of object types is presented by the following grammar:

B ::= selftype | [l_{i} : B_{i}^{i∈1..n}] | α | μα.B

The labels l_{i} are drawn from some possibly infinite set N of method names. We denote by C the powerset of N.

Define Σ = {Selftype} ∪ C. Each type denotes a regular tree over Σ. Intuitively, such a tree can be obtained from a type by infinite unfolding of the type.

Given a type, we represent the corresponding regular tree by a term over Σ, that is, a partial function

t : N ∗ → Σ

with domain D(t) satisfying the following properties:

• D(t) is nonempty and prefix-closed;

• if t(α) = Selftype, then {l | αl ∈ D(t)} = ∅; and

• if t(α) = {l_{i} ∈ N | i ∈ 1..n}, then {l | αl ∈ D(t)} = {l_{i} | i ∈ 1..n} .

Intuitively, D(t) is the set of paths from the root in the tree, and t maps each such path to the symbol at the end of the path. In the remainder of the paper, we always work with the term representation of types.

Let t be a term and α ∈ N ∗. Define the partial function t↓α : N ∗ → Σ by

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

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

A term t is said to be regular if it has only finitely many distinct subterms; i.e., if {t ↓ α | α ∈ N ∗} is a finite set. The terms denoted by object types are regular terms. The set of all regular terms over Σ is denoted T_{Σ}.

We now define operators selftype^{T_{Σ}} and [l_{i} : A_{i}^{i∈1..n}]^{T_{Σ}} on terms that correspond to the type constructs selftype and [l_{i} : A_{i}^{i∈1..n}]. For l_{1}, …, l_{n} ∈ N, A_{1}, …, A_{n} ∈ T_{Σ}, j ∈ 1..n, and α ∈ N ∗, define

D(selftype^{T_{Σ}}) = {ϵ}
selftype^{T_{Σ}}(ϵ) = Selftype
D([l_{i} : A_{i}^{i∈1..n}]^{T_{Σ}}) = {ϵ} ∪ ⋃_{i=1}^{n}{l_{i}α | α ∈ D(A_{i})}
[l_{i} : A_{i}^{i∈1..n}]^{T_{Σ}}(ϵ) = {l_{i} | i ∈ 1..n}
[l_{i} : A_{i}^{i∈1..n}]^{T_{Σ}}(l_{j}α) = A_{j}(α) .

The set T_{Σ} \ {selftype^{T_{Σ}}} is denoted P_{Σ}. At the risk of ambiguity, we omit the superscript T_{Σ} on the operators selftype^{T_{Σ}} and [l_{i} : A_{i}^{i∈1..n}]^{T_{Σ}}.

The following properties are immediate from the definitions:

(i) [l_{i} : A_{i}^{i∈1..n}]↓l_{i} = A_{i}

(ii) (A↓α)↓β = A↓αβ

The set of object types is ordered by the subtyping relation ≤ as follows. First,

selftype ≤ selftype

and second, if A ≠ selftype and B ≠ selftype, then

A ≤ B if and only if ∀l ∈ N : l ∈ D(B) ⇒ (l ∈ D(A) ∧ A↓l = B ↓l) .

Clearly, ≤ is a partial order. Intuitively, if A ≤ B, then A may contain more fields than B, and for common fields, A and B must have the same type. For example, [l : A, m : B] ≤ [l : A], but [l : [m : A]] ≰ [l : [ ]]. Notice that if A ≤ B, then D(B) ⊆ D(A).

If A, B are object types, define

B\{A\} = \{ \begin{matrix}A & if B = selftype \\ B & otherwise \end{matrix}

We now present the typing rules. If a is a ς-term, A is an object type, and E is a type environment, that is, a partial function assigning elements of P_{Σ} to variables, then the judgement E ⊢ a : A means that a has the type A in the environment E. This holds when the judgement is derivable using the following five rules:

E ⊢ x : A (provided E(x) = A)  (1)
\frac{E[x_{i} ← A] ⊢ b_{i} : B_{i}\{A\} ∀i ∈ 1..n}{E ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : A} (where A = [l_{i} : B_{i}^{i∈1..n}]) (2)
\frac{E ⊢ a : A}{E ⊢ a.l : B\{A\}} (where A ≤ [l : B])  (3)
\frac{E ⊢ a : A E[x ← A] ⊢ b : B}{E ⊢ a.l ⇐ ς(x)b : A} (where A ≤ [l : B] and B ≠ selftype) (4)
\frac{E ⊢ a : A A ≤ B}{E ⊢ a : B}  (5)

The first four rules express the typing of each of the four constructs in the object calculus and the last rule is the rule of subsumption. The type rules may be understood as a generalization of those introduced by Abadi and Cardelli in [3] and studied further by Palsberg in [10]. Specifically, if selftype is never used, then B{A} = B and the rules take the form used in [10]. The type rules may also be understood as a simplification of those introduced by Abadi and Cardelli in [4]. The key restriction is found in rule (4) where the condition B ≠ selftype ensures that a method cannot both have selftype as return type and also be overridable.

If E ⊢ a : A is derivable, we say that a is well-typed with type A.

Theorem 3.1 (Subject Reduction) If E ⊢ a : t and a ⇝ a′, then E ⊢ a′ : t.

Proof. By induction on the structure of the derivation of E ⊢ a : t. □

For an example of a type derivation, let us consider the example term from Section 1.3. Define

P ≡ [move : selftype]
Q ≡ [move, setcolor : selftype]
A ≡ [center : P]
E ≡ ∅[d ← A]
F ≡ ∅[e ← P] .

We can then derive ∅ ⊢ ColorCircle.center.move : P as follows.

\frac{\frac{\frac{\frac{\frac{E[x ← P] ⊢ x : P}{E ⊢ P oint : P}}{∅ ⊢ Circle : A}  \frac{\frac{\frac{\frac{F [y ← Q] ⊢ y : Q  F [z ← Q] ⊢ z : Q}{F ⊢ ColorP oint : Q}}{F ⊢ ColorP oint.move : Q}}{F ⊢ ColorP oint.move.setcolor : Q  Q ≤ P}}{F ⊢ ColorP oint.move.setcolor : P}}{∅ ⊢ ColorCircle : A}}{∅ ⊢ ColorCircle.center : P}}{∅ ⊢ ColorCircle.center.move : P}

Notice the use of subsumption with Q ≤ P which was also mentioned in Section 1.3.

4 From Rules to Constraints

In this section we prove that the type inference problem is log space reducible to solving a finite system of type constraints. The constraints isolate the essential combinatorial structure of the type inference problem.

Definition 4.1 Given two denumerable and disjoint sets U and V of variables, an S-system (selftype-system) over U and V is a finite set of constraints of the forms:

W ≤ W′
if U = selftype then W ≤ W′ else W′′ ≤ U
if U = selftype then W ≤ W′ else U ≤ W′′

where W, W′, W′′ are of the forms V, [l_{i} : U_{i}^{i∈1..n}], or [l_{i} : V_{i}^{i∈1..n}], and where U, U_{1}, …, U_{n} ∈ U and V, V_{1}, …, V_{n} ∈ V.

A solution for an S-system is a pair of maps (L, M), where L : U → T_{Σ} and M : V → P_{Σ}, such that all constraints are satisfied when elements of U are mapped to types by L, and elements of V are mapped to types by M.

□

For an example of an S-system, see Section 6. In comparison with the AC-systems of [10], the novel aspect of S-systems is the use of conditional constraints.

Given a ς-term c, assume that it has been α-converted so that all bound variables are distinct. We will now generate an S-system where the bound variables of c are a subset of the variables used in the constraint system. This will be convenient in the statement and proof of Theorem 4.2 below. Let X be the set of bound variables in c, and let Y be a set of variables disjoint from X consisting of one variable [[b]] for each occurrence of a subterm of b of c. Define V = X ∪ Y. Moreover, let U be a set of variables disjoint from V consisting of one variable ⟨a.l⟩ for each occurrence of a subterm a.l of c, and consisting of one variable ⟨b_{i}⟩ for each occurrence of a subterm [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] of c and for each i ∈ 1..n. (The notations [[b]], ⟨a.l⟩, and ⟨b_{i}⟩ are ambiguous because there may be more than one occurrence of the terms b, a.l, or b_{i} in c. However, it will always be clear from the context which occurrence is meant.)

We generate from c the following S-system over U and V:

• for every occurrence in c of a bound variable x, the constraint

x ≤ [[x]]  (6)

• for every occurrence in c of a subterm of the form [l_{i} = ς(x_{i})b_{i}^{i∈1..n}], the constraint

[l_{i} : ⟨b_{i}⟩ ^{i∈1..n}] ≤ [[[l_{i} = ς(x_{i})b_{i}^{i∈1..n}]]]  (7)

and for every j ∈ 1..n, the two constraints

x_{j} = [l_{i} : ⟨b_{i}⟩ ^{i∈1..n}]  (8)
if ⟨b_{j}⟩ = selftype then x_{j} = [[b_{j}]] else ⟨b_{j}⟩ = [[b_{j}]]  (9)

• for every occurrence in c of a subterm of the form a.l, the two con-

straints

[[a]] ≤ [l : ⟨a.l⟩]  (10)
if ⟨a.l⟩ = selftype then [[a]] ≤ [[a.l]] else ⟨a.l⟩ ≤ [[a.l]]  (11)

• for every occurrence in c of a subterm of the form a.l ⇐ ς(x)b, the

three constraints

[[a]] ≤ [[a.l ⇐ ς(x)b]]  (12)
[[a]] = x  (13)
[[a]] ≤ [l : [[b]]] .  (14)

Each equality A = B denotes the two inequalities A ≤ B and B ≤ A. Moreover, each constraint of the form

if U = selftype then V = V′ else U = V′′

denotes the two constraints

if U = selftype then V ≤ V′ else U ≤ V′′
if U = selftype then V′ ≤ V else V′′ ≤ U .

Denote by C(c) the S-system of constraints generated from c in this fashion. For a ς-term of size n, the S-system C(c) is of size O(n), and it is generated using O(log n) space. We show below that the solutions of C(c) correspond to the possible type annotations of c in a sense made precise by Theorem 4.2. For an example of an S-system generated from a ς-term, see Section 6.

Let E be a type environment assigning a type in P_{Σ} to each variable occurring freely in c. If M : V → P_{Σ}, we say the M extends E if E and M agree on the domain of E.

Theorem 4.2 The judgement E ⊢ c : A is derivable if and only if there exists a solution (L, M) of C(c) such that M extends E and M([[c]]) = A. In particular, if c is closed, then c is well-typed with type A if and only if there exists a solution (L, M) of C(c) such that M([[c]]) = A.

Proof. The proof uses the same technique as the proof of Lemma 4.2 in [10].

We first prove that if C(c) has a solution (L, M), then M ⊢ c : M([[c]]) is derivable. We proceed by induction on the structure of c. For the base case, M ⊢ x : M([[x]]) is derivable using rules (1) and (5), since M(x) ≤ M([[x]]). For the induction step, consider first [l_{i} = ς(x_{i})b_{i}^{i∈1..n}]. Let A = [l_{i} : L(⟨b_{i}⟩) ^{i∈1..n}]. To derive M ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : M([[[l_{i} = ς(x_{i})b_{i}^{i∈1..n}]]]), by rule (5) and the fact that A ≤ M([[[l_{i} = ς(x_{i})b_{i}^{i∈1..n}]]]), it suffices to derive M ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : A. The side condition of (2) is clearly satisfied, so it suffices to derive, for each i ∈ 1..n, M[x_{i} ← A] ⊢ b_{i} : (L(⟨b_{i}⟩)){A}. Since M(x_{i}) = A for each i ∈ 1..n, it suffices to derive M ⊢ b_{i} : (L(⟨b_{i}⟩)){A}. For each i ∈ 1..n, there are two cases. If L(⟨b_{i}⟩) = selftype, then M(x_{i}) = M([[b_{i}]]) and (L(⟨b_{i}⟩)){A} = A, so since M(x_{i}) = A, we get (L(⟨b_{i}⟩)){A} = M([[b_{i}]]), and hence the desired derivation is provided by the induction hypothesis. If L(⟨b_{i}⟩) ≠ selftype, then L(⟨b_{i}⟩) = M([[b_{i}]]) and (L(⟨b_{i}⟩)){A} = L(⟨b_{i}⟩), so we get (L(⟨b_{i}⟩)){A} = M([[b_{i}]]), and again the desired derivation is provided by the induction hypothesis.

Now consider a.l. Let A = M([[a]]). From the induction hypothesis, we obtain a derivation of M ⊢ a : A. By rule (3) and the fact that A ≤ [l : L(⟨a.l⟩)], we obtain a derivation of M ⊢ a.l : (L(⟨a.l⟩)){A}. There are two cases. If L(⟨a.l⟩) = selftype, then A ≤ M([[a.l]]) and (L(⟨a.l⟩)){A} = A, so (L(⟨a.l⟩)){A} ≤ M([[a.l]]), and hence M ⊢ a.l : M([[a.l]]) can be derived using rule (5). If L(⟨a.l⟩ ≠ selftype, then L(⟨a.l⟩) ≤ M([[a.l]]) and (L(⟨a.l⟩)){A} = L(⟨a.l⟩), so (L(⟨a.l⟩)){A} ≤ M([[a.l]]), and again M ⊢ a.l : M([[a.l]]) can be derived using rule (5).

Finally, consider a.l ⇐ ς(x)b. Let A = M([[a]]). To derive M ⊢ a.l ⇐ ς(x)b : M([[a.l ⇐ ς(x)b]]), by rule (5) and the fact that A ≤ M([[a.l ⇐ ς(x)b]]), it suffices to derive M ⊢ a.l ⇐ ς(x)b : A. From the facts that A ≤ [l : M([[b]])] and M([[b]]) ∈ P_{Σ}, we get that the side conditions of rule (4) are satisfied and that it suffices to derive M ⊢ a : A and M[x ← A] ⊢ b : M([[b]]). Since A = M(x), the desired derivations are provided by the induction hypothesis.

We then prove that if E ⊢ c : A is derivable, then there exists a solution (L, M) of C(c) such that M extends E and M([[c]]) = A.

Suppose E ⊢ c : A is derivable, and consider a derivation of minimal length. Since the derivation is minimal, there is exactly one application of the rule (1) involving a particular occurrence of a variable x, exactly one application of the rule (2) involving a particular occurrence of a subterm [l_{i} = ς(x_{i})b_{i}^{i∈1..n}], exactly one application of the rule (3) involving a particular occurrence of a subterm a.l, and exactly one application of the rule (4) involving a particular occurrence of a subterm a.l ⇐ ς(x)b. In the case of a bound variable x, there is a unique type B_{x} such that F (x) = B_{x} for any F such that a judgement F ⊢ a : B′ appears in the derivation for some occurrence of a subterm a of ς(x)b; this can be proved by induction on the structure of the derivation of F ⊢ a : B′. Finally, there can be at most one application of the rule (5) involving a particular occurrence of any subterm; if there were more than one, they could be combined using the transitivity of ≤ to give a shorter derivation.

Now construct (L, M) as follows. For every free variable x of c, define M(x) = E(x). For every bound variable x of c, define M(x) = B_{x}. For every occurrence of a subterm a of c, find the last judgement in the derivation of the form F ⊢ a : B involving that occurrence of a, and define M([[a]]) = B. Intuitively, the last judgement of the form F ⊢ a : B means the judgement after the use of subsumption. For each occurrence of a subterm a.l of c, find the unique application of the rule (3) deriving the judgement F ⊢ a.l : B{A′} from the premise F ⊢ a : A′ where A′ ≤ [l : B], and define L(⟨a.l⟩) = B. For each occurrence of a subterm [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] of c, find the unique application of the rule (2) deriving the judgement F ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : A′ from the premises F [x_{i} ← A′] ⊢ b_{i} : B_{i}{A′} for i ∈ 1..n where A′ = [l_{i} : B_{i}^{i∈1..n}], and define L(⟨b_{i}⟩) = B_{i} for i ∈ 1..n.

Certainly M extends E and M([[c]]) = A. We now show that (L, M) is a solution of C(c).

For an occurrence of a bound variable x, there are two cases. Suppose first that the variable is bound in a method that occurs in an object declaration. Find the unique application of the rule (2) deriving the judgement F ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : A from a family of premises where one of them is F [x ← A] ⊢ b : B_{i}. Then L(x) = A. The rule (1) must have been applied to obtain a judgement of the form G ⊢ x : L(x) and only rule (5) applied to that occurrence of x thereafter, thus L(x) ≤ L([[x]]). Suppose then that the variable is bound in a method that occurs in a method override. Find the unique application of the rule (4) deriving the judgement F ⊢ a.l ⇐ ς(x)b : A from two premises where one of them is F [x ← A] ⊢ b : B. As before, we get that L(x) ≤ L([[x]]).

For an occurrence of a subterm of the form [l_{i} = ς(x_{i})b_{i}^{i∈1..n}], find the unique application of the rule (2) deriving the judgement F ⊢ [l_{i} = ς(x_{i})b_{i}^{i∈1..n}] : A′ from the premises F [x_{i} ← A′] ⊢ b_{i} : B_{i}{A′} where A′ = [l_{i} : B_{i}^{i∈1..n}]. Then B_{j} = L(⟨b_{j}⟩) and M([[b_{j}]]) = B_{j}{A′} for each j ∈ 1..n. Hence, [l_{i} : L(⟨b_{i}⟩) ^{i∈1..n}] ≤ M([[[l_{i} = ς(x_{i})b_{i}^{i∈1..n}]]]) and M(x_{j}) = [l_{i} : L(⟨b_{i}⟩) ^{i∈1..n}] for each j ∈ 1..n. Moreover, for each j ∈ 1..n, if L(⟨b_{j}⟩) = selftype, then B_{j}{A′} = A′, so M(x_{j}) = A′ = B_{j}{A′} = M([[b_{j}]]), and if L(⟨b_{j}⟩) ≠ selftype, then B_{j}{A′} = B_{j}, so L(⟨b_{j}⟩) = B_{j} = B_{j}{A′} = M([[b_{j}]]).

For an occurrence of a subterm of the form a.l, find the unique application of the rule (3) deriving the judgement F ⊢ a.l : B{A′} from the premise F ⊢ a : A where A ≤ [l : B]. Then B = L(⟨a.l⟩) and A = M([[a]]). Hence, M([[a]]) = A ≤ [l : B] = [l : L(⟨a.l⟩)]. Moreover, if L(⟨a.l⟩) = selftype, then B{A′} = A′, so M([[a]]) = A′ = B{A′} ≤ M([[a.l]]), and if L(⟨a.l⟩) ≠ selftype, then B{A′} = B, so L(⟨a.l⟩) = B = B{A′} ≤ M([[a.l]]).

Finally, for an occurrence of a subterm of the form a.l ⇐ ς(x)b, find the unique application of the rule (4) deriving the judgement F ⊢ a.l ⇐ ς(x)b : A′ from the premise F ⊢ a : A′ and F [x ← A′] ⊢ b : B where A′ ≤ [l : B] and B ≠ selftype. Then M([[a]]) = A′ ≤ M([[a.l ⇐ ς(x)b]]), and A′ = M(x). Moreover, M([[b]]) = B, so M([[a]]) = A′ ≤ [l : B] = [l : M([[b]])]. □

5 Solving Constraints

To solve an arbitrary S-system, we will use a use a non-deterministic algorithm to transform it into a so-called ACS-system which then can be solved in polynomial time.

The notion of an ACS-system is a slight extension of that of an ACsystem that was studied by Palsberg [10]. The extension is the constant selftype. Intuitively, selftype enjoys a special status in an S-system because of the conditional constraints. In contrast, selftype is an “ordinary” constant in an ACS-system.

Definition 5.1 Given a denumerable set of variables W, an ACS-system over W is a finite set of constraints of the forms:

V = selftype W ≤ W′

where W, W′ are of the forms V or [l_{i} : V_{i}^{i∈1..n}], and where V, V_{1}, …, V_{n} ∈ W.

A solution for an ACS-system is a map ψ : W → T_{Σ}, such that all constraints are satisfied when elements of W are mapped to types by ψ. □

If we disallow the use of selftype in the constraints and in the solutions, then we get an AC-system. Type inference with recursive types and subtyping is log-space equivalent to solving AC-systems. Since the constant selftype has no special status in an ACS-system, it could be replaced by any other constant, e.g., Integer, Real, without changing the problem of solving constraints. If we extend the object calculus with constructs for computing with for example integers, then we can in log-space reduce the type inference problem to solving ACS-systems with Integer in the place of selftype.

In the journal version of [10], it is indicated how to extend the constraint solving algorithm for AC-systems to handle functions and records. It is equally easy to extend the algorithm to handle a constant such as selftype. Thus, solvability of an ACS-system is decidable in O(n^{3}) time.

We now define a family of mappings F_{S} from S-systems to ACS-systems. Let C be an S-system over U and V, and let S ⊆ U. Intuitively, S is a guess on the set of variables that some solution of C would map to selftype. Define F_{S}(C) to be the ACS-system over U ∪ V where

• For each U ∈ S, the constraint U = selftype is in F_{S}(C).

• For each V ∈ (U \ S) ∪ V, the constraint V ≤ [ ] is in F_{S}(C).

• If a constraint of the form W ≤ W′ is in C, then it is also in F_{S}(C).

• If a constraint of the form if U = selftype then W ≤ W′ else W′′ ≤ W′′′ is in C, then

(i) If U ∈ S, then W ≤ W′ is in F_{S}(C); and

(ii) If U ∉ S, then W′′ ≤ W′′′ is in F_{S}(C).

We can now prove our main result which relates solvability of S-systems to solvability of ACS-systems.

Theorem 5.2 (Main Result) Suppose C is an S-system over U and V. Then C is solvable if and only if there exist S ⊆ U such that F_{S}(C) is solvable.

Proof. Suppose first that C has solution (L, M). Define

S = {U ∈ U | L(U) = selftype}
ψ : U ∪ V → T_{Σ}
ψ(W) = \{ \begin{matrix}L(W) & if W ∈ U \\ M(W) & if W ∈ V \end{matrix}

Clearly, ψ is a solution of F_{S}(C).

Suppose then that we have S ⊆ U such that F_{S}(C) has solution ψ. Define

L : U → T_{Σ}
M : V → P_{Σ}
L(U) = ψ(U) if U ∈ U
M(V) = ψ(V) if V ∈ V

Clearly, (L, M) is a solution of C. □

Corollary 5.3 We can decide in nondeterministic polynomial time if an Ssystem has a solution.

Proof. Suppose C is an S-system over U and V. Guess S ⊆ U. Transform C into F_{S}(C), using log-space. Decide whether F_{S}(C) is solvable, using O(n^{3}) time. The conclusion then follows from Theorem 5.2. □

By combining Theorem 4.2 and Corollary 5.3, we obtain the following result.

Corollary 5.4 The type inference problem for the type system with selftype, recursive types, and subtyping can be decided in nondeterministic polynomial time.

Suppose we drop either or both of recursive types and subtyping. In each case, the type inference problem can be decided in nondeterministic polynomial time. by small modifications of the algorithm above, as follows. For the case of dropping recursive types, there is a slightly different algorithm for solving the generated ACS-system in O(n^{3}) time, see [10]. For the case of dropping subtyping, the only change is that when generating the S-system, the inequalities in (6), (7), (11), and (12) should be changed to equalities. For the case of dropping both recursive types as subtyping, one should combine the changed mentioned in the two previous cases.

We have thus completed the following table.

Selftype Recursive types Subtyping  Type inference

O(n^{3}) time, P-complete [10]

√  O(n^{3}) time, P-complete [10]
√  O(n^{3}) time, P-complete [10]
√ √ O(n^{3}) time, P-complete [10]
√  NP [this paper]
√  √  NP [this paper]
√  √  NP [this paper]
√  √  √  NP [this paper]

6 Example of Type Inference

We now give an example of how the type inference algorithm works. The example program is the one from Section 1.3. The expression

ColorCircle.center.move

yields the following S-system.

Occurrence  Constraints
x  x ≤ [[x]]
P oint  [move : ⟨x⟩] ≤ [[P oint]]

x = [move : ⟨x⟩] if ⟨x⟩ = selftype then x = [[x]] else ⟨x⟩ = [[x]]

y  y ≤ [[y]]
z  z ≤ [[z]]
ColorP oint  [move : ⟨y⟩ setcolor : ⟨z⟩] ≤ [[ColorP oint]]

y = [move : ⟨y⟩ setcolor : ⟨z⟩] z = [move : ⟨y⟩ setcolor : ⟨z⟩] if ⟨y⟩ = selftype then y = [[y]] else ⟨y⟩ = [[y]] if ⟨z⟩ = selftype then z = [[z]] else ⟨z⟩ = [[z]]

Circle  [center : ⟨P oint⟩] ≤ [[Circle]]

d = [center : ⟨P oint⟩] if ⟨P oint⟩ = selftype then d = [[P oint]] else ⟨P oint⟩ = [[P oint]]

ColorCircle  [[Circle]] ≤ [[ColorCircle]]

[[Circle]] = e [[Circle]] ≤ [center : [[ColorP oint.move.setcolor]]]

ColorP oint.move  [[ColorP oint]] ≤ [move : ⟨ColorP oint.move⟩]

if ⟨ColorP oint.move⟩ = selftype

then [[ColorP oint]] ≤ [[ColorP oint.move]]
else ⟨ColorP oint.move⟩ ≤ [[ColorP oint.move]]
ColorP oint.move.setcolor  [[ColorP oint.move]] ≤ [setcolor : ⟨ColorP oint.move.setcolor⟩]

if ⟨ColorP oint.move.setcolor⟩ = selftype

then [[ColorP oint.move]] ≤ [[ColorP oint.move.setcolor]]
else ⟨ColorP oint.move.setcolor⟩ ≤ [[ColorP oint.move.setcolor]]
ColorCircle.center  [[ColorCircle]] ≤ [center : ⟨ColorCircle.center⟩]

if ⟨ColorCircle.center⟩ = selftype

then [[ColorCircle]] ≤ [[ColorCircle.center]]
else ⟨ColorCircle.center⟩ ≤ [[ColorCircle.center]]
ColorCircle.center.move  [[ColorCircle.center]] ≤ [move : ⟨ColorCircle.center.move⟩]

if ⟨ColorCircle.center.move⟩ = selftype

then [[ColorCircle.center]] ≤ [[ColorCircle.center.move]]
else ⟨ColorCircle.center.move⟩ ≤ [[ColorCircle.center.move]]

We denote this S-system by C. Choose

S = { ⟨x⟩, ⟨y⟩, ⟨z⟩,
⟨ColorP oint.move⟩, ⟨ColorP oint.move.setcolor⟩,
⟨ColorCircle.center.move⟩ } .

Notice that

U \ S = { ⟨P oint⟩, ⟨ColorCircle.center⟩ } .

The ACS-system F_{S}(C) looks as follows.

⟨x⟩ = selftype  x ≤ [[x]]
⟨y⟩ = selftype  [move : ⟨x⟩] ≤ [[P oint]]
⟨z⟩ = selftype  x = [move : ⟨x⟩]
⟨ColorP oint.move⟩ = selftype  x = [[x]]
⟨ColorP oint.move.setcolor⟩ = selftype y ≤ [[y]]
⟨ColorCircle.center.move⟩ = selftype  z ≤ [[z]]
⟨P oint⟩ ≤ [ ]  [move : ⟨y⟩ setcolor : ⟨z⟩] ≤ [[ColorP oint]]
⟨ColorCircle.center⟩ ≤ [ ]  y = [move : ⟨y⟩ setcolor : ⟨z⟩]
x ≤ [ ]  z = [move : ⟨y⟩ setcolor : ⟨z⟩]
y ≤ [ ]  y = [[y]]
z ≤ [ ]  z = [[z]]
d ≤ [ ]  [center : ⟨P oint⟩] ≤ [[Circle]]
e ≤ [ ]  d = [center : ⟨P oint⟩]
[[x]] ≤ [ ]  ⟨P oint⟩ = [[P oint]]
[[y]] ≤ [ ]  [[Circle]] ≤ [[ColorCircle]]
[[z]] ≤ [ ]  [[Circle]] = e
[[P oint]] ≤ [ ]  [[Circle]] ≤ [center : [[ColorP oint.move.setcolor]]]
[[ColorP oint.move.setcolor]] ≤ [ ]  [[ColorP oint]] ≤ [move : ⟨ColorP oint.move⟩]
[[ColorCircle.center]] ≤ [ ]  [[ColorP oint]] ≤ [[ColorP oint.move]]
[[ColorCircle.center.move]] ≤ [ ]  [[ColorP oint.move]] ≤ [setcolor : ⟨ColorP oint.move.setcolor⟩]
[[ColorP oint]] ≤ [ ]  [[ColorP oint.move]] ≤ [[ColorP oint.move.setcolor]]
[[ColorP oint.move]] ≤ [ ]  [[ColorCircle]] ≤ [center : ⟨ColorCircle.center⟩]
[[Circle]] ≤ [ ]  ⟨ColorCircle.center⟩ ≤ [[ColorCircle.center]]
[[ColorCircle]] ≤ [ ]  [[ColorCircle.center]] ≤ [move : ⟨ColorCircle.center.move⟩]
[[ColorCircle.center]] ≤ [[ColorCircle.center.move]]

The constraint system F_{S}(C) has the solution ψ where:

ψ(W) = \{ \begin{matrix}selftype & if W ∈ S \\ [move : selftype] & if W ∈ \{ & x, [[x]], [[P oint]], ⟨P oint⟩, \\ & & [[ColorP oint.move.setcolor]], \\ & & [[ColorCircle.center]], \\ & & ⟨ColorCircle.center⟩, \\ & & [[ColorCircle.center.move]] \} \\ [move : selftype setcolor : selftype] & if W ∈ \{ & y, [[y]], z, [[z]], [[ColorP oint]], \\ & & [[ColorP oint.move]] \} \\ [center : [move : selftype]] & if W ∈ \{ & d, e, [[Circle]], [[ColorCircle]] \} \end{matrix}

In conclusion, if we annotate the two move methods and the setcolor method with selftype as the return type, then the program is typable.

References

[1] Martín Abadi and Luca Cardelli. A semantics of object types. In Proc. LICS’94, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 332–341, 1994.

[2] Martín Abadi and Luca Cardelli. A theory of primitive objects: Secondorder systems. In Proc. ESOP’94, European Symposium on Programming, pages 1–25. Springer-Verlag (LNCS 788), 1994.

[3] Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. In Proc. TACS’94, Theoretical Aspects of Computing Sofware, pages 296–320. Springer-Verlag (LNCS 789), 1994.

[4] Martín Abadi and Luca Cardelli. An imperative object calculus. In Proc. TAPSOFT’95, Theory and Practice of Software Development, pages 471–485. Springer-Verlag (LNCS 915), Aarhus, Denmark, May 1995.

[5] Kim B. Bruce. Safe type cheching in a statically typed objectoriented programming language. In Proc. POPL’93, Twentieth Annual SIGPLAN–SIGACT Symposium on Principles of Programming Languages, pages 285–298, 1993.

[6] Kim B. Bruce, Jon Crabtree, Thomas P. Murtagh, Robert van Gent, Allyn Dimock, and Robert Muller. Safe and decidable type checking in an object-oriented language. In Proc. OOPSLA’93, ACM SIGPLAN Eighth Annual Conference on Object-Oriented Programming Systems, Languages and Applications, pages 29–46, 1993.

[7] William Cook and Jens Palsberg. A denotational semantics of inheritance and its correctness. Information and Computation, 114(2):329– 350, 1994. Also in Proc. OOPSLA’89, ACM SIGPLAN Fourth Annual Conference on Object-Oriented Programming Systems, Languages and Applications, pages 433–443, New Orleans, Louisiana, October 1989.

[8] Bent B. Kristensen, Ole Lehrmann Madsen, Birger Møller-Pedersen, and Kristen Nygaard. The BETA programming language. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 7–48. MIT Press, 1987.

[9] Bertrand Meyer. Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs, NJ, 1988.

[10] Jens Palsberg. Efficient inference of object types. Information and Computation. To appear. Also in Proc. LICS’94, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 186–195, Paris, France, July 1994.

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

[12] Jens Palsberg and Michael I. Schwartzbach. Static typing for objectoriented programming. Science of Computer Programming, 23(1):19–53, 1994.

Recent Publications in the BRICS Report Series

RS-95-34 Jens Palsberg. Type Inference with Selftype. June 1995. 22 pp.

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.