Classes

Making groups; learning about classes

Here are some of the gory details. This is technical, and maybe you don’t need to know it.

In sheet 1 of the groups section, we make groups from scratch, by writing down the axioms of a group and making a “class” called mygroup G (not to be confused with group G, which is the “official” definition of a group in Lean’s maths library). So what is a class, and how do classes work?

A class is a structure which is tagged with the class attribute. A structure is a kind of inductive type with only one constructor. An inductive type is a way to make new types in Lean. So let’s start at the beginning with an explanation of the inductive type involved.

If (G : Type) is a type, then the idea is that we want one object which is going to do all the “group” stuff on G, and turn G into a group. This one object will thus be a collection of eight things. It will be a multiplication on G, an identity element, an inverse function G → G, and also proofs of the five group axioms (associativity, left and right identity, left and right inverse). This one object is a term of type mygroup G, where mygroup G is defined as in sheet 1 of the groups section.

But now think about how mathematicians use groups. They say “a group is a set G equipped with a bunch of data satisfying some axioms” but then they don’t say “let’s call this data (and the proofs of the fact that the data satisfies the axioms) X”. They say “let’s not give this data a name, let’s just say things like ‘G is a group’ even though really G is a set”. They’re saying “let G be both the set and the set-with-all-the-group-structure”.

In Lean this is how we do it too. Here G is a type, not a set, and then we have a term _inst_1 : mygroup G which is all the group data, but we are going to put this term into Lean’s typeclass inference structure, by using square brackets [_inst_1 : mygroup G], and in fact we are not even going to name the term, we’re just going to be writing [mygroup G]. Then when we see (g : G) this just means that g is a term of type G, but when we see g * g something magic is happening; Lean sees that we are trying to use a multiplication on the type G, and multiplication is a class, so Lean looks up G in its typeclass system and asks if there are any terms there which give G a multiplication, and then _inst_1 pops up and says “oh yeah, I’m a group structure on G so I contain a bunch of stuff, including a multiplication; use that”.

You can see this secret storage of all the group data and proofs if you look at Lean’s tactic state in the middle of a group theory proof. For example, if you click in the middle of the proof of inv_mul_cancel_left in groups sheet 1, you can see that the tactic state is

G : Type
_inst_1 : mygroup G
a b :  G
⊢ a⁻¹ * (a * b) = b

That _inst_1 is something you never need to mention, the typeclass system is taking care of it. All theorems about groups you need will magically apply to G because the typeclass inference system knows about _inst_1 and will use it whenever necessary (e.g. when you want to invert an element, or apply an axiom from group theory).

What’s the difference between a class and a structure?

With classes, the idea is that a “magic” system which we don’t have to think about (Lean’s typeclass system) finds the terms for you. Here is an example where you do not want this to happen! Say we’re proving theorems about subgroups of a group G. We have two subgroups, and maybe we want to intersect them and prove that this is a subgroup too. If we had made subgroups into a class, then it would be the job of the magic system to supply a term of type subgroup G from its list, and there will only be one possible term on the list (that’s how the system works). So it’s going to be really hard to talk about more than one subgroup of G at once; Lean will keep saying “here, I have the subgroup, use this”. Groups can have more than one subgroup, so subgroups are a structure.

In contrast, when we say “let G be a group”, then 99.9 percent of the time that group structure on G will be one fixed group structure, and it’s never going to change in the middle of a mathematical argument. So groups are a perfect example of a class – we give the magic system G and we say “please find me a multiplication on G” and the system says “oh I have exactly one group structure on G right here, you can use the multiplication from that”. A type will 99.9 percent of the time have exactly one group structure, if it has one at all, and so this is why group is a class.