agda
Operations on List's `All` defined in `Properties`
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:
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/All/Properties.agda#L393
This goes for many of the ^+ "properties".
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:
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/All/Properties.agda#L405
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/Any/Properties.agda#L350
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/All/Properties.agda#L366
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda#L180
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda#L55
In the last of those, note the use of some comparatively complicated proofs that can't be easily extracted to the Base files:
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda#L39
Finally what are the concrete disadvantages of the current scheme?
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:
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/All/Properties.agda#L405
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.
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/Any/Properties.agda#L350
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.
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Unary/All/Properties.agda#L366
Property, for a similar reason.
https://github.com/agda/agda-stdlib/blob/bfbb6399356d00812552ec9b6eef41048d123af2/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda#L180
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.
++⁻ : ∀ 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.
Ah, yes I missed that we do have an explicit argument xs in this version. Edited my comment .