Fix v2.1-rc1 by reverting (some) changes to Data.List.*

[jamesmckinna]

Fixes #2415 (I hope! @mechvel can you confirm that this reversion fixes the problem with filter you raised there?)

This reverts commit 438f9ed.
"Improve Data.List.Base (fix #2359; deprecate use of with #2123) (#2365)"

Specifically, it restores with-based definitions of the Decidable-definable functions on Lists, incl. filter

NB. We should agree what, if anything, else should be pushed (or: salvaged from #2365 ) to fix up v2.1-rc1, but this is a (the) minimal fix I could come up with. Eg can we incorporate @Taneb 's tests into the golden suite? How do we tackle the corresponding (failing!) cases for eg partition...?

[mechvel]

Fixes #2415 (I hope! @mechvel can you confirm that this reversion fixes
the problem with filter you raised there?).

How can I check and confirm? Is this by downloading the master branch?
If so, then I hope that I can download the archive of the master branch and test it on my application.
Please, advise.

I doubt about "merging the pull request". If I find an Archive of the needed library version for testing
(2.1.candidate-N), then I can download it and install.

[jamesmckinna]

Fixes #2415 (I hope! @mechvel can you confirm that this reversion fixes the
problem with filter you raised there?).

How can I check and confirm? Is this by downloading the master branch? If so, then I hope that I can download the archive of the master branch and test it on my application. Please, advise.

(Without having details of your exact personal set-up)
Recommended would be to checkout a fresh branch off master as follows:

• first, add my clone to your list of possible remote repositories

git remote add james git@github.com:jamesmckinna/agda-stdlib.git

• then (making sure you are already on an up-to-date version of master): fetch the new branch (NOT pull), then switch to it

git fetch james repair-v2.1-rc1
git checkout repair-v2.1-rc1

• run your tests... then restore the master branch as usual.

git checkout master

HTH

[mechvel]

first, add my clone to your list of possible remote repositories
[..]

I am sorry, this is too messy for me to arrange (I had an experience several years ago).
If I find an Archive of the needed library version for testing (2.1.candidate-N), then I can download it, install and check.

[jamesmckinna]

first, add my clone to your list of possible remote repositories
[..]

I am sorry, this is too messy for me to arrange (I had an experience several years ago).

I am sorry to hear that. Given that stdlib is hosted and developed on GitHub, it seems a shame not to be able to interact with it via git commands, but I see from earlier discussions how difficult that appears to be for you.

If I find an Archive of the needed library version for testing (2.1.candidate-N), then I can download it, install and check.

There we perhaps have a bigger problem: in order to produce such an archive, the maintainers need to approve and merge my recent changes to v2.1-rc1, which I am hoping that they will not do until we have some indication from you that the behaviour you have identified has been successfully corrected by the change. The essence of the collaborative distributed development method is that we only proceed once we are sure it is OK to do so: your bug report indicated that there was more work to do...

So, instead, and in the interests of getting your feedback, may I suggest that you take a fresh copy of v2.1-rc1 (however you may have obtained that previously), and then do the following:

• replace the rc1 version of src/Data/List/Base.agda with this one (the link is simply to the relevant file in the branch on GitHub defining the changes)
• replace the rc1 version of src/Data/List/Properties.agda with this one (ditto.)

Then: please re-run your tests, and let us know how things work for you (or not).

If the above also does not work for you, then I am unclear how to proceed without a much more time-consuming process (moreover one which git is expressly designed to avoid having to undertake).

[mechvel]

replace the rc1 version of src/Data/List/Base.agda with [this one](https://github.com/jamesmckinna/agda-stdlib
/blob/repair-v2.1-rc1/src/Data/List/Base.agda)
(the link is simply to the relevant file in the branch on GitHub defining the changes)
replace the rc1 version of src/Data/List/Properties.agda with [this one](https://github.com/jamesmckinna/agda-stdlib
/blob/repair-v2.1-rc1/src/Data/List/Properties.agda) (ditto.)
Then: please re-run your tests, and let us know how things work for you (or not).

I run now its type checking (about 20 minutes). Then I will need to play with removing the implicits of kind {x} {xs}
from filter-accept ... and such ( I have already inserted them in many places in order to satisfy lib-2.1-rc1, and to
continue the work).
It will also need compiling to executable (takes about 1 hour) and testing the performance of examples, because filter does run in examples.
I hope to report of the result may be tomorrow.

I am sorry to hear that. Given that stdlib is hosted and developed on GitHub, it seems a shame not to be able to interact > with it via git commands, but I see from earlier discussions how difficult that appears to be for you.

In fact I am ashamed. But I have only one head and cannot deal simultaneously with too many programming systems.
Last several years I test each appearing library version on my application in computer algebra.
There appears foo.candidate1. I download the archive, test it and report. Then there may appear foo.candidate2,
and so on. And this worked, and there was no need in studying (recalling of) any extra programming tools, how nice.

[JacquesCarette]

While I agree that we need to do this for 2.1, we also need to more deeply understand what's going on. The direct implementation really ought to be better! Is there an open issue that corresponds to puzzling that out?

[Taneb]

Was this change necessary?

[jamesmckinna]

No, not sure how it crept in, or why!?

UPDATED: hang on! This PR reverts previous changes, so those things were likely part of the original Data.List.Properties definitions... and suggest a downstream v2.2 to fix these (and many other things around this anomaly) later...?

