@@ -6,6 +6,7 @@ import Builtins
6import Prelude.Functor
6import Prelude.Functor
7import public Prelude.Applicative
7import public Prelude.Applicative
8import Prelude.Basics
8import Prelude.Basics
9+import Prelude.Foldable
11%access public export
12%access public export
@@ -33,6 +34,11 @@ flatten : Monad m => m (m a) -> m a
33flatten = join
34flatten = join
34%deprecate flatten "Please use `join`, which is the standard name."
35%deprecate flatten "Please use `join`, which is the standard name."
37+||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
38+||| Consequently, the final value is wrapped in the same `Monad`.
39+foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
40+foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
36-- Annoyingly, these need to be here, so that we can use them in other
42-- Annoyingly, these need to be here, so that we can use them in other
37-- Prelude modules other than the top level.
43-- Prelude modules other than the top level.
@@ -48,4 +54,3 @@ Applicative (IO' ffi) where
49Monad (IO' ffi) where
55Monad (IO' ffi) where
50 b >>= k = io_bind b k
56 b >>= k = io_bind b k