A Framework for Ad-Hoc Type Inference (Extended Abstract)

Hosein Askari, Ole I. Hougaard^{∗}, Michael I. Schwartzbach

         {hosask,hougaard,mis}@daimi.aau.dk

BRICS^{†}, Department of Computer Science University of Aarhus 8000 Aarhus C, Denmark

Abstract

Languages based on variations of the lambda calculus are designed to permit the slick, unification-based technique for type inference, which is by now a well-established discipline.

Other widely used languages have been created less by design and more by coincidence and compromise. It seems therefore that the question of type inference for such languages could be infeasible or should at least permit only ad-hoc solutions.

In this paper we argue the existence of a uniform framework for developing type inference algorithms, even for seemingly ad-hoc languages. This framework provides useful generalizations of well-known concepts related to type inference. It is, however, by no means a universal algorithm. In fact, the essential algorithmic problem must generally be solved from scratch.

We demonstrate the viability of our approach by developing a type inference algorithm for a full version of the Turbo Pascal language.

1 Introduction

The concept of type inference has been firmly established as a strong quality in a programming language. It has also traditionally been associated with functional programming languages, such as ML, which are based on variations of the lambda calculus and hence allow the slick, unification-based technique for polymorphic type inference.

However, type inference may certainly be just as relevant for ad-hoc languages, which have been created less by design and more by coincidence and compromise. Clearly, if the type constraints are rather obscure, then automatic support will be correspondingly more useful.

∗Direct communications to this author †Basic Research in Computer Science, Centre of the Danish Research Foundation

It can naturally be argued that these ad-hoc languages should be eliminated and replaced by simpler, theoretically well-founded alternatives. For the purposes of this paper, we will merely observe that this process is sufficiently slow to justify an interest in building tools for these existing languages. Besides, the algorithmic challenge should certainly be met.

Note that if a language has a notion of type checking, then the problem of type inference is perfectly well-defined: Given a program (partially) without type annotations, does there exist a full annotation that allows the program to be type checked? This is simply an algorithmic problem, which one may attempt to solve.

It could be expected that the type inference problem for ad-hoc languages will turn out to be infeasible or at best permit only ad-hoc solutions. Certainly, it does not seem possible to generalize the unification-based approach.

In this paper we argue the existence of a uniform framework for developing type inference algorithms that to a large extent allows the ad-hoc nature of a programming language to be factored out. This framework should be viewed as a set of formalized rules-of-thumb that may guide the development of the algorithm; by no means do we present a universal algorithm.

This paper has two main parts, where we first provide useful generalizations of well-known concepts related to type inference and then show how to adapt them to ad-hoc situations.

In Section 2 we review the well-known unification-based technique for type inference in ML-style languages. For each fundamental concept do we provide suitable generalizations that enable the inclusion of ad-hoc features. The type domain is generalized from simple regular terms to term automata that capture the essence of name equivalence. The type constraints are generalized from equalities to more arbitrary relations respecting equivalence preserving homomorphisms. Based on these generalizations we propose a technique for representing solutions to type constraints, which may suggest the structure of a type inference algorithm. The essential algorithmic problem must however be solved from scratch. Finally, we show how polymorphism may be introduced through code expansion even in the likely absence of principal type schemes.

In Section 3 we demonstrate the viability of our framework by developing a polymorphic type inference algorithm for a full version of the Turbo Pascal language. It is safe to say that this language contains no special structure that will give us an unfair advantage when applying our framework. As predicted, we must solve an algorithmic problem specific to this application. However, we do this in a more general context that should cover several variations of the problem. The Turbo Pascal type inference algorithm has been implemented as a working preprocessor and suggests some interesting possibilities.

2 Generalized Concepts

We now recapitulate the well-known technique for performing type inference in ML-style languages. While presenting the familiar concepts, we will also introduce the generalizations necessary to handle more ad-hoc languages.

2.1 Type Domain

The types of core-ML are the expressions generated by the grammar below:

\begin{aligned}T_{ML} ::= & & α | β | γ | … \\ & | & T_{ML} → T_{ML} \end{aligned}

where α, β, γ, … are type variables. Such type expressions can be described as finite terms as defined by Courcelle [2]. Here we adopt the notation of Kozen [5].

