Review: Copatterns

Copatterns.agda

{-# OPTIONS --guardedness --type-in-type #-}

module Copatterns where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning

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

record Stream (A : Set) : Set where
  coinductive
  constructor _:>_
  field
    head : A
    tail : Stream A


cycleNats : Nat -> Nat -> Stream Nat
Stream.head (cycleNats N x) = x
Stream.tail (cycleNats N zero) = cycleNats N N
Stream.tail (cycleNats N (suc x)) = cycleNats N x

{-# TERMINATING #-}
cycleNats' : Nat -> Nat -> Stream Nat
cycleNats' N zero = zero :> cycleNats' N N
cycleNats' N (suc x) = suc x :> cycleNats' N x

same : (N : Nat) -> (n : Nat) -> head (cycleNats N n) ≡ head (cycleNats' N n)
same _ zero = refl
same _ (suc n) = refl

open import Data.Product

record Monad (M : Set -> Set) : Set where
  constructor is-monad
  field
    pure : {A : Set} -> A -> M A
    _>>=_ : {A B : Set} -> M A -> (A -> M B) -> M B

open Monad

State : Set -> Set -> Set
State S A = S -> S × A

Monad-State : {S : Set} -> Monad (State S)
pure Monad-State a s = s , a
_>>=_ Monad-State ma f s =
  let s' , a = ma s
   in f a s'

record State' (S : Set) (A : Set) : Set where
  constructor state
  field
    runState : S -> S × A

open import Function

open State'

-- Monad-State'1 : {S : Set} -> Monad (State' S)
-- Monad-State'1 = is-monad (state ∘ flip _,_) $
--   λ m f -> state λ s -> let s' , a = runState m s
--                          in runState (f a) s'

Monad-State₁ : {S : Set} -> Monad (State' S)
pure Monad-State₁ a = state λ s -> s , a
_>>=_ Monad-State₁ ma f = state λ s ->
  let s' , a = runState ma s
   in runState (f a) s'

Monad-State₂ : {S : Set} -> Monad (State' S)
runState (pure Monad-State₂ a) s = s , a
runState (_>>=_ Monad-State₂ ma f) s =
  let s' , a = runState ma s
   in runState (f a) s'


open Stream

_+_ : Nat -> Nat -> Nat
zero + n = n
suc m + n = suc (m + n)

zipWith : {A B C : Set} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
head (zipWith f sa sb) = f (head sa) (head sb)
tail (zipWith f sa sb) = zipWith f (tail sa) (tail sb)

fib : Stream Nat
head fib = zero
head (tail fib) = suc zero
tail (tail fib) = zipWith _+_ fib (tail fib)