The Impact of seq on Free Theorems-Based Program Transformations Export

@article{johvoi06, 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.}, address = {Amsterdam, The Netherlands}, author = {Johann, Patricia and Voigtl\"{a}nder, Janis}, citeulike-article-id = {1410367}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1227251}, citeulike-linkout-1 = {http://wwwtcs.inf.tu-dresden.de/~voigt/seqFinal.pdf}, issn = {0169-2968}, journal = {Fundam. Inf.}, keywords = {denotational-semantics, free-theorems, functional-programming, haskell, laziness, lazy-evaluation, logical-relations, parametricity, polymorphism, program-transformation, rank-2, selective-strictness, seq, shortcut-deforestation, strict-evaluation, types}, number = {1-2}, pages = {63--102}, posted-at = {2007-06-25 11:10:15}, priority = {0}, publisher = {IOS Press}, title = {The Impact of seq on Free Theorems-Based Program Transformations}, url = {http://portal.acm.org/citation.cfm?id=1227251}, volume = {69}, year = {2006} }

TY - JOUR ID - johvoi06 L3 - citeulike-article-id:1410367 N2 - 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. IS - 1-2 JF - Fundam. Inf. SN - 0169-2968 AD - Amsterdam, The Netherlands EP - 102 TI - The Impact of seq on Free Theorems-Based Program Transformations PB - IOS Press VL - 69 SP - 63 KW - denotational-semantics KW - free-theorems KW - functional-programming KW - haskell KW - laziness KW - lazy-evaluation KW - logical-relations KW - parametricity KW - polymorphism KW - program-transformation KW - rank-2 KW - selective-strictness KW - seq KW - shortcut-deforestation KW - strict-evaluation KW - types AU - Johann, Patricia AU - Voigtländer, Janis PY - 2006/// UR - http://portal.acm.org/citation.cfm?id=1227251 ER -