Zulip Chat Archive

Stream: general

Topic: Using type classes in an extends clause


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 14 2020 at 10:13):

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

view this post on Zulip Mario Carneiro (Oct 14 2020 at 10:15):

old_structure_cmd doesn't handle dependencies between parents

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 14 2020 at 10:26):

Unfortunately that creates repetition where I was trying to eliminate it

view this post on Zulip Eric Wieser (Oct 14 2020 at 10:27):

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

view this post on Zulip Eric Wieser (Oct 14 2020 at 10:32):

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

view this post on Zulip Mario Carneiro (Oct 14 2020 at 10:35):

can you use a type alias?

view this post on Zulip 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.

view this post on Zulip 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: May 08 2021 at 03:17 UTC