Notation for `algebra_map` / `algebra.of_id`

Stream: general

[Eric Wieser]

I've been finding myself writing algebra_map R _ an awful lot, and I was wondering if it would be sensible to introduce a notation for it? My proposal would be something like

local notation `↑ₐ`:max x:max := algebra_map _ _ x

(I also wonder which ofalgebra.of_id and algebra_map should be the canonical spelling)

[Johan Commelin]

Note that we can make the two _ _ implicit because of a marvellous change to Lean that was made about 3 months ago

[Johan Commelin]

That already makes things a bit better.

[Eric Wieser]

Using opt_params?

[Eric Wieser]

Alternatively, we could add instance [algebra R A] : has_coe_t R A := ⟨algebra_map R A⟩, as I suggested in PR 4824

[Johan Commelin]

That will be quite a refactor though

[Johan Commelin]

I think one reason we didn't do that was that before widgets it could be a pain to know what a coercion was doing. That reason is no longer valid...

[Reid Barton]

This sounds potentially rather dangerous--instances for variables are already bad plus anything involving coercions is a headache.

[Johan Commelin]

The headache got a lot less because of widgets, I think

[Adam Topaz]

But do you really want to rely on widgets ?

[Adam Topaz]

(asks the emacs user...)

[Reid Barton]

Figuring out which coercion Lean successfully applied is just one head of the Lernaean Hydra of headaches that is coercions.

[Reid Barton]

I think the original suggestion sounds good though.

[Sebastian Ullrich]

Reid Barton said:

Lernaean Hydra

At first I thought you had mashed up "learning Lean" into a new word...

[Anne Baanen]

Wouldn't it be nicer anyway for the pretty-printer to print (x : A) instead of ↑x?

[Anne Baanen]

(Perhaps writing (x : _) when A is too big and can be inferred from context.)

[Sebastian Ullrich]

Anne Baanen said:

Wouldn't it be nicer anyway for the pretty-printer to print (x : A) instead of ↑x?

That's an intriguing idea, I hadn't considered that before. Not sure if it should be the default. And the pretty printer can't really know whether the type is inferrable from context, I'm afraid.

[Mario Carneiro]

I think it could get annoying when you are trying to pretend the arrow doesn't exist

[Mario Carneiro]

but it definitely sounds like a useful option

[Jannis Limperg]

The (x : A) could be shortened, for big A, by folding A in the editor and revealing it on hover or something.

[Kevin Buzzard]

There's some option to turn those arrows off completely, right? It always sounds appealing but I'm just too scared to do it :-)

[Reid Barton]

I think the (x : A) form would be useful mostly for having something you can copy&paste back into Lean

[Kevin Buzzard]

Oh that's true! Coercion arrows are probably the most common reason (at least for me) for failure of round-tripping from the pretty printer back to the elaborator .

[Eric Wieser]

So it seems the choice is between:

• local notation `↑ₐ`:max x:max := algebra_map _ _ x, write ↑ₐr = a, and see ↑ₐr in tactic states
• has_coe_t, write ↑r = a or (r : A) = a, but deal with seeing only ↑r in the goal state until something changes in lean
• Do nothing, keep writing algebra_map R A r

[Mario Carneiro]

The reason the R and A are explicit in algebra_map is because lean will very often not be able to infer them

[Mario Carneiro]

so option 1 isn't an option

[Eric Wieser]

When algebra_map is invoked, the R can be inferred from the argument, right?

[Eric Wieser]

And for something like ↑ₐr = a, the A can be inferred from the RHS

[Mario Carneiro]

What's the type again? is it R -> A?

[Eric Wieser]

That, but bundled as a ring hom

[Mario Carneiro]

yeah, lean won't like that

[Eric Wieser]

Because it's bundled?

[Mario Carneiro]

that complicates matters a lot

[Mario Carneiro]

even without that you would get in trouble if you start nesting things, because both the input and output are unbound

[Mario Carneiro]

you probably know the outermost type (at the equality or what have you) and the innermost type (the variables) but everything in between is hazy

[Mario Carneiro]

and with a coe in the middle, you don't even know if the function is dependent

[Mario Carneiro]

and the typeclass to look up depends on the types that you are trying to determine

[Mario Carneiro]

so it's all very circular

[Johan Commelin]

@Mario Carneiro I don't agree. It used to be a lot of trouble, but Gabriel fixed it. In a similar context mv_polynomial.aeval now has the arguments R and A implicit, and it works fine in mathlib.

[Johan Commelin]

We used it a ton in the Witt project, and it works.

[Eric Wieser]

If the output is unbounded you can always use (↑ₐr : A)

[Mario Carneiro]

lean works outside in, recall

[Mario Carneiro]

so usually it's the input that is unbounded

[Mario Carneiro]

except at the lhs of an equality

[Eric Wieser]

We could use ↑ₐ[R] r notation too, if there need is there, although for the niche cases (↑ₐ(r : R) : A) is still shorter than algebra_map R A r

[Mario Carneiro]

The only real way to know is to try it out

[Mario Carneiro]

I'm not too fussed about notation, if the arrow makes you feel warm and fuzzy inside then go for it

[Eric Wieser]

Maybe I'll try the coe version first