definition module UniqueState

:: Maybe a = Just a | Nothing

class Functor f
where
	fmap :: u:(v:a -> w:b) *(f v:a) -> *(f w:b)

class Applicative f | Functor f
where
	(<*>) infixl 4 :: *(f v:(w:a -> x:b)) *(f w:a) -> *(f x:b)
	pure :: u:a -> *(f u:a)

class Monad m | Applicative m
where
	bind :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
	(>>=) infixl 1 :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
	(>>=) ma a2mb :== bind ma a2mb
	(>>|) infixl 1 :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
	(>>|) ma mb :== ma >>= \_ -> mb
	return :: u:a -> *(m u:a) | Applicative m
	return x :== pure x

:: State s a = State .(s -> .(a, s))

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

instance Functor (State String)
instance Applicative (State String)
instance Monad (State String)

instance Functor Maybe
instance Applicative Maybe
instance Monad Maybe