Operations on List's `All` defined in `Properties`

[ajrouvoet]

I believe that a bunch of "properties" of List's All should really be defined in the main All module, because they are just operations on heterogeneous lists. For example, the append is defined as a property here:

agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda

Line 393 in bfbb639

++⁺ : All P xs → All P ys → All P (xs ++ ys)

This goes for many of the ^+ "properties".

[MatthewDaggitt]

Hmm so for that particular example I can see where you're coming from but the problem is that I have no idea how to draw that line... At least the current scheme is consistent. Do you have a concrete hard-and-fast rule in mind @ajrouvoet? How does it classify the following:

agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda

Line 405 in bfbb639

++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys

agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda

Line 350 in bfbb639

++⁺ˡ : Any P xs → Any P (xs ++ ys)

agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda

Line 366 in bfbb639

map⁺ : ∀ {f : A → B} → All (P ∘ f) xs → All P (map f xs)

agda-stdlib/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

Line 180 in bfbb639

++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_

agda-stdlib/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda

Line 55 in bfbb639

++⁺ : ∀ {xs ys} → Unique S xs → Unique S ys → Disjoint S xs ys → Unique S (xs ++ ys)

In the last of those, note the use of some comparatively complicated proofs that can't be easily extracted to the Base files:

agda-stdlib/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda

Line 39 in bfbb639

Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →

Finally what are the concrete disadvantages of the current scheme?

[ajrouvoet]

Let me start with your last question:

Finally what are the concrete disadvantages of the current scheme?

It is mostly that the library organization reflects on how one conceptualizes something like All. I think we should/want to encourage people to think of some definitions as (very strongly typed) but regular operations on data, whereas others are really more like properties, used primarily in proofs about those operations or about relations to other data-structures.

Hmm so for that particular example I can see where you're coming from but the problem is that I have no idea how to draw that line... At least the current scheme is consistent. Do you have a concrete hard-and-fast rule in mind @ajrouvoet?

No, unfortunately. Some hints come to mind:

• A data operation is a definition that I understand by looking at what it does to the data. A property is something that primarily establish a relation between types. It may operate on the data, but this is an 'implementation detail'.
• Does the signature mention another operation on All? Definitely a property.
• If we think of implicits as erased, do the explicit arguments still give the necessary info for the operation on the data? If no, then I'd lean towards it being a property. Some example below.

How does it classify the following:

agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda

Line 405 in bfbb639

++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys

This one feels like an operation. We have an explicit argument that tells us where to split the heterogeneous list. See also @gallais's comment below.

agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda

Line 350 in bfbb639

++⁺ˡ : Any P xs → Any P (xs ++ ys)

This feels like a property: we are primarily modifying the logical information present in the index. The fact that we also change the structure of the witness is an implementation detail.

agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda

Line 366 in bfbb639

map⁺ : ∀ {f : A → B} → All (P ∘ f) xs → All P (map f xs)

Property, for a similar reason.

agda-stdlib/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

Line 180 in bfbb639

++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_

Looking from the perspective of lists I'd say this is clearly a property. From the perspective of permutations I'm not sure if the question makes sense, because I don't have an idea of the permutation representation as a data-structure that should support certain data-operations. I only understand it in a logical context.

[gallais]

++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys

This one feels like a property, because of hint no. 3. We don't have an explicit argument that tells us where to split the heterogeneous list, so we are leaning heavily on 'logical information'.

This one feels like

splitAt : ℕ → List A → (List A × List A)

splitAt : ∀ m {n} (xs : Vec A (m + n)) →
          ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs

so definitely a program to me.

[ajrouvoet]

Ah, yes I missed that we do have an explicit argument xs in this version. Edited my comment .