Control-Flow Analysis and Type Systems

                          Nevin Heintze
  
                   School of Computer Science
                   Carnegie Mellon University
                       5000 Forbes Ave
                    Pittsburgh, PA 15213, USA

                      Phone: (412) 268-6739
                       Fax: (412) 268-5576
                         nch@cs.cmu.edu
     
                          April 1995


                           ABSTRACT

Type and control-flow systems serve different purposes, but they also
have a number of common features.  Their exact relationship has been
an open question.  In particular, two 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 that of some known type system?
   
2. Can type systems be extended to compute control-flow information,
and if so, does the control-flow information obtained correspond that
of some known control-flow system?

Recent work by Palsberg and O'Keefe addresses the first questions by
showing that the Amadio/Cardelli type system with subtyping and
recursive types is equivalent to Palsberg and Schwartzbach's safety
analysis (a control-flow system extended to reason about types) in the
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.  In addition, we provide three new results that
address the first question for type systems other than the
Amadio/Cardelli system.  Specifically, we take four type systems from
the literature (involving simple types, subtypes and recursion) and
systematically enrich them to reason about control-flow information.
Similarly, we take four control-flow systems and enrich them to reason
about type consistency.  Our main result is a series of equivalences
between these enriched type and control-flow systems: for each type
system, there is a control-flow system with equivalent reasoning
power, and vice-versa.  Hence type systems and control-flow analysis
can be viewed as complementary approaches for addressing questions of
type consistency and control-flow.

Keywords: type inference, subtypes, recursive types, control-flow
analysis, safety analysis.