1 | module Control.Monad.ST
13 | data STRef : Type -> Type -> Type where
14 | MkSTRef : IORef a -> STRef s a
22 | data ST : Type -> Type -> Type where
23 | MkST : IO a -> ST s a
27 | runST : (forall s . ST s a) -> a
29 | = let MkST prog = p {s = ()} in
30 | unsafePerformIO prog
33 | Functor (ST s) where
34 | map fn (MkST st) = MkST $
fn <$> st
37 | Applicative (ST s) where
39 | MkST f <*> MkST a = MkST $
f <*> a
50 | newSTRef : a -> ST s (STRef s a)
52 | = MkST $
do r <- newIORef val
61 | readSTRef : STRef s a -> ST s a
62 | readSTRef (MkSTRef r) = MkST $
readIORef r
67 | writeSTRef : STRef s a -> (val : a) -> ST s ()
68 | writeSTRef (MkSTRef r) val = MkST $
writeIORef r val
72 | modifySTRef : STRef s a -> (a -> a) -> ST s ()
74 | = do val <- readSTRef ref
75 | writeSTRef ref (f val)