Mercurial > hg > Members > atton > agda-proofs

comparison state/state.agda @ 4:fe1cf97997b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start proof to State Monad
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 02 Nov 2014 09:42:55 +0900
parents
children 14c22339ce06
comparison
equal deleted inserted replaced
3:36c9175d9adb 4:fe1cf97997b9
1 open import Relation.Binary.PropositionalEquality
2 open import Level
3 open ≡-Reasoning
4
5 {-
6 Haskell Definition
7 newtype State s a = State { runState :: s -> (a, s) }
8
9 instance Monad (State s) where
10 return a = State $ \s -> (a, s)
11 m >>= k = State $ \s -> let
12 (a, s') = runState m s
13 in runState (k a) s'
14 -}
15
16 module state where
17
18 record Product {l ll : Level} (A : Set l) (B : Set ll) : Set (suc (l ⊔ ll)) where
19 constructor <_,_>
20 field
21 first : A
22 second : B
23 open Product
24
25 product-create : {l ll : Level} {A : Set l} {B : Set ll} -> A -> B -> Product A B
26 product-create a b = < a , b >
27
28
29 record State {l ll : Level} (S : Set l) (A : Set ll) : Set (suc (l ⊔ ll)) where
30 field
31 runState : S -> Product A S
32 open State
33
34 state : {l ll : Level} {S : Set l} {A : Set ll} -> (S -> Product A S) -> State S A
35 state f = record {runState = f}
36
37 return : {l ll : Level} {S : Set l} {A : Set ll} -> A -> State S A
38 return a = state (\s -> < a , s > )
39
40
41 _>>=_ : {l ll lll : Level} {S : Set l} {A : Set ll} {B : Set lll} -> State S A -> (A -> State S B) -> State S B
42 m >>= k = {!!}