The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...
Type abstraction and intensional type analysis are features seemingly at odds-type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several ...
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, ...
Markus Wolf
Programming languages with language constructs for analyzing types or casting from some abstract type to its concrete implementation type seem to violate abstraction principles (especially the parametricity principle that the current concrete implementation of an abstract type can be replaced by any other concrete implementation conforming to the abstract type). However, if the type system carefully guards against "unsafe" applications of these constructs and allows concrete type instantiations to hide behind dynamically generated type names, then parametricity can be recovered. This is elaborated and rigorously proved in this paper. The first two sections introduce the topic, present the motivation, and define a simple polymorphic language (complete with syntax, type system, and operational semantics) with a cast function and a dynamic type name generation operation. The following two sections explain how parametricity for the language is proved via a classic technique using logical relations. The logical relation in itself combines a step-indexed logical relation with a Kripke logical relation. The main structure of the proof is shown. Some technical details are not fully presented in the paper, but can be downloaded in the form of a technical report from the homepage of one of the authors. The previous result showed that parametricity can be regained via the introduction of fresh type names. It is, however, not immediately obvious how to systematically replace an arbitrary expression with an expression that is parametric. To achieve this, a wrapping operator is defined. In the following sections, the logical relation is extended and refined in order to reason about parametricity in a more natural way and to include iso-recursive types. Finally, the authors show one direction of a full abstraction result of an embedding of System F (with recursion) into the language of the paper; the other direction is an open problem. The article concludes with references to related work and a conclusion. The article is very well written, but the density of technical definitions is quite high, making it difficult for the reader to follow all of the details. The basic ideas and the reasons why the technical results are correct are presented in a very compelling way. I recommended this paper to anyone interested in typed functional programming languages. Online Computing Reviews Service
Become a reviewer for Computing Reviews.
Association for Computing Machinery
New York, NY, United States
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in