Zulip Chat Archive

Stream: lean4

Topic: Class "inheritance"


Marcus Rossel (Nov 21 2021 at 09:19):

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 (Nov 21 2021 at 10:18):

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 (Nov 21 2021 at 15:11):

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 (Nov 21 2021 at 15:14):

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

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

attribute [instance] ID.toDecEq

Marcus Rossel (Nov 21 2021 at 20:22):

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 (Nov 21 2021 at 21:37):

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 (Nov 22 2021 at 09:31):

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 (Nov 22 2021 at 09:37):

I think that just changes the brackets in the constructor


Last updated: Dec 20 2023 at 11:08 UTC