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.

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

• PFunctor.FreeM.foldFreeM onValue onEffect (PFunctor.FreeM.pure a) = onValue a
• PFunctor.FreeM.foldFreeM onValue onEffect (PFunctor.FreeM.liftBind a cont) = onEffect a fun (b : P.B a) => PFunctor.FreeM.foldFreeM onValue onEffect (cont b)

@[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

@[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)

@[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)

@[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

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.

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.

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

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.