Library FingerTree.Reduce


Section Reduce.
  Variable f : TypeType.
  Definition reducer_t := ∀ A B : Type, (ABB) → (f ABB).
  Definition reducel_t := ∀ A B : Type, (BAB) → (Bf AB).
End Reduce.

Record Reduce (f : TypeType) : Type :=
  mkReduce {
    reducer : reducer_t f;
    reducel : reducel_t f
  }.

Definition idReduce := mkReduce (fun a b opop) (fun a b opop).


Definition listReduce := mkReduce (fun a b op fa bfold_right op b fa)
  (fun a b op b fafold_left op fa b).

Section toList.

  Variable f : TypeType.
  Variable r : Reduce f.
  Variable A : Type.

  Definition toList (x : f A) : list A :=
    (reducer r (cons (A:=A))) x nil.
End toList.