[jamesmckinna]

@JacquesCarette you wrote:

While I agree that we need to do this for 2.1, we also need to more deeply understand what's going on. The direct implementation really ought to be better! Is there an open issue that corresponds to puzzling that out?

I absolutely agree! That's why in my discussion both of Sergei's originating issue (blocking v2.1-rc1), and your original one, I draw attention to the fact that one set of implicit/explicit quantification choices 'works' for filter, while another does not for partition, regardless of whether the with-based, or 'direct' if (does ...)... is used. But my eyes were definitely on getting the prize-at-hand (v2.1) and leaving the 'harder' problem for later. But good to keep it alive, as I had hoped to have done in my comments on #2359 ... is this an upstream Agda issue?

[JacquesCarette]

It might be an Agda issue, I don't know. I was asking for a separate issue where we could track our findings. The current issues are appropriately focused on getting v2.1 done, and should be closed when that's done. So the findings of filter vs partition risk getting lost in all that noise.

[jamesmckinna]

@JacquesCarette you're right of course... I'd been hand-waving my way around a basic "too lazy to have filed a fresh issue" confession... ;-) See #2427

[jamesmckinna]

Meanwhile @mechvel are you able to confirm that the 'old' behaviour wrt filter has been restored to your satisfaction?

[mechvel]

Meanwhile @mechvel are you able to confirm that the 'old' behaviour wrt filter has been restored to your satisfaction?

Yes, it is restored.
I replaced the two .agda files with the files that you suggested. Now the application works as under lib-2.0,
the difference is that it uses a couple of new functions from lib-2.1-rc1.

It is nice that the application program can omit the arguments like {cToMon c} {(cToMon a) ∷( mons ++ mons')} in the proofs.
This saves may be 1/30 part of the source code complication caused by forced setting implicit arguments in function calls.
But this latter is a matter of the type checker, not of the standard library, may be it is a fundamental feature of the language and of the implementation principles.

[mechvel]

While I agree that we need to do this for 2.1, we also need to more deeply understand what's going on. The direct
implementation really ought to be better! Is there an open issue that corresponds to puzzling that out?

Can anybody explain in simple words why is it good to write

filter P? (x ∷ xs) with does (P? x)
... | false = filter P? xs
...

instead of

filter P? (x ∷ xs) with  P? x
... | no _  = filter P? xs
...

?

[jamesmckinna]

Here's my attempt to tackle @mechvel 's question above:

• matching on a proof d : Dec A has the potential to force (too much; unnecessary) computation of proof d; evaluation might be too strict
• matching on a proof does d : Bool where d : Dec A ensures that the enclosing computation cannot require the proof; evaluation is as lazy as possible

In the 'half-way' scenario where the match in the first case is of the form yes _ or no _, it could be argued that the same 'lazy' behaviour is available, although in such instances, there may (still!) be too much computation in discerning the outer constructor ofⁿ/of ʸ of the proof d part... whereas using does d as the expression to match on ensures this will never be the case.

Part of the purpose of #2365 was to attempt to isolate such usages (on the meta-principle that "functions defined in Data.List.Base shouldn't depend on proofs"... but proofs of Dec A are a funny grey area in this respect), in favour of simpler if_then_else_ definitions based on the underlying does d field...

... except that, apparently for reasons we don't yet quite understand, such definitions don't quite work wrt the typechecker in the subsequent proofs of properties, as your tests identified.

[mechvel]

Thank you for explanation.
For understanding it is needed an example.
Say, consider

postulate
  makeList : List ℕ
  P : Pred (List ℕ) _	

  P? : Decidable P

f : ℕ
f  with P? makeList
... | yes _ = 0
... | no _  = 1

How to define makeList, P, P? so that this f to run much longer than its version with does, true,false ?
(running can mean running by interpreter or running the compiled code).

[mechvel]

... except that, apparently for reasons we don't yet quite understand, such definitions don't quite work wrt the
typechecker in the subsequent proofs of properties, as your tests identified.

1. The type checker can require to set some implicit arguments to the function call. This is not a bug.
   If the type of a function f is preserved, and the implementation is changed, has the type checker right to report different things for the same call (f {x}) ?

2. Then, standard library changed the implementation of filter without changing the type of this function.
   After this, type-checking some calls for the function filter-accept (that uses filter) causes "unsolved metas" .
   So, changing an implementation for a standard function with preserving its type may cause the type-checking error in a user program, breaking backwards compatibility.
   Right?
   ....
   And we cannot detect currently: which changes in standard function implementations (preserving the type) do break user's code.
   Right?
   Agda is developed and used during many years. Really, is this problem new?
   One way out is to list in CHANGELOG.md which functions have changed their implementation, so that their calls may break old user code.
   Meanwhile the Agda implementors could think about the criterion for detecting which implementations of a function preserve the type check success.
   ....
   Am I missing something?

[mechvel]

But my discourse above is erroneous.
The requirement needs to be not only preserving the type of f but also (II) : preserving its data map.
For example, changing the implementation of filter to \_ _ -> [] preserves the type, but it will definitely break many programs that prove some properties of filter.
Probably even (II) is not sufficient to require.
So, I do not know currently how to formulate the requirement on changing implementation of standard functions.

[MatthewDaggitt]

Okay, it sounds like this patch fixes the problem so I'm going to merge it in. Feel free to continue this discussion here, or elsewhere.