Control-Flow Analysis and Type Systems^{⋆}

Nevin Heintze^{⋆⋆}

School of Computer Science Carnegie Mellon University

Abstract. We establish a series of equivalences between type systems and control-flow analyses. Specifically, we take four type systems from the literature (involving simple types, subtypes and recursion) and conservatively extend them to reason about control-flow information. Similarly, we take four standard control-flow systems and conservatively extend them to reason about type consistency. Our main result is that we can match up the resulting type and control-flow systems such that we obtain pairs of equivalent systems, where the equivalence is with respect to both type and control-flow information. In essence, type systems and control-flow analysis can be viewed as complementary approaches for addressing questions of type consistency and control-flow. Recent and independent work by Palsberg and O’Keefe has addressed the same general question. Our work differs from theirs in two respects. First, they only consider what happens when control-flow systems are used to reason about types. In contrast, we also consider the dual question: what happens when type systems are used to reason about control-flow. Hence our results establish a much closer and more symmetric notion of equivalence: Palsberg and O’Keefe’s equivalence refers only to typability properties, whereas our equivalences refer to both typability and controlflow. Second, Palsberg and O’Keefe establish only one pair of equivalent systems, whereas we establish four pairs of (stronger) equivalences.

1 Introduction

A central concept in compiler optimization and code generation is a graph of how control can flow from one program point to another. Such a graph identifies block and loop structure in a program, and this is the starting point for a large number of optimizations. In many languages, this control-flow graph can be directly constructed from a program because information about flow of control from one point to another is explicit. However, in a language with higher-order functions, the flow of control from one point to another is not readily apparent from program text because a function can be passed around as data and subsequently

⋆ This work was sponsored by the Advanced Research Projects Agency, CSTO, under the title “The Fox Project: Advanced Development of Systems Software”, ARPA Order No. 8313, issued by ESD/AVS under Contract No. F19628-91-C-0168.

⋆⋆ 5000 Forbes Ave., Pittsburgh, PA 15213, USA. Email: nch@cs.cmu.edu.

called from anywhere in the program. If this happens sufficiently often, then the lack of control-flow information can significantly limit compiler performance. To addresses this issue, systems for control-flow analysis [4, 5, 11, 2, 9] have been developed. The purpose of control-flow analysis is to compute an approximation of the possible functions that can be called from each program point.

In contrast, the purpose of a type inference system is to derive invariants about the potential bindings of variables in a program. However, in the context of higher-order functions, functions can be data and therefore can be bound to variables. Hence, there is an intuitive connection between reasoning about functions (in control-flow analysis) and reasoning about the data values to which variables may be bound (in type inference). In fact it is possible to extend type systems to perform control-flow analysis [12, 13], and conversely, extend controlflow systems to perform type analysis [8, 9]. There are also informal connections between the kinds of reasoning done by type and control-flow systems. For example, consider the essence of the application rule of a subtype system:

if M has type τ_{1} → τ_{2} and N has type τ′_{1} such that τ′_{1} ⊆ τ_{1}, then (M N) has type τ_{2}

Contrast this with a control-flow view of (M N): if the results of N are described by τ′_{1} and the functions that flow to M are such that, when called on arguments described by some τ_{1} such that τ_{1} includes τ′_{1}, they return results that are described by τ_{2}, then it is correct to use τ_{2} to describe the results returned by (M N).

Despite these informal similarities, type systems and control-flow system possess quite different structure. Type systems are typically specified using deductive systems. Such systems associate a type with each program expression and this type completely captures the type system’s view of the behavior of the expression. These systems are compositional and often have direct application to modular analysis and separate compilation. In contrast, control-flow analysis systems typically reason globally using finite sets of “function labels”. Such presentations are rarely compositional, but they are often more suggestive of feasible implementation strategies.

Given these similarities and differences, two important and complementary questions arise:

1. Can control-flow systems be extended to perform type checking/inference, and if so, does the type information obtained correspond to any known type system?

2. Can type systems be extended to compute control-flow information, and if so, does the control-flow information obtained correspond to any known control-flow system?

Recent work by Palsberg and O’Keefe [10]^{3} addresses the first of these ques-

3 The result presented there was also independently obtained in [3].

tions. Specifically, they consider Amadio/Cardelli’s type system with subtyping and recursive types, and Palsberg and Schwartzbach’s safety analysis (which is essentially a control-flow analysis that has been modified to perform type checking). They show that the two systems are equivalent in following sense: a program can be given a type by the type system iff it is accepted as safe by the safety analysis. This result effectively shows that control flow analysis can be used to perform type inference in the Amadio/Cardelli type system.

In this paper we provide the first equivalence results that address the second question. We also provide three new results that address the first question for types systems other than the Amadio/Cardelli system. The paper begins with a uniform presentation of four type systems (extended to reason about controlflow) and four control-flow systems (extended to reason about type consistency). The type systems we consider are simple types, partial types, simple recursive types, and recursive subtypes. Each system is extended in a generic way so that the types carry control-flow information. In each case, the extension preserves the structure of the underlying type system: the same sets of terms are typable under the extended system, and in fact we can fairly easily translate between derivations in the extended system and the original system. The control-flow systems we consider are “control-flow-0” (a standard system in the control-flow literature), a system based on unification, and two derived systems that exclude recursion. In each case, these systems are modified to reason about type consistency in such a way that their ability to reason about control-flow is not changed. Our main result is that the families of types systems and control-flow systems are equivalent in the following sense: for each type system there is a control-flow system such that (i) both systems compute the same control-flow information, and (ii) the type consistency components of both systems coincide.

