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.