open import 1Lab.Type

open import Meta.Idiom
open import Meta.Alt

module Meta.Foldable where

Meta: Foldable effectsπŸ”—

record Foldable (F : Effect) : Typeω where
  private module F = Effect F
  field
    foldr : βˆ€ {β„“ β„“'} {a : Type β„“} {b : Type β„“'} β†’ (a β†’ b β†’ b) β†’ b β†’ F.β‚€ a β†’ b

open Foldable ⦃ ... ⦄ public

asum
  : βˆ€ {F M : Effect} ⦃ f : Foldable F ⦄ ⦃ a : Alt M ⦄ {β„“} {A : Type β„“}
    (let module F = Effect F) (let module M = Effect M)
  β†’ F.β‚€ (M.β‚€ A) β†’ M.β‚€ A
asum = foldr _<|>_ fail

nondet
  : βˆ€ (F : Effect) {M} ⦃ f : Foldable F ⦄ ⦃ t : Map F ⦄
      ⦃ a : Alt M ⦄ ⦃ i : Idiom M ⦄
      {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ (let module F = Effect F)
  β†’ (let module M = Effect M)
  β†’ F.β‚€ A β†’ (A β†’ M.β‚€ B) β†’ M.β‚€ B
nondet F ⦃ f = f ⦄ xs k = asum ⦃ f = f ⦄ (k <$> xs)