English
For a monad m with LawfulMonad, the monadic left fold equals a left fold with binds, i.e., foldlM f b l = foldl (λ mb a. mb >>= f a) (pure b) l.
Русский
При наличии монадического устройства и закона удовлетворения, левая свёртка с монадами эквивалентна обычной свёртке слева с операцией связывания: foldlM f b l = foldl (λ mb a. mb >>= f a) (pure b) l.
LaTeX
$$$$\operatorname{foldlM} f\, b\, l = \operatorname{foldl}(\lambda mb\, a.\; mb \bind\ f\ a)\; (\operatorname{pure} b)\; l.$$$$
Lean4
theorem foldlM_eq_foldl (f : β → α → m β) (b l) :
List.foldlM f b l = foldl (fun mb a => mb >>= fun b => f b a) (pure b) l :=
by
suffices h : ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l by
simp [← h (pure b)]
induction l with
| nil => simp
| cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]
