Monadic 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.

@[unbox]

structure Std.Iterators.FilterMap (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) (f : β → PostconditionT n (Option γ)) : Type w

Internal state of the filterMap combinator. Do not depend on its internals.

• inner : IterM m β

  Internal implementation detail of the iterator library.

theorem Std.Iterators.FilterMap.ext {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} {x y : FilterMap α m n lift f} (inner : x.inner = y.inner) : x = y

theorem Std.Iterators.FilterMap.ext_iff {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} {x y : FilterMap α m n lift f} : x = y ↔ x.inner = y.inner

def Std.Iterators.Map (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) [Functor n] (f : β → PostconditionT n γ) : Type w

Internal state of the map combinator. Do not depend on its internals.

Equations

• Std.Iterators.Map α m n lift f = Std.Iterators.FilterMap α m n lift fun (b : β) => Std.Iterators.PostconditionT.map some (f b)

@[inline]

def Std.Iterators.IterM.InternalCombinators.filterMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} (lift : ⦃α : Type w⦄ → m α → n α) [Iterator α m β] (f : β → PostconditionT n (Option γ)) (it : IterM m β) : IterM n γ

Equations

• Std.Iterators.IterM.InternalCombinators.filterMap lift f it = Std.Iterators.toIterM { inner := it } n γ

@[inline]

def Std.Iterators.IterM.InternalCombinators.map {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] (lift : ⦃α : Type w⦄ → m α → n α) [Iterator α m β] (f : β → PostconditionT n γ) (it : IterM m β) : IterM n γ

Equations

• Std.Iterators.IterM.InternalCombinators.map lift f it = Std.Iterators.toIterM { inner := it } n γ

@[inline]

def Std.Iterators.IterM.filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (Option γ)) (it : IterM m β) : IterM n γ

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 _). The base iterator it being monadic in m, n can be different from m, but it.filterMapWithPostcondition f expects a MonadLiftT m n instance. 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.IterM.filterMapWithPostcondition f it = Std.Iterators.IterM.InternalCombinators.filterMap (fun ⦃x : Type ?u.26⦄ => monadLift) f it

inductive Std.Iterators.FilterMap.PlausibleStep {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] (it : IterM n γ) : IterStep (IterM n γ) γ → Prop

it.PlausibleStep step is the proposition that step is a possible next step from the filterMap iterator it. This is mostly internally relevant, except if one needs to manually prove termination (Finite or Productive instances, for example) of a filterMap iterator.

• yieldNone {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (f out).Property none → PlausibleStep it (IterStep.skip (IterM.InternalCombinators.filterMap lift f it'))
• yieldSome {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} {out : β} {out' : γ} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (f out).Property (some out') → PlausibleStep it (IterStep.yield (IterM.InternalCombinators.filterMap lift f it') out')
• skip {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → PlausibleStep it (IterStep.skip (IterM.InternalCombinators.filterMap lift f it'))
• done {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done

instance Std.Iterators.FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] [Monad n] : Iterator (FilterMap α m n lift f) n γ

Equations

• One or more equations did not get rendered due to their size.

instance Std.Iterators.instIteratorMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} : Iterator (Map α m n lift f) n γ

Equations

• Std.Iterators.instIteratorMap = inferInstanceAs (Std.Iterators.Iterator (Std.Iterators.FilterMap α m n lift fun (b : β) => Std.Iterators.PostconditionT.map some (f b)) n γ)

instance Std.Iterators.FilterMap.instFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] : Finite (FilterMap α m n lift f) n

instance Std.Iterators.instFiniteMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] : Finite (Map α m n lift f) n

instance Std.Iterators.Map.instProductive {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Productive α m] : Productive (Map α m n lift f) n

instance Std.Iterators.instIteratorCollectFilterMapOfMonad {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} : IteratorCollect (FilterMap α m n lift f) n o

Equations

• Std.Iterators.instIteratorCollectFilterMapOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.Iterators.instIteratorCollectPartialFilterMapOfMonadOfFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] : IteratorCollectPartial (FilterMap α m n lift f) n o

Equations

• Std.Iterators.instIteratorCollectPartialFilterMapOfMonadOfFinite = Std.Iterators.IteratorCollectPartial.defaultImplementation

instance Std.Iterators.FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] : IteratorLoop (FilterMap α m n lift f) n o

Equations

• Std.Iterators.FilterMap.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.Iterators.FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] : IteratorLoopPartial (FilterMap α m n lift f) n o

Equations

• Std.Iterators.FilterMap.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

instance Std.Iterators.Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift₁ : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] : IteratorCollect (Map α m n lift₁ f) n o

map operations allow for a more efficient implementation of toArray. For example, `array.iter.map f |>.toArray happens in-place if possible.

Equations

• One or more equations did not get rendered due to their size.

instance Std.Iterators.Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift₁ : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorCollectPartial α m o] : IteratorCollectPartial (Map α m n lift₁ f) n o

Equations

• One or more equations did not get rendered due to their size.

instance Std.Iterators.Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} : IteratorLoop (Map α m n lift f) n o

Equations

• Std.Iterators.Map.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.Iterators.Map.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} : IteratorLoopPartial (Map α m n lift f) n o

Equations

• Std.Iterators.Map.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

@[inline]

def Std.Iterators.IterM.mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n γ) (it : IterM m β) : IterM n γ

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 _. The base iterator it being monadic in m, n can be different from m, but it.mapWithPostcondition f expects a MonadLiftT m n instance. 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 exaple, 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.IterM.mapWithPostcondition f it = Std.Iterators.IterM.InternalCombinators.map (fun {x : Type ?u.27} => monadLift) f it

@[inline]

def Std.Iterators.IterM.filterWithPostcondition {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (ULift Bool)) (it : IterM m β) : IterM n β

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). The base iterator it being monadic in m, n can be different from m, but it.filterWithPostcondition f expects a MonadLiftT m n instance. 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 exaple, 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

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.IterM.filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n (Option γ)) (it : IterM m β) : IterM n γ

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.

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.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.IterM.filterMapM f it = Std.Iterators.IterM.filterMapWithPostcondition (fun (b : β) => Std.Iterators.PostconditionT.lift (f b)) it

@[inline]

def Std.Iterators.IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM m β) : IterM n γ

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 exaple, 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.IterM.mapM f it = Std.Iterators.IterM.filterMapWithPostcondition (fun (b : β) => some <$> Std.Iterators.PostconditionT.lift (f b)) it

@[inline]

def Std.Iterators.IterM.filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n (ULift Bool)) (it : IterM m β) : IterM n β

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.

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.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 exaple, 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

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.IterM.filterMap {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → Option γ) (it : IterM m β) : IterM m γ

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.IterM.filterMap f it = Std.Iterators.IterM.filterMapWithPostcondition (fun (b : β) => pure (f b)) it

@[inline]

def Std.Iterators.IterM.map {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → γ) (it : IterM m β) : IterM m γ

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.IterM.map f it = Std.Iterators.IterM.mapWithPostcondition (fun (b : β) => pure (f b)) it

@[inline]

def Std.Iterators.IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → Bool) (it : IterM m β) : IterM m β

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.IterM.filter f it = Std.Iterators.IterM.filterMap (fun (b : β) => if f b = true then some b else none) it