Class "inheritance"

Stream: lean4

[Marcus Rossel]

I want to define a type class that enforces DecidableEq as well as additional constraints on a given type.
Currently I've defined it this way:

class ID (α) where
  root : α
  decEq : DecidableEq α

instance ID.DecidableEq {ι} [ID ι] : DecidableEq ι := ID.decEq

Is there a nicer way of enforcing DecidableEq on α without externalizing the responsibility through [DecidableEq α]?

[Sebastian Ullrich]

I don't really understand your last sentence, but we do have actual inheritance via extends, which will declare the transitive instance automatically

[Marcus Rossel]

Sebastian Ullrich said:

I don't really understand your last sentence, but we do have actual inheritance via extends, which will declare the transitive instance automatically

By the last sentence I mean that I don't want to define ID as:

class ID (\alpha) [DecidableEq \alpha] where
  root : \alpha

... because then I would always need to include an explicit typeclass Decidable \alpha when using ID \alpha (right?):

-- I assume this doesn't work because 'DecidableEq \alpha' can't be synthesized:
variable (\alpha) [ID \alpha]

-- Instead I have to do:
variable (\alpha) [DecidableEq \alpha] [ID \alpha]

And I thought extends doesn't work with Decidable, since it is not a struct.

[Sebastian Ullrich]

Right, the rare class inductive... the closest code to extends should be

class ID (α) where
  [toDecEq : DecidableEq α]
  root : α

attribute [instance] ID.toDecEq

[Marcus Rossel]

Sebastian Ullrich said:

Right, the rare class inductive... the closest code to extends should be

class ID (α) where
  [toDecEq : DecidableEq α]
  root : α

attribute [instance] ID.toDecEq

That seems to work :grinning: Could you perhaps explain how it works? :upside_down:

[Kevin Buzzard]

What don't you understand? Giving ID.toDecEq the instance attribute makes it available to type class inference. Usually an instance is defined with instance foo : bar := ... and this is short for def foo : bar := ... + attribute [instance] foo. Here Id.toDecEq is defined as part of the class and right now there's no machinery for making it automatically an instance, so we have to do it afterwards.

[Marcus Rossel]

Ah ok, that solves one part of the mystery for me. What does the notation [toDecEq : DecidableEq \alpha] do on this case though?
That is, why the brackets?

[Kevin Buzzard]

I think that just changes the brackets in the constructor