Documentation

Init.Data.Iterators.Combinators.Monadic.FlatMap

Monadic flatMap combinator #

This file provides the flatMap iterator combinator and variants of it.

If it is any iterator, it.flatMap f maps each output of it to an iterator using f.

it.flatMap f first emits all outputs of the first obtained iterator, then of the second, and so on. In other words, it flattens the iterator of iterators obtained by mapping with f.

source
@[unbox]
structure Std.Iterators.Flatten (α α₂ β : Type w) (m : Type w → Type u_1) :
Type w

Internal implementation detail of the flatMap combinator

Instances For
    source
    theorem Std.Iterators.Flatten.ext_iff {α α₂ β : Type w} {m : Type w → Type u_1} {x y : Flatten α α₂ β m} :
    x = y ↔ x.it₁ = y.it₁ ∧ x.it₂ = y.it₂
    source
    theorem Std.Iterators.Flatten.ext {α α₂ β : Type w} {m : Type w → Type u_1} {x y : Flatten α α₂ β m} (it₁ : x.it₁ = y.it₁) (it₂ : x.it₂ = y.it₂) :
    x = y
    source
    @[always_inline]
    def Std.Iterators.IterM.flatMapAfterM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ] (f : β → m (IterM m γ)) (it₁ : IterM m β) (it₂ : Option (IterM m γ)) :
    IterM m γ

    Let it₁ and it₂ be iterators and f a monadic function mapping it₁'s outputs to iterators of the same type as it₂. Then it₁.flatMapAfterM f it₂ first goes over it₂ and then over it₁.flatMap f it₂, emitting all their values.

    The main purpose of this combinator is to represent the intermediate state of a flatMap iterator that is currently iterating over one of the inner iterators.

    Marble diagram (without monadic effects):

    it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥

    Termination properties:

    • Finite instance: only if it₁, it₂ and the inner iterators are finite
    • Productive instance: only if it₁ is finite and it₂ and the inner iterators are productive

    For certain functions f, the resulting iterator will be finite (or productive) even though no Finite (or Productive) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

    Performance:

    This combinator incurs an additional O(1) cost with each output of it₁, it₂ or an internal iterator.

    For each value emitted by the outer iterator it₁, this combinator calls f.

    Equations
    Instances For
      source
      @[always_inline]
      def Std.Iterators.IterM.flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ] (f : β → m (IterM m γ)) (it : IterM m β) :
      IterM m γ

      Let it be an iterator and f a monadic function mapping it's outputs to iterators. Then it.flatMapM f is an iterator that goes over it and for each output, it applies f and iterates over the resulting iterator. it.flatMapM f emits all values obtained from the inner iterators -- first, all of the first inner iterator, then all of the second one, and so on.

      Marble diagram (without monadic effects):

      it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥

      Termination properties:

      • Finite instance: only if it and the inner iterators are finite
      • Productive instance: only if it is finite and the inner iterators are productive

      For certain functions f, the resulting iterator will be finite (or productive) even though no Finite (or Productive) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

      Performance:

      This combinator incurs an additional O(1) cost with each output of it or an internal iterator.

      For each value emitted by the outer iterator it, this combinator calls f.

      Equations
      Instances For
        source
        @[always_inline]
        def Std.Iterators.IterM.flatMapAfter {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ] (f : β → IterM m γ) (it₁ : IterM m β) (it₂ : Option (IterM m γ)) :
        IterM m γ

        Let it₁ and it₂ be iterators and f a function mapping it₁'s outputs to iterators of the same type as it₂. Then it₁.flatMapAfter f it₂ first goes over it₂ and then over it₁.flatMap f it₂, emitting all their values.

        The main purpose of this combinator is to represent the intermediate state of a flatMap iterator that is currently iterating over one of the inner iterators.

        Marble diagram:

        it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥

        Termination properties:

        • Finite instance: only if it₁, it₂ and the inner iterators are finite
        • Productive instance: only if it₁ is finite and it₂ and the inner iterators are productive

        For certain functions f, the resulting iterator will be finite (or productive) even though no Finite (or Productive) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

        Performance:

        This combinator incurs an additional O(1) cost with each output of it₁, it₂ or an internal iterator.

        For each value emitted by the outer iterator it₁, this combinator calls f.

        Equations
        Instances For
          source
          @[always_inline]
          def Std.Iterators.IterM.flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ] (f : β → IterM m γ) (it : IterM m β) :
          IterM m γ

          Let it be an iterator and f a function mapping it's outputs to iterators. Then it.flatMap f is an iterator that goes over it and for each output, it applies f and iterates over the resulting iterator. it.flatMap f emits all values obtained from the inner iterators -- first, all of the first inner iterator, then all of the second one, and so on.

          Marble diagram:

          it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥

          Termination properties:

          • Finite instance: only if it and the inner iterators are finite
          • Productive instance: only if it is finite and the inner iterators are productive

          For certain functions f, the resulting iterator will be finite (or productive) even though no Finite (or Productive) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

          Performance:

          This combinator incurs an additional O(1) cost with each output of it or an internal iterator.

          For each value emitted by the outer iterator it, this combinator calls f.

          Equations
          Instances For
            source
            inductive Std.Iterators.Flatten.IsPlausibleStep {α α₂ β : Type w} {m : Type w → Type w'} [Iterator α m (IterM m β)] [Iterator α₂ m β] (it : IterM m β) (step : IterStep (IterM m β) β) :
            Prop

            The plausible-step predicate for Flatten iterators

            Instances For
              source
              instance Std.Iterators.Flatten.instIterator {α α₂ β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m (IterM m β)] [Iterator α₂ m β] :
              Iterator (Flatten α α₂ β m) m β
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance Std.Iterators.instFiniteFlattenOfIterM {α α₂ β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m (IterM m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m] :
              Finite (Flatten α α₂ β m) m
              source
              instance Std.Iterators.instProductiveFlattenOfFiniteIterM {α α₂ β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m (IterM m β)] [Iterator α₂ m β] [Finite α m] [Productive α₂ m] :
              Productive (Flatten α α₂ β m) m
              source
              instance Std.Iterators.Flatten.instIteratorCollect {α α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m (IterM m β)] [Iterator α₂ m β] :
              IteratorCollect (Flatten α α₂ β m) m n
              Equations
              source
              instance Std.Iterators.Flatten.instIteratorCollectPartial {α α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m (IterM m β)] [Iterator α₂ m β] :
              IteratorCollectPartial (Flatten α α₂ β m) m n
              Equations
              source
              instance Std.Iterators.Flatten.instIteratorLoop {α α₂ β : Type w} {m : Type w → Type w'} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [Iterator α m (IterM m β)] [Iterator α₂ m β] :
              IteratorLoop (Flatten α α₂ β m) m n
              Equations
              source
              instance Std.Iterators.Flatten.instIteratorLoopPartial {α α₂ β : Type w} {m : Type w → Type w'} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [Iterator α m (IterM m β)] [Iterator α₂ m β] :
              IteratorLoopPartial (Flatten α α₂ β m) m n
              Equations