Keywords

1 Introduction

It becomes clear very early in the development of mathematical libraries that a generalization over algebraic properties is essential; as soon as we are able to speak about \(\mathbb {N}\) and \(\mathbb {Z}\), we will want to have available that \(a + b = b + a\) whether \(a, b : \mathbb {N}\) or \(a, b : \mathbb {Z}\), and it would be strongly preferable that we can refer to this property by a single name.

The generalization we seek is of course well-studied as the field of abstract algebra, and the commutativity property above can be phrased as “\(\mathbb {N}\) and \(\mathbb {Z}\) are both semirings”, or using language more precise to the specific property we care about “\(\mathbb {N}\) and \(\mathbb {Z}\) are both abelian monoids”. At least when considering only those which operate on a single carrier type, algebraic structures can be connected into a directed graph; all rings are semirings and abelian groups, so we can draw a pair of edges from “ring” to “semiring” and “abelian group”. An illustration of the depth and breadth of such a graph can be seen in [19, fig. 1], while a reduced example that we will use in this paper can be seen in Fig. 1.

Encoding this directed graph into the machinery of a particular theorem prover can be done in multiple ways, which are outlined in [3, §1] and presented with example code across a variety of languages in [6, fig. 1]. This paper focuses on the typeclass approach used by mathlib [19] in the Lean 3 theorem prover [14]; though the observations generalize to other implementations in dependent type theory built upon “structure” types.

In this approach, the graph is pruned to be acyclic, and then a typeclass is created for each node carrying its operators (data fields) and the properties they satisfy (proof fields). The edges correspond to functions converting from stronger structures to weaker structures, each registered as a typeclass instance. This encodes naturally in “record” or “structure” types with multiple inheritance, where we can write down the desired edges declaratively in the form of a list of base structures, and have the language generate the necessary “forgetful” instances automatically. A simple example of this can be found in [3, §4].

Unfortunately, the devil is in the details; in Lean, Coq, Agda, and Isabelle, support for multiple inheritance is not part of the underlying type theory, so types that use multiple inheritance have to be translated by the elaborator into inductive types that do not. There are multiple ways to perform such a translation, and the choice is not inconsequential.

In Sect. 2 we outline two such approaches, and show how they can each be used to construct a much-reduced version of mathlib’s abstract algebra library. Section 3 introduces a more complex use of a typeclass from mathlib, and demonstrates how in the absence of special kernel support for \(\eta \)-reduction on structure types, its design is incompatible with “nested” approach to structures. Section 4 outlines some workarounds that permit the “nested” approach to be used even in the absence of this support. Section 5 explains how the problem is not unique to typeclass-based approaches.

The problems explored here are far from hypothetical; the migration of mathlib from Lean 3 to Lean 4 [15] forces a switch from the approach in Sect. 2.1 to that in Sect. 2.2, which has presented a significant stumbling block [5].

2 Types of Structure Inheritance

Lean 3 supports two types of structure inheritance: the default “new style”, which we will refer to as “nested”, and does not support multiple inheritance; and the legacy “old style” (enabled with ) which we will refer to as “flat”, and does support multiple inheritance. Lean 4 (as a language) does away with the “flat” mode, but extends the “nested” mode to support multiple inheritance.

Fig. 1.
figure 1

A hierarchy of algebraic typeclasses, where arrows indicate a stronger typeclass implying a weaker typeclass. Dotted arrows correspond to the “non-preferred” typeclass paths which are relevant to Sect. 2.2.

Full size image
figure b

To compare these approaches, this section demonstrates how to build the miniature algebraic hierarchy shown in Fig. 1. If we permit ourselves to use the builtin language support for multiple inheritance, we could write this as in listing 1. As they are not going to be relevant to the discussion in this paper, the proof fields such as have all been omitted.

To avoid this paper being about a specific implementation of inheritance in a specific version of Lean, we will avoid the keyword, instead emulating it via different possible encodings of inheritance into regular structures. For simplicity this paper is largely presented as about Lean, but the supplemental repository referenced in Sect. 7 demonstrates how the Lean 3 samples presented here can be replicated in CoqFootnote 1 and in Lean 4Footnote 2.

2.1 Flat Structures

