filter.agda

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

record Stream (A : Set) : Set where
  coinductive
  constructor _::_

  field
    head : A
    tail : Stream A
open Stream


_$_ : {A B : Set} -> (A -> B) -> A -> B
f $ a = f a


repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

map : {A B : Set} -> (A -> B) -> Stream A -> Stream B
head (map f as) = f (head as)
tail (map f as) = map f (tail as)

-- You cannot define filter. Why? consider `filter (const ff) as`
zip : {A B C : Set} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
head (zip f as bs) = f (head as) (head bs)
tail (zip f as bs) = zip f (tail as) (tail bs)

scan : {A B : Set} -> (B -> A -> B) -> B -> Stream A -> Stream B
head (scan f i as) = f i $ head as
tail (scan f i as) = scan f (f i $ head as) (tail as)

-- These two are where copatterns really shine, I feel
interleave : {A : Set} -> Stream A -> Stream A -> Stream A
head (interleave a b) = head a
tail (interleave a b) = interleave b (tail a)


intersperse : {A : Set} -> A -> Stream A -> Stream A
head (intersperse _ as) = head as
tail (intersperse a as) = a :: (tail as)

-- This one isn't as short when written with copatterns
drop : { A : Set} -> Nat -> Stream A -> Stream A
drop zero as = as
drop (suc n) as = drop n (tail as)





toVec : {A : Set} {n : Nat} -> Stream A -> Vec A n
toVec {_} {zero} _ = []
toVec {_} {suc n} as = (head as) :: (toVec (tail as))


zeros = repeat 0
ones = repeat 1

upwards = scan (_+_) 0 ones

alternating = interleave zeros ones

viewUpwards : Vec Nat 10
viewUpwards = toVec $ upwards

viewAlternating : Vec Nat 10
viewAlternating = toVec $ alternating

viewDrop : Vec Nat 10
viewDrop = toVec $ drop 10 upwards