Definition 2.1 Let ω denote the set of natural numbers and let Σ be a ranked alphabet. A (Σ-)term is a partial function t : ω^{∗} → Σ whose domain is nonempty, prefix-closed, and respects arities in the sense that if t(α) is defined then

{i | t(αi) is defined} = {1, 2, …, arity(t(α))}

A term is regular if it has only finitely many subterms up to isomorphism.

In the case of ML we have Σ_{ML} = {→, α, β, …}, arity(→) = 2, and arity(α) = arity(β) = ⋯ = 0.

From [2] we adopt the notion of a subtree of t rooted at a node α, t/α, defined as t/α(β) = t(αβ). We will not distinguish between the singleton tree ϵ ↦ l and the label l.

In our framework we represent types as finite term automata taken from Kozen [5].

Definition 2.2 A pure (Σ-)term automaton is a tuple

M = (Q, Σ, l, δ)

where:

• Q is a finite set of states.

• Σ is a ranked alphabet.

• l : Q → Σ is a labeling.

• δ : Q × ω → Q is a partial function such that for all q ∈ Q,

{i | δ(q, i) is defined} = {1, 2, …, arity(l(q))}

Note that the automata used here differs from the ones in [5] in that they are finite. We will make another addition to the definition.

Definition 2.3 A (Σ-)term automaton with initial state is a tuple

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

where (Q, Σ, l, δ) is a pure (Σ-)term automaton, and q_{0} ∈ Q is an initial state. We write A(Σ) for the set of Σ-term automata with initial state.

In both kinds of term automata the function δ extends into a partial function δ̂: Q × ω^{∗} → Q according to the inductive definition:

δ̂(q, ϵ) = q
δ̂(q, αi) = δ(δ̂(q, α), i)

with the understanding that the last expression is undefined if δ̂(q, α) is undefined.

Let M = (Q, q_{0}, Σ, δ, l) or M = (Q, Σ, δ, l) and q ∈ Q. The subautomaton of M rooted at q is

M[q] = (Q, q, Σ, δ, l)

For M = (Q, q_{0}, Σ, δ, l) we also define M/α defined as

M/α = M[δ̂(q_{0}, α)]

For any automaton M = (Q, q_{0}, Σ, δ, l) the partial function defined by:

t^{M}(α) = l(δ̂(q_{0}, α))

is a regular Σ-term. For q ∈ Q we write t_{q}^{M} = t^{M[q]}. Similarly for pure term automata. It is easy to see that t^{M/α} = t^{M}/α.

Conversely, every regular term corresponds to t^{M} for some term automaton, M, with initial state [7, lemma 8]. So we have the following.

Proposition 2.1 The set of regular Σ-terms is isomorphic to the set of Σ-term automata with initial state modulo term equality.

We can thus consider the ML types to be Σ_{ML}-term automata with initial state.

Let us now consider the set {t^{M} | M ∈ A(Σ)}. Clearly, it forms a free Σ-algebra. But there are type domains with restrictions on the types to which an operator can be applied. In order to deal with such situations we apply restrictions to the terms of the automata in the type domain.

Definition 2.4 Let Σ be a ranked alphabet, and let L be a regular tree language. The class of legal automata with respect to Σ and L is

A(Σ, L) = {M ∈ A(Σ) | t^{M} ∈ L}

In ML the type domain is then A(Σ_{ML}, {t^{M} | M ∈ A(Σ_{ML})}) = A(Σ_{ML})

2.2 Type Equivalence

The notion of type equivalence a central concept in a language definition, reflecting the essential properties of types. Most languages incorporate either structural equivalence or name equivalence. In the following we will generalize structural equivalence in a way that provides a simple framework for dealing with both equivalences.

It follows from the previous subsection that structural equivalence between term automata is simply equality between their terms. It is clear that for any two terms, t and t′, we have that

t = t′ ⇔ t(ϵ) = t′(ϵ) ∧ ∀i ∈ {1, 2, …, arity(t(ϵ))} : t/i = t′/i

In the case of finite trees, this is actually an unambiguous definition of the relation =. In the more general case of regular trees, there is a number of relations having the same property as =. In fact, = is the most general of the equivalence relations with the above property. We would expect that the equivalence relation t^{M} = t^{M′} would have a similar property, and it does as stated in the lemma below.

