0 | module Data.Linear.ELift1
 1 |
 2 | import public Data.Linear.Token
 3 | import public Control.Monad.MErr
 4 |
 5 | %default total
 6 |
 7 | ||| Result of a linear computation running in state thread
 8 | ||| `s` producing either a value of type `a` or an error of
 9 | ||| one of the types listed in `es`.
10 | public export
11 | data ERes : (s : Type) -> (es : List Type) -> (a : Type) -> Type where
12 |   E : HSum es   -> (1 t : T1 s) -> ERes s es a
13 |   R : (val : a) -> (1 t : T1 s) -> ERes s es a
14 |
15 | ||| An alias similar to `F1 s a` but for linear computations that could
16 | ||| fail with one of the errors listed.
17 | public export
18 | 0 E1 : Type -> List Type -> Type -> Type
19 | E1 s es a = (1 t : T1 s) -> ERes s es a
20 |
21 | ||| Replaces all errors with `neutral`, running an `E1` as an `F1`.
22 | export %inline
23 | e1ToF1 : Monoid a => E1 s es a -> F1 s a
24 | e1ToF1 act t =
25 |   case act t of
26 |     E _ t => neutral # t
27 |     R v t => v # t
28 |
29 | ||| Lifts a linear computation into an `E1 s a`.
30 | export %inline
31 | f1ToE1 : F1 s a -> E1 s es a
32 | f1ToE1 act t = let v # t := act t in R v t
33 |
34 | export
35 | mapERes : (a -> b) -> (1 _ : ERes e es a) -> ERes e es b
36 | mapERes f (E x t) = E x t
37 | mapERes f (R v t) = R (f v) t
38 |
39 | export
40 | pattempt : (1 r : ERes e es a) -> ERes e fs (Result es a)
41 | pattempt (E x t) = R (Left x) t
42 | pattempt (R v t) = R (Right v) t
43 |
44 | export
45 | toResult : (1 r : ERes s es a) -> R1 s (Result es a)
46 | toResult (E x t) = Left x # t
47 | toResult (R v t) = Right v # t
48 |
49 | export
50 | toEither : (1 r : ERes s [e] a) -> R1 s (Either e a)
51 | toEither (E (Here x) t) = Left x # t
52 | toEither (R v t)        = Right v # t
53 |
54 | export %inline
55 | throw1 : Has e es => e -> E1 s es a
56 | throw1 x t = E (inject x) t
57 |
58 | export %inline
59 | fail1 : e -> E1 s [e] a
60 | fail1 = throw1
61 |
62 | ||| An interface for lifting stateful, linear computation into
63 | ||| a monad with the potential of failure.
64 | public export
65 | interface MErr f => ELift1 (0 s : Type) f | f where
66 |   elift1 : E1 s es a -> f es a
67 |
68 | export %inline
69 | ELift1 s f => Lift1 s (f es) where
70 |   lift1 act = elift1 (f1ToE1 act)
71 |
72 | ||| Convenience alias for `ELift1 World`
73 | public export
74 | 0 EIO1 : (f : List Type -> Type -> Type) -> Type
75 | EIO1 = ELift1 World
76 |