Zulip Chat Archive

Stream: general

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


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 11 2020 at 15:09):

That already makes things a bit better.

view this post on Zulip Eric Wieser (Nov 11 2020 at 15:12):

Using opt_params?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 18 2020 at 13:28):

That will be quite a refactor though

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 18 2020 at 13:36):

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

view this post on Zulip Adam Topaz (Nov 18 2020 at 13:36):

But do you really want to rely on widgets ?

view this post on Zulip Adam Topaz (Nov 18 2020 at 13:37):

(asks the emacs user...)

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 18 2020 at 13:46):

I think the original suggestion sounds good though.

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Anne Baanen (Nov 18 2020 at 13:50):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 14:03):

but it definitely sounds like a useful option

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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 .

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:27):

so option 1 isn't an option

view this post on Zulip Eric Wieser (Nov 18 2020 at 15:27):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 15:27):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:28):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 15:28):

That, but bundled as a ring hom

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:28):

yeah, lean won't like that

view this post on Zulip Eric Wieser (Nov 18 2020 at 15:28):

Because it's bundled?

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:28):

that complicates matters a lot

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:31):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:31):

so it's all very circular

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 18 2020 at 15:32):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 15:32):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:32):

lean works outside in, recall

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:33):

so usually it's the input that is unbounded

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:33):

except at the lhs of an equality

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:36):

The only real way to know is to try it out

view this post on Zulip 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

view this post on Zulip 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