# `filterMap`, `filter` and `map` combinators #

This file provides iterator combinators for filtering and mapping.

- `IterM.filterMap` either modifies or drops each value based on an option-valued mapping function.
- `IterM.filter` drops some elements based on a predicate.
- `IterM.map` modifies each value based on a mapping function

Several variants of these combinators are provided:

- `M` suffix: Instead of a pure function, these variants take a monadic function. Given a suitable `MonadLiftT` instance, they also allow lifting the iterator to another monad first and then applying the mapping function in this monad.
- `WithPostcondition` suffix: These variants take a monadic function where the return type in the monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an iterator, and particularly for specialized termination proofs. If possible, avoid this.

source
@[inline]
def Std.Iterators.Iter.filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → PostconditionT m (Option γ)) (it : Iter β) :
IterM m γ

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `filterMap` and `filterMapM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.filterMapWithPostcondition f` is another iterator that applies a monadic function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad. If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

`f` is expected to return `PostconditionT n (Option _)`, where `n` is an arbitrary monad. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                                ---a --b--c --d-e--⊥
    it.filterMapWithPostcondition     ---a'-----c'-------⊥

(given that `f a = pure (some a')`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail, then `it.filterMapWithPostcondition` will be finite even if `it` isn't. In the first case, consider using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of the box.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. If `f` always returns `some _`, a suitable postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondition might be `fun _ => False`.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.Iter.filterMapWithPostcondition f it = Std.Iterators.IterM.filterMapWithPostcondition f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.filterWithPostcondition {α β : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → PostconditionT m (ULift Bool)) (it : Iter β) :
IterM m β

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `filter` and `filterM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.filterWithPostcondition f` is another iterator that applies a monadic predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

`f` is expected to return `PostconditionT n (ULift Bool)`, where `n` is an arbitrary monad. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                             ---a--b--c--d-e--⊥
    it.filterWithPostcondition     ---a-----c-------⊥

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might be `fun _ => False`.

Performance:

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

Equations

- Std.Iterators.Iter.filterWithPostcondition f it = Std.Iterators.IterM.filterWithPostcondition f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → PostconditionT m γ) (it : Iter β) :
IterM m γ

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.mapWithPostcondition f` is another iterator that applies a monadic function `f` to all values emitted by `it` and emits the result.

`f` is expected to return `PostconditionT n _`, where `n` is an arbitrary monad. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                          ---a --b --c --d -e ----⊥
    it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥

(given that `f a = pure a'`, `f b = pure b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.mapWithPostcondition` will be finite even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might be `fun _ => False`.

Performance:

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

Equations

- Std.Iterators.Iter.mapWithPostcondition f it = Std.Iterators.IterM.mapWithPostcondition f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.filterMapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → m (Option γ)) (it : Iter β) :
IterM m γ

If `it` is an iterator, then `it.filterMapM f` is another iterator that applies a monadic function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad. If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

If `f` is pure, then the simpler variant `it.filterMap` can be used instead.

Marble diagram (without monadic effects):

    it                ---a --b--c --d-e--⊥
    it.filterMapM     ---a'-----c'-------⊥

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail, then `it.filterMapM` will be finite even if `it` isn't. In the first case, consider using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of the box.

If that does not help, the more general combinator `it.filterMapWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.Iter.filterMapM f it = Std.Iterators.IterM.filterMapM f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.filterM {α β : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → m (ULift Bool)) (it : Iter β) :
IterM m β

If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

If `f` is pure, then the simpler variant `it.filter` can be used instead.

Marble diagram (without monadic effects):

    it             ---a--b--c--d-e--⊥
    it.filterM     ---a-----c-------⊥

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it` isn't.

In such situations, the more general combinator `it.filterWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

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

Equations

- Std.Iterators.Iter.filterM f it = Std.Iterators.IterM.filterM f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.mapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → m γ) (it : Iter β) :
IterM m γ

If `it` is an iterator, then `it.mapM f` is another iterator that applies a monadic function `f` to all values emitted by `it` and emits the result.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a `MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.map` can be used instead.

Marble diagram (without monadic effects):

    it          ---a --b --c --d -e ----⊥
    it.mapM     ---a'--b'--c'--d'-e'----⊥

(given that `f a = pure a'`, `f b = pure b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.mapM` will be finite even if `it` isn't.

If that does not help, the more general combinator `it.mapWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

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

Equations

- Std.Iterators.Iter.mapM f it = Std.Iterators.IterM.mapM f it.toIterM

Instances For

source
@[inline]
def Std.Iterators.Iter.filterMap {α β γ : Type w} [Iterator α Id β] (f : β → Option γ) (it : Iter β) :
Iter γ

If `it` is an iterator, then `it.filterMap f` is another iterator that applies a function `f` to all values emitted by `it`. `f` is expected to return an `Option`. If it returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

In situations where `f` is monadic, use `filterMapM` instead.

Marble diagram:

    it               ---a --b--c --d-e--⊥
    it.filterMap     ---a'-----c'-------⊥

(given that `f a = some a'`, `f c = c'` and `f b = f d = d e = none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though no `Productive` instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. In such situations, the missing instance needs to be proved manually.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.Iter.filterMap f it = (Std.Iterators.IterM.filterMap f it.toIterM).toIter

Instances For

source
@[inline]
def Std.Iterators.Iter.filter {α β : Type w} [Iterator α Id β] (f : β → Bool) (it : Iter β) :
Iter β

If `it` is an iterator, then `it.filter f` is another iterator that applies a predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

In situations where `f` is monadic, use `filterM` instead.

Marble diagram (without monadic effects):

    it            ---a--b--c--d-e--⊥
    it.filter     ---a-----c-------⊥

(given that `f a = f c = true` and `f b = f d = d e = false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though no `Productive` instance is provided. For example, if `f` always returns `True`, the resulting iterator will be productive as long as `it` is. In such situations, the missing instance needs to be proved manually.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned value.

Equations

- Std.Iterators.Iter.filter f it = (Std.Iterators.IterM.filter f it.toIterM).toIter

Instances For

source
@[inline]
def Std.Iterators.Iter.map {α β γ : Type w} [Iterator α Id β] (f : β → γ) (it : Iter β) :
Iter γ

If `it` is an iterator, then `it.map f` is another iterator that applies a function `f` to all values emitted by `it` and emits the result.

In situations where `f` is monadic, use `mapM` instead.

Marble diagram:

    it         ---a --b --c --d -e ----⊥
    it.map     ---a'--b'--c'--d'-e'----⊥

(given that `f a = a'`, `f b = b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

Performance:

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

Equations

- Std.Iterators.Iter.map f it = (Std.Iterators.IterM.map f it.toIterM).toIter

Instances For