Computer Science Department
School of Computer Science, Carnegie Mellon University


Typed Compilation of Recursive Datatypes

Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen,
Karl Crary, Robert Harper, Perry Cheng

Demceber 2002

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

9 pages

* Department of Computer Science, Stanford University.

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by