image by permutation power

Stream: maths

[Patrick Massot]

variables (α : Type) (g : perm α) (i : ℕ) (U : set α)
#check g '' U         -- set α
#check g^i             -- perm α
#check g^i '' U     -- maximum class-instance resolution depth has been reached

I tried adding various type annotations and parentheses, getting a variety of error messages but no luck

[Patrick Massot]

Trying (g^i) '' U is probably a better start

[Patrick Massot]

But then g is coerced to function too early

[Patrick Massot]

Is this related to the recent changes to powers?

[Mario Carneiro]

did you try ((g^i:perm α):set α) '' U?

[Kenny Lau]

but g^i isn't a set

[Patrick Massot]

He means (g^i : perm α) '' U : set α

[Patrick Massot]

That works indeed

[Mario Carneiro]

huh. You're right, that's nonsense, but lean is okay with it for some reason

[Patrick Massot]

Of course I tried (g^i : perm α) '' U

[Patrick Massot]

But didn't think of giving : set α at the end

[Mario Carneiro]

This is weird. Apparently the second type ascription isn't checked at all, the only important thing is that it's a function type so coe_fn is inserted

[Mario Carneiro]

#check ((g^i:perm α):_ → unit) '' U --ok

[Patrick Massot]

At least I can continue. But I'd be interested in a shorter way

[Patrick Massot]

wow

[Patrick Massot]

strange

[Patrick Massot]

#check (↑(g^i : perm α)) '' U also works

[Patrick Massot]

#check ↑(g^i) '' U also!

[Mario Carneiro]

#check ⇑(g^i) '' U

[Patrick Massot]

Do you understand what happens?

[Patrick Massot]

Actually I think it's not so far from stuff we already saw (but without me understanding enough to handle new instances of the problem)

[Mario Carneiro]

The explicit coercion gives no information to the expected type on the inside, so g^i : _ is inferred to g^i : perm A (usually it goes the other way around), so ⇑(g^i) gets the coe_fn instance for perm A which is A -> A, and it's simple from then on

[Patrick Massot]

And what happens when it does not work?

[Patrick Massot]

I mean when we don't help Lean at all

[Mario Carneiro]

Without a literal arrow, it first assumes the types match up. So (g^i) '' U : _ infers set ?B where g^i : A -> ?B (using U : set A). By the type of ^ we get g : A -> ?B and i : ?C which solves to i : nat and a coercion is inserted for g so ⇑g : A -> A. Finally, it tries to find has_pow (A -> A) nat and no such instance exists.

[Patrick Massot]

Thanks

[Patrick Massot]

Would it make any sense to try to define a coercion from perm X to set X -> set X and hope Lean would use that if I write g U or g^i U?

[Mario Carneiro]

The original instance resolution overflow is due to g^i '' U which by precedence quirks means g ^ (i '' U); it gets caught in a loop looking for has_coe_to_fun nat for some reason

[Patrick Massot]

Yes, I understood that bit

[Mario Carneiro]

No, coe_fn only takes one argument, the domain, unlike coe which has domain and target

[Patrick Massot]

Not sure why '' has higher precedence than ^ though

[Mario Carneiro]

so you can only coerce to one kind of function for a given object

[Patrick Massot]

What about using the general has_coe?

[Mario Carneiro]

it's way too underdetermined, I think

[Patrick Massot]

That's what I feared

[Mario Carneiro]

Any function can be treated as a set function by applying image

[Mario Carneiro]

it's basically just a functor

[Mario Carneiro]

and there are loads of those

[Kenny Lau]

I heard functor

[Patrick Massot]

Even without the perm layer, this f '' U notation is definitely the part of my file that looks further away from usual mathematical notation

[Mario Carneiro]

I know at least one math book which uses double open quotes as an infix operator for image

[Patrick Massot]

really?

[Mario Carneiro]

Takeuti-Zaring Axiomatic Set Theory :P

[Patrick Massot]

I guess it makes sense to have some kind of specific notation for beginners

[Patrick Massot]

I see

[Patrick Massot]

that kind of books

[Mario Carneiro]

I think it's more about unambiguous notation

[Mario Carneiro]

it's not a beginners book

[Patrick Massot]

It seems to be a set theory book

[Patrick Massot]

of course if you pretend to be serious when you say everything is a set then you need contortions everywhere

[Mario Carneiro]

Or if you pretend to be serious when you say everything you write is well typed

[Kevin Buzzard]

This is all (both Patrick's coercion issue and the weird '' notation) part of one underlying problem.

[Kevin Buzzard]

Mathematicians have developed a really good system for overloading notation

[Kevin Buzzard]

Patrick is exactly right about '' -- I've never seen it used to mean image so it doesn't surprise me that he hasn't, and it also doesn't surprise me that the only place Mario has is some set theory book (as opposed to what Patrick and I would call mathematics)

[Kevin Buzzard]

In maths the notation for the image of U under f : X -> Y is of course just f(U)

[Kevin Buzzard]

but I am well aware that life is not so easy in Lean

[Kevin Buzzard]

What the current fix seems to be is this exotic type class system plus clever coercions

[Kevin Buzzard]

I must be frank

[Kevin Buzzard]

I am not sure that it scales

[Kevin Buzzard]

I have seen problems with diamonds

[Kevin Buzzard]

I have seen problems with the wrong coercion being chosen

[Kevin Buzzard]

so my instinct is to

[Kevin Buzzard]

(a) give up type classes to a large extent

[Kevin Buzzard]

and (b) to give up on mathematician's overloading

[Kevin Buzzard]

With my schemes repo I've not made any attempt to do anything clever like this

[Kevin Buzzard]

If F is a sheaf then F is not the function on open sets, it's some other thing

[Kevin Buzzard]

and I have F.whatever_i_called_it for the function

[Kevin Buzzard]

It looks a bit messier

[Kevin Buzzard]

but I am coming round to the idea that it is not the end of the world to actually begin distinguishing between these things

[Kevin Buzzard]

In particular if I were writing the code Patrick is writing I simply would not attempt to identify the permutation, the bijection and the function

[Kevin Buzzard]

they would all be different notation

[Kevin Buzzard]

and I would not moan about ''

[Kevin Buzzard]

because f(U) doesn't really make sense

[Kevin Buzzard]

The reason for me is a practical one

[Kevin Buzzard]

I just want to write code that works

[Kevin Buzzard]

so I don't want to get bogged down with all the issues Patrick is running into just to make it look more like mathematics

[Sean Leather]

@Kevin Buzzard I think you should be sure that you're distinguishing between coercion issues and type class issues. I'm not sure they're the same.

[Kevin Buzzard]

You're right

[Kevin Buzzard]

but in some sense they are both solved by filling in the answers myself

[Kevin Buzzard]

and in all cases I know the answers

[Kevin Buzzard]

the issue is that they are both issues

[Kevin Buzzard]

and I don't want to be dealing with issues

[Kevin Buzzard]

and filling in the answers myself resolves them

[Kevin Buzzard]

I am very happy with how { H : blah} works

[Kevin Buzzard]

because if I have {U : set X} (OU : is_open U) then Lean is going to be able to guess what U is

[Kevin Buzzard]

but I am becoming more and more suspicious of user-added coercions

[Kevin Buzzard]

I cannot see a viable way of stopping different users creating loops

[Kevin Buzzard]

What if person X and person Y are both interested in widgets and foos

[Kevin Buzzard]

but one of them is more widgety

[Kevin Buzzard]

and one more fooey

[Kevin Buzzard]

so one has some coercion from widgets to foos

[Kevin Buzzard]

and the other a coercion from foos to widgets

[Kevin Buzzard]

and all of a sudden we have two pieces of incompatible code

[Kevin Buzzard]

user-added type class inference I guess I'm talking about here

[Kevin Buzzard]

but I am also avoiding has_coe_to_fun

[Kevin Buzzard]

and this more cautious approach solved a lot of problems for me

[Sean Leather]

I agree with what you're saying in a purely practical sense. However, I think it stems in general from Lean using elaboration (esp. but not solely via coercions and type-class instance resolution) to guess what you mean. It gets it right most of the time, but it's those few times that it doesn't that wind up frustrating you.

[Kevin Buzzard]

I think that what happened was that in these cases where it didn't work I first got completely stuck

[Kevin Buzzard]

and then I learnt how to unravel things in some cases

[Kevin Buzzard]

and then I got used to the unravelling

[Kevin Buzzard]

and then I figured unravelling wasn't so bad

[Patrick Massot]

I'm not convinced unraveling everything will scale

[Patrick Massot]

And, up to now, I've always been able to solve those kind of issue (well, Mario has always been able...)

[Patrick Massot]

And I'm very happy to see how it looks like now

[Patrick Massot]

Ok, it's summer here and I have a lot of maths to read. I'll be trying the IHES garden as a working place, without bringing a computer. See you. :sunglasses: