module Stdlib.Trait.Foldable.Polymorphic;

import Stdlib.Function open;

--- A trait for combining elements into a single result, processing one element at a time.
trait
type Foldable (F : Type -> Type) :=
  mk@{
    syntax iterator for {init := 1; range := 1};
    for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;

    syntax iterator rfor {init := 1; range := 1};
    rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
  };

open Foldable hiding {mk} public;

--- Combine the elements of the type using the provided function starting with the element in the left-most position.
{-# inline: true #-}
foldl
  {F : Type -> Type}
  {{Foldable F}}
  {Elem Acc : Type}
  (fun : Acc -> Elem -> Acc)
  (initialValue : Acc)
  (container : F Elem)
  : 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.
{-# inline: true #-}
foldr
  {F : Type -> Type}
  {{Foldable F}}
  {Elem Acc : Type}
  (fun : Elem -> Acc -> Acc)
  (initialValue : Acc)
  (container : F Elem)
  : Acc :=
  rfor (acc := initialValue) (x in container) {
    fun x acc
  };