Need help understanding a type class example

Stream: new members

[Kevin Cheung]

In the process of trying to understand the Nonempty type class definition, I constructed the following example which, a bit to my surprise, compiled:

class inductive Something where
 | oneThing : Something
 | anotherThing : Something

instance : Something := Something.oneThing

I am having a hard time understanding what the type class Something is about and what the final line with instance actually means. Any help or insight is greatly appreciated.

[Kevin Buzzard]

Do you understand

inductive Something where
 | oneThing : Something
 | anotherThing : Something

example : Something := Something.oneThing

?
Your code just that, plus "add these definitions to the typeclass inference system" (which is a big list of types which have the @[class] attribute and terms which have the @[instance] attribute). I'm just trying to establish which part you don't understand.

[Kevin Cheung]

I understand what goes on without the class and instance stuff. So the class is just syntactic sugar for [@class]?

[Kevin Buzzard]

Right! class and instance are just adding tags to declarations.

[Kevin Cheung]

Thank you. That helps.

[Kevin Buzzard]

And then the cool thing is that you can ask the typeclass inference system to come up with terms for you automatically. It's just another way of getting the system to fill in inputs to functions, like unification.

[Kevin Buzzard]

def foo (a : Nat) {b : Nat} [c : Nat] : ... means "when you're running this, let the user input a, get unification to solve for b and get the typeclass inference system to solve for c (and this will fail, because Nat isn't a class :-) ).

[Kevin Cheung]

It makes sense now. And I see that I can do something like the following:

instance instOne : Something := Something.oneThing

@[instance]
def instAnother : Something := Something.anotherThing

example [s : Something] : s = Something.oneThing ∨ s = Something.anotherThing := by
  rcases s with h | h
  . simp
  . simp

[Kevin Buzzard]

Here's an example which does work:

import Mathlib.Tactic

def foo (G : Type) [AddGroup G] : G := 0

#check foo ℤ -- works

Now foo wants the user to input a type, but then typeclass inference will supply the additive group structure on G. The #check works because somewhere in mathlib someone has written instance : AddGroup ℤ := <the group structure> so the typeclass inference system can find the instance and supply the input.

[Kevin Buzzard]

Kevin Cheung said:

It makes sense now. And I see that I can do something like the following:

instance instOne : Something := Something.oneThing

@[instance]
def instAnother : Something := Something.anotherThing

example [s : Something] : s = Something.oneThing ∨ s = Something.anotherThing := by
  rcases s with h | h
  . simp
  . simp

You can do this, but a lot of the system is set up under the assumption of "one instance per class", so this kind of code might cause problems down the line. For example, one would typically only have one AddGroup structure on a type (because otherwise + would be ambiguous) and this is why AddGroup is a class.