research-article

Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs

Authors:

Neil Sculthorpe,

Andy GillAuthors Info & Claims

Haskell '15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell

Pages 23 - 34

https://doi.org/10.1145/2804302.2804303

Published: 30 August 2015 Publication History

Abstract

A benefit of pure functional programming is that it encourages equational reasoning. However, the Haskell language has lacked direct tool support for such reasoning. Consequently, reasoning about Haskell programs is either performed manually, or in another language that does provide tool support (e.g. Agda or Coq). HERMIT is a Haskell-specific toolkit designed to support equational reasoning and user-guided program transformation, and to do so as part of the GHC compilation pipeline. This paper describes HERMIT's recently developed support for equational reasoning, and presents two case studies of HERMIT usage: checking that type-class laws hold for specific instance declarations, and mechanising textbook equational reasoning.

References

[1]

M. D. Adams, A. Farmer, and J. P. Magalh˜aes. Optimizing SYB is easy! In Workshop on Partial Evaluation and Program Manipulation, pages 71–82. ACM, 2014.

Digital Library

[2]

R. Bird. Pearls of Functional Algorithm Design. Cambridge University Press, 2010.

[3]

T. Braibant and D. Pous. Tactics for reasoning modulo AC in Coq. In International Conference on Certified Programs and Proofs, volume 7086 of LNCS, pages 167–182. Springer, 2011.

Digital Library

[4]

J. Breitner, R. A. Eisenberg, S. Peyton Jones, and S. Weirich. Safe zero-cost coercions for Haskell. In International Conference on Functional Programming, pages 189–202. ACM, 2014.

Digital Library

[5]

R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, 1977.

Digital Library

[6]

K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In International Conference on Functional Programming, pages 268–279. ACM, 2000.

Digital Library

[7]

K. Claessen, M. Johansson, D. Rosén, and N. Smallbone. Automating inductive proofs using theory exploration. In International Conference on Automated Deduction, volume 7898 of LNCS, pages 392–406. Springer, 2013.

Digital Library

[8]

N. A. Danielsson and P. Jansson. Chasing bottoms: A case study in program verification in the presence of partial and infinite values. In International Conference on Mathematics of Program Construction, volume 3125 of LNCS, pages 85–109. Springer, 2004.

[9]

A. L. de M. Santos. Compilation by Transformation in Non-Strict Functional Languages. PhD thesis, University of Glasgow, 1995.

[10]

N. Dershowitz, J. Hsiang, N. A. Josephson, and D. A. Plaisted. Associative-commutative rewriting. In International Joint Conference on Artificial Intelligence, volume 2, pages 940–944. Morgan Kaufmann, 1983.

Digital Library

[11]

A. Farmer. HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler. PhD thesis, University of Kansas, 2015.

[12]

A. Farmer, A. Gill, E. Komp, and N. Sculthorpe. The HERMIT in the machine: A plugin for the interactive transformation of GHC core language programs. In Haskell Symposium, pages 1–12. ACM, 2012.

Digital Library

[13]

A. Farmer, C. Höner zu Siederdissen, and A. Gill. The HERMIT in the stream: Fusing Stream Fusion’s concatMap. In Workshop on Partial Evaluation and Program Manipulation, pages 97–108. ACM, 2014.

Digital Library

[14]

A. Farmer, A. Gill, E. Komp, and N. Sculthorpe. http://hackage. haskell.org/package/hermit, 2015.

[15]

A. Farmer, N. Sculthorpe, and A. Gill. Hermit case studies: Proving Type-Class Laws & Making a Century, 2015. URL http://www. ittc.ku.edu/csdl/fpg/HERMIT/case-studies-2015/.

[16]

GHC Team. GHC User’s Guide, Version 7.8.4, 2014. URL http: //downloads.haskell.org/~ghc/7.8.4/docs/html.

[17]

J. Gibbons and G. Hutton. Proof methods for corecursive programs. Fundamenta Informaticae, 66(4):353–366, 2005.

Digital Library

[18]

A. Gill. Introducing the Haskell equational reasoning assistant. In Haskell Workshop, pages 108–109. ACM, 2006.

Digital Library

[19]

A. Gill and G. Hutton. The worker/wrapper transformation. Journal of Functional Programming, 19(2):227–251, 2009.

