Iterators #

The Std.Data.Iterators module provides a uniform abstraction over data that can be iterated over in a sequential way, with a focus on convenience and efficiency. It is heavily inspired by Rust's iterator library and Haskell's streamly.

An iterator is an abstraction of a sequence of values that may or may not terminate. For example, every list can be traversed with an iterator via List.iter.

Most users of the iterator API will just put together existing library functions that create, combine and consume iterators. Consider a simple example:

-- [1, 2, 3].iter : Iter (α := ListIterator α) Nat (α being implicit)
#check [1, 2, 3].iter

-- 12
#eval [1, 2, 3].iter.map (· * 2) |>.fold (init := 0) (· + ·)

An iterator that emits values in β is an element of the type Iter (α := ?) β. The implicit type argument α contains stateful information about the iterator. IterM (α := ?) m β represents iterators over a monad m. In both cases, the implementation is provided by a typeclass Iterator α m β, where m is a monad in which the iteration happens.

The heart of an iterator it : Iter β is its it.step function, which returns it.Step α β. Here, it.Step is a type that either (1) provides an output value in β and a successor iterator (yield), (2) provides only a successor iterator with no output (skip), or (3) signals that the iterator has finished and will provide no more outputs (done). For technical reasons related to termination proofs, the returned it.Step also contains proof that it is a "plausible" step obtained from it.

The step function can also be used by hand:

def sumrec (l : List Nat) : Nat :=
  go (l.iter.map (2 * ·)) 0
where
  go it acc :=
    match it.step with
    | .yield it' n _ => go it' (acc + n)
    | .skip it' _ => go it' acc
    | .done _ => acc
  termination_by it.finitelyManySteps

In general, iterators do not need to terminate after finitely many steps. This example works because the iterator type at hand has an instance of the Std.Iterators.Finite typeclass. Iterators that may not terminate but will not end up in an infinite sequence of .skip steps are called productive. This behavior is encoded in the Std.Iterators.Productive typeclass.

Stability #

The API for the usage of iterators provided in this module can be considered stable, as well as the API for the verification of programms using iterators, unless explicitly stated otherwise.

Contrarily, the API for implementation of new iterators, including the design of the Iterator typeclass, is still experimental and will change in the future. It is already planned that there will be a breaking change to make the iterators more flexible with regard to universes, a change that needs to wait for a language feature.

Module structure #

A distinction that cuts through the whole module is that between pure and monadic iterators. Each submodule contains a dedicated Monadic sub-submodule.

All of the following module names are prefixed with Std.Data.Iterators.

Basic iterator API #

Basic defines Iter and IterM as well as Iterator, Finite and Productive typeclasses.
Producers provides iterator implementations for common data types.
Consumers provides functions that take one or more iterators, iterate over them and potentially return some result. Examples are the toList function and an instance for the ForIn typeclass. These operations allow for what is also known as internal iteration, where the caller delegates the control flow during the iteration to the called consumer.
Combinators will provide operations that transform one or more iterators into a new iterator as soon as the first such combinator has been implemented.

Verification API #

Lemmas provides the means to verify programs that use iterators.

Implementation details #

Internal contains code that should not be relied upon because it may change in the future. This whole module is explicitly experimental and it is not advisable for downstream users to expect stability to implement their own iterators at this point in time.