Free Monad of a Polynomial Functor

PolyFun's layer over cslib's free monad PFunctor.FreeM: the W-type presentations, root predicates, transport along lenses, and the bundled monad-homomorphism form of FreeM.liftM with its universal property and naturality. The algebraic laws (map_pure, map_bind, foldFreeM, foldFreeM_bind, liftM_comp, liftM_lift_eq_self) are staged for cslib in ToCslib.Data.PFunctor.Free.Basic, which this module re-exports.

def Parser.Attr.freeM_unfold_proc : Lean.ParserDescr

Simplification procedure

def Parser.Attr.freeM_unfold : Lean.ParserDescr

Simp set for structurally unfolding FreeM and displayed-family operations.

This set is reserved for one-way unfolding lemmas: constructor equations for FreeM operations, displayed-family operations, and local-hom recursion through liftBind. Folding and normalization lemmas should not be tagged with this attribute.

Fixed-point presentation

def PFunctor.FreeM.toWWithReturn {P : PFunctor.{uA, uB}} {α : Type v} : P.FreeM α → (P + C α).W

Reinterpret a finite free program as the W-type of query-or-return nodes. Query nodes are the left summand and return nodes are nullary nodes in the constant right summand.

def PFunctor.FreeM.ofWWithReturn {P : PFunctor.{uA, uB}} {α : Type v} : (P + C α).W → P.FreeM α

Decode the query-or-return W-type as a finite free program.

@[simp]

theorem PFunctor.FreeM.toWWithReturn_pure {P : PFunctor.{uA, uB}} {α : Type v} (value : α) : (pure value).toWWithReturn = WType.mk (Sum.inr value) PEmpty.elim

theorem PFunctor.FreeM.toWWithReturn_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (position : P.A) (next : P.B position → P.FreeM α) : (liftBind position next).toWWithReturn = WType.mk (Sum.inl position) fun (direction : (P + C α).B (Sum.inl position)) => (next direction).toWWithReturn

@[simp]

theorem PFunctor.FreeM.ofWWithReturn_return {P : PFunctor.{uA, uB}} {α : Type v} (value : α) (next : PEmpty.{uB + 1} → (P + C α).W) : ofWWithReturn (WType.mk (Sum.inr value) next) = FreeM.pure value

@[simp]

theorem PFunctor.FreeM.ofWWithReturn_query {P : PFunctor.{uA, uB}} {α : Type v} (position : P.A) (next : P.B position → (P + C α).W) : ofWWithReturn (WType.mk (Sum.inl position) next) = liftBind position fun (direction : P.B position) => ofWWithReturn (next direction)

def PFunctor.FreeM.equivWWithReturn {P : PFunctor.{uA, uB}} {α : Type v} : P.FreeM α ≃ (P + C α).W

FreeM P α is the initial algebra, or W-type, for the polynomial P + C α.

def PFunctor.FreeM.RootSatisfies {P : PFunctor.{uA, uB}} {α : Type v} (positionPred : P.A → Prop) (leafPred : α → Prop) : P.FreeM α → Prop

Test only the root of a free polynomial tree.

A leaf demands leafPred of its result, while an internal node demands positionPred of its exposed position. This deliberately does not recurse into the continuations; callers can quantify over paths or cursors when they need a whole-tree property.

@[simp]

theorem PFunctor.FreeM.rootSatisfies_pure {P : PFunctor.{uA, uB}} {α : Type v} (positionPred : P.A → Prop) (leafPred : α → Prop) (result : α) : RootSatisfies positionPred leafPred (pure result) = leafPred result

theorem PFunctor.FreeM.rootSatisfies_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (positionPred : P.A → Prop) (leafPred : α → Prop) (position : P.A) (next : P.B position → P.FreeM α) : RootSatisfies positionPred leafPred (liftBind position next) = positionPred position

def PFunctor.FreeM.toW {P : PFunctor.{uA, uB}} {α : Type v} [IsEmpty α] : P.FreeM α → P.W

Forward direction of the equivalence with P.W when the leaf type is empty: every pure case is unreachable, and every liftBind is reinterpreted as a W-node.

def PFunctor.FreeM.ofW {P : PFunctor.{uA, uB}} {α : Type v} [IsEmpty α] : P.W → P.FreeM α

Inverse direction of the equivalence with P.W when the leaf type is empty: every W-node becomes a liftBind.

def PFunctor.FreeM.equivWOfIsEmpty {P : PFunctor.{uA, uB}} {α : Type v} [IsEmpty α] : P.FreeM α ≃ P.W

When the value type is empty, every pure is unreachable and FreeM P α is structurally identical to P.W.

@[implicit_reducible]

def PFunctor.FreeM.mapLens {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : P.FreeM α → Q.FreeM α

Transport a free polynomial tree along a polynomial lens.

The source polynomial P is the abstract/control interface. The target polynomial Q is the concrete/runtime interface. At each P-node, the lens chooses a Q-position by toFunA; when runtime supplies a Q-direction, toFunB maps it back to the corresponding P-direction selecting the control continuation.

@[simp]

theorem PFunctor.FreeM.mapLens_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) : FreeM.mapLens l (pure x) = FreeM.pure x

theorem PFunctor.FreeM.mapLens_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) : FreeM.mapLens l (liftBind a rest) = liftBind (l.toFunA a) fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))

@[simp]

theorem PFunctor.FreeM.mapLens_id {P : PFunctor.{uA, uB}} {α : Type v} (x : P.FreeM α) : FreeM.mapLens (Lens.id P) x = x

