|
CMU-CS-02-200
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-02-200
Typed Compilation of Recursive Datatypes
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen,
Karl Crary, Robert Harper, Perry Cheng
Demceber 2002
CMU-CS-02-200.ps
CMU-CS-02-200.pdf
Keywords: Typed compilation, Standard ML. recursive types, coercions
Standard ML employs an opaque (or generative) semantics of datatypes,
in which every datatype declaration produces a new type that is
different from any other type, including other identically defined
datatypes. A natural way of accounting for this is to consider
datatypes to be abstract. When this interpretation is applied to
type-preserving compilation, however, it has the unfortunate
consequence that datatype constructors cannot be inlined,
substantially increasing the run-time cost of constructor invocation
compared to a traditional compiler. In this paper we examine two
approaches to eliminating function call overhead from datatype
constructors. First, we consider a transparent interpretation of
datatypes that does away with generativity, altering the semantics of
SML; and second, we propose an interpretation of datatype constructors
as coercions, which have no run-time effect or cost and faithfully
implement SML semantics.
24 pages
|