Mercurial > hg > Members > atton > agda-proofs

comparison state/state.agda @ 14:31b1b7cc43cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove state is functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 May 2016 16:31:56 +0900
parents 14c22339ce06
children
comparison
equal deleted inserted replaced
13:14c22339ce06 14:31b1b7cc43cd
1 open import Relation.Binary.PropositionalEquality 1 open import Relation.Binary.PropositionalEquality
2 open import Level 2 open import Level
3 open ≡-Reasoning 3 open ≡-Reasoning
4
5
6 module state where
7
8 record Product {l : Level} (A B : Set l) : Set (suc l) where
9 constructor <_,_>
10 field
11 first : A
12 second : B
13 open Product
14
15 id : {l : Level} {A : Set l} -> A -> A
16 id a = a
17
18
19 infixr 10 _∘_
20 _∘_ : {l : Level} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C)
21 g ∘ f = \a -> g (f a)
4 22
5 {- 23 {-
6 Haskell Definition 24 Haskell Definition
7 newtype State s a = State { runState :: s -> (a, s) } 25 newtype State s a = State { runState :: s -> (a, s) }
8 26
11 m >>= k = State $ \s -> let 29 m >>= k = State $ \s -> let
12 (a, s') = runState m s 30 (a, s') = runState m s
13 in runState (k a) s' 31 in runState (k a) s'
14 -} 32 -}
15 33
16 module state where
17
18 record Product {l : Level} (A B : Set l) : Set (suc l) where
19 constructor <_,_>
20 field
21 first : A
22 second : B
23 open Product
24 34
25 record State {l : Level} (S A : Set l) : Set (suc l) where 35 record State {l : Level} (S A : Set l) : Set (suc l) where
26 field 36 field
27 runState : S -> Product A S 37 runState : S -> Product A S
28 open State 38 open State
29 39
30 state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A 40 state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A
31 state f = record {runState = f} 41 state f = record {runState = f}
32 42
33 return : {l : Level} {S A : Set l} -> A -> State S A 43 return : {l : Level} {S A : Set l} -> A -> State S A
34 return a = state (\s -> < a , s > ) 44 return a = state (\s -> < a , s > )
35 45
36 _>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B 46 _>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B
37 m >>= k = state (\s -> (State.runState (k (Product.first (State.runState m s))) (Product.second (State.runState m s)))) 47 m >>= k = state (\s -> (runState (k (first (runState m s))) (second (runState m s))))
48
49 {- fmap definitions in Haskell
50 instance Functor (State s) where
51 fmap f m = State $ \s -> let
52 (a, s') = runState m s
53 in (f a, s')
54 -}
55
56 fmap : {l : Level} {S A B : Set l} -> (A -> B) -> (State S A) -> (State S B)
57 fmap f m = state (\s -> < (f (first ((runState m) s))), (second ((runState m) s)) >)
58
59 -- proofs
60
61 fmap-id : {l : Level} {A S : Set l} {s : State S A} -> fmap id s ≡ id s
62 fmap-id = refl
63
64 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
65 fmap-comp {_}{_}{_}{_}{_}{g}{f}{s} = refl