Data.Stream.Hinze.Stream

Functional Pearl: Streams and Unique Fixed Points Ralf Hinze The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008) Victoria, British Columbia, Canada, September 22-24, 2008

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.

Particularly elegant examples are obtained using n+k patterns!

New instances are added for:

Memo, Idiom, Num (!), Enum, Integral, Fractional, NumExt

The great contribution of this pearl are coherent numeric instances for infinite streams, given by:

    (+)              =  zip (+)
    (-)              =  zip (-)
    (*)              =  zip (*)
    negate           =  map negate
    abs              =  map abs
    signum           =  map signum
    toEnum i         =  repeat (toEnum i)
    div              =  zip div
    mod              =  zip mod
    quotRem s t      =  unzip (zip quotRem s t)
    fromInteger      =  repeat . fromInteger
    s / t            =  zip (Prelude./) s t
    recip s          =  map recip s
    fromRational r   =  repeat (fromRational r)
    (^)              =  zip (^)
    (/)              =  zip (/)
    fact             =  map fact
    fall             =  zip fall
    choose           =  zip choose

The Stream data type and basic operations and classes

module Data.Stream

Functions on streams

(<:) :: a -> Stream a -> Stream a

Cons for streams

unzip :: Stream (a, b) -> (Stream a, Stream b)

unzip two streams

(\/) :: Stream a -> Stream a -> Stream a

iterate :: (a -> a) -> a -> Stream a

(<<) :: [a] -> Stream a -> Stream a

Recurrences

nat :: Stream Integer

nat' :: Stream Integer

fac :: Stream Integer

fib :: Stream Integer

fib' :: Stream Integer

fib'' :: Stream Integer

fibv :: Stream Integer

bin :: Stream Integer

msb :: Stream Integer

ones :: Stream Integer

ones' :: Stream Integer

onesv :: Stream Integer

carry :: Stream Integer

frac :: Stream Integer

god :: Stream Integer

jos :: Stream Integer

pot :: Stream Bool

pot' :: Stream Bool

turn :: Integral a => a -> [a]

tree :: Integral a => a -> Stream a

Finite calculus

diff :: Num a => Stream a -> Stream a

sum :: Num a => Stream a -> Stream a

sumv :: Num a => Stream a -> Stream a

Generating functions

const :: Num a => a -> Stream a

z :: Num a => Stream a

(**) :: Num a => Stream a -> Stream a -> Stream a

reciprocal :: Fractional a => Stream a -> Stream a

(//) :: Fractional a => Stream a -> Stream a -> Stream a

power :: (Fractional a, Integral b) => Stream a -> b -> Stream a