Lemma 2.2 The equivalence relation t^{M} = t^{M′} is the most general of all equivalence relations, ≈, with the property that for all M and M′:

M ≈ M′ ⇔ t^{M}(ϵ) = t^{M′}(ϵ) ∧ ∀i ∈ {1, …, arity(t^{M}(ϵ))} : M/i ≈ M′/i

That is for any ≈ with the above property M ≈ M′ ⇒ t^{M} = t^{M′}.

The property in the above lemma implies that every label in Σ is equivalence preserving. Now, let us consider a situation where only some of the labels have this property. Choose a subset S ⊆ Σ. We want the above to apply only if the label is in S. If we write

M ≈ M′ ⇔ t^{M}(ϵ) = t^{M′}(ϵ) ∈ S ∧ ∀i ∈ {1, …, arity(t^{M}(ϵ))} : M/i ≈ M′/i

then we wind up with a relation that is not necessarily reflexive. Hence we need to take the reflexive closure. The definition is as follows.

Definition 2.5 Let S ⊆ Σ. The equivalence relation ≈_{S} is the most general among the equivalence relations, ≈, with the property that for all M and M′:

M ≈ M′ ⇕ (t^{M}(ϵ) = t^{M′}(ϵ) ∈ S ∧ ∀i ∈ {1, …, arity(t^{M}(ϵ))} : M/i ≈ M′/i) ∨ (M = M′)

Definition 2.5 is unpleasantly indirect. The proposition below gives a more direct definition of ≈_{S}.

Proposition 2.3 ≈_{S} is the relation:

M ≈_{S} M′ ⇔ ∀α ∈ ω^{∗} : t^{M}(α) = t^{M′}(α) ∈ S ∨ M/α = M′/α

with the understanding that undefined equals undefined.

2.3 Type Variables

A given term in core-ML gives rise to a finite collection of type variables, in principle one for each subterm or parse tree node. However, the type variables corresponding to different occurrences of the same identifier are identified. We shall use the notation [[E]] for the type variable corresponding to the subterm E. We denote by V the set of type variables.

2.4 Type Constraints

In general, a type constraint is a relation on types. We can, however, be more specific than simply to allow arbitrary relations. Even seemingly ad-hoc constraints share some common structure.

Given a term in core-ML, we generate the required constraints inductively in the syntax as follows. For a subterm of the form λx.E we have the constraint

[[λx.E]] = [[x]] → [[E]],

and for a subterm of the form E_{1}E_{2} the constraint

[[E_{1}]] = [[E_{2}]] → [[E_{1}E_{2}]].

The type constraint [[E]] = [[E′]] → [[E′′]] can be described as follows. If M, M′ and M′′ are automata for the values of the type variables in [[E]] = [[E′]] → [[E′′]], then we require

M = M′ → M′′ ⇔ (t^{M}(ϵ) =→) ∧ (M/1 ≈_{Σ} M′) ∧ (M/2 ≈_{Σ} M′′).

Since types are automata, it is possible to define very general constraints. In particular, it is possible to define constraints which are dependent on the actual initial state (or other states) of the automaton, e.g. by demanding that the initial state should be an integer in the range from 1 to 7. We consider constraints of this sort to be an abuse of this framework. In order to avoid it, we demand that all the constraints should be resistant to replacement of the set of states as long as this replacement does not violate the type equivalence. We need a further concept to formalize this.

Definition 2.6 A homomorphism is a function:

f : (Q, q_{0}, Σ, δ, l) → (Q′, q′_{0}, Σ, δ′, l′)

where

f : Q → Q′
f(q_{0}) = q′_{0}
δ′(f(q), i) = f(δ(q), i)
l′(f(q)) = f(l(q))

It is clear that any homomorphism is term preserving. That is, if f : M → M′ is a homomorphism, then M ≈_{Σ} M′. This means that any relation over terms is resistant to any homomorphism (i.e. R(M) ⇔ R(M′), where M and M′ are as above). For general S, though, we need a stronger restriction on the homomorphisms.

Definition 2.7 An indexed family of homomorphisms:

(f_{i} : M_{i} → M′_{i})_{i∈I}

is ≈_{S}-preserving iff:

∀i, j ∈ I, q ∈ Q_{i}, q′ ∈ Q_{j} : M_{i}[q] ≈ M_{j}[q′] ⇔ M′_{i}[f_{i}(q)] ≈ M′_{j}[f_{j}(q′)]

