On the Runtime Complexity of Type-Directed Unboxing

Avoiding boxing when representing native objects is essential for the efficient compilation of any programming language. For polymorphic languages this task is difficult, but several schemes have been proposed that remove boxing on the basis of type information. Leroyʹs type-directed unboxing transformation is one of them. One of its nicest properties is that it relies only on visible types, which makes it compatible with separate compilation. However it has been noticed that it is not safe both in terms of time and space complexity -i.e. transforming a program may raise its complexity. We propose a refinement of this transformation, still relying only on visible types, and prove that it satisfies the safety condition for time complexity. The proof is an extension of the usual logical relation method, in which correctness and safety are proved simultaneously,