Class vs structure

Stream: new members

[Joseph Hua]

What is the convention in mathlib for choosing between using structure and class when defining, say, a group? If i understand correctly class is just syntax for structure

[Damiano Testa]

As far as I understand, a class is a structure that you can assume in square brackets, e.g [my_class X], signaling Lean that it should find that assumption when you call that lemma, instead of having to provide it yourself.

[Joseph Hua]

oh so @[class] tells lean to internalise any instance of the class so we don't have to write out what the lemma proving the instance was called

[Bryan Gin-ge Chen]

There's a longer discussion in chapter 10 of #tpil: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

[Kevin Buzzard]

One big difference between class and structure is that classes are used in situations where most of the time you expect only one instance per class, and structures are used when there might normally be several instances. For example group G(the type of group structures on G) is a class because given a set/type G which is going to be a group, one would in general expect there to be only one group structure on G. On the other hand subgroup G (the type of subgroups of G) is a structure not a class, because in general it's completely reasonable to expect there to be more than one subgroup of G showing up in an argument, so you don't want to pick a "special" one.

[Kyle Miller]

Along the lines of what Kevin is saying, something that classes implement is the way we use synecdoche in mathematics. Synecdoche is a figure of speech where a part stands for the whole (like "nice wheels" to compliment someone's car) or vice versa. When we say "let $G$ be a group" we treat $G$ as if it were its underlying set, even though a group is actually a structure that includes the set. This is convenient because we can, for example, seamlessly treat $G$ as if it were a monoid, too, even though that's a different structure, because we can infer the intended structure. So, to implement this, we can translate "let $G$ be a group" to "let $G$ be a type that 'is' a group," where 'is' means "has an associated instance" (in code: (G : Type*) [group G]). This way, we refer to a group by its underlying type, and Lean fills in the rest.

By the way, you can make other things classes, not just structures. For example, here is an ill-advised thing that's possible:

attribute [class] nat

instance foo : ℕ := 37

def bar [h : ℕ] : ℕ := h

#reduce bar
-- results in 37