feat(Data/PFunctor): add free monad of a polynomial functor#477
Open
quangvdao wants to merge 7 commits intoleanprover:mainfrom
Open
feat(Data/PFunctor): add free monad of a polynomial functor#477quangvdao wants to merge 7 commits intoleanprover:mainfrom
quangvdao wants to merge 7 commits intoleanprover:mainfrom
Conversation
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
quangvdao
force-pushed
the
quangvdao/pfunctor-freem
branch
from
b713d7d to
2024bc5
Compare
- 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
Collaborator
|
Can you include an explanation of the difference with FreeM in the module docstring? |
eric-wieser
reviewed
Apr 8, 2026
eric-wieser
reviewed
Apr 8, 2026
eric-wieser
reviewed
Apr 8, 2026
eric-wieser
reviewed
Apr 8, 2026
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
Author
|
Thanks @eric-wieser ! I believe I have addressed all of your comments, including the docstring explaining the difference with |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
PFunctor.FreeMfrom VCV-io (ToMathlib/PFunctor/Free.lean) to cslib.pureconstructor, yielding a lawful monad that is free overP : PFunctor.Main definitions
PFunctor.FreeM: inductive type withpureandrollconstructorsFreeM.lift/FreeM.liftA: lifting from the base polynomial functorMonadandLawfulMonadinstancesFreeM.inductionOn/FreeM.construct: propositional and dependent eliminatorsFreeM.mapM: canonical interpretation into any target monad, withsimplemmas forbind,map,seq, etc.Notes
MonadHom-related definitions (mapMHom,mapMHom') from the original VCV-io source are omitted since cslib does not haveMonadHominfrastructure. These can be added later if cslib gains monad homomorphism support.Cslib/Foundations/Data/PFunctor/FreeM.leanas a foundation for future polynomial functor work.Posted by Cursor assistant (model: claude-4.6-opus-high-thinking) on behalf of the user (Quang Dao) with approval.
Made with Cursor