Why isn't Thunk a Monad?

Stream: lean4

[François G. Dorais]

It probably doesn't need to be a monad since it works pretty well as-is. However, I wonder if there is a reason why it shouldn't be a monad.

I noticed when I tried to write def foo : Thunk α := do ... but I realized that I needed to write def foo : Thunk α := Id.run do ... and rely on the coercion from α to Thunk α.

[Kyle Miller]

Of course it "is" a monad since there are docs4#Thunk.pure docs4#Thunk.bind (to be pedantic/annoying), but I'm also wondering if there's any reason there shouldn't be a Monad instance.

Relying on the coercion feels weird since it obscures when computations are happening.

[François G. Dorais]

I just checked that this works:

instance : Monad Thunk where
  pure := Thunk.pure
  bind := Thunk.bind
  map  := Thunk.map

instance : LawfulMonad Thunk where
  map_const      := by intros; rfl
  id_map         := by intros; rfl
  bind_assoc     := by intros; rfl
  bind_pure_comp := by intros; rfl
  bind_map       := by intros; rfl
  pure_bind      := by intros; rfl
  pure_seq       := by intros; rfl
  seqLeft_eq     := by intros; rfl
  seqRight_eq    := by intros; rfl

So it really is a monad. There could still be issues related to the special support for Thunk in runtime which would make it ill-behaved.

[Sebastian Ullrich]

The compiler does not currently know anything about eliminating Thunk.pure _ >>= _. Which to be fair is mostly an issue if you then go on to define ThunkT and get implicit Thunk.pures from monad lifting everywhere.

[Henrik Böving]

We could easily add that as a rewrite rule for the new compiler :eyes:

[François G. Dorais]

So it would be mostly harmless and potentially useful to add. I made a quick PR to add it in Std.

[Adrien Champion]

@François G. Dorais I just re-did the exact same thing: Monad and LawfulMonad instances for Thunk. I'm not sure about what happened to your PR, I can't find a Monad Thunk instance anywhere (core/std/mathlib)

[Adrien Champion]

Is std still interested in a PR on this? I don't mind opening the PR

[Adrien Champion]

Also, as far as I can tell std mentions Thunk exactly thrice

Std/Data/MLList/Basic.lean
41:  | thunk : Thunk (MLListImpl m α) → MLListImpl m α

Std/Tactic/Omega/Core.lean
310:  explanation? : Thunk String := ""
352:        explanation? := Thunk.mk fun _ => j.toString

Wouldn't it make more sense to have the Monad instance in core?

[François G. Dorais]

@Adrien Champion std4#88 suffered from bit rot so it was closed. I think it's better off in core since it needs compiler support to be useful.

[Adrien Champion]

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

[Eric Wieser]

François G. Dorais said:

Adrien Champion std4#88 suffered from bit rot so it was closed. I think it's better off in core since it needs compiler support to be useful.

Since getting things into core requires quite a strong motivation, would it make sense to have it reside in Std or Mathlib in the meantime?

[François G. Dorais]

The compiler issue was described by @Sebastian Ullrich in this thread. @Henrik Böving showed this will be easy to fix in the new compiler. I think the issue is that parts of the old compiler are basically frozen, so pure-bind elimination for Thunk will probably only happen in the new compiler.