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.

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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