where M_{i} = (Q_{i}, q_{i0}, Σ, δ_{i}, l_{i}) and M′_{i} = (Q′_{i}, q′_{i0}, Σ, δ′_{i}, l′_{i}).

For an indexed family of homomorphisms, Φ = (f_{i} : M_{i} → M′_{i})_{i∈I}, we introduce the following notation:

Φ(M_{i}) = M′_{i}
dom(Φ) = {M_{i} | i ∈ I}
codom(Φ) = {M′_{i} | i ∈ I}

Definition 2.8 A constraint alphabet is a ranked alphabet, Γ, of relations, where each R ∈ Γ satisfies the following: For all automata M_{1}, …, M_{n}, and for any ≈_{S}-preserving family of homomorphisms, Φ, such that {M_{1}, …, M_{n}} ⊆ dom(Φ), we have:

R(M_{1}, ..., M_{n}) ⇔ R(Φ(M_{1}), ..., Φ(M_{n}))

where n = arity(R). A constraint from Γ is of the form R(v_{1}, …, v_{n}), where R ∈ Γ, v_{i} ∈ V, and n = arity(R).

In general, the type constraints generated for a given term can be described using simple rules following the syntax. For each production in the context-free grammar, such as X ::= aY bZc, a finite number of constraints of the form R([[X]], [[Y]], [[Z]]) are generated.

2.5 Solutions

The hardest problem in a type inference arises when trying to find a solution to the set of constraints generated from a specific program. This is often done by at any point to represent the set of solutions to the constraints read so far. We present here a uniform representation of a single solution that may sometimes suggest how to solve the constraints.

A solution to a set of constraints is an assignment of a type to each type variable that occurs in the constraints, such that the constraints are satisfied when the type variables are replaced with the assigned types. We can thus represent a solution by a partial function: S : V → A(Σ, L). We will look at an alternative representation of solutions that are more closely connected to automata, the base automaton.

Definition 2.9 A base automaton over a set V of type variables and an alphabet, Σ, is a pure Σ-term automaton, M = (Q, Σ, δ, l), where Q is a set of non-empty, finite, pairwise disjoint subsets of V. We write ⟨v⟩_{M} for the element of Q containing v if it exists.

Definition 2.10 The solution corresponding to a base automaton M = (Q, Σ, δ, l) is the partial function S_{M} defined by S_{M}(v) = (Q, ⟨v⟩_{M}, Σ, δ, l).

In the following we will show that it is sufficient to look at base automata. Actually, S-minimal base automata can always be found. An automata is Sminimal, if it cannot be smaller and still have the same ≈_{S} properties as in the definition below.

Definition 2.11 A base automaton, M, is S-minimal, iff for each automaton M′, S_{M′}(v) ≈_{S} S_{M′}(v′) ⇔ S_{M}(v) ≈_{S} S_{M}(v′) implies that M has fewer states than M′.

The advantage with S-minimal automata is that the relation ≈_{S} becomes equality between initial states.

Proposition 2.4 A base automaton M is minimal, iff S_{M}(v) ≈_{S} S_{M}(v′) ⇒ ⟨v⟩_{M} = ⟨v′⟩_{M}.

Proposition 2.5 Let S : V → A(Σ, L). There exists an S-minimal base automaton, M, and a ≈_{S}-preserving family of homomorphisms, Φ, such that for all v ∈ dom(S): S_{M}(v) = Φ(S(v)).

Corollary 2.6 Let C be a set of constraints. If C has a solution, then there is a minimal base automaton, M, such that S_{M} is a solution to C.

This means that we can restrain ourselves to looking at types of the form M[q], where M is an S-minimal base automaton. For such automata equivalence actually reduces to simple equality.

2.6 The Algorithm

In the end, type inference reduces to an algorithmic problem that is clearly outlined by the above definitions. Since the relations involved in the type constraints can be quite expressive, it is not possible to provide a completely general algorithm. For the simple case of core-ML, it is well-known that the constraints can be solved by means of the unification algorithm in time O(n), where n is the size of the program [10].

