## Stream: maths

### Topic: representations

#### Johan Commelin (May 09 2019 at 13:43):

What is going on here? I was playing around with representations together with @Ben McDonnell
After importing linear_algebra.basic a silly lemma broke at the bottom of the quoted code:

import algebra.module
import group_theory.group_action
import linear_algebra.basic -- this import breaks the commented lines at the end of the file

class group_module (G M : Type) [monoid G] [add_comm_group M]
extends mul_action G M :=
(smul_add  : ∀ (g : G) (m₁ m₂ : M), g • (m₁ + m₂) = g • m₁ + g • m₂)

namespace fixed_points
open mul_action
variables {G M : Type}
variable [group_module G M]

lemma add_mem (x y : M) (hx : x ∈ fixed_points G M) (hy : y ∈ fixed_points G M) :
x + y ∈ fixed_points G M :=
begin
intro g,
simp only [mem_stabilizer_iff, group_module.smul_add, mem_fixed_points] at *,
rw [hx, hy],
end

end fixed_points

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M]
extends group_module G M :=
(smul_comm : ∀ (g : G) (r : R) (m : M), g • (r • m) = r • (g • m))

namespace representation
open mul_action linear_map
variables {G R M : Type}
variables [group G] [ring R] [add_comm_group M] [module R M] [representation G R M]

-- set_option trace.class_instances true

-- lemma smul_mem_fixed_points (r : R) (m : M) (hm : m ∈ fixed_points G M) :
--   r • m ∈ fixed_points G M :=
-- begin
--   simp only [mem_fixed_points] at *,
--   intro g,
--   rw [smul_comm, hm],
-- end
end representation


#### Johan Commelin (May 09 2019 at 13:43):

Without the import the code runs fine. With the import it reports maximum type class error.

increase depth?

#### Johan Commelin (May 09 2019 at 13:44):

I couldn't figure out which type class it is even searching for. It performs a has_mul search and a mul_action search, and it finds those two instantly.

#### Johan Commelin (May 09 2019 at 13:44):

Bumping the depth to 100 didn't solve it.

#### Johan Commelin (May 09 2019 at 13:46):

@Mario Carneiro Any other ideas?

#### Johan Commelin (May 09 2019 at 13:47):

Modules work a lot better than half a year ago. But they are still pretty fragile, at least that's my impression...

#### Chris Hughes (May 09 2019 at 14:28):

Putting some brackets in lets you see the failing search. It's for has_scalar R M

#### Chris Hughes (May 09 2019 at 14:28):

lemma smul_mem_fixed_points (r : R) (m : M) (hm : m ∈ fixed_points G M) :
(r • m : M) ∈ fixed_points G M :=
begin
simp only [mem_fixed_points] at *,
intro g,
rw [smul_comm, hm],
end


#### Johan Commelin (May 09 2019 at 14:29):

Thanks @Chris Hughes

#### Johan Commelin (May 09 2019 at 14:29):

Now the question is... why does that import bork the class search

#### Mario Carneiro (May 09 2019 at 14:32):

is Ra discrete field?

#### Mario Carneiro (May 09 2019 at 14:32):

the tc looks for that a lot

Just any ring

#### Mario Carneiro (May 09 2019 at 14:33):

not exactly sure why... I mean it's directly looking for it

#### Johan Commelin (May 09 2019 at 14:33):

There is a module R M staring it in the face

#### Johan Commelin (May 09 2019 at 14:33):

Shouldn't be too hard to get a has_scalar R M from that.

#### Mario Carneiro (May 09 2019 at 14:33):

that's not all it's searching for

#### Mario Carneiro (May 09 2019 at 14:35):

it looks for has_scalar R M a bunch, discrete_field R a bunch more, and also discrete_field (M →ₗ[R] M)

#### Johan Commelin (May 09 2019 at 14:35):

That last one is obviously stupid...

#### Mario Carneiro (May 09 2019 at 14:36):

You misunderstand. This is not a garden path it's looking for, it's the initial problem

#### Johan Commelin (May 09 2019 at 14:37):

Hmmm... so how do we fix this?

#### Johan Commelin (May 09 2019 at 14:38):

Are we just hitting limitations of tc search?

#### Mario Carneiro (May 09 2019 at 14:38):

no, this is worse

#### Johan Commelin (May 09 2019 at 14:38):

Wow, ok. I still don't understand the problem

#### Mario Carneiro (May 09 2019 at 14:38):

it's searching for things that don't make any sense

#### Mario Carneiro (May 09 2019 at 14:38):

it needs has_scalar so that's all it should be looking for

#### Mario Carneiro (May 09 2019 at 14:39):

I don't know why these discrete_field problems are coming up

#### Mario Carneiro (May 09 2019 at 14:41):

oh! I started deleting your definitions beforehand and representation causes the problem

#### Mario Carneiro (May 09 2019 at 14:41):

of course, representation is a bad class

#### Johan Commelin (May 09 2019 at 14:42):

Huh, what's wrong with it?

