0 | module Control.Monad.Random.Random
  1 |
  2 | import Data.Ref
  3 |
  4 | import Control.Monad.Error.Interface
  5 | import public Control.Monad.Identity
  6 | import public Control.Monad.Random.Interface
  7 | import Control.Monad.Reader.Interface
  8 | import Control.Monad.State
  9 | import Control.Monad.Writer.Interface
 10 |
 11 | import System.Random.Pure
 12 | import System.Random.Pure.StdGen
 13 |
 14 | %default total
 15 |
 16 | --- Transformer ---
 17 |
 18 | public export
 19 | data RandomT : (Type -> Type) -> Type -> Type where
 20 |   MkRandomT : (forall g. RandomGen g => StateT g m a) -> RandomT m a
 21 |
 22 | public export %inline
 23 | unRandomT : RandomGen g => RandomT m a -> StateT g m a
 24 | unRandomT $ MkRandomT f = f
 25 |
 26 | public export %inline
 27 | runRandomT : RandomGen g => g -> RandomT m a -> m (g, a)
 28 | runRandomT g = runStateT g . unRandomT
 29 |
 30 | public export %inline
 31 | execRandomT : RandomGen g => Functor m => g -> RandomT m a -> m g
 32 | execRandomT g = execStateT g . unRandomT
 33 |
 34 | public export %inline
 35 | evalRandomT : RandomGen g => Functor m => g -> RandomT m a -> m a
 36 | evalRandomT g = evalStateT g . unRandomT
 37 |
 38 | --- Special runners ---
 39 |
 40 | -- Runs on freshly initialised random seed each time
 41 | public export %inline
 42 | evalRandomIO : HasIO io => RandomT io a -> io a
 43 | evalRandomIO r = evalRandomT !initStdGen r
 44 |
 45 | public export %inline
 46 | evalRandomRef : RandomGen g => Monad m => Ref m r => r g -> RandomT m a -> m a
 47 | evalRandomRef ref rand = do
 48 |   (g', x) <- runRandomT !(readRef ref) rand
 49 |   writeRef ref g' $> x
 50 |
 51 | --- Standard implementations ---
 52 |
 53 | public export %inline
 54 | Functor m => Functor (RandomT m) where
 55 |   map f x = MkRandomT $ map f $ unRandomT x
 56 |
 57 | public export %inline
 58 | Monad m => Applicative (RandomT m) where
 59 |   pure x = MkRandomT $ pure x
 60 |   f <*> x = MkRandomT $ unRandomT f <*> unRandomT x
 61 |
 62 | public export %inline
 63 | Alternative m => Monad m => Alternative (RandomT m) where
 64 |   empty = MkRandomT empty
 65 |   x <|> y = MkRandomT $ unRandomT x <|> unRandomT y
 66 |
 67 | public export %inline
 68 | Monad m => Monad (RandomT m) where
 69 |   x >>= f = MkRandomT $ unRandomT x >>= unRandomT . f
 70 |
 71 | public export %inline
 72 | MonadTrans RandomT where
 73 |   lift x = MkRandomT $ lift x
 74 |
 75 | public export %inline
 76 | HasIO m => HasIO (RandomT m) where
 77 |   liftIO x = MkRandomT $ liftIO x
 78 |
 79 | public export %inline
 80 | MonadReader r m => MonadReader r (RandomT m) where
 81 |   ask = lift ask
 82 |   local f (MkRandomT x) = MkRandomT $ local f x
 83 |
 84 | public export %inline
 85 | MonadWriter w m => MonadWriter w (RandomT m) where
 86 |   tell = lift . tell
 87 |   pass (MkRandomT x) = MkRandomT $ pass x
 88 |   listen (MkRandomT x) = MkRandomT $ listen x
 89 |
 90 | public export %inline
 91 | MonadState s m => MonadState s (RandomT m) where
 92 |   put = lift . put
 93 |   get = lift get
 94 |
 95 | public export %inline
 96 | MonadError e m => MonadError e (RandomT m) where
 97 |   throwError = lift . throwError
 98 |   catchError (MkRandomT x) h = MkRandomT $ catchError x $ unRandomT . h
 99 |
100 | --- `MonadRandom` implementation ---
101 |
102 | export
103 | Monad m => MonadRandom (RandomT m) where
104 |   getRandom = MkRandomT random'
105 |   getRandomR bounds = MkRandomT $ randomR' bounds
106 |   independent subR = MkRandomT $ do
107 |     (g', g'') <- split <$> get
108 |     put g'' *> unRandomT subR <* put g'
109 |
110 | --- Simple monad ---
111 |
112 | -- Name was chosen to not to clash with the `Random` interface.
113 | public export
114 | Rand : Type -> Type
115 | Rand = RandomT Identity
116 |
117 | public export %inline
118 | runRandom : RandomGen g => g -> Rand a -> (g, a)
119 | runRandom g = runState g . unRandomT
120 |
121 | public export %inline
122 | execRandom : RandomGen g => g -> Rand a -> g
123 | execRandom g = execState g . unRandomT
124 |
125 | public export %inline
126 | evalRandom : RandomGen g => g -> Rand a -> a
127 | evalRandom g = evalState g . unRandomT
128 |