Streams, infinite sequences of elements, play an important role in various areas of mathematics and computer science. On the one hand, they represent a fundamental concept of discrete mathematics, where infinite integer sequences are investigated, for example, for solving recurrences. On the other hand, they serve an operational purpose as data types in lazy functional programming languages, such as Haskell, where mutually recursive function definitions can give rise to programs operating on streams--with lazy evaluation, only finite prefixes of the streams are actually computed. This paper combines the constructive with the fundamental aspects, by introducing a calculus whose basic elements--streams and stream operators--are implemented in Haskell and used to reformulate various mathematical theories.

The core idea is a new technique for proving the equality of two streams. Hinze shows that a recursive stream equation, provided that it satisfies some syntactic constraints, has a unique solution; thus, to prove that two streams, s and t, are equal, it suffices to unfold their definitions to forms s = Xs and t = Xt for the same function X. The calculus is applied to numerous examples in discrete mathematics: streams used to capture recurrences, finite calculus (difference equations and summations), and generating functions (handling of power series). The presentation is lively and fun to read; by casting the formal concepts into the Haskell framework--for example, the proof of uniqueness uses Haskell’s generalized algebraic data types--the results may become accessible to a wider audience.