Documentation

Cslib.Foundations.Data.PFunctor.Free.Fold

Folding polynomial free monads #

PFunctor.FreeM.foldFreeM evaluates a free polynomial tree in an algebra given by handlers for values and operations. It satisfies the same universal property and substitution laws as Cslib.FreeM.foldFreeM.

source
def PFunctor.FreeM.foldFreeM {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) :
P.FreeM α → β

Fold a free polynomial tree into an algebra of its signature.

Equations
Instances For
    source
    @[simp]
    theorem PFunctor.FreeM.foldFreeM_pure {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) (a : α) :
    foldFreeM onValue onEffect (pure a) = onValue a
    source
    @[simp]
    theorem PFunctor.FreeM.foldFreeM_lift_bind {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) (a : P.A) (cont : P.B a → P.FreeM α) :
    foldFreeM onValue onEffect ((lift a).bind cont) = onEffect a fun (b : P.B a) => foldFreeM onValue onEffect (cont b)
    source
    @[simp]
    theorem PFunctor.FreeM.foldFreeM_lift_bind' {P : PFunctor.{uA, uB}} {β : Type u_2} {α : Type uB} (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) (a : P.A) (cont : P.B a → P.FreeM α) :
    foldFreeM onValue onEffect (lift a >>= cont) = onEffect a fun (b : P.B a) => foldFreeM onValue onEffect (cont b)
    source
    @[simp]
    theorem PFunctor.FreeM.foldFreeM_lift {P : PFunctor.{uA, uB}} {β : Type u_2} (a : P.A) (onValue : P.B a → β) (onEffect : (a : P.A) → (P.B a → β) → β) :
    foldFreeM onValue onEffect (lift a) = onEffect a onValue
    source
    theorem PFunctor.FreeM.foldFreeM_unique {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) (h : P.FreeM α → β) (h_pure : ∀ (a : α), h (pure a) = onValue a) (h_lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α), h ((lift a).bind cont) = onEffect a fun (b : P.B a) => h (cont b)) :
    h = foldFreeM onValue onEffect

    A function agreeing with the algebra on values and operations is the fold.

    source
    theorem PFunctor.FreeM.foldFreeM_bind {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (onValue : β → γ) (onEffect : (a : P.A) → (P.B a → γ) → γ) (x : P.FreeM α) (k : α → P.FreeM β) :
    foldFreeM onValue onEffect (x.bind k) = foldFreeM (fun (a : α) => foldFreeM onValue onEffect (k a)) onEffect x

    Sequencing substitutes the fold of the continuation for the value handler.

    source
    theorem PFunctor.FreeM.foldFreeM_map {P : PFunctor.{uA, uB}} {α : Type u_1} {β : Type u_2} {γ : Type u_3} (onValue : β → γ) (onEffect : (a : P.A) → (P.B a → γ) → γ) (f : α → β) (x : P.FreeM α) :
    foldFreeM onValue onEffect (map f x) = foldFreeM (onValue ∘ f) onEffect x
    source
    theorem PFunctor.FreeM.liftM_eq_foldFreeM {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] {α : Type uB} (interp : (a : P.A) → m (P.B a)) :
    FreeM.liftM interp = foldFreeM pure fun (a : P.A) (k : P.B a → m α) => interp a >>= k

    Monadic interpretation is the fold whose effect handler uses bind.