Programming-style monads in Mathlib

Stream: mathlib4

[Tanner Duve]

Hi all,

This is in regard to PR #25491, which defines and develops the theory of the free monad in the programming sense (rather than the categorical one), although several of the theorems proven do correspond to categorical properties.

@Yaël Dillies noted that Mathlib is not primarily oriented toward computer science applications, so perhaps this would be better suited to batteries. I initially had the same thought, but seeing that we already have a Control/Monads directory, I decided to propose it for Mathlib. (I’m also unfamiliar with the process of contributing to Batteries.)

That said, there are some mathematical applications. For instance, @Quang Dao has used free monads for formalizing cryptographic proofs and #20924 is implicitly using a free monad for studying query complexity. Also, we could explore the free monad purely categorically by using CategoryTheory.ofTypeMonad (FreeM F) to get a free monad on the category of types.

I do think the free monad is a foundational and elegant FP abstraction, and since it exists in other FP ecosystems (see Haskell and Scala), I think it should exist somewhere in Lean. But I'd love to get some thoughts from others on where this belongs and whether others would support merging it to Mathlib.

[Eric Wieser]

I'm happy with this being in Mathlib, at least as long as the rest of Control is there.

[Kim Morrison]

I'd prefer to see someone make a new repo to host things like this. :-)

[Kevin Buzzard]

I am torn between "mathlib should accept anything because we want growth" and "mathlib should stick to maths because it's what the maintainers are competent at". Note that a lot of the control stuff was written by Hudon who is no longer a contributor.

[Alok Singh]

Kim Morrison said:

I'd prefer to see someone make a new repo to host things like this. :-)

I'm glad mathlib is breaking out its useful tools into separate pkgs bc that's a big motivation to stay in mathlib's demesne

[Eric Wieser]

I think some of the control stuff is used in tactics; so If the whole directory were to move out of mathlib, Mathlib would take a dependency on it. I don't think we should let such a refactor get in the way of Tanner's work, nor is it clear to me that the Control folder is particular costly to maintain

[Tanner Duve]

Hey all, don't mean to necro this thread but quick update, I've opened this PR up in #CSLib , but for the sake of avoiding duplications the reviewers there want to make sure it gets resolved here before approving it. Should I close the mathlib PR and just have it put in CSLib?

[Devon Tuma]

cc @Quang Dao wherever this does eventually get merged is probably also where we want to try and merge the polynomial functor version of free monads as well

[Chris Henson]

For reference, the new PR is cslib#53. A small difference to note is that I encouraged the inclusion of an expression language using this construction, which to me feels more appropriate in Cslib than it would in Mathlib.