feat(Data/PFunctor): add free monad of a polynomial functor by quangvdao · Pull Request #477 · leanprover/cslib

quangvdao · 2026-04-07T18:53:17Z

Summary

Port PFunctor.FreeM from VCV-io (ToMathlib/PFunctor/Free.lean) to cslib.
The free monad on a polynomial functor extends the W-type construction with an extra pure constructor, yielding a lawful monad that is free over P : PFunctor.

Main definitions

PFunctor.FreeM: inductive type with pure and roll constructors
FreeM.lift / FreeM.liftA: lifting from the base polynomial functor
Monad and LawfulMonad instances
FreeM.inductionOn / FreeM.construct: propositional and dependent eliminators
FreeM.mapM: canonical interpretation into any target monad, with simp lemmas for bind, map, seq, etc.

Notes

The MonadHom-related definitions (mapMHom, mapMHom') from the original VCV-io source are omitted since cslib does not have MonadHom infrastructure. These can be added later if cslib gains monad homomorphism support.
File placed at Cslib/Foundations/Data/PFunctor/FreeM.lean as a foundation for future polynomial functor work.
Builds cleanly with no linter warnings.

Posted by Cursor assistant (model: claude-4.6-opus-high-thinking) on behalf of the user (Quang Dao) with approval.

Made with Cursor

Port `PFunctor.FreeM` from VCV-io (ToMathlib/PFunctor/Free.lean). This defines the free monad on a polynomial functor (`PFunctor`), which extends the W-type construction with an extra `pure` constructor. Main definitions: - `PFunctor.FreeM`: inductive type with `pure` and `roll` constructors - `FreeM.lift` / `FreeM.liftA`: lifting from the base functor - `Monad` and `LawfulMonad` instances - `FreeM.inductionOn` / `FreeM.construct`: elimination principles - `FreeM.mapM`: canonical interpretation into any target monad Made-with: Cursor

- Make `pure` constructor protected, add explicit `Pure`/`Bind`/`Functor`/`LawfulFunctor` instances - Add `map`, `id_map`, `comp_map` as explicit definitions before typeclass wiring - Replace `monad_pure_def`/`monad_bind_def` with `@[simp] pure_eq_pure`/`bind_eq_bind` - Rename lemmas to subject-first form: `pure_bind`, `bind_pure`, `roll_bind`, `lift_bind` - Add `bind_pure` (right identity) and `bind_pure_comp` lemmas - Remove `@[always_inline, inline, reducible]` attributes from `lift`, `liftA`, `bind` - Rename `mapM` parameter `s` to `interp` - Add `mapM_seqLeft`, `mapM_seqRight` lemmas - Update `mapM_lift` statement to simplified form Made-with: Cursor

eric-wieser · 2026-04-08T00:04:26Z

Can you include an explanation of the difference with FreeM in the module docstring?

Rename the `roll` constructor and all associated lemma/parameter names to `liftBind`, matching the naming convention of `Cslib.FreeM`. Made-with: Cursor

Flip `pure_eq_pure` to normalize `FreeM.pure` to `pure` (typeclass), matching the direction advocated in leanprover#417. Adjust proofs of `bind_pure`, `bind_pure_comp`, `bind_eq_pure_iff`, `pure_eq_bind_iff`, `pure_inj`, `mapM_bind`, and `mapM_map` to account for the new simp normal form. Made-with: Cursor

Add a "Comparison with Cslib.FreeM" section to the module docstring, showing both liftBind constructors side by side and explaining that PFunctor.FreeM avoids the universe bump from the existential in Cslib.FreeM when the effect signature is naturally polynomial. Made-with: Cursor

Both are redundant with the auto-generated FreeM.rec: - construct is FreeM.rec restricted to Type* (strictly weaker) - inductionOn is FreeM.rec restricted to Prop Plain `induction x with | pure | liftBind` works out of the box. Made-with: Cursor

Match the naming convention of Cslib.FreeM.liftM for the canonical interpreter from the free monad into a target monad. Made-with: Cursor

quangvdao · 2026-04-08T03:40:25Z

Thanks @eric-wieser ! I believe I have addressed all of your comments, including the docstring explaining the difference with FreeM

Address review comments: replace ambiguous "hidden" and "single" wording. Made-with: Cursor

eric-wieser · 2026-04-13T17:04:07Z

+```
+| liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α
+```
+Because `ι` is an implicit (existentially bound) argument, the caller need not name it,


"implicit" in lean usually means {}, but that's not relevent here. Similarly, "existentially-bound" would normally imply the use of Exists, which is also not present here. Could you clarify what you are trying say here?

- Rename FreeM.lean to Free.lean - Use P.FreeM dot notation throughout - Use Type* instead of Type v in variable declaration - Rework docstring comparison with Cslib.FreeM Made-with: Cursor

quangvdao · 2026-04-14T23:21:34Z

Thanks, addressed those as well!

@fmontesi @chenson2018 could you take a look and approve if possible?

Replace "existentially quantifies" / "existentially-bound" with clearer phrasing per review feedback. Made-with: Cursor

# Conflicts: # Cslib.lean

SamuelSchlesinger

Lets also add Interprets and friends to match the existing free monad. Also, lets add docs there pointing over to this file.

SamuelSchlesinger · 2026-05-21T20:28:10Z

+instance : Pure (P.FreeM) where pure := .pure
+
+@[simp]
+theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl


Is there a reason to differ from the convention in Foundations/Control/Monad/Free.lean?

SamuelSchlesinger · 2026-05-21T20:32:41Z

+    (FreeM.liftBind a cont).liftM interp = interp a >>= fun u => (cont u).liftM interp := rfl
+
+@[simp]
+lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl


Given that we have pure_eq_pure, I think we can remove this.

SamuelSchlesinger · 2026-05-21T20:56:10Z

+  · exact FreeM.pure.inj
+  · rintro rfl; rfl
+
+@[simp] lemma liftBind_inj (a a' : P.A)


Because liftBind.injEq already exists as a simp lemma, I think we should remove simp here. A nicer proof might exist as well, this proof is weird. Try starting with constructor, the second branch becomes rintro ⟨rfl, rfl⟩; rfl and the first one goes intro h, obtain ⟨rfl, h⟩ := FreeM.liftBind.inj h, then exact ⟨rfl, eq_of_heq h⟩.

SamuelSchlesinger · 2026-05-21T21:08:01Z

+    (lift x : P.FreeM α) ≠ PFunctor.FreeM.pure y := by simp [lift]
+
+@[simp] lemma pure_ne_lift (x : P α) (y : α) :
+    PFunctor.FreeM.pure y ≠ (lift x : P.FreeM α) := by simp [lift]


Lets make this and lift_ne_pure use P.Obj to match the rest of the file.

SamuelSchlesinger · 2026-05-21T21:41:54Z

If we want to leave Interprets stuff for a follow up I am happy to help there, but the rest seems necessary to address or at least talk through.

quangvdao requested review from chenson2018 and fmontesi as code owners April 7, 2026 18:53

quangvdao force-pushed the quangvdao/pfunctor-freem branch from b713d7d to 2024bc5 Compare April 7, 2026 20:42

eric-wieser reviewed Apr 8, 2026

View reviewed changes