Remark: we can define mapM, mapM₂ and forM using Applicative instead of Monad.
Example:
def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
| [] => pure []
| a::as => List.cons <$> (f a) <*> mapM as
However, we consider f <$> a <*> b an anti-idiom because the generated code
may produce unnecessary closure allocations.
Suppose m is a Monad, and it uses the default implementation for Applicative.seq.
Then, the compiler expands f <$> a <*> b <*> c into something equivalent to
(Functor.map f a >>= fun g_1 => Functor.map g_1 b) >>= fun g_2 => Functor.map g_2 c
In an ideal world, the compiler may eliminate the temporary closures g_1 and g_2 after it inlines
Functor.map and Monad.bind. However, this can easily fail. For example, suppose
Functor.map f a >>= fun g_1 => Functor.map g_1 b expanded into a match-expression.
This is not unreasonable and can happen in many different ways, e.g., we are using a monad that
may throw exceptions. Then, the compiler has to decide whether it will create a join-point for
the continuation of the match or float it. If the compiler decides to float, then it will
be able to eliminate the closures, but it may not be feasible since floating match expressions
may produce exponential blowup in the code size.
Finally, we rarely use mapM with something that is not a Monad.
Users that want to use mapM with Applicative should use mapA instead.
@[specialize #[]]
Equations
- List.mapM.loop f [] _fun_discr = pure (List.reverse _fun_discr)
- List.mapM.loop f (a :: as) _fun_discr = do let a ← f a List.mapM.loop f as (a :: _fun_discr)
@[specialize #[]]
def
List.forA
{m : Type u → Type v}
[inst : Applicative m]
{α : Type w}
(as : List α)
(f : α → m PUnit)
:
m PUnit
Equations
- List.forA [] f = pure PUnit.unit
- List.forA (a :: as_1) f = SeqRight.seqRight (f a) fun x => List.forA as_1 f
@[specialize #[]]
Equations
- List.filterAuxM f [] _fun_discr = pure _fun_discr
- List.filterAuxM f (h :: t) _fun_discr = do let b ← f h List.filterAuxM f t (bif b then h :: _fun_discr else _fun_discr)
@[inline]
def
List.filterM
{m : Type → Type v}
[inst : Monad m]
{α : Type}
(f : α → m Bool)
(as : List α)
:
m (List α)
Equations
- List.filterM f as = do let as ← List.filterAuxM f as [] pure (List.reverse as)
@[inline]
def
List.filterRevM
{m : Type → Type v}
[inst : Monad m]
{α : Type}
(f : α → m Bool)
(as : List α)
:
m (List α)
Equations
- List.filterRevM f as = List.filterAuxM f (List.reverse as) []
@[inline]
def
List.filterMapM
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : Type u}
(f : α → m (Option β))
(as : List α)
:
m (List β)
Equations
- List.filterMapM f as = List.filterMapM.loop f (List.reverse as) []
@[specialize #[]]
def
List.filterMapM.loop
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : Type u}
(f : α → m (Option β))
:
Equations
- List.filterMapM.loop f [] _fun_discr = pure _fun_discr
- List.filterMapM.loop f (a :: as) _fun_discr = do let a ← f a match a with | none => List.filterMapM.loop f as _fun_discr | some b => List.filterMapM.loop f as (b :: _fun_discr)
@[specialize #[]]
def
List.foldlM
{m : Type u → Type v}
[inst : Monad m]
{s : Type u}
{α : Type w}
(f : s → α → m s)
(init : s)
:
List α → m s
Equations
- List.foldlM _fun_discr _fun_discr [] = pure _fun_discr
- List.foldlM _fun_discr _fun_discr (a :: as) = do let s' ← _fun_discr _fun_discr a List.foldlM _fun_discr s' as
@[inline]
def
List.foldrM
{m : Type u → Type v}
[inst : Monad m]
{s : Type u}
{α : Type w}
(f : α → s → m s)
(init : s)
(l : List α)
:
m s
Equations
- List.foldrM f init l = List.foldlM (fun s a => f a s) init (List.reverse l)
@[specialize #[]]
def
List.firstM
{m : Type u → Type v}
[inst : Monad m]
[inst : Alternative m]
{α : Type w}
{β : Type u}
(f : α → m β)
:
List α → m β
Equations
- List.firstM f [] = failure
- List.firstM f (a :: as) = HOrElse.hOrElse (f a) fun x => List.firstM f as
@[specialize #[]]
Equations
- List.findM? p [] = pure none
- List.findM? p (a :: as) = do let a ← p a match a with | true => pure (some a) | false => List.findM? p as
@[specialize #[]]
def
List.findSomeM?
{m : Type u → Type v}
[inst : Monad m]
{α : Type w}
{β : Type u}
(f : α → m (Option β))
:
Equations
- List.findSomeM? f [] = pure none
- List.findSomeM? f (a :: as) = do let a ← f a match a with | some b => pure (some b) | none => List.findSomeM? f as
@[inline]
def
List.forIn
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(as : List α)
(init : β)
(f : α → β → m (ForInStep β))
:
m β
Equations
- List.forIn as init f = List.forIn.loop f as init
@[specialize #[]]
def
List.forIn.loop
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(f : α → β → m (ForInStep β))
:
List α → β → m β
Equations
- List.forIn.loop f [] _fun_discr = pure _fun_discr
- List.forIn.loop f (a :: as) _fun_discr = do let a ← f a _fun_discr match a with | ForInStep.done b => pure b | ForInStep.yield b => List.forIn.loop f as b
@[simp]
theorem
List.forIn_cons
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[inst : Monad m]
(f : α → β → m (ForInStep β))
(a : α)
(as : List α)
(b : β)
:
forIn (a :: as) b f = do
let x ← f a b
match x with
| ForInStep.done b => pure b
| ForInStep.yield b => forIn as b f
@[inline]
def
List.forIn'
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(as : List α)
(init : β)
(f : (a : α) → a ∈ as → β → m (ForInStep β))
:
m β
Equations
- List.forIn' as init f = List.forIn'.loop as f as init (_ : ∃ bs, bs ++ as = as)
@[specialize #[]]
def
List.forIn'.loop
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(as : List α)
(f : (a : α) → a ∈ as → β → m (ForInStep β))
(as' : List α)
(b : β)
:
Equations
- One or more equations did not get rendered due to their size.
- List.forIn'.loop as f [] _fun_discr x = pure _fun_discr
@[simp]
theorem
List.forM_nil
{m : Type u_1 → Type u_2}
{α : Type u_3}
[inst : Monad m]
(f : α → m PUnit)
:
forM [] f = pure PUnit.unit
Equations
- List.instFunctorList = { map := fun {α β} => List.map, mapConst := fun {α β} => List.map ∘ Function.const β }