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

[jsodd]

Why docs#MeasureTheory.Measure and docs#MeasureTheory.OuterMeasure are structures, whereas docs#MeasureTheory.ProbabilityMeasure is a subtype? If type classes are ways to group types together, shouldn't it also be a structure?

[Yury G. Kudryashov]

We used to use subtypes more in the past, and some types didn't migrate to structures yet.

[Yury G. Kudryashov]

The main benefit of using a subtype is that you can reuse lemmas about Subtype, but we try to establish API anyway, so it makes sense to migrate probability measures to structures.

[Yury G. Kudryashov]

Note that most of the probability theory in Mathlib is done for (μ : Measure _) [IsProbabilityMeausre μ], not a bundled ProbabilityMeasure.

[jsodd]

@Yury G. Kudryashov Thanks for the explanation! If I wanted to introduce some standard classes of probability measures, such as Gaussian measures on finite and infinite dimensional spaces, Levy measures and so on, what would be the best approach? Using classes, structures or subtypes?

[Yury G. Kudryashov]

For continuous distributions, see docs#ProbabilityTheory.gaussianPDFReal and docs#ProbabilityTheory.gaussianReal for an example.

[jsodd]

This is just one parametric family of univariate distributions. In this case it is clear that just defining it as one function is enough. General Gaussian measures are much richer and it would be fair to call them a "class", which is why I ask what is the right way to set up things like this.

[jsodd]

It's just that from my point of view, the difference between defining something as a class or a structure is more or less clear to me from these discussions (class = structure with implicit type argument, which is supposed to be inferred from the context, right?), but the benefits of preferring classes/structures over subtypes is not.

[jsodd]

By the way, it seems technically possible to use classes as structures through @. I guess the guideline for choosing between the two should be "if you find yourself in need of using @ with a class, then it should be a structure`.

[Jireh Loreaux]

This is not the distinction between class and structure. The correct distinction is that instances of classes (you can't have one for a structure) can be inferred automatically via type class synthesis. This is what allows, for example, the lemma docs#mul_one to be applied to solve x * 1 = x when x : 𝕜 and where there is a [Field 𝕜] instance in context, despite the fact that there is no mention of docs#Field in docs#mul_one. (but there is a chain of instances from Field to MulOneClass.)

[Jireh Loreaux]

Also, any instance of a class should be (essentially) unique modulo the explicit parameters to the type on which the instance is placed. In contrast, you can have as many defs of a structure as you want on the same type.

[Jireh Loreaux]

For instance, docs#Int should only have one docs#LinearOrderedCommRing instance (docs#Int.instLinearOrderedCommRing), but it could potentially have many docs#Subgroup.

[jsodd]

Jireh Loreaux said:

should be (essentially) unique

What's the modality of this "should be"? Does it mean that it's bad practice and misuse of classes? Because it seems that it's possible to define many, is it not?

[Ruben Van de Velde]

Bad practice, yeah

[Kyle Miller]

Sometimes the bad practice is acceptable, because it's too inconvenient to do it right. For example, there can be multiple topological space structures on the same type, and the type TopologicalSpace X is an interesting type on its own, with interesting and useful theory. Ideally when you work with the type as a mathematical object it would be a structure, but outside this part of the theory you want it to be a class — you want to work with X and have the TopologicalSpace structure be automatically associated to it. But, inside the theory you're breaking the rule that there should only be one instance per X.

[jsodd]

Okay, I see. But what about subtypes? Using the example from above, docs#MeasureTheory.ProbabilityMeasure is a subtype, docs#MeasureTheory.Measure is a structure. Why prefer structures to subtypes?

[Eric Wieser]

Subtypes are themselves just structures

[jsodd]

The more I compare what is a structure and what is a class in the library, the more I feel lost despite all the great explanations I've received above. If the notion of a class is for making instances, why docs#ProbabilityTheory.IsMarkovKernel is a class but docs#ProbabilityTheory.ProbabilityMeasure isn't? On one side it's perfectly common to have many Markov kernels in a given context, but on the other the notion of "markov-kernelness" is one and only and there's no way to change it. Shouldn't ProbabilityMeasure be a class for the same reason?

[Yury G. Kudryashov]

IsMarkovKernel is a typeclass saying that a given docs#ProbabilityTheory.Kernel is a Markov kernel. Lean will automatically find an instance of this class in the environment and use it as needed. There can be more than one ProbabilityMeasure on a type, so this is not a class. OTOH, docs#MeasureTheory.IsProbabilityMeasure is a class.

[Yury G. Kudryashov]

And most of the probability theory code in Mathlib deals with (μ : Measure _) [IsProbabilityMeausre μ]