Selective Strictness and Parametricity in Structural Operational Semantics
| Authors: | J. Voigtländer and P. Johann |
|---|---|
| Published: | Technical Report TUD-FI06-02, Technische Universität Dresden, June 2006. |
| BibTeX: | VJ06.bib |
| 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, provide means to enforce strict evaluation of subcomputations at will, and thus give the advanced programmer explicit control over the evaluation order. Such selective strictness, of course, does not remain without semantic consequences, and indeed breaks standard parametricity results. This paper develops an operational semantics for a core calculus representing all the language features emphasized above. Its main achievement is the characterization of observational equivalence with respect to this operational semantics by 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. |
| Download: | SelectiveStrictnessAndParametricityInStructuralOperationalSemantics.pdf |
A revised version of this work appeared in Theoretical Computer Science, see here.