Standardisation of folds

[MatthewDaggitt]

At the moment naming and typing conventions for folds differ quite a lot across the various different data types. As far as I can see there are three basic types of folds present in the standard library (feel free to suggest more if I missed any!):

1. Basic folds (applicable to everything List, Vec, Table etc.)

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → A → ∀ {n} → Vec A n → A

2. Dependent folds (applicable to everything)

foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} → 
        (∀ {n} → A → B n → B (suc n)) → B zero → Vec A m → B m

3. Non-empty folds (applicable to Vec, Table etc)

foldr : ∀ {a} {A : Set a} → (A → A → A) → ∀ {n} → Vec A (suc n) → A

Obviously 1. can be implemented in terms of 2. and 3. can be implemented in terms of 1.

The current state of play is:

Datatype	Name for 1.	Name for 2.	Name for 3.
List	foldr	-	N/A
Vec	-	foldr	foldr₁
Table	foldr	-	-
Product.N-ary	-	foldr	-

It would be great if we could add in some of the missing ones and come up with some consistent naming scheme for these across all data types for v1.0.

1. In my opinion the name foldr should always be reserved for this "normal" fold.
2. I don't have strong opinions or any good suggestions. Maybe something like dfoldr or foldrᵈ?
3. I would suggest foldr₊ to represent the non-emptiness (rather than foldr⁺ which would clash for property intoduction proofs).

[gallais]

I'd suggest also adding:

induction : ∀ {a b} {A : Set a} (B : (n : ℕ) → Vec A n -> Set b) → 
            (∀ {n} x xs → B n xs → B (suc n) (x ∷ xs)) → B zero [] →
            ∀ {m} (xs : Vec A m) → B m xs

[JacquesCarette]

My instincts for naming (in Agda) goes in the opposite direction for 1 vs 2. The standard library is quite a mixed bag in this respect, but for simpler types (sums, products), the basic operations are all deeply dependent but use the 'classical' name anyways. Then there is often a non-dependent synonym.

Because the context is dependently typed, it feels that the simpler names should be attached to the dependently typed version.

As for 'non-empty', any chance of using subscript 'ne' instead? I do a lot of stuff with rigs, and in that setting using a + subscript is quite common, and would clash in meaning.

[MatthewDaggitt]

My instincts for naming (in Agda) goes in the opposite direction for 1 vs 2. The standard library is quite a mixed bag in this respect, but for simpler types (sums, products), the basic operations are all deeply dependent but use the 'classical' name anyways. Then there is often a non-dependent synonym.

The difference is that the dependent version of foldr can't be used interchangeably at the moment with the non-dependent version as it requires you to specify B explicitly, as well as x and xs in the function. I haven't investigated how inferable those parameters are...

As for 'non-empty', any chance of using subscript 'ne' instead? I do a lot of stuff with rigs, and in that setting using a + subscript is quite common, and would clash in meaning.

Okay, no problem, we can find a different name. Hmm foldrₙₑ looks a bit ugly to me, and a little more annoying to type. It's serviceable though. Maybe foldr+ is more palatable? Or anyone else have any other suggestions superior to both?

[JacquesCarette]

I agree, foldrₙₑ does look rather ugly, I withdraw it as a contender.

The rest was really 'my feeling'. Hopefully people with more experience will chyme in.

[WolframKahl]

I occasionally use names like foldrNE.

[MatthewDaggitt]

I still haven't put much thought into these namings and its quite a big backwards non-compatible change. I think this isn't going to get fixed for v1.0.

[gallais]

Given that we use List⁺ for non-empty lists, we could use foldr⁺
for folds on non-empty structures.