typeclass

Stream: general

[Kenny Lau]

why does this have no problem:

class add_comm_monoid (α : Type u) extends add_monoid α, add_comm_semigroup α

class add_group (α : Type u) extends add_monoid α, has_neg α :=
(add_left_neg : ∀ a : α, -a + a = 0)

class add_comm_group (α : Type u) extends add_group α, add_comm_monoid α

but this gives me an error?

class has_upair extends has_zmem α :=
(upair : α → α → α)
(zmem_upair_iff_eq_or_eq : ∀ x y z, z ∈ upair x y ↔ z = x ∨ z = y)

class has_sUnion extends has_zmem α :=
(sUnion : α → α)
(zmem_sUnion_iff_zmem_zmem : ∀ x z, z ∈ sUnion x ↔ ∃ t, z ∈ t ∧ t ∈ x)

class has_sUnion_upair extends has_sUnion α, has_upair α

[Kenny Lau]

error:

invalid 'structure' header, field 'to_has_zmem' from 'zfc.has_upair' has already been declared

[Simon Hudon]

Why isn't α a parameter of has_upair and has_sUnion?

[Kenny Lau]

oh it's a variable I declared before

[Kenny Lau]

(sorry for not providing MWE)

[Simon Hudon]

Ah! I see! This is what is called diamond-shaped inheritance scheme. It causes you to inherit to_has_zmem multiple times which causes it to clash with itself.

[Simon Hudon]

(C++ programmers also know that as "diamond of death")

[Simon Hudon]

They have been carefully exorcised from the basic libraries

[Simon Hudon]

Is there a way to not make has_upair inherit has_zmem?

[Simon Hudon]

You could change:

class has_upair extends has_zmem α :=

into

class has_upair [has_zmem α] :=

[Kenny Lau]

then why does the first one work?

[Simon Hudon]

Good question. I wonder if that's because add_comm_monoid doesn't have fields. You can basically inline it in the extends clause of add_comm_group

[Simon Hudon]

If that's the case, you maybe could take advantage of it by splitting has_upair in two:

class has_upair_1 [has_zmem α] :=
(upair : α → α → α)
(zmem_upair_iff_eq_or_eq : ∀ x y z, z ∈ upair x y ↔ z = x ∨ z = y)

class has_upair_2 extends has_zmem α,  has_upair  α

I'm not sure if that would work but it might be worth a try

[Kenny Lau]

class has_sUnion_upair extends has_zmem α :=
(upair : α → α → α)
(zmem_upair_iff_eq_or_eq : ∀ x y z, z ∈ upair x y ↔ z = x ∨ z = y)
(sUnion : α → α)
(zmem_sUnion_iff_zmem_zmem : ∀ x z, z ∈ sUnion x ↔ ∃ t, z ∈ t ∧ t ∈ x)

instance has_sUnion_upair.to_has_sUnion [s : has_sUnion_upair α] : has_sUnion α :=
{ ..s }

instance has_sUnion_upair.to_has_upair [s : has_sUnion_upair α] : has_upair α :=
{ ..s }

[Kenny Lau]

this is what i did

[Simon Hudon]

The part I don't like about your solution is that I believe it forces you to duplicate the statement of your laws.

[Kenny Lau]

the part I don't like about your solution is that I would have to have has_zmem as my hypothesis each time

[Simon Hudon]

No. If you use has_upair_2, it comes with has_zmem

[Kenny Lau]

oh...

[Kenny Lau]

so your solution is basically like "distrib"

[Kenny Lau]

create a useless class that only has distributivity

[Simon Hudon]

You could say that

[Simon Hudon]

Actually, useless is not accurate: try commenting it out to see if it's useful

[Kenny Lau]

I mean distrib is useless in the sense that no mathematician cares about it

[Simon Hudon]

I think it's still useful. It might not be an interesting structure but for some theorems, you may only care about distributivity without a whole semiring

[Simon Hudon]

The same theorem or tactics could then be applicable whether you have a semiring or a distributive lattice

[Simon Hudon]

In the case of my solution, the has_upair_1 is more of a coding trick, you're right. I think it happens rarely enough that it's an ugliness we can live with. I would prefer if diamond shaped inheritance was supported properly but it has been ruled out for performance reason

[Mario Carneiro]

@Kenny Lau The original code works because it is using the old structure command to merge the fields together. People seem to be scared of anything marked "old" though, so if you want to recover this behavior with the new structure command, rather than creating a useless typeclass, you should extend has_upair and restate the axioms of has_sUnion, then construct a parent instance for has_sUnion (or vice versa).

[Kenny Lau]

so if I use old structure, everything will work?

[Mario Carneiro]

for some value of "everything"

[Kevin Buzzard]

I guess whether or not it will work in Lean 4 is another matter...

[Kevin Buzzard]

I guess the other thing is that presumably there was a reason the structure command was changed. Hmm, they might only be performance-related though.

[Simon Hudon]

I think they are. Leo considered the price to be too high despite C++ and Eiffel offering the feature with reasonable performances

[Andrew Ashworth]

eh, most large software projects have moved away from large inheritance trees

[Simon Hudon]

Have they? For performance reasons? I seem to remember it being a bottomless well of bugs in C++ because the design is kind of dumb. As far as I know, the feature is still in use in Eiffel code bases

[Andrew Ashworth]

not for performance, but because most people do inheritance wrong. this is the feeling i get from the places i've worked at with large code-bases

[Andrew Ashworth]

if you asked most people what the liskov substitution principle was they'd cross their eyes and wonder what you'd had for breakfast

[Andrew Ashworth]

well, that's a bit unfair, LSP is a bit jargon-ny, but the point is, it's easy to shoot yourself in the foot with misuse of inheritance

[Simon Hudon]

I think that's one reason Eiffel got inheritance right. Have you ever used it?