It's interesting to see how much Haskell has changed since this was written. It feels weird not having every Monad be an Applicative Functor. (Sidenote, I really like that you can define a Monad instance in Lean 4 and automatically get those. I guess Haskellers derive this stuff anyway, so it's not the biggest deal)