Programming with streams

The goal of this lecture note is introduce the concept of streams and to illustrate how to program with them.

Resources

• The .v file for the present lecture note (latest version: 09 Apr 2025).

Streams

A stream if a lazy data type for representing infinite sequences of payloads that are constructed on demand. So its declared coinductively and it only has one data constructor:

CoInductive stream (V : Type) : Type :=
  SCons : V -> stream V -> stream V.

Property a_stream_does_not_end :
  forall (V : Type)
         (vs : stream V),
    exists (v : V) (vs' : stream V),
      vs = SCons V v vs'.
Proof.
  intros V [v vs'].
  exists v, vs'.
  reflexivity.
Qed.

The accompanying .v file contains a variety of streams (e.g., the stream of the successive Peano numbers) and of utilities:

• to fetch the payload of a given stream at a given index (represented as a Peano number);
• given a stream and a number n, to construct its list prefix, i.e., the list of its first n elements;
• given a function, to map it over the successive elements of a given stream and to construct a resulting stream with the result of these applications;
• to map a stream into the stream of its prefix sums; and
• to “transduce” a stream of pairs into a stream of triples and vice versa.

It also contains a variety of examples where streams are indexed, where their prefixes are constructed, where streams are mapped over, etc. These examples illustrate how the same streams can be constructed in different ways.

Next week, we shall formalize this notion of sameness – for how can two infinite sequences that are not constructed yet can be said to be “the same”? Hmm?

Resources

• The .v file for the present lecture note (latest version: 09 Apr 2025).

Version

Created [09 Apr 2025]