Two main technical issues arise in these equivalence proofs. First, type systems and control-flow systems compute over different representations. For the type systems used in this paper, types can be viewed as (possibly infinite) trees that are decorated with control-flow information. Each type system associates one of these trees with each subexpression of the program. In contrast, the control-flow systems used in this paper compute using finite sets (which essentially contain labels of functions). Each control-flow system annotates program subexpressions with control-flow sets. A key part of the proof involves mapping from one representation to the other. While mapping from a type to a controlflow annotation can be achieved by just suppressing type structure, the mapping in the reverse direction is more complex: it involves reconstructing a type tree using the annotations of the entire program. Thus, type information is not explicit in the control-flow annotations, but rather it is distributed over the entire program. In essence, the control-flow annotations of the program collectively represent encodings of (potentially infinite) trees. The second difficulty is that the type and control-flow systems employ different notions of “consistency”. For example consider an application M N. In a control-flow system, consistency involves considering all functions that can flow to M and reasoning about the annotations of these functions. In contrast, a type system would reason about this application by considering just the types associated with M and N. Any information about the functions that can flow to M is already represented in the type associated with M. In short, types involve only local reasoning; control-flow involves highly non-local reasoning.

The equivalences established in the paper reveal much about the underlying structure of control-flow and type systems. For example, adding recursive types to a type system corresponds exactly to allowing cycles in the control-flow graph computed by a control-flow analysis. Similarly, adding subtypes to a type system corresponds exactly to replacing equalities by set containment in the consistency conditions of a control-flow system. Our results also provide a basis for exploiting the advantages of both the type and control-flow view. From the point of view of implementing an analysis, it is usually easier to start from a control-flow system. Conversely, for the purposes of designing a modular analysis system, type systems have an advantage since they are usually presented compositionally (we remark that one of the original motivations for this paper was the development of modular analysis). In addition, certain results are sometimes easier to prove in one system that the other (e.g. correctness becomes a subject reduction result in the type system). In short, type systems and control-flow analysis can be viewed as complementary approaches for addressing questions of type consistency and control-flow.

2 Preliminaries

We define a variant of the λ-calculus with labeled abstractions. The reason for the labels is that they allow us to talk about program “control-flow”. This language is suggestive of an intermediate language that might be produced by a compiler front end; it is not intended as a language for writing programs. Let labels be a countably infinite set of labels, and define terms e by:

e ::= x | λ^{l}x.e | e_{1} e_{2} | 0 | Succ e.

where l ∈ labels. The intention is that labels distinguish different occurrences of abstractions. Free and bound occurrences of variables in a term are defined in the usual way. A term is closed if all occurrences of variables are bound. A program is a closed term in which each abstraction has a unique label. Evaluation for this language is based on β-reduction:

(λ^{l}x.e) e′ ⟶_{β} e[x/e′]

where e[x/e′] denotes the result replacing of e′ by x in e, after appropriate renaming of bound variables. Note that this process preserves labels on abstractions: e.g. (λ^{l}x.(x x)) (λ^{l′}x.(x x)) ⟶_{β} (λ^{l′}x.(x x)) (λ^{l′}x.(x x)).

There are no restrictions on the reduction order: the β-reduction can be applied at any subterm at any time. However, we do require that two conditions be satisfied: (a) whenever an application (e_{1} e_{2}) appears in a term, then e_{1} cannot be 0 or of the form Succ e, and (b) whenever Succ e appears in a term, then e must not be of the form λ^{l}x.e. If these conditions are not met, then program execution terminates with an error. The possibility of this behavior leads to a very natural typing problem that forms a key part of this paper. This typing problem arises precisely because 0 and Succ have been added to the language; however our results are largely independent of the specific choice of constants, and could be generalized to other settings.

The language also gives rise to a natural control-flow problem: given a program e_{0}, construct a set of labels L such that if e_{0} evaluates to a lambda expression, the label of this expression will be contained in L. More generally, we are interested in the sets of labels for subexpressions as well.

To formalize type and control-flow systems, we introduce various systems for “correctly” annotating a term (and all of its subterms) with either type or control-flow assertions. In general, these annotated terms will have the following form: if A is a countable set of annotations, then the A-annotated terms z (or just annotated terms) are defined by:

z ::= x:A | (λ^{l}x.z):A | (z_{1} z_{2}):A | 0:A | (Succ e):A

where A ∈ A. Given an annotated term z, we define annot(z) to be the outermost annotation of z. That is, annot(exp : A) is A. We also define |z| to be the (standard) term resulting from stripping all annotations from z. Note that if A is a collection of types, then an annotated term is essentially an explicitly typed term; such a term carries with it much of the structure of a typing derivation for |z|.

3 Type Systems for Control-Flow Analysis

3.1 Simple Types

We begin by describing a type system for control-flow analysis based on simple types [7]. Consider a system of simple types where types τ are constructed from the single base type Int and → as follows:

τ ::= Int | τ_{1} → τ_{2}

The usual formulation of simple types uses a deductive system involving judgements of the form Γ ⊢ e:τ. Such a judgement indicates that, in the context Γ (a partial mapping from variables to types), e has type τ. However, for this paper, we need to simultaneously associate types with all of the subexpression of a term. Hence, we use type-annotated terms. These are annotated terms (as defined in the previous section) where the annotations are types. Using such terms, the standard simple type system can be presented as:

Γ ⊢ x:τ (if x : τ appears in Γ)  (var)
\frac{Γ, x:τ_{1} ⊢ z}{Γ ⊢ λ^{l}x.z:τ_{1}→τ_{2}} (if annot(z) is τ_{2})  (abs)

\frac{Γ ⊢ z  Γ ⊢ z′}{Γ ⊢ (z z′):τ_{2}} (if annot(z) is τ_{1}→τ_{2} and annot(z′) is τ_{1}) (app)
Γ ⊢ 0:Int  (int)
\frac{Γ ⊢ z}{Γ ⊢ (Succ z):Int} (if annot(z) is Int)  (succ)

