0 | module Control.Monad.Elin
 1 |
 2 | import public Control.Monad.MCancel
 3 | import public Data.Linear.ELift1
 4 |
 5 | %default total
 6 |
 7 | ||| A monad for running pure, stateful computations in
 8 | ||| state thread `s` with the potential of failing with one
 9 | ||| of the errors listed in `es`.
10 | public export
11 | record Elin (s : Type) (es : List Type) (a : Type) where
12 |   constructor E
13 |   run : E1 s es a
14 |
15 | bindImpl : Elin s es a -> (a -> Elin s es b) -> Elin s es b
16 | bindImpl (E g) f =
17 |   E $ \t => case g t of
18 |     E x t => E x t
19 |     R v t => run (f v) t
20 |
21 | export %inline
22 | MErr (Elin s) where
23 |   fail x          = E (E x)
24 |   succeed v       = E (R v)
25 |   bind            = bindImpl
26 |   attempt x       = E $ \t => pattempt (run x t)
27 |   mapImpl f act   = E $ \t => mapERes f (act.run t)
28 |   appImpl ff fv   = bindImpl ff (`mapImpl` fv)
29 |
30 | ||| Dummy implementation as `Elin` has no concept of self-cancelation.
31 | ||| Still, this is useful to get access to the `bracket` combinators.
32 | ||| Semantically, an `Elin` computation acts as if wrapped in a global
33 | ||| `uncancelable` wrapper.
34 | export %inline
35 | MCancel (Elin s) where
36 |   canceled          = pure ()
37 |   uncancelable body = body id
38 |   onCancel fa _     = fa
39 |
40 | export %inline
41 | ELift1 s (Elin s) where
42 |   elift1 = E
43 |
44 | export %inline
45 | HasIO (Elin World es) where
46 |   liftIO = lift1 . ioToF1
47 |
48 | ||| When universally quantified over `s`, the `Elin` monad can
49 | ||| be run to produce a pure value of type `Result es a`, even though
50 | ||| running the value might involve working with freshly allocated
51 | ||| mutable state.
52 | export %inline
53 | runElin : (forall s . Elin s es a) -> Result es a
54 | runElin p = run1 $ \t => toResult (p.run t)
55 |
56 | ||| When tagged with `World`, the `Elin` monad is just `IO` plus
57 | ||| error handling.
58 | export %inline
59 | runElinIO : Elin World es a -> IO (Result es a)
60 | runElinIO p = runIO $ \t => toResult (p.run t)
61 |