Stream.agda

-- simulating streams by Nat -> A

module Stream where

data Bool : Set where
    true  : Bool
    false : Bool

if_then_else_ : forall {A} -> Bool -> A -> A -> A
if true  then t else e = t
if false then t else e = e

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

Stream : Set -> Set
Stream A = Nat -> A

_::_ : forall {A} -> A -> Stream A -> Stream A
_::_ a as zero     = a
_::_ a as (succ n) = as n

map : forall {A B} -> (A -> B) -> Stream A -> Stream B
map f as n = f (as n)

head : forall {A} -> Stream A -> A
head as = as zero

tail : forall {A} -> Stream A -> Stream A
tail as n = as (succ n)

-- construct the stream a :: f a :: f (f a) :: ...

iterate : forall {A} -> (A -> A) -> A -> Stream A
iterate f a zero = a
iterate f a (succ n) = iterate f (f a) n

zipWith : forall {A B C} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
zipWith f as bs n = f (as n) (bs n)

-- merge with with
merge : forall {A} -> (A -> A -> Bool) -> Stream A -> Stream A -> Stream A
merge le as bs with le (head as) (head bs)
merge le as bs | true  = head as :: merge le (tail as) bs
merge le as bs | false = head bs :: merge le as (tail bs)

{-
-- without with
merge' : forall {A} -> (A -> A -> Bool) -> Stream A -> Stream A -> Stream A
merge' le as bs = if le (head as) (head bs)
                  then (head as :: merge' le (tail as) bs)
                  else (head bs :: merge' le as (tail bs))
-}

-- BOTH VARIANTS OF MERGE ARE NOT STRUCTURALLY RECURSIVE