The “flat” approach to structure inheritance is to copy all of the fields from the base classes into the derived class. If multiple base classes share a field of the same name, then these fields are mergedFootnote 3. The forgetful instances are then implemented by unpacking all the relevant fields of the derived class and passing them to each base class constructor (which in Lean can be written as ).

This can be seen for the toy example from listing 1 in listing 2a; extends both and , so inherits the union of the four fields of () and the three fields of (). The and instances generate constructor applications that reassemble the corresponding fields.

This approach is straightforward to implement in a theorem prover, and is the one used (via ) in the majority of mathlib’s algebraic hierarchy in Lean 3. A downside to this approach is that it can produce more work for unification (leading to poor performance) in long inheritance chains [3, §10].

figure q

2.2 Nested Structures

A naïve approach to multiple inheritance for would be simply to create a structure containing a field and a field. The problem with this approach is that the resulting structure contains two separate fields. Compatibility of these fields could in principle be enforced with a proof field along the lines of , but this makes the API very unpleasant to use as the user now has to rewrite between all the different copies of .

The way to modify this approach to avoid this pitfall is to add a field for each base class that doesn’t overlap with any previous base classes, otherwise fall back to the “flat” approach and add the non-overlapping fields directly. We call these non-overlapping base-classes “preferred” instances, as the projections for these fields can be registered directly with the typeclass system using . What remains are the “non-preferred” instances, which can be constructed in a similar way to what was done in Sect. 2.1, though with somewhat messier expressions. Note that unlike Sect. 2.1, this approach is influenced by the order of the base classes.

This can be seen in listing 2b; contains a field for its first base class, but would overlap so its remaining non-overlapping field () is added separately. The “preferred” projection is then registered with the typeclass system, while the “non-preferred” is painstakingly assembled piece-by-piece. To encourage Lean to avoid the “non-preferred” instance, we give it a low priority of 100 (the default is 1000).

This approach is more complicated to implement (and indeed, was not implemented in Lean until Lean 4), but can have performance advantages for unification as the “preferred” instance paths do not introduce a constructor application.

The result of listing 2b is that the graph in Fig. 1 is imbued with an asymmetry; the dotted edges are provided by “non-preferred” instances. These edges can be chosen on any spanning treeFootnote 4 of the overall graph, and indeed can be optimized to fall on the paths most used by the library [11].

For the purpose of this paper, the opposite is true; their placement has been pessimized to deliberately cause a failure, which we shall see in Sect. 3.2!

3 Typeclasses Depending on Typeclasses

In Sect. 2, we concerned ourselves with the typical examples of typeclasses which depend on a single type. In Lean, it is possible for typeclasses to depend not only on multiple types, but on typeclasses that constrain those types. A simple typeclass of this form is , which is used to declare that given a semiring R and an abelian monoid M, there is an R-module structure on M. A more complete explanation of this typeclass can be found in [20] and [3, §5]. For the purpose of this paper, we can imagine the simpler definition as follows:

figure af

Here, the proof fields within the typeclass depend on the operators imbued upon the types R and M. Just as in Sect. 2, we shall ignore these proof fields as they are not relevant to the discussion other than providing motivation for the parameters.

3.1 Equality of Typeclass Arguments

A natural use of this typeclass is to record the fact that any semiring is a module over itself, where the scalar action is just multiplication [20, §2.1]. This can be written in Lean as

figure aj

The type of this instance is misleading; while a human reader could be forgiven for assuming that the type is just , to Lean the type is

figure al

where is syntax to tell Lean that even the automatically-populated typeclass arguments should be spelled out explicitlyFootnote 5. The expressions for these implicit arguments are visualized graphically in Fig. 2a.

Lean can now tell us that a ring is a module over itself, as after all every ring is also a semiring. We can ask this question with:

figure ap

Once again, the type is misleading; the true type can be seen in Fig. 2b. Comparing the types for Fig. 2a and Fig. 2b, we see that the former unifies with the latter by setting ; for this reason, Lean finds our instance as .

3.2 Inequality of Typeclass Arguments

Let’s imagine now that we want to write a lemma that applies to a module over a ring (as opposed to a semi-module over a semiring), and states that \((-r)m = -(rm)\). We write this asFootnote 6

