Extending sized type with collection analysis

ABSTRACT

Many program optimizations and analyses, such as array-bounds checking, termination analysis, depend on knowing the size of a function's input and output. However, size information can be difficult to compute. Firstly, accurate size computation requires detecting a size relation between different inputs of a function. Secondly, size information may also be contained inside a collection (data structure with multiple elements). In this paper, we introduce some techniques to derive universal and existential size properties over collections of elements of recursive data structures. We shall show how a mixed constraint system could support the enhanced size type, and highlight examples where collection analysis are useful.

REFERENCES

• 1: Wei-Ngan Chin , Siau-Cheng Khoo, Calculating Sized Types, Higher-Order and Symbolic Computation, v.14 n.2-3, p.261-300, September 2001
• 2: Wei-Ngan Chin , Siau-Cheng Khoo, Calculating sized types, Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.62-72, January 22-23, 2000, Boston, Massachusetts, United States
• 3: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 4: Dirk Dussart , Fritz Henglein , Christian Mossin, Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time, Proceedings of the Second International Symposium on Static Analysis, p.118-135, September 25-27, 1995
• 5: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 6: Kevin Glynn , Peter J. Stuckey , Martin Sulzmann , Harald Søndergaard, Boolean Constraints for Binding-Time Analysis, Proceedings of the Second Symposium on Programs as Data Objects, p.39-62, May 21-23, 2001
• 7: Jörgen Gustavsson , Josef Svenningsson, Constraint Abstractions, Proceedings of the Second Symposium on Programs as Data Objects, p.63-83, May 21-23, 2001
• 8: Nicolas Halbwachs, About synchronous programming and abstract interpretation, Science of Computer Programming, v.31 n.1, p.75-89, May 1998 [doi>10.1016/S0167-6423(96)00041-X ]
• 9: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487 ]
• 10: L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras: Part I. North-Holland, 1971.
• 11: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 12: Naoki Kobayashi, Type-based useless variable elimination, Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.84-93, January 22-23, 2000, Boston, Massachusetts, United States
• 13: Daniel Le Métayer, Proving properties of programs defined over recursive data structures, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.88-99, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215567]
• 14: S. Nishimura. Parametric polymorphic type inference in constraint form. In Second JSSST Workshop on Programming and Programming Languages, pages 38--49, March 2000.
• 15: Martin Odersky , Martin Sulzmann , Martin Wehr, Type inference with constrained types, Theory and Practice of Object Systems, v.5 n.1, p.35-55, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4 ]
• 16: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 17: David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224168]
• 18: Keith Wansbrough , Simon Peyton Jones, Once upon a polymorphic type, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-28, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292545]
• 19: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 20: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Reliability, Theory

Keywords:
collection analysis, fix-point, mixed constraints, polymorphism, sized type