Taming Selective Strictness
| Authors: | D. Seidel and J. Voigtländer |
|---|---|
| Published: | In 4. Arbeitstagung Programmiersprachen (ATPS'09, acceptance rate 8/11) der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte" im Rahmen der GI-Jahrestagung Informatik 2009, Lübeck, Germany, Proceedings, volume 154 of Lecture Notes in Informatics, pages 2916-2930, GI, October 2009. |
| BibTeX: | SV09b.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.pdf |
| Rights: | Copyright held by the GI, see here. |
An extended version of this work appeared in Acta Informatica, see here.