Numeric instances for infinite streams. An implementation of:
Functional Pearl: Streams and Unique Fixed Points, Ralf Hinze, University of Oxford
Streams, infinite sequences of elements, live in a coworld: they are
given by a coinductive data type, operations on streams are implemented
by corecursive programs, and proofs are conducted using coinduction. But
there is more to it: suitably restricted, stream equations possess
unique solutions, a fact that is not very widely appreciated. We show
that this property gives rise to a simple and attractive proof technique
essentially bringing equational reasoning to the coworld. In fact, we
redevelop the theory of recurrences, finite calculus and generating
functions using streams and stream operators building on the cornerstone
of unique solutions. The development is constructive: streams and stream
operators are implemented in Haskell, usually by one-liners. The
resulting calculus or library, if you wish, is elegant and fun to use.
Finally, we rephrase the proof of uniqueness using generalised algebraic
data types.
Along with the usual instances for infinite streams, this provides:
Num, Enum, Real, Fractional, as well as recurrences on streams,
finite calculus, generators
