0 | module Control.Monad.Pure
 1 |
 2 | import public Data.Linear.Token
 3 |
 4 | %default total
 5 |
 6 | ||| A monad of pure computations with suport for localized
 7 | ||| mutable state.
 8 | |||
 9 | ||| When universally quantified over `s`, this is like
10 | ||| `Control.Monad.ST` from base, but proper compiler support
11 | ||| for efficient code generation.
12 | |||
13 | ||| On the other hand, `Pure World` is isomorphic to `IO`.
14 | public export
15 | record Pure (s,a : Type) where
16 |   constructor P
17 |   run : F1 s a
18 |
19 | %inline
20 | bind : Pure s a -> (a -> Pure s b) -> Pure s b
21 | bind (P v) f = P $ \t => let x # t := v t in run (f x) t
22 |
23 | export %inline
24 | Functor (Pure s) where
25 |   map f (P g) = P $ mapF1 f g
26 |
27 | export %inline
28 | Applicative (Pure s) where
29 |   pure v    = P (v #)
30 |   ff <*> fv = bind ff (<$> fv)
31 |
32 | export %inline
33 | Monad (Pure s) where
34 |   (>>=) = bind
35 |
36 | export %inline
37 | Lift1 s (Pure s) where
38 |   lift1 = P
39 |
40 | export %inline
41 | HasIO (Pure World) where
42 |   liftIO = lift1 . ioToF1
43 |
44 | ||| Runs a pure computation, probably with localized mutable state.
45 | export %inline
46 | runPure : (forall s . Pure s a) -> a
47 | runPure p = run1 p.run
48 |
49 | ||| `Pure World` can be run in any monad that wraps `IO`.
50 | export %inline
51 | runPureIO : HasIO io => Pure World a -> io a
52 | runPureIO = runIO . run
53 |