Transparent and Opaque Interpretations of Datatypes

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1998
Accession Number
ADA358589

Entities

People

  • Chris Stone
  • Karl Crary
  • Leaf Petersen
  • Perry Cheng
  • Robert Harper

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Compilers
  • Computer Science
  • Computers
  • Equations
  • Identities
  • Language
  • Software Development
  • Specifications
  • Standards

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Pulsed Power and Plasma Physics.