Projecting Class Members

Stream: new members

[Yasmine Sharoda]

Hello, I defined a class with two members, a binary operation and a unit.

class PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

Now, when defining the homomorphism between two instances of the class, I find that a difference in accessing e versus op

structure pclasshom {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (PMClass.op x y) = PMClass.op (hom x) (hom y))

where qualifying e with the class name does not type check, and qualifying op with the instance name does not type check.
Worth saying, that when changing class into structure, they can both be qualified by the instance name.
So why do they behave differently?

[Yakov Pechersky]

Can you give an example of some statement that doesn't type check with the definitions as you have them?

[Mario Carneiro]

Since e does not have any explicit arguments:

#print PMClass.e
-- @[reducible] def PMClass.e : Π {m : Type} [c : PMClass m], m := ...

p1.e does not typecheck

[Adam Topaz]

One of the main points of using classes is so that you don't need to manually write things like p1.e. E.g.:

class PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

open PMClass

structure pclasshom {a : Type} {b : Type} [PMClass a] [PMClass b] : Type :=
 (hom : a -> b)
 (pres : hom e = e)
 (pres2 : ∀ x y : a, hom (op x y) = op (hom x) (hom y))

[Yasmine Sharoda]

Sure.. the following definition is not accepted

structure pclasshom {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (p1.op x y) = p2.op (hom x) (hom y))

And the following one too

structure pclasshom {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (PMClass.e) = PMClass.e)
 (pres2 : ∀ x y : a, hom (PMClass.op x y) = PMClass.op (hom x) (hom y))

[Yasmine Sharoda]

Mario Carneiro said:

Since e does not have any explicit arguments:

#print PMClass.e
-- @[reducible] def PMClass.e : Π {m : Type} [c : PMClass m], m := ...

p1.e does not typecheck

But p1.e actually typechecks, as in the pres axiom. p1.op is the one that doesn't.

[Yasmine Sharoda]

Adam Topaz said:

One of the main points of using classes is so that you don't need to manually write things like p1.e. E.g.:

class PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

open PMClass

structure pclasshom {a : Type} {b : Type} [PMClass a] [PMClass b] : Type :=
 (hom : a -> b)
 (pres : hom e = e)
 (pres2 : ∀ x y : a, hom (op x y) = op (hom x) (hom y))

Are there any more strong reasons to use one of them over the other?

[Adam Topaz]

If you don't use [PMClass a] you will always need to manually feed in the PMClass instance whenever you want to use pclasshom.

[Yasmine Sharoda]

Adam Topaz said:

If you don't use [PMClass a] you will always need to manually feed in the PMClass instance whenever you want to use pclasshom.

like you would normally do with other theorem provers? I am just asking as my scope is more of uniformity across different systems.

[Adam Topaz]

Actually, I'm a little surprised that this is okay:

structure PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

attribute [class] PMClass

structure pclasshom' {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (p1.op x y) = p2.op (hom x) (hom y))

But this is not:

class PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

structure pclasshom' {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (p1.op x y) = p2.op (hom x) (hom y))

[Adam Topaz]

I always thought that class foo ... was equivalent to structure foo .... + attribute [class] foo, but I guess there are some subtle differences.

[Yasmine Sharoda]

Adam Topaz said:

Actually, I'm a little surprised that this is okay:

structure PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

attribute [class] PMClass

structure pclasshom' {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (p1.op x y) = p2.op (hom x) (hom y))

But this is not:

class PMClass (m : Type) : Type :=
 (e : m)
 (op : m -> m -> m)

structure pclasshom' {a : Type} {b : Type} (p1 : PMClass a) (p2 : PMClass b) : Type :=
 (hom : a -> b)
 (pres : hom (p1.e) = p2.e)
 (pres2 : ∀ x y : a, hom (p1.op x y) = p2.op (hom x) (hom y))

Absolutely, there is something that needs investigation here.

[Mario Carneiro]

I always thought that class foo ... was equivalent to structure foo .... + attribute [class] foo, but I guess there are some subtle differences.

class foo is equivalent to @[class] structure foo, not structure foo ... attribute [class] foo. The difference is that the former has the opportunity to change the definitions of the fields

[Mario Carneiro]

Yasmine Sharoda said:

Mario Carneiro said:

Since e does not have any explicit arguments:

#print PMClass.e
-- @[reducible] def PMClass.e : Π {m : Type} [c : PMClass m], m := ...

p1.e does not typecheck

But p1.e actually typechecks, as in the pres axiom. p1.op is the one that doesn't.

It's not supposed to

[Mario Carneiro]

but there are some funny behaviors when projection notation is used on structure fields, I think lean gets confused and supplies it even though it makes no sense to

[Mario Carneiro]

class PMClass (m : Type) : Type := (e : m)

@[reducible]
def PMClass.e' {m : Type} [c : PMClass m] : m := PMClass.e

#print PMClass.e  -- def PMClass.e : Π {m : Type} [c : PMClass m], m
#print PMClass.e' -- def PMClass.e' : Π {m : Type} [c : PMClass m], m

variables {m : Type} [c : PMClass m]
#check c.e  -- ok
#check c.e' -- fail

