Top

Published in:

2019 | OriginalPaper | Chapter

Improving Haskell

Authors : Martin A. T. Handley, Graham Hutton

Published in: Trends in Functional Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Saint: An API-Generic Type-Safe Interpreter

next chapter High-Performance Defunctionalisation in Futhark

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

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

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

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

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

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

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_6CrossRef

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

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

10.

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

11.

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

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)

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)

15.

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

16.

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

17.

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

18.

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

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_1CrossRef

20.

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

21.

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

22.

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

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)

24.

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

25.

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

26.

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

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)MathSciNetMATH

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_41CrossRef

29.

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

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-5CrossRefMATH

31.

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

32.

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

33.

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

34.

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

35.

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

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_5CrossRefMATH

37.

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

38.

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

39.

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

40.

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

Title: Improving Haskell
Authors: Martin A. T. Handley
Graham Hutton
Publisher: Springer International Publishing
Book: Trends in Functional Programming
Print ISBN: 978-3-030-18505-3

Electronic ISBN: 978-3-030-18506-0

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-18506-0_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner