Document Open Access Logo

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Author Anne Baanen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.4.pdf
  • Filesize: 0.73 MB
  • 20 pages

Document Identifiers

Author Details

Anne Baanen
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands

Funding

NWO Vidi grant No. 016.Vidi.189.037, Lean Forward.

Acknowledgements

I want to thank the anonymous reviewers and Jeremy Avigad, Jasmin Blanchette, Bryan Gin-Ge Chen, Johan Commelin, Sander Dahmen, Manuel Eberl, Rob Lewis, Assia Mahboubi, Filippo A. E. Nuccio, Kazuhiko Sakaguchi, Enrico Tassi and Eric Wieser for their helpful comments on earlier versions on this manuscript.

Cite AsGet BibTex

Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.4

Abstract

The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • formalization of mathematics
  • dependent type theory
  • typeclasses
  • algebraic hierarchy
  • Lean prover

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: A case study in functional analysis. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, volume 12167 of LNCS, pages 3-20. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_1.
  2. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs 2009, volume 5674 of LNCS, pages 84-98. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_8.
  3. Clemens Ballarin. Locales: A module system for mathematical theories. J. Autom. Reason., 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  4. Clemens Ballarin. Exploring the structure of an algebra text with locales. J. Autom. Reason., 64(6):1093-1121, 2020. URL: https://doi.org/10.1007/s10817-019-09537-9.
  5. Edwin C. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  6. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In CPP '20, Certified Programs and Proofs, pages 299-312. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373830.
  7. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In Zena M. Ariola, editor, FSCD 2020, volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  8. Johan Commelin and Robert Y. Lewis. Formalizing the ring of Witt vectors. In Catalin Hrițcu and Andrei Popescu, editors, CPP '21, Certified Programs and Proofs, pages 264-277. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439919.
  9. L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean theorem prover (system description). In A. P. Felty and A. Middeldorp, editors, Automated Deduction - CADE-25, volume 9195 of LNCS, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  10. Leonardo de Moura, Jeremy Avigad, Soonho Kong, and Cody Roux. Elaboration in dependent type theory. CoRR, abs/1505.04324, 2015. URL: http://arxiv.org/abs/1505.04324.
  11. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE-28, volume 12699 of LNCS, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  12. Dominique Devriese and Frank Piessens. On the bright side of type classes: Instance arguments in Agda. SIGPLAN Not., 46(9):143-155, September 2011. URL: https://doi.org/10.1145/2034574.2034796.
  13. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs 2009, volume 5674 of LNCS, pages 327-342. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_23.
  14. Adam Grabowski, Artur Kornilowicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, FedCSIS 2016, volume 8 of Annals of Computer Science and Information Systems, pages 363-371. IEEE, 2016. URL: https://doi.org/10.15439/2016F520.
  15. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP 2013, volume 7998 of LNCS, pages 279-294. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  16. Ralf Jung. Exponential blowup when using unbundled typeclasses to model algebraic hierarchies, 2019. Accessed 2022-02-01. URL: https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html.
  17. Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales - A sectioning concept for Isabelle. In Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, and Laurent Théry, editors, TPHOLs'99, volume 1690 of LNCS, pages 149-166. Springer, 1999. URL: https://doi.org/10.1007/3-540-48256-3_11.
  18. A. Mahboubi and E. Tassi. The Mathematical Components Libraries. Zenodo, Genève, Switzerland, 2017. URL: https://doi.org/10.5281/zenodo.4457887.
  19. Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects and implicits. SIGPLAN Not., 45(10):341-360, October 2010. URL: https://doi.org/10.1145/1932682.1869489.
  20. The Rust team. The Rust reference 1.57.0, 2021. Accessed 2021-12-22. URL: https://doc.rust-lang.org/1.57.0/reference/index.html.
  21. Amokrane Saïbi. Typing algorithm in type theory with inheritance. In Principles of Programming Languages, POPL '97, pages 292-301. ACM, 1997. URL: https://doi.org/10.1145/263699.263742.
  22. Kazuhiko Sakaguchi. Validating mathematical structures. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, volume 12167 of LNCS, pages 138-157. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_8.
  23. Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. Tabled typeclass resolution. CoRR, abs/2001.04301, 2020. URL: http://arxiv.org/abs/2001.04301.
  24. Matthieu Sozeau and Nicolas Oury. First-class type classes. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, TPHOLs 2008, volume 5170 of LNCS, pages 278-293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  25. Bas Spitters and Eelis van der Weegen. Developing the algebraic hierarchy with type classes in Coq. In Matt Kaufmann and Lawrence C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 490-493. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_35.
  26. The mathlib Community. The Lean mathematical library. In J. Blanchette and C. Hrițcu, editors, CPP 2020, Certified Programs and Proofs, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  27. Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis. Maintaining a library of formal mathematics. In Christoph Benzmüller and Bruce R. Miller, editors, CICM 2020, volume 12236 of LNCS, pages 251-267. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53518-6_16.
  28. P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Principles of Programming Languages, POPL '89, pages 60-76. ACM, 1989. URL: https://doi.org/10.1145/75277.75283.
  29. Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy P. Felty, editors, TPHOLs'97, volume 1275 of LNCS, pages 307-322. Springer, 1997. URL: https://doi.org/10.1007/BFb0028402.
  30. Eric Wieser. Scalar actions in Lean’s mathlib. CoRR, abs/2108.10700, 2021. URL: http://arxiv.org/abs/2108.10700.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact