## Stream: general

### Topic: Notation for algebra_map / algebra.of_id

#### Eric Wieser (Nov 11 2020 at 15:04):

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 (Nov 11 2020 at 15:08):

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

#### Johan Commelin (Nov 11 2020 at 15:09):

That already makes things a bit better.

#### Eric Wieser (Nov 11 2020 at 15:12):

Using opt_params?

#### Eric Wieser (Nov 18 2020 at 13:27):

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 (Nov 18 2020 at 13:28):

That will be quite a refactor though

#### Johan Commelin (Nov 18 2020 at 13:29):

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 (Nov 18 2020 at 13:33):

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

#### Johan Commelin (Nov 18 2020 at 13:36):

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

#### Adam Topaz (Nov 18 2020 at 13:36):

But do you really want to rely on widgets ?

#### Reid Barton (Nov 18 2020 at 13:46):

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

#### Reid Barton (Nov 18 2020 at 13:46):

I think the original suggestion sounds good though.

#### Sebastian Ullrich (Nov 18 2020 at 13:48):

Reid Barton said:

Lernaean Hydra

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

#### Anne Baanen (Nov 18 2020 at 13:49):

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

#### Anne Baanen (Nov 18 2020 at 13:50):

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

#### Sebastian Ullrich (Nov 18 2020 at 13:56):

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 (Nov 18 2020 at 14:03):

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

#### Mario Carneiro (Nov 18 2020 at 14:03):

but it definitely sounds like a useful option

#### Jannis Limperg (Nov 18 2020 at 14:06):

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

#### Kevin Buzzard (Nov 18 2020 at 15:12):

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 (Nov 18 2020 at 15:13):

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

#### Kevin Buzzard (Nov 18 2020 at 15:14):

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 (Nov 18 2020 at 15:17):

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 (Nov 18 2020 at 15:26):

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 (Nov 18 2020 at 15:27):

so option 1 isn't an option

#### Eric Wieser (Nov 18 2020 at 15:27):

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

#### Eric Wieser (Nov 18 2020 at 15:27):

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

#### Mario Carneiro (Nov 18 2020 at 15:28):

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

#### Eric Wieser (Nov 18 2020 at 15:28):

That, but bundled as a ring hom

#### Mario Carneiro (Nov 18 2020 at 15:28):

yeah, lean won't like that

#### Eric Wieser (Nov 18 2020 at 15:28):

Because it's bundled?

#### Mario Carneiro (Nov 18 2020 at 15:28):

that complicates matters a lot

#### Mario Carneiro (Nov 18 2020 at 15:29):

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

#### Mario Carneiro (Nov 18 2020 at 15:30):

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 (Nov 18 2020 at 15:30):

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

#### Mario Carneiro (Nov 18 2020 at 15:31):

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

#### Mario Carneiro (Nov 18 2020 at 15:31):

so it's all very circular

#### Johan Commelin (Nov 18 2020 at 15:31):

@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 (Nov 18 2020 at 15:32):

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

#### Eric Wieser (Nov 18 2020 at 15:32):

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

#### Mario Carneiro (Nov 18 2020 at 15:32):

lean works outside in, recall

#### Mario Carneiro (Nov 18 2020 at 15:33):

so usually it's the input that is unbounded

#### Mario Carneiro (Nov 18 2020 at 15:33):

except at the lhs of an equality

#### Eric Wieser (Nov 18 2020 at 15:33):

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 (Nov 18 2020 at 15:36):

The only real way to know is to try it out

#### Mario Carneiro (Nov 18 2020 at 15:37):

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

#### Eric Wieser (Nov 18 2020 at 15:47):

Maybe I'll try the coe version first

Last updated: May 15 2021 at 22:14 UTC