view state/state.agda @ 50:ccb34e3f1514

Rename named-product to subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 01:40:55 +0000
parents 31b1b7cc43cd
children
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)

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

instance Monad (State s) where
  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))))

{- fmap definitions in Haskell
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