The Impact of seq on Free Theorems-Based Program Transformations

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 GirardReynolds 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 "inequati...

• Type: Journal
• Year: 2006
• Where: FUIN
• Authors: Patricia Johann, Janis Voigtländer
• Keywords: Free Theorems, FUIN 2006, Pure Functional Programs, So-called Free Theorems