# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1414888975 -32400
# Node ID fe1cf97997b987b42e848f2d4ad56179d5ba5a85
# Parent  36c9175d9adb22c255cd39aeb8692d4c5bb2da5f
Start proof to State Monad

diff -r 36c9175d9adb -r fe1cf97997b9 state/state.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/state/state.agda	Sun Nov 02 09:42:55 2014 +0900
@@ -0,0 +1,42 @@
+open import Relation.Binary.PropositionalEquality
+open import Level
+open ≡-Reasoning
+
+{-
+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'
+-}
+
+module state where
+
+record Product {l ll : Level} (A : Set l) (B : Set ll) : Set (suc (l ⊔ ll)) where 
+  constructor <_,_>
+  field
+    first  : A
+    second : B
+open Product
+
+product-create : {l ll : Level} {A : Set l} {B : Set ll} -> A -> B -> Product A B
+product-create a b = < a , b >
+
+
+record State {l ll : Level} (S : Set l) (A : Set ll) : Set (suc (l ⊔ ll)) where
+  field
+    runState : S -> Product A S
+open State
+
+state : {l ll : Level} {S : Set l} {A : Set ll} -> (S -> Product A S) -> State S A
+state f = record {runState = f}
+
+return : {l ll : Level} {S : Set l} {A : Set ll} -> A -> State S A
+return a = state (\s -> < a , s > )
+
+
+_>>=_ : {l ll lll : Level} {S : Set l} {A : Set ll} {B : Set lll} -> State S A -> (A -> State S B) -> State S B
+m >>= k = {!!}
\ No newline at end of file