An Efficient Type- and Control-Flow Analysis for System F

At IFL'12, we presented a novel monovariant flow analysis for System F (with recursion) that yields both type-flow and control-flow information. [5] The type-flow information approximates the type expressions that may instantiate type variables and the control-flow information approximates the λ- and Λ-expressions that may be bound to variables. Furthermore, the two flows are mutually beneficial: control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while type flow filters the λ- and Λ-expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the variable under the type flow). Using a specification-based formulation of the type- and control-flow analysis, we proved the analysis to be sound, decidable, and computable. Unfortunately, naïvely implementing the analysis using a standard least fixed-point iteration yields an O(n13) algorithm. In this work, we give an alternative flow-graph-based formulation of the type- and control-flow analysis. We prove that the flow-graph-based formulation induces solutions satisfying the specification-based formulation and, hence, that the flow-graph-based formulation of the analysis is sound. We give a direct algorithm implementing the flow-graph-based formulation and demonstrate that it is O(n4). By distinguishing the size l of expressions in the program from the size m of types in the program and performing an amortized complexity analysis, we further demonstrate that the algorithm is O(l3 + m4).