Documentation

Init.Data.List.Control

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.

@[inline]
def List.mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : αm β) (as : List α) :
m (List β)
Equations
Instances For
    @[specialize #[]]
    def List.mapM.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : αm β) :
    List αList βm (List β)
    Equations
    Instances For
      @[specialize #[]]
      def List.mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : αm β) :
      List αm (List β)
      Equations
      Instances For
        @[specialize #[]]
        def List.forM {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : αm PUnit) :
        Equations
        Instances For
          @[specialize #[]]
          def List.forA {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : αm PUnit) :
          Equations
          Instances For
            @[specialize #[]]
            def List.filterAuxM {m : TypeType v} [Monad m] {α : Type} (f : αm Bool) :
            List αList αm (List α)
            Equations
            Instances For
              @[inline]
              def List.filterM {m : TypeType v} [Monad m] {α : Type} (f : αm Bool) (as : List α) :
              m (List α)
              Equations
              Instances For
                @[inline]
                def List.filterRevM {m : TypeType v} [Monad m] {α : Type} (f : αm Bool) (as : List α) :
                m (List α)
                Equations
                Instances For
                  @[inline]
                  def List.filterMapM {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : αm (Option β)) (as : List α) :
                  m (List β)
                  Equations
                  Instances For
                    @[specialize #[]]
                    def List.filterMapM.loop {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : αm (Option β)) :
                    List αList βm (List β)
                    Equations
                    Instances For
                      @[specialize #[]]
                      def List.foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : sαm s) (init : s) :
                      List αm s
                      Equations
                      Instances For
                        @[inline]
                        def List.foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : αsm s) (init : s) (l : List α) :
                        m s
                        Equations
                        Instances For
                          @[specialize #[]]
                          def List.firstM {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : αm β) :
                          List αm β
                          Equations
                          Instances For
                            @[specialize #[]]
                            def List.anyM {m : TypeType u} [Monad m] {α : Type v} (f : αm Bool) :
                            List αm Bool
                            Equations
                            Instances For
                              @[specialize #[]]
                              def List.allM {m : TypeType u} [Monad m] {α : Type v} (f : αm Bool) :
                              List αm Bool
                              Equations
                              Instances For
                                @[specialize #[]]
                                def List.findM? {m : TypeType u} [Monad m] {α : Type} (p : αm Bool) :
                                List αm (Option α)
                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def List.findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : αm (Option β)) :
                                  List αm (Option β)
                                  Equations
                                  Instances For
                                    @[inline]
                                    def List.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : αβm (ForInStep β)) :
                                    m β
                                    Equations
                                    Instances For
                                      @[specialize #[]]
                                      def List.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm (ForInStep β)) :
                                      List αβm β
                                      Equations
                                      Instances For
                                        instance List.instForInList {m : Type u_1 → Type u_2} {α : Type u_3} :
                                        ForIn m (List α) α
                                        Equations
                                        • List.instForInList = { forIn := fun {β : Type u_1} [Monad m] => List.forIn }
                                        @[simp]
                                        theorem List.forIn_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αβm (ForInStep β)) (b : β) :
                                        forIn [] b f = pure b
                                        @[simp]
                                        theorem List.forIn_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [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} [Monad m] (as : List α) (init : β) (f : (a : α) → a asβm (ForInStep β)) :
                                        m β
                                        Equations
                                        Instances For
                                          @[specialize #[]]
                                          def List.forIn'.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (f : (a : α) → a asβm (ForInStep β)) (as' : List α) (b : β) :
                                          (∃ (bs : List α), bs ++ as' = as)m β
                                          Equations
                                          Instances For
                                            instance List.instForIn'ListInferInstanceMembershipInstMembershipList {m : Type u_1 → Type u_2} {α : Type u_3} :
                                            ForIn' m (List α) α inferInstance
                                            Equations
                                            • List.instForIn'ListInferInstanceMembershipInstMembershipList = { forIn' := fun {β : Type u_1} [Monad m] => List.forIn' }
                                            @[simp]
                                            theorem List.forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : αβm (ForInStep β)) :
                                            (forIn' as init fun (a : α) (x : a as) (b : β) => f a b) = forIn as init f
                                            instance List.instForMList {m : Type u_1 → Type u_2} {α : Type u_3} :
                                            ForM m (List α) α
                                            Equations
                                            • List.instForMList = { forM := fun [Monad m] => List.forM }
                                            @[simp]
                                            theorem List.forM_nil {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : αm PUnit) :
                                            @[simp]
                                            theorem List.forM_cons {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : αm PUnit) (a : α) (as : List α) :
                                            forM (a :: as) f = do f a forM as f
                                            Equations