Typed compilation of recursive datatypes

13 years 11 months ago
Typed compilation of recursive datatypes
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 conatypes 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. Categories and Subject Descriptors D.3.3 [Programming Languages]...
Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, K
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where TLDI
Authors Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Comments (0)