notation conflict about coq-ext-lib HOT 24 CLOSED

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?

from coq-ext-lib.

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.

from coq-ext-lib.

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?

from coq-ext-lib.

This is also related to DeepSpec/InteractionTrees#156

from coq-ext-lib.

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

from coq-ext-lib.

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

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

from coq-ext-lib.

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.

from coq-ext-lib.

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

from coq-ext-lib.

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?

from coq-ext-lib.

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.

from coq-ext-lib.

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.

from coq-ext-lib.

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

from coq-ext-lib.

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

from coq-ext-lib.

from coq-ext-lib.

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

from coq-ext-lib.

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.

from coq-ext-lib.

Here's my plan:

• Rename current MonadNotation into MonadNotationLegacy, export both MonadNotationLegacy and MonadLetNotation in MonadNotation (#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*.

from coq-ext-lib.

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.

from coq-ext-lib.

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.

from coq-ext-lib.

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.

from coq-ext-lib.

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

from coq-ext-lib.

from coq-ext-lib.

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

from coq-ext-lib.

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.

from coq-ext-lib.