Taming Selective Strictness

Authors: D. Seidel and J. Voigtländer
Published: Technical Report TUD-FI09-06, Technische Universität Dresden, June 2009.
BibTeX: SV09c.bib
Abstract: Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for restrengthening them. By a refined type system which tracks the use of strict evaluation, we rule out unnecessary restrictions that otherwise emerge from the general suspicion that strict evaluation may be used at any point. Additionally, we provide an implemented algorithm determining all refined types for a given term.
Download: TamingSelectiveStrictness_TR.pdf

A revised version of this work appeared in Acta Informatica, see here.