We emphasize that this is just a reorganization of the standard formulation of simple types. We now describe a uniform method for enriching a type system to perform control-flow analysis. The first step is to enrich types so that they carry information about labels of abstractions. Corresponding to simple types, we define control-flow types by:

τ ::= ⟨L, Int⟩ | ⟨L, τ_{1}→τ_{2}⟩

where L ranges over finite subsets of labels. Note that the set of labels L in ⟨L, Int⟩ is unnecessary because no functions can have type Int; we retain this notation for uniformity with later definitions. The next step is to modify the typing rules of the system to accommodate control-flow types. For simple types, we modify the above typing rules and obtain the system of Figure 1. Note the side condition on the abs rule to track labels of abstractions. We write ⊢_{λ} z and say that z is correctly typed, if the judgement empty ⊢ z is derivable (empty is the empty context). A program e_{0} is said to be ⊢_{λ} -typable if there exists a control-flow annotated term z such that |z| = e_{0} and ⊢_{λ} z. An important property of the control-flow type system is that it preserves the essential character of the underlying type system. In particular, the set of typable terms remains unchanged: e_{0} is ⊢_{λ} -typable iff e_{0} is typable in the standard simply typed system. In fact there is a very close correspondence between the two systems. If ⊢_{λ} z, then by stripping away the control-flow information in the annotations appearing in z, we can construct a derivation to show that |z| has simple type τ in the simply typed system, where τ is annot(z) with all controlflow information removed. Conversely, if a term e has simple type τ in the simply typed system, then we can look at the derivation of this judgement, and by systematically inserting trivial control-flow information^{4}, obtain an annotated term z such that ⊢_{λ} z and |z| is e. The control-flow calculus also possesses standard properties such as subject reduction:

Proposition 1 Subject Reduction. If ⊢_{λ} z and z →_{β} z′ then ⊢_{λ} z′.

4 That is, each type τ is systematically replaced by the expression ⟨L_{e}, τ⟩, where L_{e} is the set of labels in e.

Γ ⊢ x:τ (if x : τ appears in Γ)  (var)
\frac{Γ, x:τ_{1} ⊢ z}{Γ ⊢ λ^{l}x.z:⟨L, τ_{1}→τ_{2}⟩} (if l ∈ L and annot(z) is τ_{2})  (abs)
\frac{Γ ⊢ z  Γ ⊢ z′}{Γ ⊢ (z z′):τ_{2}} (if annot(z) is ⟨L, τ_{1}→τ_{2}⟩ and annot(z′) is τ_{1}) (app)
Γ ⊢ 0:⟨L, Int⟩  (int)
\frac{Γ ⊢ z}{Γ ⊢ (Succ z):⟨L, Int⟩} (if annot(z) is ⟨∅, Int⟩)  (succ)

Fig. 1. Inference rules for control-flow type system based on simple types.

This property establishes not only the correctness of the type aspects of the system, but also its control-flow aspects. For example, if ⊢_{λ} e : τ and e reduces to λ^{l}x.e′, then subject reduction implies that τ must have the form ⟨L, τ_{1}→τ_{2}⟩ such that l ∈ L.

We now address the control-flow component of the system. First note that typing is not unique: given an untyped term e_{0}, there may be many correctly typed terms z such that |z| = e_{0}. For example, corresponding to the untyped term (λ^{l}x.x), we can construct a family of correctly typed terms:

(λ^{l}x.(x : τ)) : ⟨L, τ→τ⟩

where τ is any control-flow type, and L is any (finite) set of labels containing l. Part of this choice lies at the “type” level; there is also choice at the “controlflow” level. Recall that the sets of labels that are associated with each expression in a correctly typed term represent an upper bound on the functions that can flow to that expression. Smaller sets mean more accurate control-flow information, and so from a control-flow perspective, we seek annotated terms with minimal label sets.

To address this issue, we first formalize the control-flow content of an annotated term z. For any control-flow type τ, define that cf(τ) (the control-flow component of τ) is L such that τ has the form ⟨L, ⋯⟩. Lifting this to annotated terms z, define that cf(z) denotes the result of replacing each annotation τ appearing in z by cf(τ). That is, cf(z) is an annotated term in which annotations are finite subsets of labels; this term identifies exactly the control-flow content of z, stripping away the extra type structure. Now, there is a natural information ordering > between control-flow annotated terms that have the same underlying term structure:

1. e:L > e:L′ if L ⊇ L′ and e is x or 0.

2. (λ^{l}x.z):L > (λ^{l}x.z′):L′ if L ⊇ L′ and z > z′.

3. (z_{1} z_{2}):L > (z′_{1} z′_{2}):L′ if L ⊇ L′ and z_{1} > z′_{1} and z_{2} > z′_{2}.

4. (Succ z):L > (Succ z′):L′ if L ⊇ L′ and z > z′.

We remark that this ordering can be lifted to order types and also to order correctly τ-annotated terms. The resulting orderings would give a covariant treatment of functions. Note that this ordering cannot be used as the basis for a semantic subtyping relationship – even ignoring the “type” component of control-flow types, it is not the case that “z_{1} > z_{2}” implies that a subterm z_{1} of z can be replaced by z_{2} to obtain another correctly typed term. Importantly, > gives rise to a notion of minimality with respect to control flow information (this follows directly from results in Section 4):

Proposition 2 Minimality. For any typable program e_{0}, the set of control-flow annotated terms {cf(z) : |z| = e and ⊢_{λ} z} has a minimal element, call it cf(⊢_{λ})(e_{0}).

In summary, we can define typing and control-flow aspects of ⊢_{λ}

