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}}
{Acc : Type}
(fun : Acc -> Elem -> Acc)
(initialValue : Acc)
(container : Container)
: Acc :=
for (acc := initialValue) (x in container) {
fun 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}}
{Acc : Type}
(fun : Elem -> Acc -> Acc)
(initialValue : Acc)
(container : Container)
: Acc := foldl (flip fun) initialValue container;