Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Trends in Functional Programming

TFP 2018: Trends in Functional Programming pp 114–135Cite as

Improving Haskell

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11457))

Abstract

Lazy evaluation is a key feature of Haskell, but can make it difficult to reason about the efficiency of programs. Improvement theory addresses this problem by providing a foundation for proofs of program improvement in a call-by-need setting, and has recently been the subject of renewed interest. However, proofs of improvement are intricate and require an inequational style of reasoning that is unfamiliar to most Haskell programmers. In this article, we present the design and implementation of an inequational reasoning assistant that provides mechanical support for improvement proofs, and demonstrate its utility by verifying a range of improvement results from the literature.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Moran, A.K., Sands, D.: Improvement in a Lazy Context: An Operational Theory for Call-By-Need. Extended version of [40] (1999)

    Google Scholar 

  2. Hackett, J., Hutton, G.: Worker/wrapper/makes it/faster. In: ICFP (2014)

    Google Scholar 

  3. Schmidt-Schauß, M., Sabel, D.: Improvements in a functional core language with call-by-need operational semantics. In: PPDP (2015)

    Google Scholar 

  4. Hackett, J., Hutton, G.: Parametric polymorphism and operational improvement. University of Nottingham (2017, in preparation)

    Google Scholar 

  5. Harper, R.: The Structure and Efficiency of Computer Programs. Carnegie Mellon University (2014)

    Google Scholar 

  6. Farmer, A.: Hermit: Mechanized Reasoning During Compilation in the Glasgow Haskell Compiler. Ph.D. thesis, University of Kansas (2015)

    Google Scholar 

  7. Sculthorpe, N., Farmer, A., Gill, A.: The HERMIT in the tree: mechanizing program transformations in the GHC core language. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 86–103. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41582-1_6

    Chapter  Google Scholar 

  8. Farmer, A., Höner zu Siederdissen, C., Gill, A.: The Hermit in the stream. In: PEMP (2014)

    Google Scholar 

  9. Farmer, A., Sculthorpe, N., Gill, A.: Reasoning with the Hermit: tool support for equational reasoning on GHC core programs. In: Haskell Symposium (2015)

    Google Scholar 

  10. Adams, M.D., Farmer, A., Magalhães, J.P.: Optimizing SYB Is easy! In: PEPM (2014)

    Google Scholar 

  11. Adams, M.D., Farmer, A., Magalhães, J.P.: Optimizing SYB traversals is easy!. Sci. Comput. Program. 112, 170–193 (2015)

    Article  Google Scholar 

  12. Farmer, A., Gill, A., Komp, E., Sculthorpe, N.: The Hermit in the machine: a plugin for the interactive transformation of GHC core language programs. In: Haskell Symposium (2012)

    Google Scholar 

  13. Handley, M.A.T.: GitHub Repository for the University of Nottingham Improvement Engine (Unie) (2017). https://github.com/mathandley/Unie

  14. Wadler, P.: The Concatenate Vanishes. University of Glasgow (1987)

    Google Scholar 

  15. Sestoft, P.: Deriving a lazy abstract machine. JFP 7(3), 231–264 (1997)

    MathSciNet  MATH  Google Scholar 

  16. Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995)

    Google Scholar 

  17. Sculthorpe, N., Frisby, N., Gill, A.: The Kansas university rewrite engine. JFP 24, 434–473 (2014)

    Google Scholar 

  18. Lämmel, R., Visser, E., Visser, J.: The Essence of Strategic Programming (2002)

    Google Scholar 

  19. Gibbons, J.: Datatype-generic programming. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol. 4719, pp. 1–71. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76786-2_1

    Chapter  Google Scholar 

  20. Gill, A., Hutton, G.: The worker/wrapper transformation. JFP 19(2), 227–251 (2009)

    MATH  Google Scholar 

  21. Sculthorpe, N., Hutton, G.: Work it, wrap it, fix it, fold it. JFP 24(1), 113–127 (2014)

    MathSciNet  MATH  Google Scholar 

  22. Tullsen, M.A.: Path, A Program Transformation System for Haskell. Ph.D. thesis. Yale University (2002)

    Google Scholar 

  23. Guttmann, W., Partsch, H., Schulte, W., Vullinghs, T.: Tool support for the interactive derivation of formally correct functional programs. J. Univers. Comput. Sci. 9, 173 (2003)

    Google Scholar 

  24. Thompson, S., Li, H.: Refactoring tools for functional languages. JFP 23(3), 293–350 (2013)

    MathSciNet  MATH  Google Scholar 

  25. Li, H., Reinke, C., Thompson, S.: Tool support for refactoring functional programs. In: Haskell Workshop (2003)

    Google Scholar 

  26. Gill, A.: Introducing the Haskell equational reasoning assistant. In: Haskell Workshop (2006)

    Google Scholar 

  27. Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. JFP 19(5), 545–579 (2009)

    MathSciNet  MATH  Google Scholar 

  28. Bornat, R., Sufrin, B.: Jape: a calculator for animating proof-on-paper. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 412–415. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63104-6_41

    Chapter  Google Scholar 

  29. Bornat, R., Sufrin, B.: Animating formal proof at the surface: the jape proof calculator. Comput. J. 42(3), 177–192 (1999)

    Article  Google Scholar 

  30. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-662-07964-5

    Book  MATH  Google Scholar 

  31. Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Chalmers University of Technology (2007)

    Google Scholar 

  32. Wadler, P.: Strictness analysis aids time analysis. In: POPL (1988)

    Google Scholar 

  33. Bjerner, B., Holmström, S.: A composition approach to time analysis of first order lazy functional programs. In: FPCA (1989)

    Google Scholar 

  34. Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  35. Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: POPL (2008)

    Article  MathSciNet  Google Scholar 

  36. Brady, E., Hammond, K.: A dependently typed framework for static analysis of program execution costs. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol. 4015, pp. 74–90. Springer, Heidelberg (2006). https://doi.org/10.1007/11964681_5

    Chapter  MATH  Google Scholar 

  37. Çiçek, E., Barthe, G., Gaboardi, M., Garg, D., Hoffmann, J.: Relational cost analysis. In: POPL (2017)

    Google Scholar 

  38. Sansom, P.M., Peyton Jones, S.L.: Formally based profiling for higher-order functional languages. TOPLAS (1997)

    Google Scholar 

  39. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell Programs. In: ICFP (2011)

    Google Scholar 

  40. Moran, A.K., Sands, D.: Improvement in a lazy context: an operational theory for call-by-need. In: POPL (1999)

    Google Scholar 

Download references

Acknowledgements

We’d like to thank Jennifer Hackett and Neil Sculthorpe for many useful discussions, and the anonymous referees for their useful suggestions. This work was funded by EPSRC grant EP/P00587X/1, Mind the Gap: Unified Reasoning About Program Correctness and Efficiency.

Author information

Authors and Affiliations

  1. School of Computer Science, University of Nottingham, Nottingham, UK

    Martin A. T. Handley & Graham Hutton

Authors
  1. Martin A. T. Handley
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Graham Hutton
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Martin A. T. Handley or Graham Hutton .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Michał Pałka

  2. Chalmers University of Technology, Gothenburg, Sweden

    Magnus Myreen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Handley, M.A.T., Hutton, G. (2019). Improving Haskell. In: Pałka, M., Myreen, M. (eds) Trends in Functional Programming. TFP 2018. Lecture Notes in Computer Science(), vol 11457. Springer, Cham. https://doi.org/10.1007/978-3-030-18506-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-18506-0_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-18505-3

  • Online ISBN: 978-3-030-18506-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation