Zulip Chat Archive

Stream: lean4

Topic: Why isn't Thunk a Monad?


François G. Dorais (Jan 16 2023 at 15:38):

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 (Jan 16 2023 at 15:45):

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 (Jan 16 2023 at 16:28):

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 (Jan 16 2023 at 16:33):

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 (Jan 16 2023 at 17:53):

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

François G. Dorais (Jan 16 2023 at 18:32):

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


Last updated: Dec 20 2023 at 11:08 UTC