The notation "p ^" clashes with the infix "_ ^ _" in the standard library

[JasonGross]

These notations clash, even if they're in different scopes, which is annoying. The only way, it seems, to get these notations to work together is to declare "p ^" to be at the same level as " ^ ", which happens to be level 30. This breaks many other things, though...

[mikeshulman]

What does infix " ^ " mean?

[JasonGross]

In the standard library, we have

$ git grep ' \^ ' | grep Notation
interp/notation.ml:    let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in
plugins/setoid_ring/Algebra_syntax.v:Notation "x ^ y" := (power x y).
theories/Init/Notations.v:Reserved Notation "x ^ y" (at level 30, right associativity).
theories/Numbers/Cyclic/Int31/Cyclic31.v: Local Notation wB := (2 ^ (Z.of_nat size)).
theories/Numbers/NaryFunctions.v:Notation "A ^ n" := (nprod A n) : type_scope.
theories/Numbers/NatInt/NZDomain.v:Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).
theories/QArith/QArith_base.v:Notation " q ^ z " := (Qpower q z) : Q_scope.
theories/QArith/Qcanon.v:Notation " q ^ n " := (Qcpower q n) : Qc_scope.

In HoTT,

$ git grep ' \^ ' | grep Notation
coq/theories/Init/Notations.v:Reserved Notation "x ^ y" (at level 30, right associativity).
ssrplugin/theories-old/finfun.v:Notation "T ^ n" := (@finfun_of (finexp_domFinType n) T (Phant _)) : type_scope.

[mikeshulman]

In other words, "exponentiation". Okay, are we likely to be using these notations together?

[JasonGross]

Ah, yes, "exponentiation", sorry. The problem isn't that they are confused, but that the notation in Overture.v makes using "^" as exponentiation impossible. Coq sees "^" at level 3, discovers that it doesn't apply (or isn't in scope), and doesn't look for "^" at level 30. And I can't put " ^ " at level 3, because it's at level 30 in the reserved notations, and you can't put a notation in two different levels (even though you can put notations involving the same symbols at different levels). So if I, e.g., define "C ^ D" to mean "the category of functors from D to C", I can't use that notation if I've imported Overture.

[mikeshulman]

Can you just not use "C ^ D" for the functor category? (-:

[peterlefanulumsdaine]

I actually never quite came round to the change from !() to ()^ in the library. The latter is very pretty in short expressions, but becomes rather less readable than the former in long path-algebra: postfix operators tend to get lost at the end of lines, and in long piles of closing parens.

Also, ^ is much more often used as a binary infix operator, while ! is familiar as a prefix.

So one possible solution to the present issue would be to revert to the older notation !(_) throughout, if enough other people would support that.

(Although I realise -- I dont actually know/recall what were the reasons for switching to (_)^ in the Christmas rewrite were, so I may be missing some advantage of it here.)

-p.

Sent from my iPhone

On Jul 26, 2013, at 4:00, Jason Gross notifications@github.com wrote:

These notations clash, even if they're in different scopes, which is annoying. The only way, it seems, to get these notations to work together is to declare "p ^" to be at the same level as " ^ ", which happens to be level 30. This breaks many other things, though...

— Reply to this email directly or view it on GitHub.

[mikeshulman]

I think the goal was to suggest "^-1".

[JasonGross]

Why not use ^-1 to mean one thing in type_scope (or function scope or whatever), and another thing in path_scope?

[mikeshulman]

Because we want to have both of those scopes open at once.

[JasonGross]

If you bind path_scope to paths, it should work in most cases, except when you're trying to invert a path "at top level", like p ^ = p' or something (as long as the inversion is inside transport or something it'll work fine). (I would also be happy with !. I could also use [ , ] for functor category, but then I need to think about clashes with some other notations, such as F [ - , x ] (meant to be like F( - , x), applying F to x in the second component and getting back a functor on the first component).

[JasonGross]

Alternatively, if you wanted to use more Coq black magic, you could follow the workaround/suggestion I gave in https://coq.inria.fr/bugs/show_bug.cgi?id=3090 to make the notation ^-1 discriminate on the type of its arguments. I make use of this trick to use ↓ for the various comma and slice categories, and to use ∘ for the various composition and whiskering operators, as suggested in the HoTT book.

[mikeshulman]

I probably wouldn't use "^" anyway, since it reverses the order of its arguments versus all the other function-type operators like --> in type theory. What about just Fun A B?

[andrejbauer]

I would argue against any magic and to generally keep things simple. Let us not surprise users. By the way, Jason, how did you manage to use the HoTT library and the standard library at the same time?

[JasonGross]

That sounds reasonable. I do not use the full standard library, but the part of the standard library left in hoq includes declaring a level for, and reserving, the notation " ^ ". Perhaps I/we should go remove this reserved notation declaration? (Sorry if my use of "standard library" to refer to coq/theories/Init/Notations.v was confusing.)

[andrejbauer]

The reserved notations are there precisely so that users do not get any surprises, but if we have a good reason to violate that principle, we could. I never understood why p^ or p^-1 was any better than !p, though.

[mikeshulman]

Why did we change to p^ then? I don't remember being the advocate of it myself, although I suppose I could have forgotten. Anyway, it sounds like we should change back to !p.

[andrejbauer]

There are 35 forks of the HoTT library. Now is the time for all the lurkers to speak out, orelse we'll change inverse paths back to !p.

[Alizter]

It has been a while since this was discussed, can anybody offer anything new in this discussion?

At the moment we are in a position where a lot of the library is reliant on the notation ^ and it looks to be a great pain to go and change all of these to !.

Personally I am not a huge fan of ! since to me it suggests ¬ but I could be swayed otherwise. Are there any practical advantages to using ! since it is a prefix notation?

Otherwise, if everybody is content with ^ we should close this issue.

[mikeshulman]

Interesting that this old discussion seemed to have almost reached a conclusion but then no one did anything about it. I've gotten very used to ^ by now myself, and learned enough linear logic that prefix ! now suggests something very different to me, so I'd probably incline to keep it as-is now.

[Alizter]

I will close this issue as it seems unlikely to be changed.