1 implementation module UniqueState
5 runState :: u:(State .s .a) .s -> v:(.a,.s), [u <= v]
6 runState (State f) s = f s
8 instance Functor (State String)
10 //fmap :: u:(v:a -> w:b) x:(State String v:a) -> x:(State String w:b), [x <= u,x <= v,x <= w]
12 # (a`, s`) = runState a s
15 instance Applicative (State String)
17 //(<*>) 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]
19 # (f`, s`) = runState f s
20 # (a`, s``) = runState a s`
23 //pure :: u:a -> v:(State String u:a), [v <= u]
24 pure x = State (\s -> (x, s))
26 instance Monad (State String)
28 //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]
30 # (v, s`) = runState a s
34 instance Functor Maybe
36 fmap f (Just x) = Just (f x)
39 instance Applicative Maybe
41 (<*>) (Just f) (Just x) = Just (f x)