Fritz Henglein, Jesper J\orgensen. Formally optimal boxing. In POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Also DIKU Semantics Report D-179, Pages 213-226, New York, NY, USA, January 1994.
Download paper: (link)
Download paper:
Adobe portable document (pdf)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
An important implementation decision in polymorphically typed functional programming languages is whether to represent data in boxed or unboxed form and when to transform them from one representation to the other. Using a langnage 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 funboxing 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 actuations E, which can be understood as moving boxing/unboxing operations along data flow paths in the source progl am. We call a completion eopt formally optimal if every other completion for the same program (and at the same representation type) reduces to e opt 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
[ Dyntyp ] [ Parametricity ]
Fritz Henglein
Jesper J\orgensen
@InProceedings{hejo94,
Author = {Henglein, Fritz and J\orgensen, Jesper},
Title = {Formally optimal boxing},
BookTitle = {POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
Pages = {213--226},
Publisher = {ACM},
Address = {New York, NY, USA},
Month = {January},
Year = {1994}
}
Get EndNote Reference (.ref)