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.
{-# specialize: true #-}
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.
{-# inline: case #-}
fromPolymorphicFoldable
  {f : Type -> Type}
  {{foldable : Poly.Foldable f}}
  {elem}
  : Foldable (f elem) elem :=
  mkFoldable@{
    for := Poly.for;
    rfor := Poly.rfor
  };

{-# inline: true #-}
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.
{-# inline: 2 #-}
foldr
  {container elem : Type}
  {{Foldable container elem}}
  {B : Type}
  (g : elem -> B -> B)
  : B -> container -> B := foldl (flip g);