Computer Science Department
School of Computer Science, Carnegie Mellon University
Karl Crary, Robert Harper, Perry Cheng,
Also appears as Fox Memorandum CMU-CS-FOX-98-04
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.