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 β)

Applies the monadic action f on every element in the list, left-to-right, and returns the list of results.

See List.forM for the variant that discards the results. See List.mapA for the variant that works with Applicative.

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 β)

      Applies the applicative action f on every element in the list, left-to-right, and returns the list of results.

      NB: If m is also a Monad, then using mapM can be more efficient.

      See List.forA for the variant that discards the results. See List.mapM for the variant that works with Monad.

      Warning: this function is not tail-recursive, meaning that it may fail with a stack overflow on long lists.

      Equations
      Instances For
        @[specialize #[]]
        def List.forM {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : αm PUnit) :

        Applies the monadic action f on every element in the list, left-to-right.

        See List.mapM for the variant that collects results. See List.forA for the variant that works with Applicative.

        Equations
        Instances For
          @[specialize #[]]
          def List.forA {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : αm PUnit) :

          Applies the applicative action f on every element in the list, left-to-right.

          NB: If m is also a Monad, then using forM can be more efficient.

          See List.mapA for the variant that collects results. See List.forM for the variant that works with Monad.

          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} (p : αm Bool) (as : List α) :
              m (List α)

              Applies the monadic predicate p on every element in the list, left-to-right, and returns those elements x for which p x returns true.

              Equations
              Instances For
                @[inline]
                def List.filterRevM {m : TypeType v} [Monad m] {α : Type} (p : αm Bool) (as : List α) :
                m (List α)

                Applies the monadic predicate p on every element in the list, right-to-left, and returns those elements x for which p x returns true.

                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 β)

                  Applies the monadic function f on every element x in the list, left-to-right, and returns those results y for which f x returns some y.

                  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

                      Folds a monadic function over a list from left to right:

                      foldlM f x₀ [a, b, c] = do
                        let x₁ ← f x₀ a
                        let x₂ ← f x₁ b
                        let x₃ ← f x₂ c
                        pure x₃
                      
                      Equations
                      Instances For
                        @[simp]
                        theorem List.foldlM_nil {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : βαm β) (b : β) :
                        List.foldlM f b [] = pure b
                        @[simp]
                        theorem List.foldlM_cons {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : βαm β) (b : β) (a : α) (l : List α) :
                        List.foldlM f b (a :: l) = do let initf b a List.foldlM f init l
                        @[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

                        Folds a monadic function over a list from right to left:

                        foldrM f x₀ [a, b, c] = do
                          let x₁ ← f c x₀
                          let x₂ ← f b x₁
                          let x₃ ← f a x₂
                          pure x₃
                        
                        Equations
                        Instances For
                          @[simp]
                          theorem List.foldrM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αβm β) (b : β) :
                          List.foldrM f b [] = pure b
                          @[specialize #[]]
                          def List.firstM {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : αm β) :
                          List αm β

                          Maps f over the list and collects the results with <|>.

                          firstM f [a, b, c] = f a <|> f b <|> f c <|> failure
                          
                          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.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} :
                                        ForIn m (List α) α
                                        Equations
                                        • List.instForIn = { forIn := fun {β : Type ?u.20} [Monad m] => List.forIn }
                                        @[simp]
                                        theorem List.forIn_eq_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] :
                                        List.forIn = 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 xf 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'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} :
                                            ForIn' m (List α) α inferInstance
                                            Equations
                                            • List.instForIn'InferInstanceMembership = { forIn' := fun {β : Type ?u.20} [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.instForM {m : Type u_1 → Type u_2} {α : Type u_3} :
                                            ForM m (List α) α
                                            Equations
                                            • List.instForM = { 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