Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-29T01:25:06.292Z Has data issue: false hasContentIssue false
  • English
  • Français

Work it, wrap it, fix it, fold it

Part of: JFP Research Articles

Published online by Cambridge University Press:  16 April 2014

NEIL SCULTHORPE  and
GRAHAM HUTTON
NEIL SCULTHORPE
Affiliation:
University of Kansas, USA (e-mail: [email protected])
GRAHAM HUTTON
Affiliation:
University of Nottingham, UK (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different correctness conditions. In this paper we show how these two approaches can be generalised in a uniform manner by combining their correctness conditions, extend the theory with new conditions that are both necessary and sufficient to ensure the correctness of the worker/wrapper technique, and explore the benefits that result. All the proofs have been mechanically verified using the Agda system.

Type
Articles
Information
Journal of Functional Programming , Volume 24 , Issue 1 , January 2014 , pp. 113 - 127
Copyright
Copyright © Cambridge University Press 2014 

References

Backhouse, R. (2002) Galois connections and fixed point calculus. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Backhouse, R., Crole, R. & Gibbons, J. (eds). New York, NY: Springer, pp. 89–150 Google Scholar
Bird, R. & de Moor, O. (1997) Algebra of Programming. Upper Saddle River, NJ: Prentice Hall.Google Scholar
Burstall, R. M., & Darlington, J. (1977) A transformation system for developing recursive programs. J. ACM 24 (1), 44–67.CrossRefGoogle Scholar
Farmer, A., Gill, A., Komp, E. & Sculthorpe, N. (2012) The HERMIT in the machine: A plugin for the interactive transformation of GHC core language programs. In Proceedings of the 2012 Haskell Symposium, Copenhagen, Denmark. New York, NY: ACM, pp. 1–12.Google Scholar
Gammie, P. (2011) Strict unwraps make worker/wrapper fusion totally correct. J. Funct. Program. 21 (2), 209–213.CrossRefGoogle Scholar
Gill, A. & Hutton, G. (2009) The worker/wrapper transformation. J. Funct. Program. 19 (2), 227–251.Google Scholar
Hoare, T. (1972) Proof of correctness of data representations. Acta Inform. 1 (4), 271–281.Google Scholar
Hutton, G., Jaskelioff, M., & Gill, A. (2010) Factorising folds for faster functions. J. Funct. Program. 20 (3&4), 353–373.Google Scholar
Meijer, E., Fokkinga, M. M., & Paterson, R. (1991) Functional programming with bananas, lenses, envelopes and barbed wire. In Functional Programming Languages and Computer Architecture, Hughes, J. (ed). Berlin, Germany: Springer, pp. 124–144.CrossRefGoogle Scholar
Morgan, C. & Gardiner, P. H. B. (1990) Data refinement by calculation. Acta Inform. 27 (6), 481–503.Google Scholar
Peyton Jones, S. & Launchbury, J. (1991) Unboxed values as first class citizens in a non-strict functional language. In Functional Programming Languages and Computer Architecture, Hughes, J. (ed). Berlin, Germany: Springer, pp. 636–666.Google Scholar
Scherlis, W. L. (1980) Expression Procedures and Program Derivation. PhD thesis, Stanford University, Stanford, CA.Google Scholar
Schmidt, D. A. (1986) Denotational Semantics: A Methodology for Language Development. Boston, MA: Allyn & Bacon.Google Scholar
Sculthorpe, N., Farmer, A. & Gill, A. (2013) The HERMIT in the tree: Mechanizing program transformations in the GHC core language. In Implementation and Application of Functional Languages 2012, Hinze, R. (ed), Lecture Notes in Computer Science, vol. 8241. New York, NY: Springer, pp. 86–103.CrossRefGoogle Scholar
Tullsen, M. (2002) PATH, A Program Transformation System for Haskell. PhD thesis, Yale University, Yale. CT.Google Scholar
Voigtländer, J. (2008) Asymptotic improvement of computations over free monads. In Mathematics of Program Construction, Audebaud, P. & Paulin-Mohring, C. (eds), Lecture Notes in Computer Science, vol. 5133. New York, NY: Springer, pp. 388–403.Google Scholar
Winskel, G. (1993) The Formal Semantics of Programming Languages – An Introduction. Foundation of Computing series. Cambridge, MA: MIT.Google Scholar
Supplementary material: File

SCULTHORPE and HUTTON supplementary material

Supplementary files

Download SCULTHORPE and HUTTON supplementary material(File)
File 679.2 KB
Submit a response

Discussions

No Discussions have been published for this article.