hinze-streams-1.0: Data/Stream/Hinze/Stream.hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-- |
-- 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
module Data.Stream.Hinze.Stream (
-- * The Stream data type and basic operations and classes
module Data.Stream,
-- * Functions on streams
(<:),
unzip,
(\/),
iterate,
(<<),
-- * Recurrences
nat, nat', fac, fib, fib', fib'', fibv, bin,
msb, ones, ones', onesv, carry, frac, god, jos,
pot, pot',
turn,
tree,
-- * Finite calculus
diff,
sum,
sumv,
-- * Generating functions
const,
z,
(**),
reciprocal,
(//),
power
) where
import Prelude hiding
(head, tail, const, repeat, map, zip, unzip, iterate, lookup, sum, (**), (/), (^))
import qualified Prelude
import Data.Stream.Hinze.Memo
import Data.Stream.Hinze.Idiom
import Data.Stream.Hinze.NumExt
-- Use Wouter's Stream data type:
import Data.Stream (Stream(..), head, tail)
default (Integer, Rational)
-- TODO: does not work in GHC (power nat 2).
---
-- data Stream a = Cons a (Stream a) deriving (Eq, Ord)
--
-- data Stream a = Cons { head :: a, tail :: Stream a }
--
-- | Cons for streams
infixr 5 <:
(<:) :: a -> Stream a -> Stream a
a <: s = Cons a s
---
{-
< Natural -> A ~= Stream A
< data Natural = Zero | Succ Natural
< instance Memo Natural Stream where
< tabulate f = f Zero <: tabulate (f . Succ)
<
< lookup s Zero = head s
< lookup s (Succ n) = lookup (tail s) n
-}
-- | Streams of type 'Stream a' are memoised functions of type 'Natural -> A|'
instance (Integral a) => Memo a Stream where
tabulate f = f 0 <: tabulate (f . (+ 1))
lookup s 0 = head s
lookup s (n + 1) = lookup (tail s) n
lookup _ _ = error "lookup: negative argument"
---
-- | Stream are idioms aka applicative functors.
--
instance Idiom Stream where
pure a = s where s = a <: s
s <> t = (head s) (head t) <: (tail s) <> (tail t)
repeat a = s where s = a <: s
map f s = f (head s) <: map f (tail s)
zip g s t = g (head s) (head t) <: zip g (tail s) (tail t)
---
-- | Instance declarations.
-- |
first :: Int -> Stream aT -> [aT]
first 0 _s = []
first (n + 1) s = head s : first n (tail s)
first _ _ = error "first: negative argument"
-- | Showing a stream
showStream :: (Show a) => Int -> Stream a -> ShowS
showStream l s = showString "<" . showl (first l s)
where showl [] = showString "..>"
showl (a : as) = shows a . showString ", " . showl as
{-
-- Wouter's class derives (Eq, Ord), Ralf hacks around. We go with
-- Wouter (i.e. they diverge).
instance (Show a) => Show (Stream a) where
showsPrec _d = showStream len -- HACK
instance (Eq a) => Eq (Stream a) where
s == t = first len s == first len t -- HACK
instance (Ord a) => Ord (Stream a) where
s <= t = first len s <= first len t -- HACK
-}
-- | `Generic' instances for |Functor| and numeric classes.
-- > instance Functor Stream where
-- > fmap = map
-- | Num instance for streams
instance (Num a) => Num (Stream a) where
(+) = zip (+)
(-) = zip (-)
(*) = zip (*)
negate = map negate
abs = map abs
signum = map signum
fromInteger = repeat . fromInteger
-- | Enumerate streams
instance (Enum a) => Enum (Stream a) where
toEnum i = repeat (toEnum i)
fromEnum = error "fromEnum: not defined for streams"
-- Fake Real instance
instance (Real a) => Real (Stream a) where
toRational = error "toRational: not defined for streams"
-- | Integral streams
instance (Integral a) => Integral (Stream a) where
div = zip div
mod = zip mod
quotRem s t = unzip (zip quotRem s t)
toInteger = error "toInteger: not defined for streams"
-- | Fractional streams
instance (Fractional a) => Fractional (Stream a) where
s / t = zip (Prelude./) s t
recip s = map recip s
fromRational r = repeat (fromRational r)
-- | unzip two streams
unzip :: Stream (a, b) -> (Stream a, Stream b)
unzip s = (a <: as, b <: bs)
where (a, b ) = head s
(as, bs) = unzip (tail s)
-- | Extra numeric instances
instance (NumExt a) => NumExt (Stream a) where
(^) = zip (^)
(/) = zip (/)
fact = map fact
fall = zip fall
choose = zip choose
------------------------------------------------------------------------------
-- $ Recurrences
-- NB. The streams can be given the more general type |(Num a) => Stream a|.
-- However, sometimes this triggers unresolved overloading errors.
nat, nat', fac, fib, fib', fib'', fibv,
bin, msb, ones, ones', onesv, carry, frac, god, jos :: Stream Integer
pot, pot' :: Stream Bool
nat = 0 <: nat + 1
nat' = tail nat
fac = 1 <: (nat + 1) * fac
fib = 0 <: fib'
fib' = 1 <: fib' + fib
fib'' = tail fib'
fibv = 0 <: fibv + (1 <: fibv)
infixr 5 \/
(\/) :: Stream a -> Stream a -> Stream a
s \/ t = head s <: t \/ tail s
bin = 0 <: 2 * bin + 1 \/ 2 * bin + 2
iterate :: (a -> a) -> (a -> Stream a)
iterate f a = a <: iterate f (f a)
pot = True <: pot \/ repeat False
pot' = tail pot
msb = 1 <: 2 * msb \/ 2 * msb
ones = 0 <: ones'
ones' = 1 <: ones' \/ ones' + 1
carry = 0 \/ carry + 1
turn :: (Integral a) => a -> [a]
turn 0 = []
turn (n + 1) = turn n ++ [n] ++ turn n
turn _ = error "turn: negative argument"
tree :: (Integral a) => a -> Stream a
tree n = n <: turn n << tree (n + 1)
infixr 5 <<
(<<) :: [a] -> Stream a -> Stream a
[] << s = s
(a : as) << s = a <: (as << s)
frac = nat \/ frac
god = 2 * frac + 1
jos = 1 <: 2 * jos - 1 \/ 2 * jos + 1
------------------------------
-- $ Finite calculus
-------------------------------
diff :: (Num a) => Stream a -> Stream a
diff s = tail s - s
sum :: (Num a) => Stream a -> Stream a
sum s = t where t = 0 <: t + s
onesv = 0 <: onesv + 1 - carry
sumv :: (Num a) => Stream a -> Stream a
sumv s = 0 <: repeat (head s) + sumv (tail s)
------------------------------------------------------------------------------
-- $ Generating functions
------------------------------------------------------------------------------
const :: (Num a) => a -> Stream a
const n = n <: repeat 0
z :: (Num a) => Stream a
z = 0 <: 1 <: repeat 0
infixl 7 **
(**) :: (Num a) => Stream a -> Stream a -> Stream a
s ** t = head s * head t <: repeat (head s) * tail t + tail s ** t
reciprocal :: (Fractional a) => Stream a -> Stream a
reciprocal s = t where a = recip (head s)
t = a <: repeat (- a) * (tail s ** t)
infixl 7 //
(//) :: (Fractional a) => Stream a -> Stream a -> Stream a
s // t = s ** reciprocal t
power :: (Fractional a, Integral b) => Stream a -> b -> Stream a
power s n
| n >= 0 = pow s n
| otherwise = reciprocal (pow s (- n))
where pow _t 0 = const 1
pow t (k + 1) = t ** pow t k
pow _ _ = error "power: impossible"
{-
------------------------------------------------------------------------------
-- Proof of existence and uniqueness of solutions
------------------------------------------------------------------------------
class Coalgebra s where
head :: s a -> a
tail :: s a -> s a
unfold :: (Coalgebra s) => s a -> Stream a
unfold s = head s <: unfold (tail s)
data Expr :: * -> * where
Var :: Stream a -> Expr a
Repeat :: a -> Expr a
Plus :: (Num a) => Expr a -> Expr a -> Expr a
Nat :: Expr Integer
instance Coalgebra Expr where
head (Var s) = head s
head (Repeat a) = a
head (Plus e1 e2) = head e1 + head e2
head Nat = 0
tail (Var s) = Var (tail s)
tail (Repeat a) = Repeat a
tail (Plus e1 e2) = Plus (tail e1) (tail e2)
tail Nat = Plus Nat (Repeat 1)
eval :: Expr a -> Stream a
eval = unfold
repeat k = eval (Repeat k)
s1 + s2 = eval (Plus (Var s1) (Var s2))
nat = eval Nat
-}
------------------------------------------------------------------------------
{-
Examples.
> main :: IO ()
> main = do
> print $ fib
> print $ nat * nat
> print $ tail fib ^ 2 - fib * tail (tail fib)
> print $ tail fib ^ 2 - fib * tail (tail fib) == (-1) ^ nat
> print $ pot
> print $ msb
> print $ (nat' - msb)
> print $ ones
> print $ jos
> print $ (jos - 1) / 2
> print $ diff (nat ^ 3)
> print $ diff (2 ^ nat)
> print $ carry
> print $ jos
> print $ diff (fall nat 3)
> print $ 3 * fall nat 2
> print $ sum (0 \/ 1 :: Stream Integer)
> print $ sum (2 * nat + 1)
> print $ sum carry
> print $ nat ** 10 ^ nat
> print $ 9 * (nat ** 10 ^ nat)
> print $ 9 * (nat ** 10 ^ nat) + nat'
-}