[Mario Carneiro]

The square brackets means that you are not supposed to supply the value. If you want to supply the value, mark it as a structure, and then the projections will have c as an explicit argument

[Mario Carneiro]

or to supply the value at a particular application, use @, as in @PMClass.e _ c

[Jacques Carette]

Context: @Yasmine Sharoda and I work together - she's looking to have our theory generator produce Lean as well as Agda. The underlying question is "class or structure or both?" In a generative context, it's just as cheap to generate both than choosing (unlike in a human context, where such redundancy is quite painful). But to generate these, we need to know exactly what we should be generating!

So PMClass is really a short-hand for "the class version of Pointed Magma", whose homomorphisms are the same as monoid homomorphisms, and so a good test case for questions. Especially when oddities such as the ones documented above arise, making a proper exporter harder to write.

It might be worth starting a separate thread (where?) to discuss the general design, i.e what should (for example)

• a Monoid
• a Monoid homomorphism
• the 'term language' induced by a Monoid? [There are a host of variants of this]
• a product Monoid

all look like?

[Mario Carneiro]

a monoid should be a class, a monoid hom a structure, and a product monoid should be an instance

[Mario Carneiro]

the term language is probably an inductive

[Yasmine Sharoda]

Mario Carneiro said:

class PMClass (m : Type) : Type := (e : m)

@[reducible]
def PMClass.e' {m : Type} [c : PMClass m] : m := PMClass.e

#print PMClass.e  -- def PMClass.e : Π {m : Type} [c : PMClass m], m
#print PMClass.e' -- def PMClass.e' : Π {m : Type} [c : PMClass m], m

variables {m : Type} [c : PMClass m]
#check c.e  -- ok
#check c.e' -- fail

Actually I tried this code on the web interface and it did not accept it. It was accepted when the body of PMClass.e' became c.e.
There really is something different about instance resolution of constants versus unary and binary operations.. As I am looking to automatically generate code, I want to have a better understanding on how this work.
Maybe referring me to material on classes versus structures would be helpful.

[Mario Carneiro]

Note that PMClass.e and c.e are using the dot in two different ways. The first one is a namespaced name, and the second one is projection notation (once upon a time this was written c^.e and I think that still works, but . is overloaded for both meanings now).

[Mario Carneiro]

The difference is not about unary vs binary, it's about whether the field takes an argument of type m

[Mario Carneiro]

Do you have a link for the failed test? You might be running an old version of lean

[Mario Carneiro]

test

[Mario Carneiro]

Oh right, thanks to zulip you can also click "View in Lean community playground" in the top right of the code block

[Mario Carneiro]

With the original lean playground (the link scheme doesn't mix with markdown, but copy paste the below), which runs

#print lean.version -- (3,4,1)

you get a different bug relating to how lean treats elaborates structure fields differently. Here's a better test showing the difference on lean 3.4.1:

class PMClass (m : Type) : Type := (e : m)

@[reducible]
def PMClass.e' : ∀ {m : Type} [c : PMClass m], m := PMClass.e

#print PMClass.e  -- def PMClass.e : Π {m : Type} [c : PMClass m], m
#print PMClass.e' -- def PMClass.e' : Π {m : Type} [c : PMClass m], m

variables {m : Type} [c : PMClass m]
#check c.e  -- ok
#check c.e' -- fail

#check (PMClass.e : m)  -- fail
#check (PMClass.e : Π {m : Type} [c : PMClass m], m)  -- ok
#check (PMClass.e' : m) -- ok

[Yasmine Sharoda]

Mario Carneiro said:

Do you have a link for the failed test? You might be running an old version of lean

Here is the code that fails. Indeed it is version 3.4.1.. thanks for noticing that

[Mario Carneiro]

The lean community editor runs

#print lean.version -- (3,21,0)

btw

[Mario Carneiro]

3.4.1 is about 2 years old now

[Yasmine Sharoda]

Mario Carneiro said:

3.4.1 is about 2 years old now

Thanks for this clue.. as google takes one to the older interface.

[Mario Carneiro]

Just to be clear, what you are witnessing are (long-standing) bugs in lean, this isn't how implicit arguments are supposed to work

[Mario Carneiro]

One simple fix we often do is to restate axioms outside a structure, just like PMClass.e' here

[Mario Carneiro]

because the bug only occurs when you are referring to one of the fields themselves, not a wrapper definition around it

[Mario Carneiro]

But with the modern version, you only hit the bug if you do something you shouldn't be doing in the first place, which is to use projection notation on a variable of class type

[Mario Carneiro]

so it shouldn't cause problems for your code generation

[Yasmine Sharoda]

Mario Carneiro said:

But with the modern version, you only hit the bug if you do something you shouldn't be doing in the first place, which is to use projection notation on a variable of class type

Yes, now that I shifted to the right version, things make more sense.. projecting from a class uses namespace, while from a structure uses the instance name..
Are there any references comparing classes and structures that I can read to get more depth on that?

[Yasmine Sharoda]

Related to the same topic.. I get an error when projecting a class member in a function definition. I tried having a definition for op as suggested above but didn't help. Here is the code