Lightweight Higher-Order Rewriting in Haskell | SpringerLink
Skip to main content
Springer Nature Link
Log in

Lightweight Higher-Order Rewriting in Haskell

  • Conference paper
  • First Online:
Trends in Functional Programming (TFP 2015)

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

Included in the following conference series:

  • 565 Accesses

Abstract

We present a generic Haskell library for expressing rewrite rules with a safe treatment of variables and binders. Both sides of the rules are written as typed EDSL expressions, which leads to syntactically appealing rules and hides the underlying term representation. Matching is defined as an instance of Miller’s higher-order pattern unification and has the same complexity as first-order matching. The restrictions of pattern unification are captured in the types of the library, and we show by example that the library is capable of expressing useful simplifications that might be used in a compiler.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 4804
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 6006
Price includes VAT (Japan)
  • 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

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://hackage.haskell.org/package/ho-rewriting-0.2.

  2. 2.

    https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghc-language-features.html.

  3. 3.

    Note the partial type annotation in . It is used to constrain the type parameter of the RHS without saying anything about the representation of the RHS. Partial type signatures require the recent extension to GHC. However, this extension is not strictly needed: an equivalent formulation of the RHS would be .

  4. 4.

    The property is almost true: it holds if we replace all wildcards in \(l\) with unique meta-variables.

  5. 5.

    https://github.com/emilaxelsson/ho-rewriting/blob/0.2/examples/Feldspar.hs.

References

  1. Antoy, S., Hanus, M.: Declarative programming with function patterns. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol. 3901, pp. 6–22. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Axelsson, E., Claessen, K.: Using circular programs for higher-order syntax: functional pearl. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, pp. 257–262. ACM, New York (2013)

    Google Scholar 

  3. Axelsson, E., Claessen, K., Dévai, G., Horváth, Z., Keijzer, K., Lyckegård, B., Persson, A., Sheeran, M., Svenningsson, J., Vajda, A.: Feldspar: a domain specific language for digital signal processing algorithms. In: 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign, pp. 169–178. IEEE (2010)

    Google Scholar 

  4. Bahr, P., Hvitved, T.: Compositional data types. In: Proceedings of the Seventh ACM SIGPLAN Workshop on Generic Programming, pp. 83–94. ACM, New York (2011)

    Google Scholar 

  5. Brown, N.C., Sampson, A.T.: Matching and modifying with generics. In: Draft Proceedings of Trends in Functional Programming, pp. 304–318 (2008)

    Google Scholar 

  6. Carette, J., Kiselyov, O., Shan, C.C.: Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. J. Funct. Programm. 19(5), 509–543 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cervesato, I., Pfenning, F.: A linear spine calculus. J. Logic Comput. 13(5), 639–688 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  8. Dévai, G.: Extended pattern matching for embedded languages. Annales Univ. Sci. Budapestiensis de Rolando Eötvös Nominatae, Sectio Comutatorica 36, 277–297 (2012)

    MATH  Google Scholar 

  9. Felgenhauer, B., Avanzini, M., Sternagel, C.: A Haskell library for term rewriting. CoRR abs/1307.2328 (2013). http://arxiv.org/abs/1307.2328

  10. Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoret. Comput. Sci. 13(2), 225–230 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  11. Huet, G.: Résolution d’équations dans les langages d’ordre 1, 2,.., \(\omega \). Ph.D. thesis, Université Paris VII (1976)

    Google Scholar 

  12. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. logic Comput. 1(4), 497–536 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  13. Mohnen, M.: Context patterns in Haskell. In: Kluge, W. (ed.) IFL’96. LNCS, vol. 1268, pp. 41–57. Springer, Berlin, Heidelberg (1997)

    Chapter  Google Scholar 

  14. Nadathur, G., Miller, D.: An overview of Lambda-Prolog. Technical report MS-CIS-88-40, University of Pennsylvania, Department of Computer and Information Science (1988)

    Google Scholar 

  15. van Noort, T., Yakushev, A.R., Holdermans, S., Jeuring, J., Heeren, B., Magalhães, J.P.: A lightweight approach to datatype-generic rewriting. J. Funct. Programm. 20, 375–413 (2010)

    Article  MATH  Google Scholar 

  16. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007

    Google Scholar 

  17. Oosterhof, N., Hölzenspies, P., Kuper, J.: Application patterns. In: van Eekelen, M. (ed.) Trends in Functional Programming, pp. 370–382. Tartu University Press, Tallinn (2005)

    Google Scholar 

  18. Pfenning, F., Schürmann, C.: System description: twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Sculthorpe, N., Frisby, N., Gill, A.: The kansas university rewrite engine. J. Funct. Programm. 24, 434–473 (2014)

    Article  MathSciNet  Google Scholar 

  20. Serrano, A., Hage, J.: Feedback upon feedback. Presented at Trends in Functional Programming (2015). ftp://ftp-sop.inria.fr/indes/TFP15/TFP2015_submission_22.pdf

  21. Swierstra, W.: Data types à la carte. J. Funct. Programm. 18, 423–436 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  22. Wierzbicki, T.M.: Complexity of the higher order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 82–96. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Yokoyama, T., Hu, Z., Takeichi, M.: Design and implementation of deterministic higher-order patterns (2005). http://takeichi.ipl-lab.org/yicho/YoHT05.pdf

Download references

Acknowledgements

This research was funded by the Swedish Foundation for Strategic Research (in the RAWFP project). The anonymous referees provided useful input.

Author information

Authors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Emil Axelsson & Andrea Vezzosi

Authors
  1. Emil Axelsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrea Vezzosi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Emil Axelsson .

Editor information

Editors and Affiliations

  1. INRIA Sophia Antipolis, Sophia Antipolis, France

    Manuel Serrano

  2. Dept.Information and Computing Sc., Utrecht University, Utrecht, The Netherlands

    Jurriaan Hage

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Axelsson, E., Vezzosi, A. (2016). Lightweight Higher-Order Rewriting in Haskell. In: Serrano, M., Hage, J. (eds) Trends in Functional Programming. TFP 2015. Lecture Notes in Computer Science(), vol 9547. Springer, Cham. https://doi.org/10.1007/978-3-319-39110-6_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-39110-6_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-39109-0

  • Online ISBN: 978-3-319-39110-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation