module Stdlib.Trait.Foldable.Monomorphic;
import Stdlib.Function open;
import Stdlib.Trait.Foldable.Polymorphic as Poly;
--- A trait for combining elements into a single result, processing one element at a time.
trait
type Foldable (container elem : Type) :=
mkFoldable {
syntax iterator for {init := 1; range := 1};
for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
syntax iterator rfor {init := 1; range := 1};
rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
};
open Foldable public;
--- Make a monomorphic ;Foldable; instance from a polymorphic one.
--- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance.
fromPolymorphicFoldable
{f : Type -> Type}
{{foldable : Poly.Foldable f}}
{elem}
: Foldable (f elem) elem :=
mkFoldable@{
for := Poly.for;
rfor := Poly.rfor
};
foldl
{container elem}
{{Foldable container elem}}
{B : Type}
(g : B -> elem -> B)
(ini : B)
(ls : container)
: B := for (acc := ini) (x in ls) {g acc x};
--- Combine the elements of the type using the provided function starting with the element in the right-most position.
foldr
{container elem : Type}
{{Foldable container elem}}
{B : Type}
(g : elem -> B -> B)
: B -> container -> B := foldl (flip g);