Skip to content

Instantly share code, notes, and snippets.

@isovector
Created January 29, 2022 19:39
Show Gist options
  • Save isovector/37a1c1e21a3618e4f4885482a1454396 to your computer and use it in GitHub Desktop.
Save isovector/37a1c1e21a3618e4f4885482a1454396 to your computer and use it in GitHub Desktop.
Review: Copatterns
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment