Parsing problems with the PermutationReasoning combinators in Data.List.Relation.Binary.Permutation.Propositional

[jamesmckinna]

(micro-issue arising in the course of #2317 / #2311 )
UPDATED: two instances of what might be considered parsing 'bugs', but might merely be 'peeves'... but the first does seem to be a semantic failure of the current setup?

Suggest adding a comment in the definition of the combinators, or in the README to draw attention to this issue?
Or is there a 'better' definition which might help avoid these problems?

• On master, the reasoning step here makes a combination of a prep/'prefix' step with a use of shift reflected symmetrically; but if

      _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩

is replaced with

      _ ∷ (_ ∷ ws ++ _) <⟨ shift _ _ _ ⟨

then the parser complains...

• The step-swap combinator, defined as:

  -- Skip reasoning about the first two elements
  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
  step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))

  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z

seems to work in the handful of places in the library where it is used:

• defining shift
• defining drop-mid′
• defining drop-mid′
  but with some bracketing required, as well as only ever being used with refl as the intermediate step.

But attempting to deploy it in the associated README leads to the following unpleasant need for re-bracketing when trying to re-express example lem₂ using the combinator, as follows:

-- In practice it is further useful to extend `PermutationReasoning` with
-- specialised syntax `_∷_<⟨_⟩_` and `_∷_∷_<<⟨_⟩_` to support the
-- distinguished use of the `prep` and `swap` steps, allowing
-- the above proof to be recast in the following form:

lem₂ᵣ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
lem₂ᵣ = begin
  1 ∷ (2 ∷ (3 ∷ [])) <⟨ swap 2 3 refl ⟩
  1 ∷ 3 ∷ (2 ∷ [])   <<⟨ refl ⟩
  3 ∷ 1 ∷ (2 ∷ [])   ∎

Removing any of these brackets (or any other bracketing) seems to cause the parser to fall over.

[jamesmckinna]

