implementation module UniqueState

import StdEnv

runState :: u:(State .s .a) .s -> v:(.a,.s), [u <= v]
runState (State f) s = f s

instance Functor (State String)
where
	//fmap :: u:(v:a -> w:b) x:(State String v:a) -> x:(State String w:b), [x <= u,x <= v,x <= w]
	fmap f a = State (\s
		# (a`, s`) = runState a s
		= (f a`, s`))

instance Applicative (State String)
where
	//(<*>) infixl 4 :: u:(State String v:(w:a -> x:b)) y:(State String w:a) -> z:(State String x:b), [z <= u,u <= v,y <= w,z <= x,z <= y]
	(<*>) f a = State (\s
		# (f`, s`) = runState f s
		# (a`, s``) = runState a s`
		= (f` a`, s``))

	//pure :: u:a -> v:(State String u:a), [v <= u]
	pure x = State (\s -> (x, s))

instance Monad (State String)
where
	//bind :: u:(State String v:a) w:(v:a -> x:(State String y:b)) -> x:(State String y:b), [x <= u,u <= v,x <= w,x <= y]
	bind a f = State (\s
		# (v, s`) = runState a s
		# a` = f v
		= runState a` s`)

instance Functor Maybe
where
	fmap f (Just x) = Just (f x)
	fmap _ _ = Nothing

instance Applicative Maybe
where
	(<*>) (Just f) (Just x) = Just (f x)
	(<*>) _ _ = Nothing

	pure x = Just x

instance Monad Maybe
where
	bind (Just x) f = f x
	bind _ _ = Nothing