Free Theorems In The Presence Of seq
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Patricia Johann Ph.D, Professor (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
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, the standard parametricity theorem fails for nonstrict languages supporting a polymorphic strict evaluation primitive like Haskell’s seq. Contrary to the folklore surrounding seq and parametricity, we show that not even quantifying only over strict and bottom-reflecting relations in the - clause of the underlying logical relation — and thus restricting the choice of functions with which such relations are instantiated to obtain free theorems to strict and total ones — is sufficient to recover from this failure. By addressing the subtle issues that arise when propagating up the type hierarchy restrictions imposed on a logical relation in order to accommodate the strictness primitive, we provide a parametricity theorem for the subset of Haskell corresponding to a Girard-Reynolds-style calculus with fixpoints, algebraic datatypes, and seq. A crucial ingredient of our approach is the use of an asymmetric logical relation, which leads to “inequational” versions of free theorems enriched by preconditions guaranteeing their validity in the described setting. Besides the potential to obtain corresponding preconditions for standard equational free theorems by combining some new inequational ones, the latter also have value in their own right, as is exemplified with a careful analysis of seq’s impact on familiar program transformations.
Free Theorems In The Presence Of seq
PDF (Portable Document Format)
3575 KB
Created on 9/28/2021
Views: 725
Additional Information
- Publication
- Johann, P. and Voigtlander, J. (2004). Free Theorems in the Presence of seq. Proceedings, Principles of Programming Languages 2004 (POPL '04), pp. 99-110. January 14–16, 2004, Venice, Italy. NC Docks permission to re-print granted by author(s). Publisher version of record available at: http://doi.acm.org/10.1145/964001.964010
- Language: English
- Date: 2004
- Keywords
- Controlling strict evaluation, correctlless proofs, de-notational semantics, Haskell, logical relations, parrunetricity, short cut fusion