feat(Control): free monads #53
Merged
Conversation
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
chenson2018
requested changes
Aug 29, 2025
tannerduve
force-pushed
the
tannerduve/free-monad
branch
from
80d0b23 to
1f7c6f4
Compare
Collaborator
|
@tannerduve This all looks good to me. As you mentioned, in leanprover-community/mathlib4#25491 this has been approved and marked as |
chenson2018
approved these changes
Sep 3, 2025
Collaborator
|
@fmontesi This looks good to me, the corresponding Mathlib PR has been closed. |
fmontesi
requested changes
Sep 8, 2025
Collaborator
fmontesi
left a comment
fmontesi
left a comment
There was a problem hiding this comment.
Nice to see free monads!
A comment I couldn't put in the files view: please move Control/Monad to Foundations/Control/Monad.
tannerduve
force-pushed
the
tannerduve/free-monad
branch
from
bd13a7f to
c56a44a
Compare
fmontesi
approved these changes
Sep 17, 2025
fmontesi
pushed a commit
that referenced
this pull request
Sep 20, 2025
* create Free.lean * create Effects.lean * import Free.lean from Mathlib PR * import Effects.lean from Mathlib PR * add test file * add monad fold * adding code for fold * formatting * adding some comments * add effect language example in tests * docstrings and suggestions * references and file organization * use LC context * Move Control/Monad to Foundations/Control/Monad and example to tests
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
This PR introduces the Free monad construction for representing effectful computations as syntax trees, enabling clean separation between program syntax and interpretation semantics. Given a type constructor
F : Type ->T Typeyou get a monad "for free".Implementation: Uses the "freer monad" approach since the traditional free monad is not strictly positive and thus fails termination checking. The
FreeM F αtype represents computation trees where nodes (liftBind) are effect requests with continuations, and leaves (pure) are final values.Core contributions
Cslib/Foundations/Control/Monad/Free.lean:FreeMdefinition withFunctor/Monadinstances andLawfulFunctor/LawfulMonadproofs. Includes canonical interpreterliftMwhich is the universal morphism that uniquely defines the free monad.Cslib/Foundations/Control/Monad/Free/Fold.lean: Fold function on the free monad, and uniqueness proof of the universal property of "the unique morphism from an initial algebra" (catamorphism).Cslib/Foundations/Control/Monad/Free/Effects.lean: Standard monad implementations as free monads:FreeState s: State monad withget/putoperationsFreeWriter w: Writer monad, logging computations withtelloperationFreeCont r: Cont monad, continuation-passing computationsCsLibTests/FreeMonad.lean: Complete verified interpreter for an expression language with state, errors, and tracing. Shows how multiple effects can be combined using sum types without monad transformers. Includes big-step operational semantics and correctness proof relating the fold-based interpreter to the semantics.Applications
Embedded DSLs, compilers and interpreters, program analysis, formalizing cryptography, formalizing computational complexity
This enables building interpreters where syntax (what effects to perform) is cleanly separated from semantics (how to interpret those effects), supporting multiple interpretations of the same programs.