The HERMIT in the Tree

Mechanizing Program Transformations in the GHC Core Language
  • Neil SculthorpeEmail author
  • Andrew Farmer
  • Andy Gill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8241)


This paper describes our experience using the HERMIT toolkit to apply well-known transformations to the internal core language of the Glasgow Haskell Compiler. HERMIT provides several mechanisms to support writing general-purpose transformations: a domain-specific language for strategic programming specialized to GHC’s core language, a library of primitive rewrites, and a shell-style–based scripting language for interactive and batch usage.

There are many program transformation techniques that have been described in the literature but have not been mechanized and made available inside GHC — either because they are too specialized to include in a general-purpose compiler, or because the developers’ interest is in theory rather than implementation. The mechanization process can often reveal pragmatic obstacles that are glossed over in pen-and-paper proofs; understanding and removing these obstacles is our concern. Using HERMIT, we implement eleven examples of three program transformations, report on our experience, and describe improvements made in the process.


GHC Mechanization Transformation Worker/wrapper 



We thank Ed Komp for his work on implementing the HERMIT system, Jason Reich for suggesting the Mean example, and the anonymous reviewers for their constructive comments and feedback. This material is based upon work supported by the National Science Foundation under Grant No. 1117569.


  1. 1.
    Bird, R.S.: Tabulation techniques for recursive programs. ACM Comput.Surv. 12(4), 403–417 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44–67 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Chin, W.N., Khoo, S.C., Jones, N.: Redundant call elimination via tupling. Fundam. Informaticae 69(1–2), 1–37 (2006)MathSciNetzbMATHGoogle Scholar
  4. 4.
    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: 2012 ACM SIGPLAN Haskell Symposium, pp. 1–12. ACM, New York (2012)CrossRefGoogle Scholar
  5. 5.
    GHC Team: The Glorious Glasgow Haskell Compilation System User’s Guide, Version 7.6.2. (2013)
  6. 6.
    Gill, A.: Introducing the Haskell equational reasoning assistant. In: 2006 ACM SIGPLAN Haskell Workshop, pp. 108–109. ACM, New York (2006)CrossRefGoogle Scholar
  7. 7.
    Gill, A., Hutton, G.: The worker/wrapper transformation. J. Funct. Program. 19(2), 227–251 (2009)CrossRefzbMATHGoogle Scholar
  8. 8.
    Guttmann, W., Partsch, H., Schulte, W., Vullinghs, T.: Tool support for the interactive derivation of formally correct functional programs. J. Univ. Comput. Sci. 9(2), 173–188 (2003)Google Scholar
  9. 9.
    Hu, Z., Iwasaki, H., Takeichi, M., Takano, A.: Tupling calculation eliminates multiple data traversals. In: 2nd ACM SIGPLAN International Conference on Functional Programming, pp. 164–175. ACM, New York (1997)CrossRefGoogle Scholar
  10. 10.
    Hughes, R.J.M.: A novel representation of lists and its application to the function “reverse”. Inf. Process. Lett. 22(3), 141–144 (1986)CrossRefGoogle Scholar
  11. 11.
    Hutton, G.: Programming in Haskell. Cambridge University Press, Cambridge (2007)CrossRefzbMATHGoogle Scholar
  12. 12.
    Li, H., Thompson, S.: A domain-specific language for scripting refactoring in Erlang. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 501–515. Springer, Heidelberg (2012)Google Scholar
  13. 13.
    Li, H., Thompson, S., Orosz, G., Tóth, M.: Refactoring with wrangler, updated: data and process refactorings, and integration with eclipse. In: 7th ACM SIGPLAN Erlang Workshop, pp. 61–72. ACM, New York (2008)CrossRefGoogle Scholar
  14. 14.
    Li, H., Thompson, S., Reinke, C.: The Haskell refactorer, HaRe, and its API. Electron. Notes Theor. Comput. Sci. 141(4), 29–34 (2005)CrossRefGoogle Scholar
  15. 15.
    Liu, Y.A., Stoller, S.D.: Dynamic programming via static incrementalization. Higher-Order Symbolic Comput. 16(1–2), 37–62 (2003)CrossRefzbMATHGoogle Scholar
  16. 16.
    Pettorossi, A.: A powerful strategy for deriving efficient programs by transformation. In: 1984 ACM Symposium on LISP and Functional Programming, pp. 273–281. ACM, New York (1984)CrossRefGoogle Scholar
  17. 17.
    Peyton Jones, S.: The Implementation of Functional Programming Languages. Prentice Hall, New York (1987)zbMATHGoogle Scholar
  18. 18.
    Peyton Jones, S.L., Launchbury, J.: Unboxed values as first class citizens in a non-strict functional language. In: 5th ACM Conference on Functional Programming Languages and Computer Architecture, pp. 636–666. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  19. 19.
    Jones Peyton, S., Santos, A.L.M.: A transformation-based optimiser or Haskell. Sci. Comput. Program. 32(1–3), 3–47 (1998)CrossRefzbMATHGoogle Scholar
  20. 20.
    Peyton Jones, S., Tolmach, A., Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC. In: 2001 ACM SIGPLAN Haskell Workshop, pp. 203–233. ACM, New York (2001)Google Scholar
  21. 21.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)Google Scholar
  22. 22.
    Santos, A.: Compilation by transformation in non-strict functional languages. Ph.D. thesis, University of Glasgow (1995)Google Scholar
  23. 23.
    Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Newton (1986)Google Scholar
  24. 24.
    Sculthorpe, N., Frisby, N., Gill, A.: KURE: A Haskell-embedded strategic programming language with custom closed universes (in preparation)Google Scholar
  25. 25.
    Sculthorpe, N., Hutton, G.: Work it, wrap it, fix it, fold it (in preparation)Google Scholar
  26. 26.
    Sulzmann, M., Chakravarty, M.M.T., Peyton Jones, S., Donnelly, K.: System F with type equality coercions. In: 3rd ACM SIGPLAN Workshop on Types in Language Design and Implementaion, pp. 53–66. ACM, New York (2007)Google Scholar
  27. 27.
    Tullsen, M.: PATH, a program transformation system for Haskell. Ph.D. thesis, Yale University (2002)Google Scholar
  28. 28.
    Wadler, P.: The concatenate vanishes. University of Glasgow, Tech. rep. (1989)Google Scholar
  29. 29.
    Yorgey, B.A., Weirich, S., Cretin, J., Peyton Jones, S., Vytiniotis, D., Magalhães, J.P.: Giving Haskell a promotion. In: 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, pp. 53–66. ACM, New York (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Information and Telecommunication Technology CenterThe University of KansasLawrenceUSA

Personalised recommendations