Number of instances of a type class

Stream: new members

[VayusElytra]

Hi, I read this sentence in mathematics in Lean and am very curious what it means: "the type class system assumes every type has only one instance of each type class".
How does the type class system deal with sets which can have multiple of a certain structure then?

[Paul Rowe]

Typically the answer is that a type synonym is introduced. The idea is you "wrap" the type with something to create a new type. Then APIs are introduced to allow you to view elements of the type however you need. Take a look at docs#Lex and stuff around it to see how it works for putting a lexicographic order on, say, a product type.

[Chris Bailey]

It looks like the passage clarifies right after by giving the example that additive and multiplicative structures are implemented separately and harmonized later.

I would probably have expressed the idea differently; you can declare more than one instance of a class for a given type, but only one instance is actually "picked" during resolution, or you specify which one you're talking about manually.

[VayusElytra]

Makes sense, thank you both. How does one specify this in practice?

[Chris Bailey]

Anywhere an "inst impliclt"/typeclass parameter appears, you can choose to specify what you want instead of having Lean do it for you (either via named args or by exposing all implicits with @) like so:

def foo {A : Type} [myInhabited : Inhabited A] := myInhabited.default

instance instInhabitedNat0 : Inhabited Nat where
  default := 0

instance instInhabitedNat1 : Inhabited Nat where
  default := 1

-- 0
#eval foo (myInhabited := instInhabitedNat0)
-- 1
#eval @foo Nat instInhabitedNat1

In practice with complex classes that express structure this gets very messy, which I think is part of the motivation for implementing them separately as the author describes. There are also practical issues like the operation for Group being a field and not a parameter, but I think that gets into stuff that the mathlib people or someone who has more intimate knowledge of those design decisions would be better able to speak to.