It is sometimes thought that for more general languages one must seek to develop a more general notion of unification. It is our experience that this is not so. In spite of the uniform framework we present, it seems that ad-hoc languages give rise to ad-hoc algorithms. We have seen occurrences of algorithms as varied as the following: determinization of non-deterministic finite state automata [9], dynamic transitive closure [6], and in this paper a mixture between a name equivalent version of unification and a special case of general satisfiability.

2.7 Polymorphism

An integral part of the ML language is its approach to polymorphism. It is traditionally linked to the notion of principal type scheme, but we shall argue that the proper generalization is that of code expansion.

Functions defined by the polymorphic let-construct in ML are assigned a principal type scheme, which is instantiated with fresh type variables at all call sites. Imagine now that we syntactically expand these let-constructs. This will yield a potentially exponentially larger monomorphic term that is typable if and only if the original term is typable. This is not surprising, since type variables are derived from parse tree nodes. Mairson [8] and Kfoury et al [4] have shown that type inference in the polymorphic case is complete for deterministic exponential time, so we have not even compromised efficiency in the asymptotic sense.

For more ad-hoc type systems it is less likely that principal type schemes will exist. Thus, our generalized approach to polymorphism will be that of code expansion, which is clearly always a meaningful transformation. For ML-style languages we obtain in principle the traditional result, even if we are then left to discover the possibilities of compact representations of types and efficient polymorphic code generation.

3 An Application to Turbo Pascal

We now have generalized the concepts underlying the technique for ML-style type inference. We next endeavor to demonstrate that these generalizations are sensible and practical, rather than merely a formal exercise. To that purpose we develop an algorithm for type inference in the Turbo Pascal language—truly a worthy representative of the ad-hoc school of languages.

There is of course not a formalized description of the Turbo Pascal type system. We have therefore had to rely on the informal reference manual, from which we have been able to deduce a formal model that has been verified through experiments with the implementation.

3.1 Type Domain

We define the type domain for Turbo Pascal by giving the alphabet and the regular tree language. This is an example where the regular tree language is different from the free algebra generated by Σ.

Turbo Pascal provides a finite set C_{T P} of type constants and a ranked alphabet:

Σ_{T P} = C_{T P}
∪ {(a_{1}, …, a_{n}) | n > 0 ∧ i ≠ j ⇒ a_{i} ≠ a_{j}}
∪ {record(a_{1}, …, a_{n}) | n ≥ 0 ∧ i ≠ j ⇒ a_{i} ≠ a_{j}}
∪{set, array,^{∧} , file}

where arity(c) = 0 for all c ∈ C, arity(a_{1}, …, a_{n}) = 0, arity(set) = arity(file) = arity(^{∧}) = 1, arity(record(a_{1}, …, a_{n})) = n), and arity(array) = 2.

In Turbo Pascal there is a subset O_{0} ⊆ C_{T P} of ordinal types. This set is extended to O = O_{0} ∪ {(a_{1}, …, a_{n}) | n > 0 ∧ i ≠ j ⇒ a_{i} ≠ a_{j}}. Furthermore we have the set \overline{F} of Σ_{T P} -terms not containing the label file. The regular tree language L_{T P} is the set of Σ_{T P} -terms such that the subterm of a node with label set will be in O, the left subterm of a node with label array will be in O, and the subterm of a node with label file will be in \overline{F}. That is

L_{T P} = \{t | ∀α : t(α) ∈ \{set, array\} ⇒ t/α1 ∈ O ∧ t(α) = file ⇒ t/α1 ∈ \overline{F} \}

To see that L_{T P} is a regular tree language simply construct the obvious grammar with nonterminals ord generating O and notfile generating \overline{F}.

All in all, the type domain in Turbo Pascal is A(Σ_{T P} , L_{T P}).

3.2 Type Equivalence

The Turbo Pascal type system is distinguished from many others by using the notion of name equivalence, whereas ML incorporates structural equivalence. That is, two types are considered equal if and only if they have the same tree structure. As we have seen, this corresponds to term equality between automata. In name equivalence, types are equal if and only if they have the same name or they are explicitly defined to be equal in an equational system.

In general, we consider a ranked alphabet, Σ, and a countably infinite set, V, of variables. The set of right-hand sides over V and Σ is R(V, Σ) = V ∪ {l(v_{1}, …, v_{n}) | l ∈ Σ, arity(l) = n, v_{i} ∈ V}. An equational system, E, over V and Σ, is a finite subset E ⊆ V × R(V, Σ). We will say that E is well-defined, if the left-hand sides are all different, closed if any variable on a right-hand side occurs on a left-hand side, and normalized if every right-hand side is of the form l(v_{1}, …, v_{n}).

If E is well-defined, we will view it as a partial function E : V → R(V, Σ). So for (v, r) ∈ E, we will write E(v) = r. Similarly, we take dom(E) and codom(E) to be {v | (v, r) ∈ E} and {r | (v, r) ∈ E}, respectively.

Definition 3.1 Let E be a well-defined, closed type equation system. The name equivalence relation with respect to E is the reflexive, symmetric, and transitive closure of the relation E ∩ V × V. We write this relation as ∼_{E}, and the equivalence classes as ⟨v⟩_{E} = {v′ | v ∼_{E} v′}.

Definition 3.2 Let E be a well-defined, closed equational system over V and Σ. The quotient of E is an equational system over 2^{V} and Σ ∪ {Ω}:

\begin{matrix}E/ ∼_{E} & = & \{(⟨v⟩_{E}, l(⟨v_{1}⟩_{E}, …, ⟨v_{n}⟩_{E})) | (v, l(v_{1}, …, v_{n})) ∈ E\} \\ ∪ & \{(⟨v⟩_{E}, Ω) | ∀v′ ∈ ⟨v⟩_{E} : E(v) ∈ V\} \end{matrix}

Clearly, E/ ∼_{E} is well-defined, closed, and normalized.

Definition 3.3 Let E and E′ be well-defined, closed equational systems. We say that E and E′ are congruent, iff E/ ∼_{E}= E′/ ∼_{E′}.

Definition 3.4 Let E be a well-defined, closed, and normalized equational system over V and Σ. We define Auto(E) = (Q, Σ, δ, l), where Q = dom(E), and for each (v, λ(v_{1}, …, v_{n})) ∈ E, we have δ(v, i) = v_{i} and l(v) = λ.

For a well-defined, closed equational system, E, we can construct the automaton Auto(E/ ∼_{E}). With this construction we can prove the proposition below.

Proposition 3.1 The set of base automata over V and Σ ∪ {Ω} is isomorphic to the set of well-defined, closed equational systems over V and Σ modulo congruence.

In Turbo Pascal the programmer defines an equational system, and then uses the type variables to annotate the program.

Definition 3.5 A type in Turbo Pascal is a pair (E, v), where E is a welldefined, closed equation system over V and Σ_{T P}, and v ∈ dom(E).

Definition 3.6 Two types, (E, v) and (E′, v′) are name equivalent, iff E and E′ are congruent and v ∼_{E} v′. We write this as (E, v) ≈ (E′, v′).

Lemma 3.2 Let M = Auto(E/ ∼_{E}) and M′ = Auto(E′/ ∼_{E′}). We have that

(E, v) ≈ (E′, v′) ⇔ S_{M}(v) ≈_{∅} S_{M′}(v′)

It is impractical to use the relation ≈_{∅}. Consider for example the following program:

Var x: Integer; Var y: Integer; x := y

Any programmer would expect this to work properly. So in Turbo Pascal the name equivalence relation is loosened to ≈_{C_{T P}} (which we shall write ≈_{C}).

3.3 Type Variables

As for ML we generate a finite collection of type variables, but in this case only for parse tree nodes corresponding to expressions or variable references, since these are the only ones that can have types. We identify type variables corresponding to different occurrences of the same variable reference. We use the same notation as for ML.

3.4 Type Constraints

The Turbo Pascal constraints are quite complex. They reflect the ad-hoc nature of the language.

In Turbo Pascal we have a finite set W of finite sets of terms. The intention with W is to represent restrictions to overloading of operators. We have the constraint alphabet:

Γ_{T P} = {∈w | w ∈ W}
∪ {=l | l ∈ Σ_{T P} }
∪ {Rec_{α} | α is a field name}
∪ {=, Tc,:=, Io, Op}

where ∈ w has arity 1, = l has arity arity(l) + 1, Rec_{α}, =, Tc, :=, and Io has arity 2, and Op has arity 3. Let us look more closely at the constraints from this alphabet.

• v ∈ w is used to restrict the other constraints, when they are too general. If M is the type corresponding to v, we must have t^{M} ∈ w.

• v = l(v_{1}, …, v_{n}) appears in connection with referencing subvariables. E.g. for the variable reference ^{∧}x we have the constraint [[x]] = ^{∧}([[^{∧}x]]). If M, M_{1}, …, M_{n} are the types of v, v_{1}, …, v_{n} then we require t^{M}(ϵ) = l ∧ ∀i ∈ {1, …, n} : M/i ≈_{C} M_{i}.

• Rec_{α}(v, v′) is similar to the above. The variable reference x.α gives rise to the constraint Rec_{α}([[x]], [[x.α]]). If v and v′ have types M and M′ there must be a sequence α_{1}, …, α_{n} and an i between 1 and n, such that t^{M}(ϵ) = record(α_{1}, ..., α_{n}) ∧ α = α_{i} ∧ M′ ≈_{C} M/i. This definition differs from the above by allowing records to be extended.

• v = v′ arises in a number of places. For example in procedure calls, where the actual type must equal the formal type of a variable parameter. M and M′ is a solution to v = v′, iff M ≈_{C} M′.

• v Tc v′, v := v′, v Io v′, and Op(v, v′, v′′). These constraints are concerned with type coercion, overloading and the like. They are the most complex of the Turbo Pascal constraints. As examples of where they arise, we can take x := e, where the constraint is [[x]] := [[e]] or e + e′, where we generate the constraints Op([[e]], [[e′]], [[e + e′]]), [[e]] ∈ w, [[e′]] ∈ w, and [[e + e′]] ∈ w, where

w = {Integer, Real, String, Char, array(Integer, Char)} ∪ {t | t(ϵ) = set}.

The definitions of these relations show how complex they are. For example Tc is defined as the least symmetric relation such that M Tc M′, if one of the following holds:

– M ≈_{C} M′

– t^{M}, t^{M′} ∈ {Integer, Real}

– t^{M}(ϵ) = t^{M′}(ϵ) = set ∧ M/1 Tc M′/1

– t^{M} = t^{M′} = array(Integer, Char)

– t^{M} = String ∧ t^{M′} ∈ {String, Char, array(Integer, Char)}

– t^{M} = Pointer ∧ t^{M}(ϵ) =^{∧}

To see that the relations in Γ_{T P} are resistant to ≈_{C}-preserving families of homomorphisms, it is enough to note that these are defined only by the terms of the automata and the relation ≈_{C}.

3.5 Solutions

In Turbo Pascal it becomes very natural to represent the solution as a base automaton, since this is isomorphic to type equations. As we have hoped for the concept of a base automaton suggests an algorithm that can solve some of the constraints. For the rest of the constraints we have to be more inventive. The construction of the algorithm is outlined in the next subsection.

3.6 The Algorithm

The Turbo Pascal type constraints may seem quite arbitrary and without any redeeming structure. For example, the relation Tc is reflexive and symmetric, but not transitive. Even worse, the relation := is neither reflexive, symmetric, transitive, nor antisymmetric. Nonetheless, these relations have some structure that can be exploited to obtain an algorithm.

The basic idea of the algorithm is to represent a set of solutions (base automata) by a base automaton labeled by sets of labels. The idea is to label each state with the set of labels that it might take according to the constraints read so far. For each label we have the possible transitions out of the state. If we have yet to read a constraint for any of the variables in the state, we say that those variables are fresh. We mark this by a special label, ∗.

By using base automata over label sets we can represent the set of solutions to the relations ∈w, =l, Rec_{α}, and =. Furthermore, by using name equivalent unification we can maintain a representation of the set of solutions to a set of constraints over these relations. What remains is to deal with the relations Tc, :=, Io, and Op. As one might expect, these relations are too complex to fit into the model of base automata over sets of labels.

In general, we consider relations R(M_{1}, …, M_{n}), which can be described as finite disjunctions of clauses, where each clause is a finite conjunction of literals, and each literal is either of the form l(q) = λ or M_{i}[q] ≈_{C} M_{j}[q′]. Finding solutions to such relations is in general NP-hard, so we add extra requirements to the relations R. If these requirements are satisfied we can find a solution to a set of O(n) constraints over O(n) variables in time O(n^{2} log n).

