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> .