Zulip Chat Archive

Stream: general

Topic: Using type classes in an extends clause


Eric Wieser (Oct 05 2020 at 16:31):

I'm finding that this code:

universe u

-- works fine without this
set_option old_structure_cmd true

/-- A semigroup is a type with an associative op. -/
class base_semigroup (G : Type u) (op : G  G  G) :=
(op_assoc' :  a b c : G, op (op a b) c = op a (op b c))

class mul_semigroup (G : Type u) extends has_mul G, base_semigroup G (*)

gives me the weird error

type mismatch at application
  @has_mul.mul G mul
term
  mul
has type
  G  G  G
but is expected to have type
  has_mul G

If I remove old_structure_cmd then it works fine.

Eric Wieser (Oct 05 2020 at 16:34):

Using (@has_mul.mul G ‹has_mul G›) doesn't help either, it still infers an object of the wrong type

Eric Wieser (Oct 14 2020 at 10:13):

Pinging this since I'm still curious what's going on here

Mario Carneiro (Oct 14 2020 at 10:15):

old_structure_cmd doesn't handle dependencies between parents

Mario Carneiro (Oct 14 2020 at 10:19):

What actually needs to go in that position is (@has_mul.mul G ⟨mul⟩), but it seems that the elaboration context is not correct to even allow you to write this

Mario Carneiro (Oct 14 2020 at 10:21):

the workaround is to do

class mul_semigroup (G : Type u) extends has_mul G :=
(op_assoc' :  a b c : G, (*) ((*) a b) c = (*) a ((*) b c))

instance mul_semigroup.to_base_semigroup (G) [mul_semigroup G] :
  base_semigroup G (*) := mul_semigroup.op_assoc'

which is what old_structure_cmd does anyway

Eric Wieser (Oct 14 2020 at 10:26):

Unfortunately that creates repetition where I was trying to eliminate it

Eric Wieser (Oct 14 2020 at 10:27):

But I suppose it does at least enable the generalization I was hoping for

Eric Wieser (Oct 14 2020 at 10:32):

For context, my motivation is needing two different group structures on the same type, (⋏) and (*)

Mario Carneiro (Oct 14 2020 at 10:35):

can you use a type alias?

Eric Wieser (Oct 14 2020 at 12:03):

No, because if I use

abbreviation mul_semigroup [has_mul G] := base_semigroup G (*)

then every user of mul_semigroup has to remember to provide has_mul explicitly.

Eric Wieser (Oct 14 2020 at 12:08):

(oh, unless you meant to make a ⋏ b = to_wedge a * to_wedge b, in which case yes, that was my backup plan)


Last updated: Dec 20 2023 at 11:08 UTC