Formally optimal boxing

ABSTRACT

An important implementation decision in polymorphically typed functional programming language is whether to represent data in boxed or unboxed form and when to transform them from one representation to the other. Using a language with explicit representation types and boxing/unboxing operations we axiomatize equationally the set of all explicitly boxed versions, called completions, of a given source program. In a two-stage process we give some of the equations a rewriting interpretation that captures eliminating boxing/unboxing operations without relying on a specific implementation or even semantics of the underlying language. The resulting reduction systems operate on congruence classes of completions defined by the remaining equations E, which can be understood as moving boxing/unboxing operations along data flow paths in the source program. We call a completion eopt formally optimal if every other completion for the same program (and at the same representation type) reduces to eopt under this two-stage reduction. We show that every source program has formally optimal completions, which are unique modulo E. This is accomplished by first “polarizing” the equations in E and orienting them to obtain two canonical (confluent and strongly normalizing) rewriting systems. The completions produced by Leroy's and Poulsen's algorithms are generally not formally optimal in our sense. The rewriting systems have been implemented and applied to some simple Standard ML programs. Our results show that the amount of boxing and unboxing operations is also in practice substantially reduced in comparison to Leroy's completions. This analysis is intended to be integrated into Tofte's region-based implementation of Standard ML currently underway at DIKU.

REFERENCES

• BGS82: Rodney A. Brooks , Richard P. Gabriel , Guy L. Steele, Jr., An optimizing compiler for lexically scoped LISP, Proceedings of the 1982 SIGPLAN symposium on Compiler construction, p.261-275, June 23-25, 1982, Boston, Massachusetts, United States
• Bjø92: Niko}aj Bjerner. Minimal typing derivations. DIKU Student Report, July 1992.
• BTCGS91: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• BTGS90: V. Breazu-Tannen , C. A. Gunter , A. Scedrov, Computing with coercions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.44-60, June 27-29, 1990, Nice, France [doi>10.1145/91556.91590]
• CF91: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• CG90: P.-L. Curien , G. Ghelli, Coherence of subsumption, Proceedings of the fifteenth colloquium on CAAP'90, p.132-146, May 1990, Copenhagen, Denmark
• DM82: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• Ghe90: G. Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Universita di Piss, Dipartimento di informatica, March 1990.
• Hen93: Fritz Henglein, Dynamic typing: syntax and proof theory, Selected papers of the symposium on Fourth European symposium on programming, p.197-230, June 1994, Rennes, France
• HM93: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• KKR+86: David Kranz , Norman Adams , Richard Kelsey , Jonathan Rees , Paul Hudak , James Philbin, ORBIT: an optimizing compiler for scheme, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.219-233, June 25-27, 1986, Palo Alto, California, United States
• Ler92: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• Mil78: R. Milner. A theory of type polymorphism in programming. J. Computer and System Sciences, 17:348-375, 1978.
• Pet89: John Peterson, Untagged data in tagged environments: choosing optimal representations at compile time, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.89-99, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99377]
• PJL91: Simon L. Peyton Jones , John Launchbury, Unboxed values as first class citizens in a non-strict functional language, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.636-666, June 1991, Cambridge, Massachusetts, United States
• Pou93: Eigil Poulsen. Representation analysis for efficient implementation of polymorphism. Master's thesis, DIKU, University of Copenhagen, 1993.
• Rey83: J. Reynolds. Types, abstraction and parametric polymorphism. Information Processing, pages 513-523, 1983.
• Ste77: G. Steele. Fast arithmetic in MacLisp. In Proc. 1977 MACSYMA Users' Conference, NASA Scientific and Technical Information Office, Washington, D.C., July 1977.
• TT94: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• Wad89: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• WF92: A. Wright and M. Fagan. Soft typing and global representation optimization. Manuscript, July 1992.

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

General Terms:
Languages, Theory, Verification

Keywords:
polymorphism, representation analysis, type inference