comments on lib-2.1 candidate 1

[mechvel]

(1) Visibility of Data.Product.zipWith

Checking ForTests (/home/mechvel/inAgda/doconA/3.2/source/ForTests.agda). Multiple definitions of zipWith. Previous definition at /home/mechvel/agda/stLib/2.1-rc1/src/Data/List/Base.agda:83,1-8 when scope checking the declaration open import Data.Product public hiding (map; zip)

Is this backwards compatible?

(2) What is the matter with Data.List.Properties.filter-accept, filter-reject ?

Unlike with lib-2.0, it appears "Unsolved", and it requires implicit arguments to be set

• this is under the same type checker Agda 2.6.4.3 Built with flags (cabal -f)
  • optimise-heavily, the type check keys are "--auto-inline --guardedness"

And it occurs non-backwards compatible. The effect often occurs that Agda silently hangs forever, then one has to guess and search for filter-accept in the currently processed module. My program has probably thousand of places where the implicit arguments filter-accept/reject need to be inserted. After this is fixed, the whole my application works.

I wonder of why the effect is produced while the type checker version is the same and the function definition is the same.

Can you explain the effect?

(3) reverse and ⊆.

lib-2.1-rc1 has in Data.List.Relation.Binary.Subset.Setoid.Properties

reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
reverse⁺            : as ⊆ bs → reverse as ⊆ reverse bs
reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs

But there are also needed

reverse-preservesʳ-⊆ :  ∀ {xs} → rev Preserves (xs ⊆_)
reverse-preservesʳ-⊆ {xs} {ys} xs⊆ys =  xs⊆rev-ys
  where
  xs⊆rev-ys : xs ⊆ (rev ys)
  xs⊆rev-ys = reverse∈⁺ S ∘ xs⊆ys

reverse-preservesˡ-⊆ :  ∀ {xs} → rev Preserves (_⊆ xs)
reverse-preservesˡ-⊆ {xs} {ys} ys⊆xs =  rev-ys⊆xs
  where
  rev-ys⊆xs : (rev ys) ⊆ xs
  rev-ys⊆xs {z} z∈rev-ys = ys⊆xs z∈ys
    where
    revrev-ys≡ys = reverse-involutive ys

    z∈revrev-ys :  z ∈ rev (rev ys)
    z∈revrev-ys =  reverse∈⁺ S z∈rev-ys

    z∈ys = subst (z ∈_) revrev-ys≡ys z∈revrev-ys

(you can change the implementation). Here reverse⁺ is renamed to reverse∈⁺ in order to avoid clash with reverse⁺ for ⊆.

(3.2) "NB. the unit and counit of this adjunction are given by:"

reverse-η : ∀ {xs} → xs ⊆ reverse xs
reverse-η = Membershipₚ.reverse⁺ S
reverse-ε : ∀ {xs} → reverse xs ⊆ xs
reverse-ε = Membershipₚ.reverse⁻ S

Eta and epsilon do not look clear here to many people. Is not it better to call them xs⊆reverse-xs and reverse-xs⊆xs and to provide the implementation directly?

[jamesmckinna]

Re: (3) see the discussion on #2378 Your two proposed new lemmas are easy compositions via ⊆-trans of reverse⁺/reverse⁻ with the unit/counit (so your implementations could be drastically simplified...), and as with the discussion on the PR, there's a Fairbairn-threshold judgment to be made about the value of such contributions ...

As to eta and epsilon, these are conventional names from category theory, and the properties follow from the self-adjunction introduced in the PR. But as above, they are left as comments because they amount to (no more than) yet more synonyms for lemmas originally defined in Any...

[jamesmckinna]

Re: (1) (My earlier comment deleted; based on a misreading/misunderstanding of the original point).

The introduction of Data.Product.zipWith in #2373 passes all tests, so from a developer/maintainer's perspective it's a non-breaking addition. What we cannot control for is client uses of modules, as here, with a hiding directive, giving rise t the problems you've seen. I guess it's a clash between an 'open-world' assumption (module API signatures can expand/widen arbitrarily) vs. a 'closed-world' one (hiding directives depend for their consistency/correctness on no such expansion)

Our more recent approach for stdlib consists of both

• explicit using directives on import, rather than relying on 'open-world' arbitrary open import
• use of qualified names for module import, to give more fine-grained namespace control

Relying on 'monotonic' behaviour of hiding directives is unsafe, so probably should in general be avoided in client code?

[jamesmckinna]

Re: (2) Which implicit arguments now need to be inserted in your code? The definitions were first introduced in commit 84d7962cfd90379a6d1d5ef2cdd9d3ae411ee603 (2019) and then recently refactored just to make the with-based pattern analysis less strict in the contradiction branches... which shouldn't have affected argument inference, AFAIU, as the binding structure has not changed in the interim

[mechvel]

With lib-2.0 it worked , for example, filter-accept nonzeroMon? a≉0. And lib-2.1-rc1 requires filter-accept nonzeroMon? {mon}{mons +ms mons'} a≉0. I believe you can test this by considering simple examples with filter-accept, filter-reject.

a) Users (like myself) may have a thousand occurrences of this to be changed in the user code. I have spent at least four hours, because the arguments to insert often differ, this is not by copy-paste. b) If a large module has filter-accept/reject applied in the old style, the command of agda ... CheckAll.agda under lib-2.1-rc1 may hung silently for a long time for unknown reason ... This part was not difficult for me to discover, but some people will be frightened.

[MatthewDaggitt]

1. So, as @jamesmckinna says, I'm afraid this is unavoidable. It's impossible to add new definitions to existing modules while guaranteeing that it won't clash with existing code.

2. This is a real problem that we would like to fix. Please can you provide a minimal example that type-checks in isolation only relying on Standard library code?

3. Additional lemmas can be requested to be added to v2.2, but the window for adding new code has now closed.

[mechvel]

This is a real problem that we would like to fix. Please can you provide a minimal example that type checks in isolation only relying on Standard library code?

What example are you talking of? Here is an example for filter-accept :

open import Data.List using (List; _∷_; filter)
open import Data.List.Properties using (filter-accept)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Unary using (Pred; Decidable)

module _ {α α= β} (S : Setoid α α=)
   (open Setoid S using (Carrier))  (P : Pred Carrier β) (P? : Decidable P)
   where
eq :  (x : Carrier) (xs : List Carrier) → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
eq x xs Px =
   filter-accept P?  -- {x}{xs}
                    Px

Under lib-2.1-rc1 the report is "Unsolved metas", And I believe that under lib-2.0 it will type-check (when I used lib-2.0, all similar functions were type-checked). And this is under the same Agda 2.6.4.3 !

(Built with flags (cabal -f) - optimise-heavily, applied with --auto-inline --guardedness).

[jamesmckinna]

As to the nature of the 'bug':

• a priori, there seems no way to infer xs in the type of filter-accept (whereas for x it's 'obviously' OK, because constrained by P x); is it an 'accident' that we could get away with it being implicitly quantified before? (apparently it's OK for the with-based definition)
• eg. derun-accept/derun-reject in the same module which seems to require explicit quantification over xs...
• ... but in fact do not, so we should also correct the types of those functions (and check whether the new definitions affect their downstream use by clients...)

Reversion to the status quo ante (eg by reverting commit 438f9ed, although that unfortunately touches both the new definitions in Data.List.Base and their properties in Data.List.Properties ... which have been usefully refactored) seems to be the correct way forward, but also raises questions of consistency/coherence of this whole suite of functions, and their properties, as a whole... so I'm not clear how to proceed.

[mechvel]

I do not understand the details you are talking of. But I find now that the function filter has a bit different implementation in lib-2.0 and in lib-2.1-rc1. So, I am not surprised now of that this could imply the difference in type-checking proofs for filter-accept.
As to me, I would vote for avoiding usage of true/false instead of yes/no. I do not understand the subject, but it looks as something like built-in things.

[jamesmckinna]

Indeed. #2365 changed the implementation of a suite of functions including, but not only, filter. The change in behaviour you have uncovered seems to affect each of the functions differently, so the overall situation seems more complicated than simply that of the individual case of filter...