Open jamesmckinna opened 5 months ago
(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?
First thought: what's the precedence for all of these things?
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,
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...
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?
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! :sob:
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!
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....
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:
∷
in the reasoning operator syntax. I'm not sure what we'd rename it to...List._∷_
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.
@MatthewDaggitt thanks for the penetrating analysis/diagnosis (of both problems; but the first is pure :facepalm: 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...?)
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....
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.]
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).
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...
Fair point! I'll continue to experiment as part of #2317 and perhaps #1761 but willing to give way at this stage...
Data.Nat.Primality.Factorisation
... but still a potential refactoring opportunity...
(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 aprep
/'prefix' step with a use ofshift
reflected symmetrically; but ifis replaced with
then the parser complains...
The
step-swap
combinator, defined as: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 withrefl
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 examplelem₂
using the combinator, as follows:Removing any of these brackets (or any other bracketing) seems to cause the parser to fall over.