Zulip Chat Archive

Stream: new members

Topic: Need help understanding a type class example


Kevin Cheung (Sep 18 2024 at 10:20):

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 (Sep 18 2024 at 10:39):

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 (Sep 18 2024 at 10:41):

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

Kevin Buzzard (Sep 18 2024 at 10:42):

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

Kevin Cheung (Sep 18 2024 at 10:42):

Thank you. That helps.

Kevin Buzzard (Sep 18 2024 at 10:42):

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 (Sep 18 2024 at 10:44):

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 (Sep 18 2024 at 10:45):

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 (Sep 18 2024 at 10:46):

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 (Sep 18 2024 at 10:48):

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.


Last updated: May 02 2025 at 03:31 UTC