Formally Optimal Boxing

13 years 8 months ago
Formally Optimal Boxing
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 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 eo...
Fritz Henglein, Jesper Jørgensen
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1994
Where POPL
Authors Fritz Henglein, Jesper Jørgensen
Comments (0)