{-# 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'
-}