@[simp]

theorem PFunctor.FreeM.mapLens_comp {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (l₂ : Q.Lens R) (l₁ : P.Lens Q) (x : P.FreeM α) : FreeM.mapLens l₂ (FreeM.mapLens l₁ x) = FreeM.mapLens (l₂ ∘ₗ l₁) x

theorem PFunctor.FreeM.mapLens_bind {P : PFunctor.{uA, uB}} {α β : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : P.FreeM α) (f : α → P.FreeM β) : FreeM.mapLens l (x.bind f) = (FreeM.mapLens l x).bind fun (a : α) => FreeM.mapLens l (f a)

@[simp]

theorem PFunctor.FreeM.mapLens_bind' {P : PFunctor.{uA, uB}} {α β : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : P.FreeM α) (f : α → P.FreeM β) : FreeM.mapLens l (x >>= f) = do let a ← FreeM.mapLens l x FreeM.mapLens l (f a)

def PFunctor.FreeM.liftMHom {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : P.FreeM →ᵐ m

FreeM.liftM as a monad homomorphism.

@[simp]

theorem PFunctor.FreeM.liftMHom_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) : (FreeM.liftMHom s).toFun α = fun (x : P.FreeM α) => FreeM.liftM s x

def PFunctor.FreeM.liftMHom' {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : P.FreeM →ᵐ m

FreeM.liftM as a monad homomorphism, packaging the interpretation of positions as a natural transformation NatHom P.Obj m.

@[simp]

theorem PFunctor.FreeM.liftMHom'_toFun_eq {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] [LawfulMonad m] (s : NatHom (↑P) m) : (FreeM.liftMHom' s).toFun α = fun (x : P.FreeM α) => FreeM.liftM (fun (t : P.A) => (fun {α : Type uB} (x : ↑P α) => s.toFun α x) ⟨t, id⟩) x

Universal property and naturality of the fold

FreeM.liftM s is the universal fold: the unique monad homomorphism out of FreeM P extending a handler s (liftMHom_unique), and it is natural in the target monad — post-composing with a monad morphism φ : m →ᵐ n is the fold of the post-composed handler (liftM_natural, liftMHom_comp). This is the freeness of FreeM P; downstream it lets a semantic monad morphism (e.g. an evaluation-distribution map) be pushed through a fold uniformly, rather than re-run by induction per interpretation.

theorem PFunctor.FreeM.liftMHom_unique {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (F : P.FreeM →ᵐ m) (h : ∀ (a : P.A), (fun {α : Type uB} (x : P.FreeM α) => F.toFun α x) (lift a) = s a) : F = FreeM.liftMHom s

Universal property of FreeM.liftM (freeness of FreeM P): a monad homomorphism out of FreeM P is determined by its action on generators. If F : FreeM P →ᵐ m agrees with s on every FreeM.lift a, then F = FreeM.liftMHom s. So handlers (a : P.A) → m (P.B a) are in bijection with monad homomorphisms FreeM P →ᵐ m — the universal property behind simulateQ.

@[simp]

theorem PFunctor.FreeM.liftM_natural {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {α : Type uB} [Monad m] (s : (a : P.A) → m (P.B a)) {n : Type uB → Type u} [Monad n] (φ : m →ᵐ n) (x : P.FreeM α) : (fun {α : Type uB} (x : m α) => φ.toFun α x) (FreeM.liftM s x) = FreeM.liftM (fun (a : P.A) => (fun {α : Type uB} (x : m α) => φ.toFun α x) (s a)) x

Naturality of the fold along a monad morphism: pushing a monad morphism φ : m →ᵐ n through FreeM.liftM s is the fold of the post-composed handler fun a => φ (s a) — the value-level naturality square of the universal fold.

theorem PFunctor.FreeM.liftMHom_comp {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) {n : Type uB → Type u} [Monad n] [LawfulMonad n] (φ : m →ᵐ n) : φ ∘ₘ FreeM.liftMHom s = FreeM.liftMHom fun (a : P.A) => (fun {α : Type uB} (x : m α) => φ.toFun α x) (s a)

Bundled form of liftM_natural: composing the fold monad-homomorphism FreeM.liftMHom s with a monad morphism φ is the fold of the post-composed handler.

theorem PFunctor.FreeM.run_liftM_mapHom {P : PFunctor.{uA, uB}} {m : Type uB → Type v} {n : Type uB → Type u} [Monad m] [Monad n] {σ α : Type uB} (φ : m →ᵐ n) (impl : (a : P.A) → StateT σ m (P.B a)) (x : P.FreeM α) (s : σ) : (FreeM.liftM (fun (a : P.A) => (fun {α : Type uB} (x : StateT σ m α) => (StateT.mapHom φ).toFun α x) (impl a)) x).run s = (fun {α : Type uB} (x : m α) => φ.toFun α x) ((FreeM.liftM impl x).run s)

Stateful naturality of the fold: running a fold whose stateful handler is post-composed by a StateT-lifted monad morphism StateT.mapHom φ is φ applied to the run of the original fold — the shape a StateT-threaded semantic morphism (e.g. an evaluation-distribution map through a stateful handler) instantiates, collapsing a per-interpretation induction to one use of liftM_natural.

theorem PFunctor.FreeM.liftMHom_lift_eq_id {P : PFunctor.{uA, uB}} : FreeM.liftMHom lift = MonadHom.id P.FreeM