Digital Library

[20]

J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris Diderot, 1972.

[21]

W. Guttmann, H. Partsch, W. Schulte, and T. Vullinghs. Tool support for the interactive derivation of formally correct functional programs. Journal of Universal Computer Science, 9(2):173–188, 2003.

[22]

J. Jeuring, P. Jansson, and C. Amaral. Testing type class laws. In Haskell Symposium, pages 49–60. ACM, 2012.

Digital Library

[23]

H. Kirchner and P.-E. Moreau. Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories. Journal of Functional Programming, 11(2):207–251, 2001.

Digital Library

[24]

H. Li, S. Thompson, and C. Reinke. The Haskell refactorer, HaRe, and its API. In Workshop on Language Descriptions, Tools, and Applications, volume 141 of ENTCS, pages 29–34. Elsevier, 2005.

Digital Library

[25]

E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Conference on Functional Programming Languages and Computer Architecture, volume 523 of LNCS, pages 124–144. Springer, 1991.

Digital Library

[26]

S.-C. Mu, H.-S. Ko, and P. Jansson. Algebra of programming in Agda: Dependent types for relational program derivation. Journal of Functional Programming, 19(5):545–579, 2009.

Digital Library

[27]

S. Peyton Jones, A. Tolmach, and T. Hoare. Playing by the rules: Rewriting as a practical optimisation technique in GHC. In Haskell Workshop, pages 203–233. ACM, 2001.

[28]

J. S. Reich, M. Naylor, and C. Runciman. Advances in lazy smallcheck. In International Symposium on Implementation and Application of Functional Languages, volume 8241 of LNCS, pages 53–70. Springer, 2013.

[29]

J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, volume 19 of LNCS, pages 408–423. Springer, 1974.

Digital Library

[30]

D. Rosén. Proving equational Haskell properties using automated theorem provers. Master’s thesis, University of Gothenburg, 2012.

[31]

C. Runciman, M. Naylor, and F. Lindblad. Smallcheck and Lazy Smallcheck: Automatic exhaustive testing for small values. In Haskell Symposium, pages 37–48. ACM, 2008.

Digital Library

[32]

N. Sculthorpe and G. Hutton. Work it, wrap it, fix it, fold it. Journal of Functional Programming, 24(1):113–127, 2014.

[33]

N. Sculthorpe, A. Farmer, and A. Gill. The HERMIT in the tree: Mechanizing program transformations in the GHC core language. In International Symposium on Implementation and Application of Functional Languages, volume 8241 of LNCS, pages 86–103. Springer, 2013.

[34]

N. Sculthorpe, N. Frisby, and A. Gill. The Kansas University Rewrite Engine: A Haskell-embedded strategic programming language with custom closed universes. Journal of Functional Programming, 24(4): 434–473, 2014.

[35]

T. Sheard and S. Peyton Jones. Template metaprogramming for Haskell. In Haskell Workshop, pages 1–16. ACM, 2002.

Digital Library

[36]

W. Sonnex, S. Drossopoulou, and S. Eisenbach. Zeno: An automated prover for properties of recursive data structures. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of LNCS, pages 407–421. Springer, 2012.

Digital Library

[37]

M. Sulzmann, M. M. T. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. In Workshop on Types in Language Design and Implementation, pages 53–66. ACM, 2007.

Digital Library

[38]

J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. Program calculation in Coq. In Algebraic Methodology and Software Technology, volume 6486 of LNCS, pages 163–179. Springer, 2011.

Digital Library

[39]

S. Thompson and H. Li. Refactoring tools for functional languages. Journal of Functional Programming, 23(3):293–350, 2013.

[40]

M. Tullsen. PATH, A Program Transformation System for Haskell. PhD thesis, Yale University, 2002.

Digital Library

[41]

N. Vazou, E. L. Seidel, and R. Jhala. LiquidHaskell: Experience with refinement types in the real world. In Haskell Symposium, pages 39– 51. ACM, 2014.

Digital Library

[42]

N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton Jones. Refinement types for Haskell. In International Conference on Functional Programming, pages 269–282. ACM, 2014.

Digital Library

[43]

D. Vytiniotis and S. Peyton Jones. Evidence normalization in System FC. In International Conference on Rewriting Techniques and Applications, pages 20–38. Schloss Dagstuhl, 2013.

