Control-flow analysis and type systems

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 control-flow. Second, Palsberg and O'Keefe establish only one pair of equivalent systems, whereas we establish four pairs of (stronger) equivalences.