figure au

To complete our setup, let’s check that this lemma applies to the R-module structure on R:

figure av

If we use the “flat” design in listing 2a, then this continues to work as expected. The same is not true of the “nested” design in listing 2b, which fails to synthesize type class instance for

figure aw

which is shown graphically in Fig. 2c. The lemma is an example of how typeclass resolution can be steered through a specific node of the graph in Fig. 1.

In Lean 3, the reason this fails is nothing to do with typeclass search; the problem is that the type in Fig. 2c is not equal to type in Fig. 2b, due to the implicit arguments (shown in red) not being considered equal. Considerations of equality between the red paths in Fig. 2 and 2c are often referred to as a “typeclass diamonds” due to the shape they form when overlaid; though this is a rather more subtle diamond problems than the ones described in [20, §5] and [2, §3.1] as it is caused by code that would normally be invisible to the user.

To mathematicians, this diagram obviously commutes; weakening a ring to an abelian monoid via a semiring is the same as doing so via an abelian group. But Lean doesn’t care about “obviously”: when determining equality of types, it’s not enough for them to just be provably the same; they need to be definitionally (sometimes called judgmentally) so. A proof of can be used to determine if two terms are judgmentally equal; under listing 2b, we get an error confirming they are not:

figure ba
Fig. 2.
figure 2

Paths taken through the graph in Fig. 1 when filling the two implicit arguments of the type of . Dotted lines again refer to “non-preferred” edges. (Color figure online)

Full size image

3.3 Impact of the Inheritance Strategy

The in Sect. 3.2 that fails under listing 2b but not listing 2a tells us that the nested inheritance is certainly to blame here. The underlying cause is the difference between the “preferred” and “non-preferred” paths.

The “non-preferred” edges in listing 2b are implemented directly as a constructor application via the syntax; so by virtue of following “non-preferred” edges, the red path in Fig. 2c unfolds to an application of the constructor. The “preferred” edges correspond to a projection; unless applied to something that unifies against a constructor, these operations themselves do not unify against a constructor. As the red path in Fig. 2b consists of only “preferred” edges, it only unifies with this constructor if unifies with a constructor.

If is a concrete instance such as , then it will almost certainly unify with a constructor, and the overall unification problem is solvable. However if is a free variable, it will only unify with a constructor in systems which support “\(\eta \)-reduction for structures”. Lean 3 is not such a system, which makes unification impossible.

3.4 Other Examples in mathlib

The typeclass is far from the only typeclass in mathlib that follows the pattern introduced in Sect. 3; some others typeclasses (all of which fall afoul of the issue in Sect. 3.2) include

  • , indicating that A is an R-algebras.

  • , indicating that there is a \(\star \) operator compatible with the existing ring structure on R.

  • , indicating that the existing norm, \(\star \), and ring structure are suitable to declare R a \(C^\star \)-ring.

Like the example, the design of the first of these is brought on by a need to work with two separate carrier types, and the need to avoid “dangerous instances” [3, §5.1].

The other two can be described as “mixin” typeclasses, and are motivated by a desire to avoid a combinatorial explosion of typeclass variations: an attempt at without mixins could easily end up needing all 16 variations of unital/non-unital commutative/non-commutative normed? star rings/fields. This motivation is largely a pragmatic one; the introduction of a tool like Coq’s Hierarchy Builder [7] to mathlib would eliminate the cost of manually authoring such an explosion of typeclasses.

4 Mitigation Strategies

4.1 Perform \(\eta \)-Reduction of Structures in the Kernel

A key difference between the type theory of Lean 3 and Lean 4 is that Lean 4 adds a kernel reduction rule that \(\eta \)-reduces structuresFootnote 7, which is precisely what we concluded we needed in Sect. 3.3. The following example demonstrates what this means:

figure bu

In essence, any value from a type is considered judgmentally equal to its constructor applied to its projections.

This feature was motivated by various “convenience” definitional equalities (as requested by [8]), such as wanting for an equivalence ; but in a thankful coincidence happens to be precisely the tool needed to resolve the trap in Sect. 3.2 that Lean 4 dropping support for “flat” structures would otherwise have ensnared us in. In particular, the Lean 4 version of the failing above succeeds.