1. Let typable(⊢_{λ}) denote the set of terms typable under ⊢_{λ}.

2. Let control-flow( ⊢_{λ} ) denote the partial mapping that maps a program e_{0} into cf(⊢_{λ})(e_{0}).

3.2 Partial Types

The second control-flow type system we describe is based on partial types [14] (with constants 0 : Int and Succ : Int → Int). Partial types extend simple types with a new type Ω that is a supertype of all other types (some papers use ⊤ instead of Ω). To illustrate its effect, consider the term

(λf. … (f 0) … (f λy.0) …)(λx.x)

which defines the identity function, binds it to the variable f, and then applies it to an integer in one place and an integer function in another. It is not possible to give this term a type using simple types because the term requires that f simultaneously has a type Int → τ and a type (τ′ → Int) → τ. However, by using the Ω type, we can give f the type Ω→Ω. In other words, Ω can be used to “unify” different types (or parts of types) that have incompatible structure, but little can be done with expressions that are given this type – they can neither be applied nor used as an argument of Succ.

We extend the developments of the previous section to define a type system for control-flow analysis based on partial types. In this extended system, types are defined by:

τ ::= ⟨L, Int⟩ | ⟨L, Ω⟩ | ⟨L, τ_{1}→τ_{2}⟩

These types are ordered as follows:

1. ⟨L, ⋯⟩ ≤ ⟨L′, Ω⟩ if L ⊆ L′

2. ⟨L, τ_{1}→τ_{2}⟩ ≤ ⟨L′, τ′_{1}→τ′_{2}⟩ if L ⊆ L′, τ′_{1} ≤ τ_{1} and τ_{2} ≤ τ′_{2}.

Note that this ordering not only involves the “type” structure, but it also involves control-flow information. For example,

⟨{l_{1}}, Int→Int⟩ ≤ ⟨{l_{1}, l_{2}}, Int→Int⟩

Γ ⊢ x:τ (if x : τ′ appears in Γ and τ′ ≤ τ)  (var)
\frac{Γ, x:τ′_{1} ⊢ z}{Γ ⊢ λ^{l}x.z:⟨L, τ_{1}→τ_{2}⟩} (if τ_{1} ≤ τ′_{1}, annot(z) ≤ τ_{2} and l ∈ L)  (abs)

\frac{Γ ⊢ z  Γ ⊢ z′}{Γ ⊢ (z z′):τ} ( \begin{matrix}if annot(z) is ⟨L, τ_{1}→τ_{2}⟩, \\ annot(z′) ≤ τ_{1} and τ_{2} ≤ τ \end{matrix} )  (app)
Γ ⊢ 0:τ (if ⟨L, Int⟩ ≤ τ )  (int)

\frac{Γ ⊢ z}{Γ ⊢ (Succ z):τ} (if annot(z) ≤ ⟨∅, Int⟩ and ⟨∅, Int⟩ ≤ τ)  (succ)

Fig. 2. Rules of inference for simple subtype system.

Typing rules for these types can be obtained by modifying the rules in Figure 1 so that both the assumptions and conclusions of the rules can be weakened using the subtype relationship. The resulting rules are given in Figure 2, and we write ⊢_{λ(Ω)} z if empty ⊢_{λ(Ω)} z is derivable using these rules. We remark that if we are only interested in questions of typability (that is, given a term e, does there exist a typed term z such that e = |z|) then the system in Figure 2 is equivalent to just adding a subsumption rule to Figure 1. However, we shall be concerned with the specific structure of the types that appear in (correctly) type-annotated terms, and how these relate to the annotations obtained using control-flow systems. For this purpose, the system of Figure 2 is the appropriate formulate because it leads to typed terms that have the simplest correspondence with the annotated terms that arise from control-flow systems.

A program e_{0} is said to be ⊢_{λ(Ω)}-typable if there exists a control-flow annotated term z such that |z| = e_{0} and ⊢_{λ(Ω)} z. As in the previous subsection, the control-flow type system and the underlying basic type system (this time partial types) are closely related. They have the same sets of typable terms, and derivations in one system can be replayed (after appropriate addition or suppression of structure) in the other system. The ⊢_{λ(Ω)} system also satisfies the subject reduction property (the obvious modification of Proposition 1). Moreover, the > preference ordering can be used to order the accuracy of control-flow information in annotated terms. An appropriate version of the minimality proposition (Proposition 2) also holds, and so, given a ⊢_{λ(Ω)} -typable program e_{0}, we can define a “best” control-flow annotated term cf(⊢_{λ(Ω)} )(e_{0}). Hence, typability and control-flow aspects of ⊢_{λ(Ω)} can be given:

1. Let typable(⊢_{λ(Ω)} ) denote the set of terms typable under ⊢_{λ(Ω)} .

2. Let control-flow(⊢_{λ(Ω)} ) denote the partial mapping that maps a program e_{0} into cf(⊢_{λ(Ω)} )(e_{0}).

3.3 Recursive Types

The third system is based on recursive types, another extension of simple types. This time types are extended by adding a fixpoint construction μα.τ. The effect of this addition is that terms involving recursion such as (λ^{l}x.(x x)) (λ^{l′}x.(x x)) can be typed. To define a control-flow type system based on recursive types, we first define open types σ as follows:

σ ::= α | ⟨L, Int⟩ | ⟨L, σ_{1}→σ_{2}⟩ | μα.σ

where α ranges over a countably infinite collection of type variables, and μα. is treated as a binding construct. Free and μ-bound occurrences of type variables in open types are defined in the usual way. We define an equality on open types by:

μα.σ = σ[μα.σ/α]

