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