Abstract
Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph perspective encodes naturally in the typeclass system of theorem provers such as Lean, where nodes can be represented as structures (or records) containing the requisite axioms. This design inevitably needs some form of multiple inheritance; a ring is both a semiring and an abelian group.
In the presence of dependently-typed typeclasses that themselves consume typeclasses as type-parameters, such as a vector space typeclass which assumes the presence of an existing additive structure, the implementation details of structure multiple inheritance matter. The type of the outer typeclass is influenced by the path taken to resolve the typeclasses it consumes. Unless all possible paths are considered judgmentally equal, this is a recipe for disaster.
This paper provides a concrete explanation of how these situations arise (reduced from real examples in mathlib), compares implementation approaches for multiple inheritance by whether judgmental equality is preserved, and outlines solutions (notably: kernel support for \(\eta \)-reduction of structures) to the problems discovered.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Albeit somewhat non-idiomatically.
- 2.
At least, in old versions without pertinent fixes!.
- 3.
Unless they are of different types, which raises an error.
- 4.
In general this is a spanning diamond-free directed acyclic graph, but for this paper it suffices to consider a tree.
- 5.
This style of display can be enabled with
in Lean 3 and 
in Lean 4. - 6.
Omitting the usual
and 
notation to keep listing 2 short. - 7.
Strictly speaking, it \(\eta \)-reduces
types with one constructor; 
s are not native to the type theory of Lean, and instead just syntax for generating a suitable inductive type. - 8.
Via
. - 9.
Some motivating discussion can be found in [1].
- 10.
Or alternatively, by packing the ring and both modules into a single structure, as
. This is a viable approach for a module over two rings (as rarely are many rings needed), but doesn’t scale for n modules over the same ring. - 11.
Presumably due to simplicity of implementation; there is no mention in [7] that using nested inheritance instead would have run into the issues described here.
References
Abel, A.: On Extensions to Definitional Equality in Agda (2009). https://www.cse.chalmers.se/~abela/talkAIM09.pdf
Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 3–20. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_1
Baanen, A.: Use and abuse of instance parameters in the Lean mathematical library. In: ITP 2022, Haifa, Israel (2022). https://arxiv.org/abs/2202.01629
Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. 64(6), 1093–1121 (2019). https://doi.org/10.1007/s10817-019-09537-9
Buzzard, K.: leanprover/lean4#2074: typeclass inference failure (2023). https://github.com/leanprover/lean4/issues/2074
Carette, J., Farmer, W.M., Sharoda, Y.: Leveraging the information contained in theory presentations. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 55–70. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53518-6_4
Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description). In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 34:1–34:21. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.34. ISSN 1868-8969
Ebner, G.: leanprover/lean4#777: Definitional eta for structures (2021). https://github.com/leanprover/lean4/issues/777
Ebner, G.: leanprover/lean4#2210: Skip proof arguments during unification, and try structure eta last (2023). https://github.com/leanprover/lean4/pull/2210
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23
Gouëzel, S.: leanprover-community/mathlib4#3840: tweak priorities for linear algebra (2023). https://github.com/leanprover-community/mathlib4/pull/3840
Gouëzel, S.: #mathlib4 Some observations on eta experiment (2023). https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some. 20observations.20on.20eta.20experiment/near/355336941
Mahboubi, A., Tassi, E.: Mathematical Components (2022). https://zenodo.org/record/7118596. Zenodo Version Number: 1.0.2
de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26
Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37
Poll, E., Thompson, S.: Integrating computer algebra and reasoning through the type system of Aldor. In: Kirchner, H., Ringeissen, C. (eds.) FroCoS 2000. LNCS (LNAI), vol. 1794, pp. 136–150. Springer, Heidelberg (2000). https://doi.org/10.1007/10720084_10
Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 138–157. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_8
Spitters, B., Van Der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795–825 (2011). https://doi.org/10.1017/S0960129511000119
The mathlib Community: The lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, New Orleans, LA, USA, pp. 367–381. ACM (2020). https://doi.org/10.1145/3372885.3373824
Wieser, E.: Scalar actions in Lean’s mathlib. In: CICM 2021, Timisoara, Romania (2021). https://arxiv.org/abs/2108.10700
Acknowledgments
The author is grateful to: Gabriel Ebner, for campaigning for \(\eta \)-reduction support in Lean 4; Kazuhiko Sakaguchi, for providing insight into analogous situations in Coq; the anonymous referees, as well as Yaël Dillies and Filippo A. E. Nuccio, for valuable feedback on the manuscript; and the wider Lean community for collaboratively diagnosing [5] that the diamond problems discussed in Sect. 3.2 existed. The author is funded by a scholarship from the Cambridge Trust.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Wieser, E. (2023). Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies. In: Dubois, C., Kerber, M. (eds) Intelligent Computer Mathematics. CICM 2023. Lecture Notes in Computer Science(), vol 14101. Springer, Cham. https://doi.org/10.1007/978-3-031-42753-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-031-42753-4_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42752-7
Online ISBN: 978-3-031-42753-4
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
