Generalized collection / sequence etc functions.

[t-more]

There's a similar issue on the topic for a few years earlier, but I really believe it would be a good idea to have generalized names for common container / sequence / etc operations.

The main purpose of such type classes would to make programming easier, not formalisms.

Two examples classes:

"Sized" giving a general notion of the size of some object

record Sized {a} (A : Set a) : Set a where
  field
    size : A → Nat
open Sized {{...}} public

instance
  SizedNat : Sized Nat
  size {{SizedNat}} n = n

  SizedList : Sized (List A)
  size {{SizedList}} = length

"Collection" generalizing the concept of a multi-set. (Excluding extensionality of course)

record Collection {a b} (A : Set a) (C : Set b) : Set (a ⊔ b) where
  field
    insert : A → C → C
    remove : A → C → C
    removeOne : A → C → C
    member : A → C → Bool
    occurences : A → C → Nat
open Collection {{...}} public

record Collection/Laws {a b} (A : Set a) (C : Set b) : Set (a ⊔ b) where
  field
    overlap {{super}} : Collection A C
    insert-member : (a : A) → (c : C) → member a (insert a c) ≡ true
    insert-remove : (a : A) → (c : C) → member a (remove a c) ≡ false
    remove-local : (a a' : A) → (c : C) → a' ≢ a
                 → member a' (remove a c) ≡ member a' c
    insert-local : (a a' : A) → (c : C) → (a' ≢ a)
                 → member a' (insert a c) ≡ member a' c

instance
  CollectionList : {{_ : Eq A}} → Collection A (List A)
  insert {{CollectionList}} = _∷_
  remove {{CollectionList}} a = List.filter (λ x → not (x ==? a))
  removeOne {{CollectionList}} a List.[] = List.[]
  removeOne {{CollectionList}} a (x ∷ xs) =
    if x ==? a then xs else x ∷ removeOne a xs
  member {{CollectionList}} = List.elem
  occurences {{CollectionList}} x xs = List.length (List.filter (_==? x) xs)

  CollectionString : Collection Char String
  insert {{CollectionString}} c str =
    packString (List.singleton c) <> str
  remove {{CollectionString}} c str = packString (remove c (unpackString str))
  removeOne {{CollectionString}} c str =  packString (removeOne c (unpackString str))
  member {{CollectionString}} c str = member c (unpackString str)
  occurences {{CollectionString}} c str = occurences c (unpackString str)

[t-more]

I would like to ping this, issue. The thing is that I've implemented red-black trees (for dictionary / maps) and 2-3 finger trees (for dequeues etc) for prelude. But to make this work smoothly we need to generalize many of the functions currently exported by Prelude.

The the alternative would possibly do add these types into the Container module instead. But it would be nice (from a programmers perspective) if we could avoid naming conflicts with prelude.