| Abstract: |
Parametric polymorphism constrains the behavior of pure
functional programs in a way that allows the derivation of
interesting theorems about them solely from their types, i.e.,
virtually for free. The formal background of such "free theorems"
is well developed for extensions of the Girard-Reynolds polymorphic
lambda calculus by algebraic datatypes and general
recursion, provided the resulting calculus is endowed with either
a purely strict or a purely nonstrict semantics. But modern
functional languages like Clean and Haskell, while using nonstrict
evaluation by default, also provide means to enforce strict
evaluation of subcomputations at will. The resulting selective
strictness gives the advanced programmer explicit control over
evaluation order, but is not without semantic consequences: it breaks
standard parametricity results. This paper develops an operational
semantics for a core calculus supporting all the language features
emphasized above. Its main achievement is the characterization of
observational approximation with respect to this operational semantics
via a carefully constructed logical relation. This establishes the
formal basis for new parametricity results, as illustrated by several
example applications, including the first complete correctness proof
for short cut fusion in the presence of selective strictness. The
focus on observational approximation, rather than equivalence, allows
a finer-grained analysis of computational behavior in the presence of
selective strictness than would be possible with observational
equivalence alone.
|