Equality-based flow analysis versus recursive types

ABSTRACT

Equality-based control-flow analysis has been studied by Henglein, Bondorf and Jørgensen, DeFouw, Grove, and Chambers, and others. It is faster than the subset-based-0-CFA, but also more approximate. Heintze asserted in 1995 that a program can be safety checked with an equality-based control-flow analysis if and only if it can be typed with recursive types. In this article we falsify Heintze's assertion, and we present a type system equivalent to equality-based control-flow analysis. The new type system contains both recursive types and an unusual notion of subtyping. We have s ≤ t if s and t unfold to the same regular tree, and we have ⊥≤t≤⊤ where t is a function type. In particular, there is no nontrivial subtyping between function types.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 2: J. Michael Ashley, A practical and flexible flow analysis for higher-order languages, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-194, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237773]
• 3: BONDORF, t. AND JORGENSEN, J. 1993. Efficient analyses for realistic off-line partial evaluation. J. of Func. Program. 3, 3, 315-346.
• 4: Kim Bruce , Luca Cardelli , Giuseppe Castagna , Gary T. Leavens , Benjamin Pierce, On binary methods, Theory and Practice of Object Systems, v.1 n.3, p.221-242, Fall 1995
• 5: Greg DeFouw , David Grove , Craig Chambers, Fast interprocedural class analysis, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.222-236, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268965]
• 6: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 7: Nevin Heintze, Control-Flow Analysis and Type Systems, Proceedings of the Second International Symposium on Static Analysis, p.189-206, September 25-27, 1995
• 8: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 9: Fritz Henglein, Dynamic typing, Symposium proceedings on 4th European symposium on programming, p.233-253, January 1992, Rennes, France
• 10: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 11: Jens Palsberg, Closure analysis in constraint form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.47-62, Jan. 1995 [doi>10.1145/200994.201001]
• 12: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• 13: Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268963]
• 14: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 15: Marc Shapiro , Susan Horwitz, Fast and accurate flow-insensitive points-to analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 15-17, 1997, Paris, France [doi>10.1145/263699.263703]
• 16: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 17: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages, Theory

Keywords:
flow analysis, type systems