0 | ||| Provides a monad transformer `EitherT` that extends an inner monad with the
  1 | ||| ability to throw and catch exceptions.
  2 |
  3 | module Control.Monad.Error.Either
  4 |
  5 | import Control.Monad.Trans
  6 |
  7 | %default total
  8 |
  9 | ||| A monad transformer extending an inner monad with the ability to throw and
 10 | ||| catch exceptions.
 11 | |||
 12 | ||| Sequenced actions produce an exception if either action produces an
 13 | ||| exception, with preference for the first exception. If neither produce an
 14 | ||| exception, neither does the sequence of actions.
 15 | |||
 16 | ||| `MaybeT m a` is equivalent to `EitherT () m a`, that is, an computation
 17 | ||| that can only throw a single, information-less exception.
 18 | public export
 19 | data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
 20 |   MkEitherT : m (Either e a) -> EitherT e m a
 21 |
 22 | ||| Unwrap an `EitherT` computation.
 23 | public export
 24 | %inline
 25 | runEitherT : EitherT e m a -> m (Either e a)
 26 | runEitherT (MkEitherT x) = x
 27 |
 28 | ||| Run an `EitherT` computation, handling results and exceptions with separate
 29 | ||| functions.
 30 | |||
 31 | ||| This is a version of `either` lifted to work with `EitherT`.
 32 | public export
 33 | eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
 34 | eitherT f g x = runEitherT x >>= either f g
 35 |
 36 | ||| Map over the underlying monadic computation.
 37 | public export
 38 | %inline
 39 | mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
 40 | mapEitherT f = MkEitherT . f . runEitherT
 41 |
 42 | ||| Map over the result or the exception of a monadic computation.
 43 | public export
 44 | bimapEitherT : Functor m => (a -> c) -> (b -> d)
 45 |             -> EitherT a m b -> EitherT c m d
 46 | bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x
 47 |
 48 | ||| A version of `Left` lifted to work with `EitherT`.
 49 | |||
 50 | ||| This is equivalent to `throwE`.
 51 | public export
 52 | %inline
 53 | left : Applicative m => e -> EitherT e m a
 54 | left = MkEitherT . pure . Left
 55 |
 56 | ||| A version of `Right` lifted to work with `EitherT`.
 57 | |||
 58 | ||| This is equivalent to `pure`.
 59 | public export
 60 | %inline
 61 | right : Applicative m => a -> EitherT e m a
 62 | right = MkEitherT . pure . Right
 63 |
 64 | ||| Swap the result and the exception of a monadic computation.
 65 | public export
 66 | swapEitherT : Functor m => EitherT e m a -> EitherT a m e
 67 | swapEitherT = mapEitherT (map (either Right Left))
 68 |
 69 | -------------------------------------------------
 70 | -- Methods of the 'exception' theme
 71 | -------------------------------------------------
 72 |
 73 | ||| Throw an exception in a monadic computation.
 74 | public export
 75 | %inline
 76 | throwE : Applicative m => e -> EitherT e m a
 77 | throwE = MkEitherT . pure . Left
 78 |
 79 | ||| Handle an exception thrown in a monadic computation.
 80 | |||
 81 | ||| Since the handler catches all errors thrown in the computation, it may
 82 | ||| raise a different exception type.
 83 | public export
 84 | catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
 85 | catchE et f
 86 |   = MkEitherT $ runEitherT et >>= either (runEitherT . f) (pure . Right)
 87 |
 88 |
 89 | -------------------------------------------------
 90 | -- Interface Implementations
 91 | -------------------------------------------------
 92 |
 93 | public export
 94 | Eq (m (Either e a)) => Eq (EitherT e m a) where
 95 |  (==) = (==) `on` runEitherT
 96 |
 97 | public export
 98 | Ord (m (Either e a)) => Ord (EitherT e m a) where
 99 |  compare = compare `on` runEitherT
100 |
101 | public export
102 | Show (m (Either e a)) => Show (EitherT e m a) where
103 |   showPrec d (MkEitherT x) = showCon d "MkEitherT" $ showArg x
104 |
105 | -- I'm not actually confident about having this instance but it is a sane
106 | -- default and since idris has named implementations it can be swapped out at
107 | -- the use site.
108 | public export
109 | Monad m => Semigroup (EitherT e m a) where
110 |   MkEitherT x <+> MkEitherT y = MkEitherT $ do
111 |     r@(Right _) <- x
112 |       | Left _ => y
113 |     pure r
114 |
115 | public export
116 | Functor m => Functor (EitherT e m) where
117 |   map f e = MkEitherT $ map f <$> runEitherT e
118 |
119 | public export
120 | Foldable m => Foldable (EitherT e m) where
121 |   foldr f acc (MkEitherT e)
122 |     = foldr (\x,xs => either (const xs) (`f` xs) x) acc e
123 |
124 |   null (MkEitherT e) = null e
125 |
126 | public export
127 | Traversable m => Traversable (EitherT e m) where
128 |   traverse f (MkEitherT x)
129 |     = MkEitherT <$> traverse (either (pure . Left) (map Right . f)) x
130 |
131 | public export
132 | Applicative m => Applicative (EitherT e m) where
133 |   pure = MkEitherT . pure . Right
134 |   f <*> x = MkEitherT [| runEitherT f <*> runEitherT x |]
135 |
136 | public export
137 | Monad m => Monad (EitherT e m) where
138 |   x >>= k = MkEitherT $ runEitherT x >>= either (pure . Left) (runEitherT . k)
139 |
140 | ||| Alternative instance that collects left results, allowing you to try
141 | ||| multiple possibilities and combine failures.
142 | public export
143 | (Monad m, Monoid e) => Alternative (EitherT e m) where
144 |   empty = left neutral
145 |   MkEitherT x <|> my = MkEitherT $ do
146 |     Left l <- x
147 |       | Right r => pure (Right r)
148 |     Left l' <- runEitherT my
149 |       | Right r => pure (Right r)
150 |     pure (Left (l <+> l'))
151 |
152 | public export
153 | MonadTrans (EitherT e) where
154 |   lift = MkEitherT . map Right
155 |
156 | public export
157 | HasIO m => HasIO (EitherT e m) where
158 |   liftIO act = MkEitherT $ liftIO (io_bind act (pure . Right))
159 |