Abstract
By “thunkifying” the arguments to function applications and “dethunkifying” variables one can translate a λ-expression e into a λ-expression e′, such that call-by-value evaluation of e′ gives the same result as call-by-name evaluation of e. By using the result of a strictness analysis, some of these thunkifications can be avoided. In this paper we present a type system for strictness analysis; present a translation algorithm which exploits the strictness proof tree; and give a combined proof of the correctness of the analysis/translation.
Supported by the DART-project funded by the Danish Research Council.
The work reported here evolved from numerous discussions with Hanne Rüs Nielson and Flemming Nielson. Also thanks to Jens Palsberg for useful feedback.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Torben Amtoft. Strictness types: An inference algorithm and an application. Technical Report PB-448, DAIMI, University of Aarhus, Denmark, 1993.
Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986.
Olivier Danvy and John Hatcliff. Thunks (continued). In M. Billaud et al., editor, Analyse statique, Bordeaux 92 (WSA '92), pages 3–11, September 1992.
Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3), 1993.
John Hughes. Why functional programming matters. Computer Journal, 32(2):98–107, 1989.
Thomas P. Jensen. Strictness analysis in logical form. In John Hughes, editor, International Conference on Functional Programming Languages and Computer Architecture, pages 352–366. Springer Verlag, LNCS 523, August 1991.
Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In International Conference on Functional Programming Languages and Computer Architecture, pages 260–272. ACM Press, September 1989.
Torben Poort Lange. The correctness of an optimized code generation. Technical Report PB-427, DAIMI, University of Aarhus, Denmark, November 1992. Also in the proceedings of PEPM '93, Copenhagen, ACM press.
Alan Mycroft. The theory of transforming call-by-need to call-by-value. In B. Robinet, editor, International Symposium on Programming, Paris, pages 269–281. Springer Verlag, LNCS 83, April 1980.
Hanne Riis Nielson and Flemming Nielson. Context information for lazy code generation. In ACM Conference on Lisp and Functional Programming, pages 251–263. ACM Press, June 1990.
Mitchell Wand. Specifying the correctness of binding-time analysis. In ACM Symposium on Principles of Programming Languages, pages 137–143. ACM Press, January 1993.
David A. Wright. A new technique for strictness analysis. In TAPSOFT 91, pages 235–258. Springer Verlag, LNCS 494, April 1991.
David A. Wright. An intensional type discipline. Australian Computer Science Communications, 14, January 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amtoft, T. (1993). Minimal thunkification. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_43
Download citation
DOI: https://doi.org/10.1007/3-540-57264-3_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57264-0
Online ISBN: 978-3-540-48027-3
eBook Packages: Springer Book Archive