Needed for self hosting, and probably ought to be in the prelude by the usual rule of thumb
Unified · Split
| @@ -580,6 +580,12 @@ interface Foldable (t : Type -> Type) where · 579 unmodified lines | ||
| 580 | 580 | foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc |
| 581 | 581 | foldl f z t = foldr (flip (.) . flip f) id t z |
| 582 | 582 | |
| 583 | +||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`. | |
| 584 | +||| Consequently, the final value is wrapped in the same `Monad`. | |
| 585 | +public export | |
| 586 | +foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a | |
| 587 | +foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0) | |
| 588 | + | |
| 583 | 589 | ||| Combine each element of a structure into a monoid. |
| 584 | 590 | public export |
| 585 | 591 | concat : (Foldable t, Monoid a) => t a -> a |