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 |
 77 | export %inline
 78 | liftInject1 : Has e es => ELift1 s f => E1 s [e] a -> f es a
 79 | liftInject1 f =
 80 |   elift1 $ \t => case f t of
 81 |     E (Here x) t => E (inject x) t
 82 |     R x t        => R x t
 83 |
 84 | export %inline
 85 | resultToE1 : F1 s (Result es a) -> E1 s es a
 86 | resultToE1 f t =
 87 |   case f t of
 88 |     Left  x # t => E x t
 89 |     Right x # t => R x t
 90 |
 91 | export %inline
 92 | eitherToE1 : Has e es => F1 s (Either e a) -> E1 s es a
 93 | eitherToE1 f t =
 94 |   case f t of
 95 |     Left  x # t => E (inject x) t
 96 |     Right x # t => R x t
 97 |
 98 | export %inline
 99 | eliftResult : ELift1 s f => F1 s (Result es a) -> f es a
100 | eliftResult f = elift1 (resultToE1 f)
101 |
102 | export %inline
103 | eliftEither : Has e es => ELift1 s f => F1 s (Either e a) -> f es a
104 | eliftEither f = elift1 (eitherToE1 f)
105 |