#### Mario Carneiro (May 09 2019 at 14:42):

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M]
extends group_module G M


This creates an instance group_module G M <= representation G ?R M and lean gets lost at ring ?R

#### Mario Carneiro (May 09 2019 at 14:43):

you shouldn't extend something with fewer explicit type parameters

#### Mario Carneiro (May 09 2019 at 14:45):

it's pretty easy to fix:

class representation (G R M : Type) [monoid G] [ring R]
[add_comm_group M] [module R M] [group_module G M] :=
(smul_comm : ∀ (g : G) (r : R) (m : M), g • (r • m) = r • (g • m))


#### Johan Commelin (May 09 2019 at 14:46):

You know what this means, though

#### Johan Commelin (May 09 2019 at 14:46):

When a mathematician says: Let $G$ be a finite group, and let $V$ be a representation over a field $K$.

#### Johan Commelin (May 09 2019 at 14:46):

That all fits nicely on one line.

#### Johan Commelin (May 09 2019 at 14:47):

To turn that line into Lean, we all of a sudden need 25 type class assumptions. And only 3 or 4 of them are actually interesting.

#### Johan Commelin (May 09 2019 at 14:47):

Can we have extends'?

#### Mario Carneiro (May 09 2019 at 14:48):

If you need the totality of representations, then you should bundle M, or R or something

#### Johan Commelin (May 09 2019 at 14:48):

Sure, but I don't want that category, yet.

#### Mario Carneiro (May 09 2019 at 14:48):

well, with the parameters pulled out representation is a prop

#### Mario Carneiro (May 09 2019 at 14:49):

it's not quite saying the same thing as your one line

#### Johan Commelin (May 09 2019 at 14:49):

I want extends' that signals to Lean: "Hey, if someone writes variable [representation G R M], please add [add_comm_group M] [module R M] [group_module G M] yourself."

#### Reid Barton (May 09 2019 at 14:49):

you need lean' for extends'

#### Mario Carneiro (May 09 2019 at 14:49):

sebastian proposed that back in the stone age, I don't know what happened to that proposal

#### Johan Commelin (May 09 2019 at 14:56):

Hmmz... I'm really not so happy with stacking all these assumptions on top of each other.

#### Johan Commelin (May 09 2019 at 14:57):

@Mario Carneiro Do you see another solution, except for bundling?

#### Mario Carneiro (May 09 2019 at 14:57):

the problem is that if you describe your structure as data shared between objects then you potentially need one for every subset of objects in the context

#### Mario Carneiro (May 09 2019 at 14:59):

make fewer classes?

#### Johan Commelin (May 09 2019 at 14:59):

group_module is not just some random definition. They are pretty useful gadgets in their own right.

#### Mario Carneiro (May 09 2019 at 15:00):

okay but do you care about them right now?

#### Johan Commelin (May 09 2019 at 15:00):

Not exactly right now

#### Johan Commelin (May 09 2019 at 15:01):

But I somehow thought that refactoring it in later only made things harder

#### Mario Carneiro (May 09 2019 at 15:01):

on the contrary, I think it's best to refactor when you know what you want

#### Johan Commelin (May 09 2019 at 15:02):

Well, I do know that I want every representation to also be a G-module

#### Johan Commelin (May 09 2019 at 15:03):

Kevin has a student who is working on G-modules.

#### Johan Commelin (May 09 2019 at 15:03):

Ben wants to work on representation theory

#### Johan Commelin (May 09 2019 at 15:03):

It would be nice if their work was somewhat compatible at the end of the day...

#### Mario Carneiro (May 09 2019 at 15:05):

I assure you that having written down the definition group_module is nowhere near enough to ensure everyone's work is compatible at the end of the day

#### Johan Commelin (May 09 2019 at 15:05):

Ooh, I believe that.

#### Johan Commelin (May 09 2019 at 15:06):

I was just surprised that having written down two def's and two lemmas already brought the system to its knees

#### Johan Commelin (May 09 2019 at 15:06):

I now understand the error

#### Johan Commelin (May 09 2019 at 15:06):

I don't yet see a nice solution.

#### Mario Carneiro (May 09 2019 at 15:06):

the too many classes thing is a slow problem that won't get in your way in the immediate future, so I suggest you go with it for now

#### Sebastien Gouezel (May 12 2019 at 08:54):

you shouldn't extend something with fewer explicit type parameters

class normed_space (α : Type*) (β : Type*) [normed_field α]
extends normed_group β, vector_space α β :=
(norm_smul : ∀ (a:α) b, norm (a • b) = has_norm.norm a * norm b)


which seems to work pretty well?

#### Mario Carneiro (May 12 2019 at 09:36):

I am pretty sure you can also use that to cook up a bad typeclass search

#### Mario Carneiro (May 12 2019 at 09:36):

it's possible we just haven't run across it by accident yet

#### Mario Carneiro (May 12 2019 at 09:46):

Here's a bad typeclass search example:

import analysis.normed_space.basic

