0 | module Control.Monad.Random.Interface
 1 |
 2 | import Control.Monad.Error.Either
 3 | import Control.Monad.Maybe
 4 | import Control.Monad.Reader.Reader
 5 | import Control.Monad.RWS.CPS
 6 | import Control.Monad.State.State
 7 | import Control.Monad.Trans
 8 | import Control.Monad.Writer.CPS
 9 |
10 | import public System.Random.Pure
11 |
12 | %default total
13 |
14 | public export
15 | interface Monad m => MonadRandom m where
16 |   getRandom  : Random a => m a
17 |   getRandomR : Random a => (a, a) -> m a
18 |
19 |   independent : m a -> m a
20 |
21 | public export %inline
22 | getRandomFor : MonadRandom m => (0 a : _) -> Random a => m a
23 | getRandomFor _ = getRandom
24 |
25 | --- Lifting implementations for standard transformers ---
26 |
27 | export
28 | MonadRandom m => MonadRandom (EitherT e m) where
29 |   getRandom  = lift getRandom
30 |   getRandomR = lift . getRandomR
31 |   independent $ MkEitherT x = MkEitherT $ independent x
32 |
33 | export
34 | MonadRandom m => MonadRandom (MaybeT m) where
35 |   getRandom  = lift getRandom
36 |   getRandomR = lift . getRandomR
37 |   independent $ MkMaybeT x = MkMaybeT $ independent x
38 |
39 | export
40 | MonadRandom m => MonadRandom (ReaderT r m) where
41 |   getRandom  = lift getRandom
42 |   getRandomR = lift . getRandomR
43 |   independent $ MkReaderT x = MkReaderT $ independent . x
44 |
45 | export
46 | MonadRandom m => MonadRandom (RWST r w s m) where
47 |   getRandom  = lift getRandom
48 |   getRandomR = lift . getRandomR
49 |   independent $ MkRWST x = MkRWST $ \r, s, w => independent $ x r s w
50 |
51 | export
52 | MonadRandom m => MonadRandom (StateT s m) where
53 |   getRandom  = lift getRandom
54 |   getRandomR = lift . getRandomR
55 |   independent $ ST x = ST $ independent . x
56 |
57 | export
58 | MonadRandom m => MonadRandom (WriterT s m) where
59 |   getRandom  = lift getRandom
60 |   getRandomR = lift . getRandomR
61 |   independent $ MkWriterT x = MkWriterT $ independent . x
62 |