Higher-order binding-time analysis

ABSTRACT

The partial evaluation process requires a binding-time analysis. Binding-time analysis seeks to determine which parts of a program's result is determined when some part of the input is known. Domain projections provide a very general way to encode a description of which parts of a data structure are static (known), and which are dynamic (not static). For first-order functional languages Launchbury [Lau91a] has developed an abstract interpretation technique for binding-time analysis in which the basic abstract value is a projection. Unfortunately this technique does not generalise easily to higher-order languages. This paper develops such a generalisation: a projection-based abstract interpretation suitable for higher-order binding-time analysis. Launchbury [Lau91b] has shown that binding-time analysis and strictness analysis are equivalent problems at first order, and for projection-based analyses have exactly the same safety condition. We argue that the same is true at higher order, and hence our development also leads to a higher-order projection-based strictness analysis. The principal limitation of our technique is the restriction to monomorphic typing.

REFERENCES

• Abr85: Samson Abramsky, Strictness analysis and polymorphic invariance, on Programs as data objects, p.1-23, April 1986, Copenhagen, Denmark
• Abr89: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• BHA86: G. L. Burn , C. L. Hankin , S. Abramsky, The theory of strictness analysis for higher order functions, on Programs as data objects, p.42-62, April 1986, Copenhagen, Denmark
• Con90: Charles Consel, Binding time analysis for high order untyped functional languages, Proceedings of the 1990 ACM conference on LISP and functional programming, p.264-272, June 27-29, 1990, Nice, France [doi>10.1145/91556.91668]
• Dav92: Kei Davis, A Note on the Choice of Domains for Projection-Based Program Analysis, Proceedings of the 1991 Glasgow Workshop on Functional Programming, p.73-81, August 12-14, 1991
• DW90: Kei Davis , Philip Wadler, Backwards Strictness Analysis: Proved and Improved, Proceedings of the 1989 Glasgow Workshop on Functional Programming, p.12-30, August 21-23, 1989
• DW91: Davis, K. and Wadler, P. "Strictness analysis in 4D." In Functional Programming, Glasgow 1990: Proceedings of the 1990 Glasgow Workshop on Functional Programming, 13-15 August 1990, Ullapool, Scotland. Simon L. Peyton Jones et al., eds. Springer Workshops in Computing. Springer- Verlag, 1991.
• Fer92: Ferguson, A. "Concrete Data Structures" In Functional Programming: Proceedings of the 1992 Glasgow Workshop, 6-8 July 1992, A yr, Scotland. Springer Workshops in Computing. Springer- Verlag (to appear).
• HL92: Hughes, R.J:M. and Launchbury, J. Projections for polymorphic first-order strictness analysis. Math. Struct. in Comp. Science, vol. 2, pp. 301- 326, CUP, 1992.
• Hun89: Sebastian Hunt, Frontiers and open sets in abstract interpretation, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.1-13, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99371]
• Hun91: Hunt, S. "PERs Generalise Projections for Strictness Analysis." Functional Programming, Glasgow 1990: Proceedings of the 1990 Glasgow Work. shop on Functional Programming, 13-15 August 1990, Ullapool, Scotland. Simon L. Peyton Jones et al., eds. Springer Workshops in Computing. Springer-Verlag, 1991.
• HS91: Sebastian Hunt , David Sands, Binding time analysis: a new PERspective, ACM SIGPLAN Notices, v.26 n.9, p.154-165, Sept. 1991
• Kam92: Samuel Kamin, Head-strictness is not a monotonic abstract property, Information Processing Letters, v.41 n.4, p.195-198, March 18, 1992 [doi>10.1016/0020-0190(92)90179-Y]
• Lau91a: Launchbury, J. Projection Factorisations in Partial Evaluation. PhD Thesis, Glasgow University, Nov 89. Distinguished Dissertation in Computer Science, Vol 1, CUP, 1991.
• Lau91b: John Launchbury, Strictness and binding-time analyses: two for the price of one, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.80-91, June 24-28, 1991, Toronto, Ontario, Canada
• Lau91c: John Launchbury, A strongly-typed self-applicable partial evaluator, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.145-164, June 1991, Cambridge, Massachusetts, United States
• Mog89: Torben Æ. Mogensen, Binding Time Analysis for Polymorphically Typed Higher Order Languages, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.298-312, March 13-17, 1989
• WH87: Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States
• Wad90: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages