Refined Typing to Localize the Impact of Forced Strictness on Free Theorems
| Authors: | D. Seidel and J. Voigtländer |
|---|---|
| Published: | Acta Informatica, volume 48(3), pages 191-211, Springer, 2011. |
| DOI: | 10.1007/s00236-011-0136-9 |
| BibTeX: | SV11a.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 overcoming this weakness in specific situations. Employing a refined type system which tracks the use of enforced strict evaluation, we rule out unnecessary restrictions that otherwise emerge. Additionally, we provide (and implement) an algorithm determining all refined types for a given term. |
| Download: | RefinedTypingToLocalizeTheImpactOfForcedStrictnessOnFreeTheorems.pdf |
| Rights: | Copyright held by Springer. The definitive version of this work is available from http://dx.doi.org/10.1007/s00236-011-0136-9. |
The implementation of the algorithm developed in this paper is accessible via a web interface here.