### view state/state.agda @ 77:a2e6f61d5f2bdefaulttip

author atton Thu, 09 Feb 2017 06:32:03 +0000 31b1b7cc43cd
line wrap: on
line source
```
open import Relation.Binary.PropositionalEquality
open import Level
open ≡-Reasoning

module state where

record Product {l : Level} (A B : Set l) : Set (suc l) where
constructor <_,_>
field
first  : A
second : B
open Product

id : {l : Level} {A : Set l} -> A -> A
id a = a

infixr 10 _∘_
_∘_ : {l : Level} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C)
g ∘ f = \a -> g (f a)

{-
newtype State s a = State { runState :: s -> (a, s) }

return a = State \$ \s -> (a, s)
m >>= k  = State \$ \s -> let
(a, s') = runState m s
in runState (k a) s'
-}

record State {l : Level} (S A : Set l) : Set (suc l) where
field
runState : S -> Product A S
open State

state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A
state f = record {runState = f}

return : {l : Level} {S A : Set l} -> A -> State S A
return a = state (\s -> < a , s > )

_>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B
m  >>= k =  state (\s -> (runState (k (first (runState m s))) (second (runState m s))))

instance Functor (State s) where
fmap f m = State \$ \s -> let
(a, s') = runState m s
in (f a, s')
-}

fmap : {l : Level} {S A B : Set l} -> (A -> B) -> (State S A) -> (State S B)
fmap f m = state (\s -> < (f (first ((runState m) s))), (second ((runState m) s)) >)

-- proofs

fmap-id : {l : Level} {A S : Set l} {s : State S A} -> fmap id s ≡ id s
fmap-id = refl

fmap-comp : {l : Level} {S A B C : Set l} {g : B -> C} {f : A -> B} {s : State S A} ->  ((fmap g) ∘ (fmap f)) s ≡ fmap (g ∘ f) s
fmap-comp {_}{_}{_}{_}{_}{g}{f}{s} = refl
```