where σ[μα.σ/α] denotes the result of replacing free occurrences of α by μα.τ in τ (after renaming of bound variables, if necessary). This is extended in the obvious way to become a congruence on open types: if σ_{1} = σ_{2} and σ′ is the result of replacing σ_{1} by σ_{2} in σ then σ′ = σ. In what follows, we do not distinguish between open types in the same equivalence class. That is, when we write a type τ, we implicitly mean the equivalence class of τ (except where indicated otherwise). Finally, types τ are defined to be those expressions σ that do not contain free type variables.

The typing rules for this new system consist of exactly the rules previously given in Figure 3.1. We write ⊢_{λ(μ)} z if empty ⊢ z is derivable. A program e_{0} is said to be ⊢_{λ(μ)}-typable if there exists a control-flow annotated term z such that |z| = e_{0} and ⊢_{λ(μ)} z. This control-flow type system preserves many of the basic properties of the underlying recursive type system. The set of typable terms is the same, and subject reduction is preserved. An appropriate version of the minimality proposition (Proposition 2) also holds; for a ⊢_{λ(μ)} -typable program e_{0}, let cf( ⊢_{λ(μ)} )(e_{0}) denote the minimal control-flow annotated term thus obtained. Typability and control-flow aspects of ⊢_{λ(μ)} can now be defined:

1. Let typable(⊢_{λ(μ)} ) denote the set of terms typable under ⊢_{λ(μ)} .

2. Let control-flow(⊢_{λ(μ)} ) denote the partial mapping that maps a program e_{0} into cf(⊢_{λ(μ)} )(e_{0}).

3.4 Amadio/Cardelli’s System

Finally, we define a control-flow type system that combines partial types and recursive types. The starting point of this development is essentially Amadio and Cardelli’s recursive subtype system [1] (with extensions for 0 and Succ). For definitional convenience, we shall use a formulation of recursive subtypes that differs slightly from those used previously in the literature [1, 6, 10]. We therefore begin by presenting this system without the control-flow information component. Define open types σ as follows:

σ ::= α | Int | Ω | σ_{1}→σ_{2} | μα.σ

where α ranges over type variables. Occurrences of types variables are defined to be free and μ-bound in an open types σ in the usual way. Again we define a congruence on open types:

μα.σ = σ[μα.σ/α]  (1)

We do not distinguish between open types in the same congruence class: when we write τ we implicitly mean the congruence class of τ w.r.t. Equation 1 (except if indicated otherwise). Types τ are defined to be those expressions σ that do not contain free type variables.

Next, we define an ordering between congruence classes of types. This ordering is defined by successive approximation (see [1, 6] for related constructions). Specifically, define an ordering ≤_{k}, k ≥ 0, as follows:

1. τ ≤_{0} τ′

2. τ ≤_{k} Ω

3. μα.α ≤_{k} τ

4. Int ≤_{k} Int

5. τ_{1}→τ_{2} ≤_{k} τ′_{1}→τ′_{2} if τ′_{1} ≤_{k−1} τ_{1} and τ_{2} ≤_{k−1} τ′_{2}

where τ and τ′ are arbitrary types. We now define that τ ≤ τ′ if τ ≤_{k} τ′ for all k ≥ 0. Observe that this ordering can be used to define an equivalence on types that is coarser than the underlying congruence on types defined by Equation 1. Specifically, define an equivalence relation on types by: τ ≡ τ′ iff τ ≤ τ′ and τ′ ≤ τ. To illustrate the difference between these two relations, observe that μα.⊤ → α ≡ μα.⊤ → α, but these two types are not equivalent under the congruence defined by Equation 1.

Now, if we ignore Int, identify ⊤ with Ω and treat ⊥ as shorthand for μα.α, then this ordering is equivalent to the one given by Amadio and Cardelli (call it ≤_{ac}) in the following sense (the proof here is fairly lengthly; we omit it because it is not the main concern of the paper):

Proposition 3. For all τ_{1} and τ_{2} not containing Int, τ_{1} ≤ τ_{2} iff τ_{1} ≤_{ac} τ_{2}.

To extend this system to control-flow, we first define open types σ by:

σ ::= α | ⟨L, Int⟩ | ⟨L, Ω⟩ | ⟨L, σ_{1}→σ_{2}⟩ | μα.σ

where α ranges over type variables. Then, types τ are those expressions σ that do not contain free type variables. A congruence on types is defined by μα.σ = σ[μα.σ/α], and an ordering ≤_{k}, k ≥ 0, is defined by:

1. τ ≤_{0} τ′

2. ⟨L, ⋯⟩ ≤_{k} ⟨L′, Ω⟩ if L ⊆ L′

3. μα.α ≤_{k} τ

4. ⟨L, Int⟩ ≤_{k} ⟨L′, Int⟩ if L ⊆ L′

5. ⟨L, τ_{1}→τ_{2}⟩ ≤_{k} ⟨L′, τ′_{1}→τ′_{2}⟩ if τ′_{1} ≤_{k−1} τ_{1}, τ_{2} ≤_{k−1} τ′_{2} and L ⊆ L′.

We define that τ ≤ τ′ if τ ≤_{k} τ′ for all k ≥ 0. The inference rules for these types are the exactly those from Figure 2. We write ⊢_{λ(Ω,μ)} to denote the typecorrectness judgement thus defined. Again subject reduction carries over to the control-flow types system, and typability for the control-flow system coincides with that for the underlying Amadio/Cardelli system. An appropriate version of the minimality proposition (Proposition 2) also holds, and so we can define, given a ⊢_{λ(Ω, μ)} -typable program e_{0}, the minimal control-flow annotated version of e_{0}, call it cf(⊢_{λ(Ω, μ)} )(e_{0}). Typability and control-flow aspects of ⊢_{λ(Ω,μ)} can now be given:

1. Let typable(⊢_{λ(Ω, μ)} ) denote the set of terms typable under ⊢_{λ(Ω, μ)} .

2. Let control-flow( ⊢_{λ(Ω, μ)} ) denote the partial mapping that maps a program e_{0} into cf(⊢_{λ(Ω, μ)} )(e_{0}).

4 Control-Flow Analysis

The purpose of control-flow is to determine information about the functions that can be called from various program points during execution of a program. In the following development, a function shall be identified by its label. We define control-flow systems using annotated terms and consistency conditions between “neighboring” annotations. By varying these consistency conditions and introducing some additional restrictions, we shall define a family of four controlflow systems.

If we were concerned only with control-flow information, it would be sufficient to annotate terms using control-flow flow information (finite subsets of labels). However, we wish to construct control-flow systems that capture typing properties (in addition to control-flow properties), for the purpose of establishing closer links with the type systems presented in Section 3. Hence, we shall use annotations γ that are finite subsets of labels ∪{Int}. Our presentations of control-flow systems is closely related to those by Palsberg and Schwartzbach [8, 9].

4.1 Standard CFA

We begin a system that corresponds to a widely studied notion of control-flow analysis [4, 5, 11, 8, 9], often called control-flow-0. The system we give is equivalent to the system described by Palsberg and Schwartzbach in [8, 9]. The only difference is in presentation: we directly use annotated terms instead of set variables and constraints. We present the system by defining that an annotated term z is well-annotated if it satisfies the following conditions:

1. if λ^{l}x.z′:γ appears in z then l ∈ γ.

2. if (z_{1} z_{2}):γ appears in z then Int ∉ annot(z_{1}) and for all l ∈ annot(z_{1}), if λ^{l}x.z′ appears in z then:

(a) annot(z′) ⊆ γ, and

(b) if x occurs free in z′ with annotation γ_{x} then annot(z_{2}) ⊆ γ_{x}.

3. if 0:γ appears in z then γ ⊇ {Int}

4. if (Succ z′):γ appears in z then γ ⊇ {Int} and annot(z′) ⊆ {Int}.

We shall refer to this system as cfa_{⊆}. As in the previous section, we shall define typing and control-flow properties of this system by relating untyped programs and annotated terms. First, consider typing. Define that a program e_{0} is cfa_{⊆}-type-consistent if there exists an annotated term z such that e_{0} = |z| and z is well-annotated according to the above definition. Next consider controlflow. Clearly there will in general be many well-annotated versions of e_{0}, each identifying potentially different control-flow information. These terms can be related using the ordering > defined in Section 3. Strictly speaking, > orders terms that are annotated with finite subsets of labels, but it can clearly be generalized to order any annotated terms where the annotations are sets.

Proposition 4 Minimality. For any cfa_{⊆}-type-consistent term e_{0}, there is >- minimal well-annotated term z such that |z| = e_{0}.

This proposition follows from the fact that well-annotated terms are closed under intersection. Specifically, if z_{1} and z_{2} are well-annotated terms such that |z_{1}| = |z_{2}| then we can define an annotated term z_{1} ∩ z_{2} by intersecting the corresponding annotations of z_{1} and z_{2}, and this new term will be well-annotated and such that |z_{1}| = |z_{2}| = |z_{1} ∩ z_{2}|. This follows immediately from inspection of the well-annotated conditions.

Using Proposition 4, we can define the control-flow component of cfa_{⊆}. First, recall that annotated terms used in the system may include Int. To give just the control-flow information of an annotated term, let cf(z) denote the result of replacing each annotation A appearing in z by A−{Int}. Finally, given a program e_{0} that is cfa_{⊆}-type-consistent, define that cf(cfa_{⊆})(e_{0}) is cf(z) where z is the >-minimal well-annotated term such that |z| = e_{0}. We can now define typing and control-flow aspects of cfa_{⊆} as follows:

1. Let typable(cfa_{⊆}) denote the set of type-consistent terms under cfa_{⊆}.

2. Let control-flow(cfa_{⊆}) denote the partial mapping that maps a program e_{0} into cf(cfa_{⊆}).

4.2 Standard CFA without Recursion

The cfa_{⊆} system defined in the previous subsection can reason about recursion. For example, one well-annotated version of (λ^{l}x.(x x)) (λ^{l′}x.(x x)) is

((λ^{l}x.(x:{l′} x:{l′}) : {}) : {l} (λ^{l′}x.(x:{l′} x:{l′}) : {}) : {l′}) : {}

We now define a control-flow system that is based on equality but specifically excludes programs involving recursion. In this modified system, an annotated term z is well-annotated if it satisfies the conditions given in Subsection 4.1 and in addition there is a non-reflexive ordering ≻ on labels such that

1. if λ^{l}x.z′:γ appears in z and x occurs free in z′ with annotation γ_{x}, then (∀l′ ∈ γ_{x})(l ≻ l′).

Call this system cfa_{⊆,¬Y}. A program e_{0} is cfa_{⊆,¬Y} -type-consistent if there exists an annotated term z such that e_{0} = |z| and z is well-annotated according to the above definition. Given, a type-consistent program e_{0}, we can again use > to define a unique minimal well-annotated term corresponding to e_{0}, and so using cf we can cf(cfa_{⊆,¬Y})(e_{0}) in analogy with the previous subsection. Hence, typing and control-flow aspects of cfa_{⊆,¬Y} can be defined:

1. Let typable(cfa_{⊆,¬Y}) denote the set of type-consistent terms under cfa_{⊆,¬Y}.

2. Let control-flow(cfa_{⊆,¬Y}) denote the partial mapping that maps a program e_{0} into cf(cfa_{⊆,¬Y}).

4.3 CFA via Equality

