Skip to main content
SpringerLink
Log in

The Negligible and Yet Subtle Cost of Pattern Matching

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10695))

Included in the following conference series:

Abstract

The model behind functional programming languages is the closed \(\lambda \) -calculus, that is, the fragment of the \(\lambda \)-calculus where evaluation is weak (i.e. out of abstractions) and terms are closed. It is well-known that the number of \(\beta \) (i.e. evaluation) steps is a reasonable cost model in this setting, for all natural evaluation strategies (call-by-name/value/need). In this paper we try to close the gap between the closed \(\lambda \)-calculus and actual languages, by considering an extension of the \(\lambda \)-calculus with pattern matching. It is straightforward to prove that \(\beta \) plus matching steps provide a reasonable cost model. What we do then is finer: we show that \(\beta \) steps only, without matching steps, provide a reasonable cost model also in this extended setting—morally, pattern matching comes for free, complexity-wise. The result is proven for all evaluation strategies (name/value/need), and, while the proof itself is simple, the problem is shown to be subtle. In particular we show that qualitatively equivalent definitions of call-by-need may behave very differently.

This work is part of a wider research effort, the COCA HOLA project [3].

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    The kernel of Coq is the subset of the codebase which ensures that only valid proofs are accepted. Hence the use of an abstract machine, which has a better ratio efficiency/complexity than the use of a compiler or a naive interpreter.

  2. 2.

    We do not prove the equivalence between the two formulations of CbNeed studied in the paper, but the difference is essentially that in one case \(\mathtt{c}(\varvec{t})\) is reduced to (via \(\rightarrow _{\mathtt{cstr}}\)) while in the other case it is left unchanged—the two calculi compute the same result, up to substitutions, just with very different complexities.

References

  1. Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  2. Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: RTA, pp. 6–21 (2012)

    Google Scholar 

  3. Accattoli, B.: COCA HOLA (2016). https://sites.google.com/site/beniaminoaccattoli/coca-hola

  4. Accattoli, B.: The complexity of abstract machines. In: WPTE@FSCD 2016, pp. 1–15 (2016)

    Google Scholar 

  5. Accattoli, B.: The useful MAM, a reasonable implementation of the strong \(\lambda \)-calculus. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 1–21. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-52921-8_1

    Google Scholar 

  6. Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP 2014, pp. 363–376. ACM (2014)

    Google Scholar 

  7. Accattoli, B., Barras, B.: Environments and the complexity of abstract machines (2017). Accepted to PPDP 2017

    Google Scholar 

  8. Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL, pp. 659–670 (2014)

    Google Scholar 

  9. Accattoli, B., Coen, C.S.: On the relative usefulness of fireballs. In: LICS 2015, pp. 141–155. IEEE Computer Society (2015)

    Google Scholar 

  10. Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Logical Methods Comput. Sci. 12(1), 1–46 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  11. Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 206–226. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_12

    Chapter  Google Scholar 

  12. Accattoli, B., Guerrieri, G.: Implementing open call-by-value. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 1–19. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68972-2_1

    Chapter  Google Scholar 

  13. Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4–16. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29822-6_4

    Chapter  Google Scholar 

  14. Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 36–50. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44145-9_3

    Google Scholar 

  15. Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  16. Barras, B.: Auto-validation d’un système de preuves avec familles inductives. Ph.D. thesis, Université Paris 7 (1999)

    Google Scholar 

  17. Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: FPCA 1995, pp. 226–237. ACM (1995)

    Google Scholar 

  18. Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 137–153. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_9

    Google Scholar 

  19. Cirstea, H., Kirchner, C.: The rewriting calculus - part I. Logic J. IGPL 9(3), 339–375 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  20. Coq Development Team: The coq proof-assistant reference manual, version 8.6 (2016). http://coq.inria.fr

  21. Dal Lago, U., Martini, S.: Derivational complexity is an invariant cost model. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 100–113. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15331-0_7

    Chapter  Google Scholar 

  22. Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 163–174. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_14

    Chapter  Google Scholar 

  23. Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP 2013, pp. 97–108. ACM (2013)

    Google Scholar 

  24. Fernández, M., Siafakas, N.: New developments in environment machines. Electr. Notes Theor. Comput. Sci. 237, 57–73 (2009)

    Article  MATH  Google Scholar 

  25. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235–246. ACM (2002)

    Google Scholar 

  26. Jay, C.B., Kesner, D.: First-class patterns. J. Funct. Program. 19(2), 191–225 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  27. Jeannin, J., Kozen, D.: Computing with capsules. J. Automata Lang. Comb. 17(2–4), 185–204 (2012)

    MathSciNet  MATH  Google Scholar 

  28. Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74915-8_20

    Chapter  Google Scholar 

  29. Klop, J.W., van Oostrom, V., de Vrijer, R.C.: Lambda calculus with patterns. Theor. Comput. Sci. 398(1–3), 16–31 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  30. Launchbury, J.: A natural semantics for lazy evaluation. In: POPL 1993, pp. 144–154. ACM Press (1993)

    Google Scholar 

  31. Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275–317 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  32. Milner, R.: Local bigraphs and confluence: two conjectures. Electr. Notes Theor. Comput. Sci. 175(3), 65–73 (2007)

    Article  MATH  Google Scholar 

  33. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  34. Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 60–82. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36377-7_4

    Chapter  Google Scholar 

  35. Sergey, I., Vytiniotis, D., Peyton Jones, S.L.: Modular, higher-order cardinality analysis in theory and practice. In: POPL 2014, pp. 335–348 (2014)

    Google Scholar 

  36. Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231–264 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  37. Wadsworth, C.P.: Semantics and pragmatics of the lambda-calculus. Ph.D. thesis, Oxford (1971). Chapter 4

    Google Scholar 

  38. Walker, D.: Substructural type systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 3–43. The MIT Press (2004)

    Google Scholar 

  39. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01).

Author information

Authors and Affiliations

  1. INRIA, UMR 7161, LIX, École Polytechnique, Palaiseau, France

    Beniamino Accattoli & Bruno Barras

Authors
  1. Beniamino Accattoli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Barras
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Beniamino Accattoli .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Accattoli, B., Barras, B. (2017). The Negligible and Yet Subtle Cost of Pattern Matching. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation