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 | ||| Alias for `E1 s es ()`
 22 | public export
 23 | 0 E1' : Type -> List Type -> Type
 24 | E1' s es = E1 s es ()
 25 |
 26 | ||| Replaces all errors with `neutral`, running an `E1` as an `F1`.
 27 | export %inline
 28 | e1ToF1 : Monoid a => E1 s es a -> F1 s a
 29 | e1ToF1 act t =
 30 |   case act t of
 31 |     E _ t => neutral # t
 32 |     R v t => v # t
 33 |
 34 | ||| Lifts a linear computation into an `E1 s a`.
 35 | export %inline
 36 | f1ToE1 : F1 s a -> E1 s es a
 37 | f1ToE1 act t = let v # t := act t in R v t
 38 |
 39 | export
 40 | mapERes : (a -> b) -> (1 _ : ERes e es a) -> ERes e es b
 41 | mapERes f (E x t) = E x t
 42 | mapERes f (R v t) = R (f v) t
 43 |
 44 | export
 45 | pattempt : (1 r : ERes e es a) -> ERes e fs (Result es a)
 46 | pattempt (E x t) = R (Left x) t
 47 | pattempt (R v t) = R (Right v) t
 48 |
 49 | export
 50 | toResult : (1 r : ERes s es a) -> R1 s (Result es a)
 51 | toResult (E x t) = Left x # t
 52 | toResult (R v t) = Right v # t
 53 |
 54 | export
 55 | toEither : (1 r : ERes s [e] a) -> R1 s (Either e a)
 56 | toEither (E (Here x) t) = Left x # t
 57 | toEither (R v t)        = Right v # t
 58 |
 59 | export %inline
 60 | throw1 : Has e es => e -> E1 s es a
 61 | throw1 x t = E (inject x) t
 62 |
 63 | export %inline
 64 | fail1 : e -> E1 s [e] a
 65 | fail1 = throw1
 66 |
 67 | ||| An interface for lifting stateful, linear computation into
 68 | ||| a monad with the potential of failure.
 69 | public export
 70 | interface MErr f => ELift1 (0 s : Type) f | f where
 71 |   elift1 : E1 s es a -> f es a
 72 |
 73 | export %inline
 74 | ELift1 s f => Lift1 s (f es) where
 75 |   lift1 act = elift1 (f1ToE1 act)
 76 |
 77 | ||| Convenience alias for `ELift1 World`
 78 | public export
 79 | 0 EIO1 : (f : List Type -> Type -> Type) -> Type
 80 | EIO1 = ELift1 World
 81 |
 82 | export %inline
 83 | liftInject1 : Has e es => ELift1 s f => E1 s [e] a -> f es a
 84 | liftInject1 f =
 85 |   elift1 $ \t => case f t of
 86 |     E (Here x) t => E (inject x) t
 87 |     R x t        => R x t
 88 |
 89 | export %inline
 90 | resultToERes : Result es a -> E1 s es a
 91 | resultToERes (Left x)  t = E x t
 92 | resultToERes (Right x) t = R x t
 93 |
 94 | export %inline
 95 | eitherToERes : Has e es => Either e a -> E1 s es a
 96 | eitherToERes (Left x)  t = E (inject x) t
 97 | eitherToERes (Right x) t = R x t
 98 |
 99 | export %inline
100 | resultToE1 : F1 s (Result es a) -> E1 s es a
101 | resultToE1 f t = let r # t := f t in resultToERes r t
102 |
103 | export %inline
104 | eitherToE1 : Has e es => F1 s (Either e a) -> E1 s es a
105 | eitherToE1 f t = let r # t := f t in eitherToERes r t
106 |
107 | export %inline
108 | eliftResult : ELift1 s f => F1 s (Result es a) -> f es a
109 | eliftResult f = elift1 (resultToE1 f)
110 |
111 | export %inline
112 | eliftEither : Has e es => ELift1 s f => F1 s (Either e a) -> f es a
113 | eliftEither f = elift1 (eitherToE1 f)
114 |