notation conflict

[vzaliva]

There is notatoin conflict between extlib and standard library:

"` x : t <- c1 ;; c2" := bind c1 (fun x : t => c2) : monad_scope (default interpretation)
" `  t " := proj1_sig t : program_scope (default interpretation)

[liyishuai]

This was introduced in #93. @YaZko should we wrap this notation in a specific module so that it's not introduced by MonadNotation change this notation?

[vzaliva]

This is also related to DeepSpec/InteractionTrees#156

[YaZko]

Oh I did not think of this conflict with proj1_sig.
Afaik @alxest is the only user of this bind with cast annotation notation currently. We can either change the backtick for an unused token, or indeed export it in a specific module. The former would probably be better?

[liyishuai]

I agree on changing the notation. What token do you have in mind?

[Lysxia]

A crazy idea is to ditch the _ <- _ ;; _ notation(s) and use let* for everything:

let* x : t := c1 in
let* x := c2 in
c3

[YaZko]

I actually quite like it! But if we go this way we should still provide both styles of notations in two different modules I think.

I don't have a good head token in mind for the old style type-annotated one I must say.

[vzaliva]

I think the problem is with "breaking let". How would '(x,y) <- foo ;; bar would look in your let* notation?

[YaZko]

I'm not sure I see how that would be any different?

 Notation "let* pat := c1 in c2" :=
    (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))	
    (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.

Or am I missing something?

[vzaliva]

Sorry if this stupid question, I am not very experienced with defining notations.
So to answer my own question, would it be:

let* `(a,b) := foo in bar

The question is whether it would conflict with proj1_sig notation.

[YaZko]

I think you may be confusing two things. One thing is the ability to support notation to do deep pattern matching while binding in the style that Coq supports for its own let notation. The syntax for that is with a simple quote, and is achieved currently with:

Notation "' pat <- c1 ;; c2" :=
    (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))
    (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.

And can therefore be done the same way with the let* style. This notation has been there forever and does not conflict with anything.

The second thing is to support type annotations over the binder, which was added only recently. It is performed by:

Notation "` x : t <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x : t => c2))
    (at level 61, t at next level, c1 at next level, x ident, right associativity) : monad_scope.

It currently uses a backtick as syntax because the parser needs to be able to distinguish this notation from the others. This backtick is the one that conflict with the one from proj1_sig. So we are here discussing choosing a different head token for this case.
Alternatively, Li-yao is suggesting that moving to let* would help the parser avoid ambiguity, rather than having to introduce a different head token for each binding construct we have like is currently the case.

[vzaliva]

Thank you! Now I fully understand it. Why do we need backtick there at all? How about this:

Require Import ExtLib.Structures.Monad.
Require Import ExtLib.Data.Monads.OptionMonad.

Import MonadNotation.
Local Open Scope monad_scope.

Notation "'(' x ':' t ')' <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x : t => c2))
 (at level 61, t at next level, c1 at next level, x ident, right associativity) : monad_scope.

Definition foo (A:Type) (a: option A): option A
  := (x:A) <- a ;; ret x.

[alxest]

@YaZko Thanks for letting me know this issue!
@vzaliva That is neat, but it seems to have some conflict with existing notations.
Below are the problematic cases.

Check (let '(x, y) := (0, 0) in (x, y)).
Check ((fun '(x, y) => (x, y)): (nat * nat) -> (nat * nat)).
Check ('(x, y) <- (ret (0, 0)) ;; ret (x, y)).

[liyishuai]

@gmalecha Should we consider deprecating _ <- _ ;; _ notation in favor of let*?

[vzaliva]

Please do not drop existing monad notation! It is widely used and quite convenient. The problem I reported was with backtick, not the whole notation.

…

On Sun, Aug 16, 2020, 05:57 Yishuai Li ***@***.***> wrote: @gmalecha <https://github.com/gmalecha> Should we consider deprecating _ <- _ ;; _ notation in favor of let*? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#97 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAAVENO3DG5MAUGUXRG23JDSA7JSFANCNFSM4P3UIMEA> .

[liyishuai]

By "deprecating" I meant "prefer let*" rather than "removing". Users can avoid the conflict by importing MonadLetNotation, before MonadNotation is fixed.

[YaZko]

Yes the simplest solution is probably to offer two module, one called MonadNotation with the let* notation indicated as preferred, and one called MonadNotationLegacy with the current notations.
Then for the latter if someone has a good unicode to suggest instead of the backtick we can use it, but there's less pressure to avoid conflicts: if someone happens to have a conflict, they can prefer the let* notation.

[liyishuai]

Here's my plan:

• Rename current MonadNotation into MonadNotationLegacy, export both MonadNotationLegacy and MonadLetNotation in MonadNotation (Revert backtick notation in #93 #99).
• Ask dependants to either change Import MonadNotation into Import MonadNotationLegacy, or use the new let* notation.
• Remove Export MonadNotationLegacy from MonadNotation, to only include let*.

[liyishuai]

If HELIX has an OPAM release in coq-extra-dev, then ExtLib's CI will run tests to make sure our changes don't break HELIX.

[gmalecha]

This is the danger with notation.

This might sound curmudgeonly, but it seems odd to overhaul an entire system away from a standard convention used in many places simply to support a type annotation.

Personally, I think changing to let* everywhere is not a great idea for 2 reasons:

1. Haskell has made monad notation very standard, so keeping with it is a good idea in my mind.
2. let* has a meaning in lisp that is different than what it means here.

Given that we are aware of only one user of the backtick notation, I suggest that we remove that. It might be easy to express that with the infix >>= notation, e.g. c >>= fun '(a,b) : t => ....

I'm not sure the state of the let* notation, but perhaps moving it to a separate module would be a good idea.

[gmalecha]

It might also be reasonable to rename let* to letM or something like that which hints more strongly at monads, but that is just a taste thing.

[liyishuai]

Should we remove `let* notation (which has 0 users) as well?

[vzaliva]

I like the idea of new alternative let* notation. I am just not sure it should deprecate the existing one. As to backtick problem I think there is still a chance to make it work. We can try to play with priorities. P.S. As a side note I am not too worried about confusion with Lisp's let*. Galina is closer to OCaml that to Lisp and let* is now standard in OCaml.

…

On Sun, Aug 16, 2020, 18:37 Yishuai Li ***@***.***> wrote: Should we remove `let* notation (which has 0 users) as well? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#97 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAAVENJIKKSGHH3GNPOP7CLSBCCWPANCNFSM4P3UIMEA> .

[liyishuai]

Should we remove the backtick notations (#99) from the next release, until the solution gets finalized here?

[alxest]

For what it's worth (as the only user of the notation), I have no objection to removing it.
I am using it quite usefully (esp. it helps type inference && inserting coercion), but I can define it inside my project or replace it with what @gmalecha suggested.