[44]

D. Vytiniotis, S. Peyton Jones, K. Claessen, and D. Rosén. HALO: Haskell to logic through denotational semantics. In Symposium on Principles of Programming Languages, pages 431–442. ACM, 2013.

Digital Library

[45]

P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Symposium on Principles of Programming Languages, pages 60–76. ACM, 1989.

Digital Library

Cited By

Christiansen JDylus SBunkenburg NEisenberg R(2019)Verifying effectful Haskell programs in CoqProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342592(125-138)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342592
Handley MHutton G(2019)Improving HaskellZivilgesellschaft und Wohlfahrtsstaat im Wandel10.1007/978-3-030-18506-0_6(114-135)Online publication date: 24-Apr-2019
https://doi.org/10.1007/978-3-030-18506-0_6
Vazou NBreitner JKunkel RVan Horn DHutton G(2018)Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)ACM SIGPLAN Notices10.1145/3299711.324275653:7(132-144)Online publication date: 17-Sep-2018
https://dl.acm.org/doi/10.1145/3299711.3242756
Show More Cited By

Index Terms

Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs
Haskell '15

A benefit of pure functional programming is that it encourages equational reasoning. However, the Haskell language has lacked direct tool support for such reasoning. Consequently, reasoning about Haskell programs is either performed manually, or in ...
The HERMIT in the machine: a plugin for the interactive transformation of GHC core language programs
Haskell '12: Proceedings of the 2012 Haskell Symposium

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks. This paper introduces a programmatic and compiler-...
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
Haskell 2018: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Haskell '15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell

August 2015

212 pages

ISBN:9781450338080

DOI:10.1145/2804302

Program Chair:
Ben Lippmeier

ACM SIGPLAN Notices Volume 50, Issue 12
Haskell '15
December 2015
212 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2887747
Editor:
Matthew Fluet
Rochester Institute of Technology
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 August 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ICFP'15

Sponsor:

SIGPLAN

ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming

September 3 - 4, 2015

BC, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
211
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Christiansen JDylus SBunkenburg NEisenberg R(2019)Verifying effectful Haskell programs in CoqProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342592(125-138)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342592
Handley MHutton G(2019)Improving HaskellZivilgesellschaft und Wohlfahrtsstaat im Wandel10.1007/978-3-030-18506-0_6(114-135)Online publication date: 24-Apr-2019
https://doi.org/10.1007/978-3-030-18506-0_6
Vazou NBreitner JKunkel RVan Horn DHutton G(2018)Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)ACM SIGPLAN Notices10.1145/3299711.324275653:7(132-144)Online publication date: 17-Sep-2018
https://dl.acm.org/doi/10.1145/3299711.3242756
Vazou NBreitner JKunkel RVan Horn DHutton GWu N(2018)Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell10.1145/3242744.3242756(132-144)Online publication date: 17-Sep-2018
https://dl.acm.org/doi/10.1145/3242744.3242756
Grebe MYoung DGill A(2017)Rewriting a shallow DSL using a GHC compiler extensionACM SIGPLAN Notices10.1145/3170492.313604852:12(246-258)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3170492.3136048
Grebe MYoung DGill AFlatt MErdweg S(2017)Rewriting a shallow DSL using a GHC compiler extensionProceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3136040.3136048(246-258)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3136040.3136048
Kolesar JPiskac RHallahan W(2022)Checking equivalence in a non-strict languageProceedings of the ACM on Programming Languages10.1145/35633406:OOPSLA2(1469-1496)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563340
Liu YParker JRedmond PKuper LHicks MVazou N(2020)Verifying replicated data types with typeclass refinements in Liquid HaskellProceedings of the ACM on Programming Languages10.1145/34282844:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428284
Grebe MGill A(2019)Threading the Arduino with HaskellMicrobial Metabolic Engineering10.1007/978-3-030-14805-8_8(135-154)Online publication date: 21-Feb-2019
https://doi.org/10.1007/978-3-030-14805-8_8
Arvidsson AJohansson MTouche R(2019)Proving Type Class Laws for HaskellMicrobial Metabolic Engineering10.1007/978-3-030-14805-8_4(61-74)Online publication date: 21-Feb-2019
https://doi.org/10.1007/978-3-030-14805-8_4
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents