Affiliations: Department of Computer Science, Rutgers University,
Camden, NJ 08102 USA. E-mail: [email protected] | Department of Computer Science, Dresden University of
Technology, 01062 Dresden, Germany. E-mail: [email protected]
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. Unfortunately, standard
parametricity results – including so-called free theorems – fail
for nonstrict languages supporting a polymorphic strict evaluation primitive
such as Haskell's seq. A folk theorem maintains that such results hold for a
subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints
and algebraic datatypes even when seq is present provided the relations which
appear in their derivations are required to be bottom-reflecting and
admissible. In this paper we show that this folklore is incorrect, but that
parametricity results can be recovered in the presence of seq by restricting
attention to left-closed, total, and admissible relations instead. The key
novelty of our approach is the asymmetry introduced by left-closedness, which
leads to "inequational" versions of standard parametricity results together
with preconditions guaranteeing their validity even when seq is present. We use
these results to derive criteria ensuring that both equational and inequational
versions of short cut fusion and related program transformations based on free
theorems hold in the presence of seq
Keywords: Haskell, control primitives, correctness proofs, denotational semantics, functional programming languages, logical relations, mixing strict and nonstrict evaluation, parametricity, polymorphism, program transformations, rank-2 types, short cut fusion, theorems for free