variables {α : Type} (a : α)
set_option trace.class_instances true

def normify : Type → Type := sorry
instance [field α] : normed_field (normify α) := sorry

#check -a


The reason we haven't come across this yet is because normed_field is pretty high in the hierarchy so there aren't many ways to get lower down yet. Here I've made up a perfectly normal instance for some made up normify operator that, in conjunction with normed_space, causes a loop that causes basically every typeclass search to overflow (like has_neg A here)

#### Patrick Massot (May 12 2019 at 10:00):

Mario, do you see a way to modify how type class search works that would solve this issue? Or is it the concept of type class itself that is irremediably broken and we should switch everything to unification hints?

#### Mario Carneiro (May 12 2019 at 10:02):

not typeclass search per se, but "prolog-like" needs some tweaking to make it not quite so stupid in some cases, i.e. loop detection and some forward inference

#### Patrick Massot (May 12 2019 at 10:03):

Is this something you could play with in the fork?

#### Patrick Massot (May 12 2019 at 10:04):

It's such a fundamental part of Lean that, to me, it looks much more important to fix than VM override or FFI or pretty much anything else

#### Mario Carneiro (May 12 2019 at 10:04):

possibly... It's a really hard problem in general though, and lots and lots of words have been spent on it, months of peoples' work can gone into proposals and alterations and no one has found that silver bullet yet

#### Patrick Massot (May 12 2019 at 10:05):

But prolog itself isn't so dumb, right? Why can't we look at what they do there?

#### Mario Carneiro (May 12 2019 at 10:06):

It's such a fundamental part of Lean that, to me, it looks much more important to fix

the problem with fixing fundamental things is that everything else has to adapt

#### Mario Carneiro (May 12 2019 at 10:06):

there is a high cost of switching and only a vague promise of something better on the other end

#### Patrick Massot (May 12 2019 at 10:07):

also it looks like this is not something that is currently worked on in the Lean 4 repository, so maybe there is hope to contribute some battle tested idea in this direction. Whereas things related to programming are clearly worked on by Leo and Sebastian, so everything done in the fork will be erased

#### Mario Carneiro (May 12 2019 at 10:07):

Prolog gives more mechanisms for being able to control how the search goes. For example you can say "no backtracking past this point"

#### Mario Carneiro (May 12 2019 at 10:08):

typeclasses are essential to lean. If you think you can sneak a change to it past leo I think you are mistaken

#### Patrick Massot (May 12 2019 at 10:08):

Who said "sneak"? Of course you don't want to sneak anything

#### Mario Carneiro (May 12 2019 at 10:09):

Meaning, you have to be working in conjunction with leo on the stuff

#### Patrick Massot (May 12 2019 at 10:09):

I wrote "contribute a battle tested idea"

#### Mario Carneiro (May 12 2019 at 10:09):

so unless he's interested in such a collaboration there's no chance of it happening in lean 4

#### Mario Carneiro (May 12 2019 at 10:09):

or if he does something himself

#### Mario Carneiro (May 12 2019 at 10:12):

also, nothing in the fork will be erased. I'm not sure exactly what will happen, but there is no way I am going to accept a regression like that

#### Mario Carneiro (May 12 2019 at 10:13):

"replaced with something better" is okay, "deleted with no alternatives" is not

#### Patrick Massot (May 12 2019 at 10:14):

Sure, you'll be able to continue using the fork if you want. But I guess most users will switch to Lean 4. And when I write "erased", I mean from the point of view of users. Nothing will be erased in the sense that the repository will still be there.

#### Patrick Massot (May 12 2019 at 10:15):

Leo doesn't have to care about that fork, he won't have to "delete" anything, he can simply and rightfully ignore it

#### Mario Carneiro (May 12 2019 at 10:16):

we still have to deal with integrating lean 4 and mathlib. That's not an easy task, and by the end of it we will probably know what the answer to this is

#### Mario Carneiro (May 12 2019 at 10:20):

Lean 4 promises to put a lot more into lean code that we can modify. If all the stuff in the fork is now in lean, then the contents of it can simply move to mathlib

#### Patrick Massot (May 12 2019 at 10:22):

I guess type class inference will stay C++ forever, it's a performance critical mission

possibly

#### Mario Carneiro (May 12 2019 at 10:23):

lean is compiled now, maybe it can be made to work

#### Mario Carneiro (May 12 2019 at 10:24):

I don't know if Lean 4 will ever be "open for business" as in accepting issues or PRs. It's really hard to tell if that was just a phase of lean 3 during the transition, or if that's the new normal

#### Mario Carneiro (May 12 2019 at 10:24):

but I think the fork has a reason to exist at least until that day

#### Kevin Buzzard (May 12 2019 at 12:10):

Leo told me

Sebastian and I have a few ideas on how to improve the typeclass inference procedure, but we didn't get there yet. We are currently working on the new compiler, parser and expander.

From what Mario says, the whole thing sounds extremely delicate.

Last updated: May 12 2021 at 06:14 UTC