Until 2023-02-22, the structure \(\eta \)-reduction rule was disabled in Lean 4 during typeclass search; both due to performance concerns, and an absence of any evidence that it was necessary in the first place. As evidence mounted [5], a compromise was reached to unblock the Lean 4 version of mathlib that allowed it to be temporary enabledFootnote 8 in places where there was no other choice but taking the performance hit. After some unification performance improvements which are out of scope for this paper, this behavior was turned on globally on 2023-05-16 [9].

Lean 4 is not the only language to have taken an experimental approach to structural \(\eta \); Coq supports it too, under the disabled-by-default option. In contrast, Agda enables it by default for typesFootnote 9, but allows it to be disabled via .

4.2 Use “Flat” Inheritance

The obvious approach to avoiding problems with “nested” inheritance is to simply not use it. Unfortunately, in the absence of elaborator support for translating a variation of listing 1 into listing 2a (such as in Lean 4) this would have to be done by hand, which can be rather tedious and error-prone.

There is however a trick; since the elaborator can translate listing 1b into listing 2b, we can construct a pathological graph such that all the edges we care about are forced to be “non-preferred”. We do this by adding an empty structure as the first base class of every structure, which ensures that the base classes always overlap (due to the field), and so the only “preferred” base class is the unused projection. The spanning tree of “preferred” base classes across all such typeclasses is a star with at its center, as shown in Fig. 3a.

This forces all the typeclass resolution to go through the “non-preferred” paths, which behave identically to their “flat” counterparts by unfolding to a constructor application.

Fig. 3.
figure 3

Alternate placements of the “preferred” spanning tree, with the diamond discussed in Fig. 2 overlaid in red (Color figure online).

Full size image

4.3 Carefully Select “Preferred” Paths

In Sect. 2.2, we mention that the choice of where to place the spanning tree of “preferred” paths could be optimized for performance. In light of Sect. 3.2, we could instead attempt to optimize to ensure that the problematic diamonds never arise. Indeed, there are many arrangements of the “preferred” paths in Fig. 1 that do not run into the specific example in Fig. 2c, such as Fig. 3b.

For our purposes, an adequate rule for why the red arrows of Fig. 3 commute but the ones of Fig. 2 do not is that the paths commute only if their last segments are either both “preferred” (as in Fig. 3b) or both “non-preferred” (as in Fig. 3a).

As discussed in [12] and visualized in Fig. 4, it is not in general possible to choose a spanning tree for a set of 8 typeclasses arranged in a cube, while simultaneously making the pairs of paths around each face commute. This can be adapted into a working solution by inserting extra nodes in the style of Sect. 4.2’s to force some additional paths to be “non-preferred”, but this is far from an elegant solution.

Fig. 4.
figure 4

An algebraic hierarchy where no spanning tree placement can ensure all squares commute, shown with one such inadequate spanning tree. The red paths highight the one square that does not commute. and are abbreviated from mathlib’s and (iative). (Color figure online)

Full size image

4.4 Ban Non-root Structures in Dependent Arguments

The problem in Sect. 3.2 is caused by a typeclass argument to a typeclass being inferable both via “preferred” and “non-preferred” routes. In Sect. 4.2, this can be worked around by ensuring every path is maximally “non-preferred”. An alternative is to ensure that every path is “preferred”, by only accepting typeclass arguments that appear as roots of the spanning subgraph. This could look like

figure cm

where each of the operators for R and M is taken as a separate typeclass argument.

This approach has two main downsides: it results in larger proof terms, because now it has 6 typeclass arguments instead of four, which have to be resolved all the way down to the smallest typeclass instead of stopping part-way along the graph; and it doesn’t extend to cases where not just the data fields carrying the operators on the type arguments, but also the proof fields carrying their properties, are needed to define the fields of the dependent typeclass.

5 Implications for Packed Structures

Up until this point we have focused only on typeclasses, as these are (at the time of this paper) the idiomatic way to represent algebraic structure in Lean. While Coq also supports typeclasses, and the previous examples can be faithfully reproduced in it, this is not the idiomatic way to do things in MathComp.