The next system we consider essentially corresponds to the analysis considered by Bondorf and Jorgensen [2]. The only differences are that we do not consider arbitrary data-constructors, and we include Int to reason about type consistency. The definition of well-annotated programs for this system is a modification of the definition in Subsection 4.1 in which subset is replaced by equality. Specifically, an annotated term z is well-annotated if:

1. if (λ^{l}x.z′):γ appears in z then l ∈ γ.

2. if (z_{1} z_{2}):γ appears in z then Int ∉ annot(z_{1}) and for all l ∈ annot(z_{1}), if λ^{l}x.z′ appears in z then:

(a) annot(z′) = γ, and

(b) if x occurs free in z′ with annotation γ_{x} then annot(z_{2}) = γ_{x}.

3. if 0:γ appears in z then γ = {Int}

4. if (Succ z′):γ appears in z then γ = annot(z′) = {Int}.

Call this system cfa_{=}. Definitions of type-consistency, minimality and also cf(cfa_{=})(e_{0}) can be given analogously to those in the previous subsections. Typing and control-flow aspects of cfa_{=} are defined by:

1. Let typable(cfa_{=}) denote the set of type-consistent terms under cfa_{=}.

2. Let control-flow(cfa_{=}) denote the partial mapping that maps a program e_{0} into cf(cfa_{=}).

4.4 CFA via Equality without Recursion

As with cfa_{⊆}, the cfa_{=} system can reason about recursion. We now define a fourth control-flow analysis system that combines cfa_{=} with the recursion restriction. In this new system, an annotated term z is well-annotated if it satisfies the conditions given in Subsection 4.1 and in addition satisfies the recursion restriction given in Subsection 4.2. Call this system cfa_{=,¬Y}. Definitions of typeconsistency, minimality and cf(cfa_{=,¬Y})(e_{0}) can be given analogously to those in the previous subsections. Typing and control-flow aspects of cfa_{=} are defined by:

1. Let typable(cfa_{=,¬Y}) denote the set of type-consistent terms under cfa_{=,¬Y}.

2. Let control-flow(cfa_{=,¬Y}) denote the partial mapping that maps a program e_{0} into cf(cfa_{=,¬Y}).

5 Types ≡ Control-Flow

We now establish a series of correspondences between the four type systems and the form control-flow systems that have been presented. In short, we prove the following equivalences:

⊢_{λ} ≡ cfa_{=,¬Y} ⊢_{λ(μ)} ≡ cfa_{=}
⊢_{λ(Ω)} ≡ cfa_{⊆,¬Y} ⊢_{λ(Ω, μ)} ≡ cfa_{⊆}

That is, the two subtype systems correspond to the control-flow systems based on ⊆; the two other type systems correspond to the control-flow systems based on =. Non-recursive type systems correspond to control-flow systems that exclude control-flow cycles, and recursive type systems correspond to control-flow systems that do not restrict control-flow cycles.

For each pair of type and control-flow system, we establish that the type and control-flow components of the systems correspond. For example, for ⊢_{λ} and cfa_{=,¬Y} we prove that (a) typable( ⊢_{λ} ) = typable(cfa_{=,¬Y}), and (b) controlflow( ⊢_{λ} ) = control-flow(cfa_{=,¬Y}). These connections are proved by showing that a “correctly annotated” term in one system can be used to reconstruct a closely related “correctly annotated” term in the other system. Specifically, for each pair of systems, we prove the following two theorems:

Theorem 5. If z_{type} is correctly typed then there exists a well-annotated term z_{cfa} such that |z_{type}| = |z_{cfa}| and cf(z_{type}) > cf(z_{cfa}).

Proof Sketch(for ⊢_{λ(Ω, μ)} and cfa_{⊆}) Suppose that ⊢_{λ(Ω, μ)} z_{type}. Unfortunately, we cannot proceed to define a well-annotated term z_{cfa} directly using the control-flow information in z_{type} because there is some slack in the definition of correctly typed terms with respect to the specification of control-flow information. In essence, the set of control-flow information associated with a term can often be enlarged using subtyping, without affecting correctness of the type annotations. Due to minor structural differences between type systems and control-flow analysis, such enlargements cannot necessarily be replayed in a control-flow analysis. Hence, we must first trim this slack. In the context of z_{type}, define a function trim on types as follows: trim(τ) is the result of replacing the control-flow component of τ with the set of all labels l ∈ cf(τ) such that if λ^{l}x.z : τ_{l} appears in z_{type}, then τ_{l} ≤ τ. Then, define that trim(z_{type}) is the annotated term such that all types τ appearing in z_{type} (and subexpressions thereof that are types) are systematically replaced by trim(τ). It is easy to verify that ⊢_{λ(Ω, μ)} trim(z_{type}) and that z_{type} > trim(z_{type}).

Now, consider systematically replacing the annotations in trim(z_{type}) as follows: an annotation τ is replaced by cf(τ) ∪ {Int} if ⟨{}, Int⟩ ≤ τ and cf(τ) otherwise. Call the resulting term z_{cfa}. Clearly |z_{cfa}| = |z_{types}| and cf(z_{type}) > cf(z_{cfa}). It remains to show that z_{cfa} is well-annotated according to the control-flow definitions. This is mostly straightforward; the most interesting case is application, and here the proof follows the following property of any annotation appearing in trim(z_{type})

if l ∈ cf(τ) and λ^{l}x.z : τ_{l} appears in trim(z_{type}), then τ_{l} ≤ τ.

This is an immediate consequence of the trim construction.

The proof for the other three cases of this theorem are modifications of this basic result. For type systems that do not include recursion, the above construction can be modified to yield a well-annotated terms that does not involve control-flow cycles. For type systems that do not involve subtyping, the type systems do not include the subtyping rule, and when translated to well-annotated terms (via the above construction), this means that the control-flow consistency conditions become equalities rather than inclusions.