Turbo Pascal constraints violates these requirements in a few places, but in each case we can argue that the algorithm succeeds here as well. It seems that in general the requirements on the strong labels and the partition of the labels can be weakened somewhat without affecting the correctness of the algorithm, but it is not clear at the moment how to describe the full generality of the algorithm.

3.7 Polymorphism

As predicted in the previous section, Turbo Pascal does not allow principal types schemes. This can be demonstrated by the following simple example.

Procedure P(var x; y); begin

x := 2∗y; end;

In the above procedure, both the type of [[x]] and the type of [[y]] can be any of the types Integer and Real but not independently. If the type of [[x]] is Integer then the type of [[y]] must be Integer as well. If the type of [[x]] is Real then the type of [[y]] can be any of the types Integer and Real. Clearly, it is impossible to express this interdependence through type schemas, where the interdependence of two types is expressed through common type variables. It might be possible to express the interface of a procedure in a more compact form than just the set of constraints. At this moment, however, it is not clear to us how this should be done. The only remaining possibility is to resort to code expansion. In any case, we would have to generate expanded code since Turbo Pascal has no native polymorphism.

We proceed by taking a procedure, which is called from two places within the program. We make a copy of the procedure with a new name, and replace one of the two calls by a similar call to the new procedure. We repeat this until no procedure is called from two different places. In the presence of recursive procedures this method will lead to infinite copying. This means, that just as in ML we must disallow recursive polymorphism.

We can view the problem as one concerning graphs in the following way. Any procedure is a node in the graph. In addition there is a main node for the main body of the program. For each procedure call there is an edge from the calling procedure to the called procedure. Assuming that all nodes in the graph are reachable from the main node, we can proceed by a breadth-first search from the main node, coloring the nodes as we meet them and copying a node when we meet it for the second time. In order to deal with cycles in the graph (corresponding to recursive calls) we construct the component graph before beginning the search. The component graph has as nodes the maximal, strongly connected components and as edges those going between different components.

By proceeding down the block structure of a program in a depth-first, postorder fashion and using the above method on each scope we have the full code expansion algorithm. In the worst case the size of the expanded graph is exponential, so the asymptotic time of code expansion will be exponential in the size of the program. For a program of size n we get that the total time for type inference with code expansion is 2^{O(d log n)}, where d is the longest path through the component graph. This is the same time bound that Kanellakis and Mitchell [3] found for type inference of ML.

4 Conclusion

The framework that we have presented is sufficiently general to cover the spectrum from ML to Turbo Pascal. Even so, it is sufficiently specific to provide substantial assistance in the development of algorithms.

The tool that we have constructed for Turbo Pascal suggests how the benefits of type inference may also come to influence the programming methodology for standard imperative languages. The algorithm we have presented can easily be adapted to, say, Modula-2 or C.

It is safe to assume that ad-hoc languages will continue to have a presence in our culture. We hope by this work to demonstrate that modern tools can provide substantial help in using them.

References

[1] Bruno Courcelle. Infinite trees in normal form and recursive equations having a unique solution. Mathematical Systems Theory, 13:131–180, 1979.

[2] Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25(1):95–169, 1983.

[3] Paris C. Kanellakis and John C. Mitchell. Polymorphic unification and ML typing. In 16th ACM conf. on Principles Of Programming Languages, pages 105–116, 1989.

[4] A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. An analysis of ML typability. Journal of the ACM, 41:368–398, 1994.

[5] Dexter Kozen. Logical aspects of set constraints. TR 94-1421, Department of Computer Science, Cornell University, Ithaca, New York, May 1994.

[6] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. In Proc. 33rd Symposium on Foundations of Computer Science., pages 363–371. IEEE, October 1992.

[7] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In Proc. 20th Symp. Princip. Programming Lang., pages 419–428. ACM, January 1992.

[8] Harry G. Mairson. Decidability of ML typing is complete for deterministic exponential time. In Seventeenth Symposium on Principles of Programming Languages, pages 382–401. ACM Press, January 1990.

[9] Michael I. Schwartzbach. Type inference with inequalities. In Proceedings of TAPSOFT’91. Springer-Verlag (LNCS 493), 1991.

[10] M. Wand. A simple algorithm and proof for type inference. Fundamentae Informaticae, X:115–122, 1987.