(UPDATED) Eg. I tried the following:

  -- Skip reasoning about the first two elements
  step-swap′ : ∀ {x y} {xs ys zs : List A} ws → ws ≡ x ∷ y ∷ xs →
              (y ∷ x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → ws IsRelatedTo zs
  step-swap′ {x} {y} ws refl rel xs↭ys = ↭-go (swap x y xs↭ys) rel

  Step-Swap : ∀ {ys zs} (ws  : List A) → Set a
  Step-Swap {ys} {zs} ws@(x ∷ y ∷ xs) = (y ∷ x ∷ ys) IsRelatedTo zs → xs ↭ ys → ws IsRelatedTo zs
  Step-Swap {ys} {zs} ws@_            = ∀ {xs} → ws IsRelatedTo zs → xs ↭ ys → ws IsRelatedTo zs

  step-swap : ∀ {ys zs} (ws  : List A) → Step-Swap {ys} {zs} ws
  step-swap ws@(x ∷ y ∷ xs) rel xs↭ys = step-swap′ ws refl rel xs↭ys
  step-swap ws@(x ∷ [])     rel _     = rel
  step-swap ws@[]           rel _     = rel

  syntax step-swap ws ys↭zs xs↭ys = ws <<⟨ xs↭ys ⟩ ys↭zs

which works for the first two existing examples in the second point of the OP above, but not the third!

And the best I seem to be able to do for the README example is:

lem₂ᵣ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
lem₂ᵣ = begin
  1 ∷ (2 ∷ 3 ∷ []) <⟨ swap 2 3 refl ⟩
  1 ∷ 3 ∷ 2 ∷ []   <<⟨ refl ⟩
  3 ∷ 1 ∷ 2 ∷ []   ∎

Is there some strictness problem behind the scenes? Eg in failing to force evaluation of ws to a suitable pattern shape?

UPDATED: the third example succeeds provided I bracket the initial term, suggesting some sort of evaluation/strictness problem?

[JacquesCarette]

First thought: what's the precedence for all of these things?

[jamesmckinna]

Well, not exactly sure what you intend by that, but... if you refactor a bunch of proofs cf. #2317 , and then try to add a new one/observe the behaviour of the old ones in the light of other refactoring, and you... don't get the behaviour you've come to expect, then .., is that not noteworthy?

As to the matters at hand,

• I think we all believed the introduction of new syntax for the symmetric reasoning combinator would henceforth allow us/users to avoid explicit symmetry, but now there's a 'counterexample'...
• more generally, but specific to this context-of-use, the custom combinators for Permutation don't quite behave as nicely as we might hope... so again a question arises: can we go better?

So: perhaps not a 'bug', but surely noteworthy?

We don't have a label:ux (the main Agda issue tracker does) but I tag this one as precisely that: complex parsing is hard to debug and hard to develop an adequate mental model for as a 'non-expert' user, so paying attention to avoiding such anomalies seems... something to aim for...?

But happy to close if status:invalid. The behaviour is at least documented now...

[JacquesCarette]

You're legitimately confused because I wrote down the wrong word! Stupid fingers. I mean 'precedence' not 'precedent' !!! (Fixed now)

It was meant to be a purely technical suggestion to look at the low level parsing machinery. I wonder if (ab)using 'syntax' notations is going to get into weird corners as how exactly it gets desugared / parsed might not be all that well documented?

[jamesmckinna]

Thanks @JacquesCarette ! yes, I'm sure it is a low-level parsing thing, and/but despite my (ostensible!) credentials as a Computer Scientist (sic), I find that as a User, I simply can't hold the precedence tables in my head to figure ought what ought to happen to any given phrase, only to marvel when it works, and be frustrated when parsing is ambiguous, as seems to be the case here (which I am sure is to do with clashes in the syntax declarations between the use of ∷ in the combinator notation (infixr 2), _∷_ in the pattern bindings, and _∷_ in the expressions being matched against (each infixr 5)).

Apologies for the tantrum-as-issue, but this kind of thing is... exasperating, and I realise I don't have the wherewithal to fix it on my own... boo-hoo! 😭

[MatthewDaggitt]

The cause of the first point is very simple. We don't simply don't define the symmetric version of _∷_<⟨_⟩_ which explains why _∷_<⟨_⟨_ doesn't parse!

[MatthewDaggitt]

In the second point, you can remove half the brackets:

lem₂ᵣ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
lem₂ᵣ = begin
  1 ∷ (2 ∷ 3 ∷ []) <⟨ swap 2 3 refl ⟩
  1 ∷ 3 ∷ (2 ∷ [])   <<⟨ refl ⟩
  3 ∷ 1 ∷ 2 ∷ []     ∎

but I agree you can't remove the other two pairs....

[MatthewDaggitt]

Okay so yes the fundamental problem is that the combinators don't interact right when you've got a real List._∷_ in the expression. The problem is the parser is not type-directed so when you have a long string of ∷s in a row, it's ambiguous about which one to make into the ∷ for the combinator.

So I think these two operators are fundamentally broken as is. There are a few options:

1. We can rename the ∷ in the reasoning operator syntax. I'm not sure what we'd rename it to...
2. We can do nothing but add a comment saying that this syntax doesn't interact properly with List._∷_
3. We can deprecate this syntax entirely.

To be honest I'd probably vote for option 3. To me Option 1 of changing the ∷ symbol undermines the entire point of the combinators. Option 2 seems like its just setting users up to fail. Furthermore while the step syntax is okay-ish, the swap syntax has never made much sense to me.

[jamesmckinna]

@MatthewDaggitt thanks for the penetrating analysis/diagnosis (of both problems; but the first is pure 🤦 for me), as well as a lucid account of possible ways to proceed.

I definitely agree with you about options 1, and 2, and that's perhaps why I found myself experimenting with the Swap-Step/swap-step reimplementation, because at least that removes the overloading of the symbol in the syntax, in favour of achieving the 'same' pattern-matching behaviour in the semantics of the rule (and which does permit the elimination of 1 additional parenthesis pair in lem₂ᵣ... ;-)). Part of doing those experiments was as a warm-up to trying to think up a better way to deploy shift in PermutationReasoning via a suitable combinator (it's almost always followed by an appeal to an equality, rather than another permutation, so there's a generality/abstraction code-smell there; but also, the underlying function doesn't seem to quite do enough heavy lifting, so I'd been playing with how to find a sweet spot in that design space... for another time!), but I got bogged down trying to 'fix' the existing ones...

Overall I think I'd be OK with deprecating the swap-step syntax, not least because its gets very little use, and only ever with the refl inner step for transitivity (Fairbairn again!), but it seems like a potentially good downstream project for someone to come up with a 'better' set of Permutation reasoning combinators. But are you also suggesting deprecating the prep syntax as well?

Meanwhile, who's going to handle the deprecation? (I think I've forgotten how to deprecate syntax declarations, but I seem to recall it's fiddly...?)

[MatthewDaggitt]

But are you also suggesting deprecating the prep syntax as well?

Yes as its equally broken.

Meanwhile, who's going to handle the deprecation? (I think I've forgotten how to deprecate syntax declarations, but I seem to recall it's fiddly...?)

It's not fiddly so much as impossible. We can and should attach a WARNING to the original definition used in the syntax, but last time I checked that doesn't cause it to fire when you use the syntax? Otherwise, we just say that the definition is deprecated and that people can't shouldn't use it. Less than ideal, but at some point in the future Agda might get updated so that we can attach the warnings to the syntax....

[JacquesCarette]

Now I've caught up with all of this, and I agree that

syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z

is fundamentally broken -- there is really no sane way for Agda to know what you mean here.

One could consider replacing ∷ with ::: for option 1. It's not pretty, I agree, but it would work. If this syntax is deprecated, what would the reasoning step look like without any syntax? [I'm not against deprecation, I'm just wanting to explore the possibilities a bit more first.]

[jamesmckinna]

Re: "fundamentally broken", I agree, but I do nevertheless claim that the Swap-Step/swap-step approach does correctly play well with pattern matching (because ws on the LHS of the syntax is unconstrained, it's up to the type-checker to resolve it to the right 'shape', but yes, parsing still gets in the way, so sometimes extra brackets are required).

[MatthewDaggitt]

While I agree that type-checking is fine, I feel the extra brackets add severe levels of bafflement, as evidenced by your original question!

I can easily imagine people in future playing with the same sort of expressions also reporting it as a bug...

[jamesmckinna]

Fair point! I'll continue to experiment as part of #2317 and perhaps #1761 but willing to give way at this stage...

[jamesmckinna]

#2333 removes all uses of these combinators... apart from their (modest!) use in Data.Nat.Primality.Factorisation... but still a potential refactoring opportunity...