RFC: Monad Thunk

Stream: lean4

[Adrien Champion]

As discussed in the original thread, writing a Monad Thunk (and LawfulMonad Thunk) instance is trivial.

[Adrien Champion]

My understanding is that there is a monad-related simplification for Thunks that we want in there, and that would require having the Monad Thunk instance in core. According to @François G. Dorais:

The issue is that Thunk already has special compiler support to ensure that thunks are evaluated at most once. That support does not currently include the simplification of pure x >>= f to f x.

[Adrien Champion]

I'd be interested in comments and updates on what can be done to add it in core, and I can probably take care of it if it doesn't require super deep technical hacking

[Henrik Böving]

If it is about:

I'm not clear on what you mean by "compiler support". I can open a similar PR to yours on core easily, but if I have to fiddle with internals for "compiler support" that's another story, would probably need some mentoring at least

Then I can sadly only give you our standard answer when it comes to things that touch the compiler right now: The FRO is not putting in ressources into the compiler right now, we are planning on changing that in FRO year 2 but until then matters concerning the compiler are on hold. (unless there is a critical issue of course).

If we provide the Monad and LawfulMonad instances the code that is generated will most likely not be optimal due to the missign compiler support so using the Monad instance would be somewhat of a foot gun.

[Eric Wieser]

I think these instances would be fine in mathlib, perhaps with a warning in a docstring

[David Thrane Christiansen]

How easily will people notice that kind of docstring? Would those affected by the issue ever actually see the warning pop up?

Docstrings are great, but perhaps not for this particular case.

[Eric Wieser]

Perhaps then they should be abbrevs, with a comment saying "you can make this an instance, but watch out for X"

[Adrien Champion]

Regardless of what we do regarding the Monad Thunk instance, maybe we should document this bit in the Thunk doc itself. People (like me) may write the instance themselves and use it without knowing about the pure/bind issue. Maybe we could even link this thread?