Instead, Coq’s “Hierarchy builder” [7, §4] generates “packed” structures [10] with a field for the type itself, rather than consuming the type as a parameter. These structures are then ineligible for typeclass search, but can be located automatically via “canonical structures” (or as they are known in Lean, “unification hints”) instead. These can in fact be built on top of the typeclasses from Sect. 2.1 or Sect. 2.2:

figure cn

A naïve encoding of a module in this packed view would be:

figure co

As has no parameters and is therefore not dependently-typed, it cannot fall afoul of the problem in Sect. 3.2.

Unfortunately, this encoding is effectively useless mathematically [18, §3]; we have no way to talk about two modules over the same ring without something involving equality of types and operatorsFootnote 10 like ; a much worse version of the duplicate fields described at the start of Sect. 2.2.

A more reasonable representation that avoids this problem is to only partially pack the structure, as

figure ct

which allows . This is roughly analogous to the approach taken in Coq’s MathComp [13] and in mathlib’s category theory library.

While this representation avoids the specific problem in Sect. 3.2 due to its type not depending on the path (the red arrows in Fig. 2), it is nonetheless dependently-typed. This make it vulnerable to an analogous problem where the diamond is instead formed by the path (the blue arrows in Fig. 2) after adding two new and nodes.

Fortunately for MathComp, the “Hierarchy builder” uses flat packed structuresFootnote 11, and so avoids these issues for the same reason that flat typeclasses do in Sect. 3.1.

6 Related Work

While this work is of course directly related to the work of porting Lean 3’s mathlib to Lean 4, the lessons here are transferable to Coq (where [7] seemingly correctly chose to use flat structures by coincidence) and Agda (which has adopted structure \(\eta \)-reduction globally due to other motivations [1]); even if only to provide further understanding of why the respective choices that have already been made in those systems are the correct ones. To the author’s awareness, no previously demonstrated algebraic motivations have been given for \(\eta \)-reduction in the kernel. Some in-depth analysis of “coherence” in algebraic typeclass paths is provided by [17, definition 3.3] (another name for our comparison in Fig. 2), but it does not provide an example to show why \(\eta \)-reduction specifically should be assumed.

The analysis in Sects. 3 and 4 is only relevant to systems that use dependent type theory, as concerns of equalities between the values of type parameters cannot arise in a language that does not permit those parameters in the first place. The Isabelle proof assistant which uses simple type theory is therefore immune to this class of problem; and at any rate [4, §5.4] advocates avoiding its record types entirely for algebraic structure, in favor of using locales.

Algebraic hierarchies certainly do not only exist in proof assistants; they are an essential part of computer algebra systems too. However, most computer algebra systems do not make use of dependent types [16, §1], with a notable exception being the Axiom Library Compiler, Aldor. Despite supporting dependent types, the type system of Aldor is too restrictive for Sects. 3 and 4 to be relevant. Aldor does not implement definitional equality of types (referred to as “value-equality” by [16, §2.4]), and so falls at a much earlier hurdle than the one in Sect. 3; it does not consider and to be the same type [16, §2.3], meaning that even Fig. 2b would be considered a mismatch, and every square in Fig. 4 would not commute.

This work focuses on how a seemingly innocuous implementation detail can be crucial to ensuring the success of existing approaches to algebraic hierarchies in dependently-typed proof assistants. The broader analysis of these hierarchies, and possible alternative designs (for which computer algebra systems can provide inspiration), is left to [3, 6, 7, 18].

7 Conclusion

In this paper we have shown that for the “nested” approach to multiple inheritance to be viable in the context of dependently-typed typeclasses or packed structures, either we have to severely restrict how such inheritance is used (Sects. 4.2 to 4.4), or the kernel of the theorem prover must implement \(\eta \)-reduction for structures (Sect. 4.1).

This scenario was a major stumbling block for mathlib’s transition from Lean 3 to Lean 4, as typeclasses of this form are used extensively in linear algebra. This paper provides a clear explanation of exactly what was going wrong, and a selection of various solutions that were considered before ultimately settling on the kernel change.

The code examples throughout this paper, along with translations into Lean 4 and Coq, and the version information needed to run them, can be found at https://github.com/eric-wieser/lean-multiple-inheritance.