representations

Stream: maths

[Johan Commelin]

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₂)

attribute [simp] group_module.smul_add

namespace fixed_points
open mul_action
variables {G M : Type}
variables [monoid G] [add_comm_group M]
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]

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

[Mario Carneiro]

increase depth?

[Johan Commelin]

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]

Bumping the depth to 100 didn't solve it.

[Johan Commelin]

@Mario Carneiro Any other ideas?

[Johan Commelin]

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

[Chris Hughes]

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

[Chris Hughes]

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]

Thanks @Chris Hughes

[Johan Commelin]

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

[Mario Carneiro]

is Ra discrete field?

[Mario Carneiro]

the tc looks for that a lot

[Johan Commelin]

Just any ring

[Mario Carneiro]

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

[Johan Commelin]

There is a module R M staring it in the face

[Johan Commelin]

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

[Mario Carneiro]

that's not all it's searching for

[Mario Carneiro]

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

[Johan Commelin]

That last one is obviously stupid...

[Mario Carneiro]

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

[Johan Commelin]

Hmmm... so how do we fix this?

[Johan Commelin]

Are we just hitting limitations of tc search?

[Mario Carneiro]

no, this is worse

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

of course, representation is a bad class

[Johan Commelin]

Huh, what's wrong with it?

[Mario Carneiro]

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]

you shouldn't extend something with fewer explicit type parameters

[Johan Commelin]

Oh boy... that's really bad.

[Mario Carneiro]

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]

You know what this means, though

[Johan Commelin]

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

[Johan Commelin]

That all fits nicely on one line.

[Johan Commelin]

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]

Can we have extends'?

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

well, with the parameters pulled out representation is a prop

[Mario Carneiro]

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

[Johan Commelin]

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]

you need lean' for extends'

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

make fewer classes?

[Johan Commelin]

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

[Mario Carneiro]

okay but do you care about them right now?

[Johan Commelin]

Not exactly right now

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Ben wants to work on representation theory

[Johan Commelin]

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

[Mario Carneiro]

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]

Ooh, I believe that.

[Johan Commelin]

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

[Johan Commelin]

I now understand the error

[Johan Commelin]

I don't yet see a nice solution.

[Mario Carneiro]

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]

you shouldn't extend something with fewer explicit type parameters

What about the existing

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

Is this something you could play with in the fork?

[Patrick Massot]

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]

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]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

I wrote "contribute a battle tested idea"

[Mario Carneiro]

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

[Mario Carneiro]

or if he does something himself

[Mario Carneiro]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Mario Carneiro]

possibly

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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.