Confusion about type class syntax in mathlib

Stream: lean4

[aprilgrimoire]

Hi! In Theorem Proving In Lean, I got familiar with the concept of type classes. However, in Mathlib documentations, I see an unfamiliar syntax:

class SubringClass (looksS : Type u_1) (R : outParam (Type u)) [Ring R] [SetLike S R] extends SubsemiringClass S R, NegMemClass S R :

Prop

What's the Prop in the end doing? It seems like the output type of some function, but that doesn't make sense for a typeclass.

Thank you.

[Mario Carneiro]

the function in question is the class itself

[Mario Carneiro]

SubringClass is a function which takes a bunch of types and "returns" a proposition asserting that those types have the structure of a subring

[Mario Carneiro]

in general, type constructors are functions too, e.g. List is a function with the type List : Type -> Type, because List A is a Type given A : Type

[Mario Carneiro]

And class is just the same thing as @[class] structure, i.e. it's a data type constructor together with an annotation which makes it work with the typeclass inference mechanism

[Kyle Miller]

(The class keyword turns out to have some other effects too @Mario Carneiro, like it changes the binders for the self parameter for projections to be inst implicit, and it causes parent projections to become instances.)

[Mario Carneiro]

(that's not the only lie I wrote above)

[aprilgrimoire]

Thanks. That seems complicated, and I didn't see documentations for this feature. Also sometimes I see more complicated return types (for example, sort u) for type classes. How should I understand such declarations in mathlib4 documentations?

[Kyle Miller]

If you replace class with def and remove the extends SubsemiringClass S R, NegMemClass S R, the syntax would look familiar, right? It's saying what the resulting type of the type is.

The inductive command has similar syntax: https://lean-lang.org/doc/reference/latest//The-Lean-Language/The-Type-System/#inductive-declarations (it's described briefly in the second paragraph).

The section on structures doesn't yet mention it, but it's in the syntax description itself: https://lean-lang.org/doc/reference/latest//The-Lean-Language/The-Type-System/#structures

[Kyle Miller]

The syntax

class Foo (X : Type) where ...

is sort of short for

class Foo (X : Type) : Type _ where ...

By explicitly putting Prop there, you make sure it's a proposition. Instances of the class are proofs — they're proofs that are automatically inferred using the typeclass system.

(It's a small lie that it's like it puts Type _ there. It actually puts Sort _ there and then later decides whether to use Type _ or Prop based on some heuristics.)

[aprilgrimoire]

Thanks. What is an instance of a class? Is it a structure containing all the related functions needed to instantiate the type class? How does lean handle type coercion between universes? A Prop is also a Type _, right? So what's the point of putting Prop instead of Type _?