Standard ML employs an opaque (or "generative") interpretation of datatype specifications, in which every datatype specification provides a new, abstract type that is different from any other type, including other identically specified datatypes. An alternative interpretation is the transparent one, in which a datatype specification exposes the underlying recursive type implementation of the datatype.

It is commonly believed that the transparent interpretation is strictly more permissive than the opaque interpretation; that all programs typable under the opaque discipline are also typable under the transparent discipline. The purpose of this note is to illustrate that this common belief is incorrect (in the usual equational theory for types), and to discuss some of the implications of that fact.

7 pages

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

This page maintained by reports@cs.cmu.edu