LISP and Symbolic Computation, 10(1)61-91
An Unboxed Operational Semantics for ML PolymorphismAtsushi Ohori, Research Institute for Mathematical Sciences, Kyoto University, Sakyo-ku, Kyoto 606 Japan
Tomonobu Takamizawa, Research Institute for Mathematical Sciences, Kyoto University, Sakyo-ku, Kyoto 606 Japan
|
Abstract: We present an unboxed operational semantics for an
ML-style polymorphic language. Different from the conventional
formalisms, the proposed semantics accounts for actual representations
of run-time objects of various types, and supports a refined notion of
polymorphism that allows polymorphic functions to be applied directly
to values of various different representations. In particular,
polymorphic functions can receive multi-word constants such as
floating-point numbers without requiring them to be ?boxed? (i.e.,
heap allocated.) This semantics will serve as an alternative basis for
implementing polymorphic languages. The development of the semantics
is based on the technique of the type-inference-based compilation for
polymorphic record operations [20]. We first develop a lower-level
calculus, called a polymorphic unboxed calculus, that accounts for
direct manipulation of unboxed values in a polymorphic language. This
unboxed calculus supports efficient value binding through integer
representation of variables. Different from de Bruijn indexes, our
integer representation of a variable corresponds to the actual offset
to the value in a run-time environment consisting of objects of
various sizes. Polymorphism is supported through an abstraction
mechanism over argument sizes. We then develop an algorithm that
translates ML into the polymorphic unboxed calculus by using type
information obtained through type inference. At the time of
polymorphic let binding, the necessary size abstractions are inserted
so that a polymorphic function is translated into a function that is
polymorphic not only in the type of the argument but also in its
size. The ML type system is shown to be sound with respect to the
operational semantics realized by the translation.
Keywords: operational semantics, polymorphism, type inference, unboxed objects, ML |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)