Theorem 6. If z_{cfa} is well-annotated then there exists a correctly typed term z_{type} such that |z_{cfa}| = |z_{type}| and cf(z_{cfa}) = cf(z_{type}).

Proof Sketch(for ⊢_{λ(Ω, μ)} and cfa_{⊆}) Suppose that z_{cfa} is well-annotated according to cfa_{⊆}. Consider the following translation T (γ) from annotations γ appearing in z_{cfa} into types (note that T is only well defined for certain wellannotated terms z_{cfa}; we shall address this below)

T (γ) = \{ \begin{matrix}μα.α & if γ = \{\} \\ Int & if γ = \{Int\} \\ ⟨γ, T (dom(γ)) → T (ran(γ))⟩ & if γ ≠ \{\} and γ ⊆ labels \\ Ω & otherwise \end{matrix}

where dom and ran are defined by:

dom(γ) = ⋂ \{γ : \begin{matrix}λ^{l}x.z & appears in z_{cfa} such that \\ x occurs free in z with annotation γ \end{matrix} \}
ran(γ) = ⋃{annot(z) : λ^{l}x.z appears in z_{cfa}}

To explain these, consider an abstraction λ^{l}x.z appearing in z_{cfa}. Annotations on the free occurrences of x in z represent upper bounds on the arguments to which this abstraction can be “safely” applied. Hence, dom(γ), the intersection of these annotations over all l ∈ γ, is the largest set that satisfies all of these bounds, and this represents an upper bound on possible applications of a term with label γ. Similarly, ran(γ) represents a lower bound on the possible results of an application of a term with annotation γ.

The above translation is not well defined if z_{cfa} involves control-flow cycles. To deal with this situation, we modify the mapping T as follows. First, we set aside a distinct type variable α_{γ} for each annotation γ. We then modify the above definition to give a translation T γ̃ which carries the sequence of annotations γ̃ that have already been considered. The key modification is the part for arrow types: if γ ⊆ labels then T γ̃(γ) is

α_{γ}  if γ ∈ γ̃
μα_{γ}.⟨γ, T^{γ̃,γ}(dom(γ)) → T^{γ̃,γ}(ran(γ))⟩ otherwise

In other words, the recursion operator μ is used to fold infinite types into finite ones. Now define that T (τ) is T^{∅}(τ) where ∅ denotes the empty sequence. A key property of T is that if γ_{1} ⊆ γ_{2} then T (γ_{1}) ⊆ T (γ_{2}). Finally, define that z_{types} is the term that results from systematically replacing each annotation γ in z_{cfa} by T (γ). Clearly |z_{cfa}| = |z_{type}| and cf(z_{cfa}) = cf(z_{type}), and it only remains to show that z_{types} is correctly typed. This is essentially a structural induction on z_{types} (although note that contexts have to be constructed), and is fairly straightforward.

Again the proofs for the other three cases of this theorem are modifications of this basic result. For control-flow systems that exclude recursion, note that the original definition of T is sufficient since the ordering ≻ on labels means that cycles cannot appear in this definition. Hence, it is clear that the image of T consists of non-recursive types. For control-flow systems that do not involve subtyping, the control-flow consistency conditions become equalities rather than inclusions. When translated to types, such annotations correspond to type derivations that do not require subtyping (we remark that when the above construction is applied to a cfa_{=,¬Y} -well-annotated term, the resulting term can contain ⊥; by replacing such occurrences by Int, we obtain the desired result).

References

1. R. Amadio and L. Cardelli, “Subtyping Recursive types”, ACM-TOPLAS, 15(4):575-631, 1993. (Also in POPL-91, pp. 104–118).

2. A. Bondorf and J. Jorgensen, “Efficient Analysis for Realistic Off-Line Partial Evaluation”, Journal of Function Programming, 3(3), pp. 315–346, 1993.

3. N. Heintze, “Control-Flow Analysis and Type Systems”, Carnegie Mellon University technical report CMU-CS-94-227, 16pp, December 1994.

4. N. Jones, “Flow Analysis of Lambda Expressions”, Symp. on Functional Languages and Computer Architecture, pp. 66-74, 1981.

5. N. Jones, “Flow Analysis of Lazy Higher-Order Functional Programs”, in Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin (Eds.), Ellis Horwood, 1987.

6. D. Kozen, J. Palsberg, M. Schwartzbach, “Efficient Recursive Subtyping” POPL-93, pp. 419–428, 1993.

7. R. Milner, “A Theory of Type Polymorphism in Programming”, Journal of Computer System Science, 17, pp. 348–375.

8. J. Palsberg and M. Schwartzbach, “Safety Analysis versus Type Inference for Partial Types” Information Processing Letters, Vol 43, pp. 175–180, North-Holland, September 1992.

9. J. Palsberg and M. Schwartzbach, “Safety Analysis versus Type Inference” Information and Computation, to appear.

10. J. Palsberg and P. O’Keefe, “A Type System Equivalent to Flow Analysis”, POPL-95, pp. 367–378, 1995.

11. O. Shivers, “Control Flow Analysis in Scheme”, Proc. 1988 ACM Conf. on Programming Language Design and Implementation, Atlanta, pp. 164–174, 1988.

12. Y. Tang and P. Jouvelot, “Control-Flow Effects for Escape Analysis”, WSA’92, Bordeaux, France, 1992.

13. Y. Tang and P. Jouvelot, “Separate Abstract Interpretation for Control-Flow Analysis”, TACS-94, LNCS 789, pp.224-243, 1994.

14. S. Thatte, “Type Inference with Partial Types”, ICALP-88, LNCS 317, pp. 615– 629, 1988.

This article was processed using the LaTEX macro package with LLNCS style