0 | module Control.Monad.Maybe
  1 |
  2 | -------------------------------------------------
  3 | -- The monad transformer `MaybeT m a` equips a monad with the ability to
  4 | -- return no value at all.
  5 |
  6 | -- Sequenced actions of `MaybeT m a` produce a value `a` only if all of the
  7 | -- actions in the sequence returned a value.
  8 |
  9 | -- This is isomorphic to `EitherT ()` and therefore less powerful than `EitherT e a`
 10 | -- ability to not return a result.
 11 | -------------------------------------------------
 12 |
 13 | import Control.Monad.Trans
 14 | import Data.Maybe
 15 |
 16 | %default total
 17 |
 18 | ||| A monad transformer extending an inner monad with the ability to not return
 19 | ||| a result.
 20 | |||
 21 | ||| Sequenced actions produce a result only if both actions return a result.
 22 | |||
 23 | ||| `MaybeT m a` is equivalent to `EitherT () m a`, that is, an computation
 24 | ||| that can only throw a single, information-less exception.
 25 | public export
 26 | data MaybeT : (m : Type -> Type) -> (a : Type) -> Type where
 27 |   MkMaybeT : m (Maybe a) -> MaybeT m a
 28 |
 29 | ||| Unwrap a `MaybeT` computation.
 30 | public export
 31 | %inline
 32 | runMaybeT : MaybeT m a -> m (Maybe a)
 33 | runMaybeT (MkMaybeT x) = x
 34 |
 35 | ||| Check if a monadic computation returns a result. This returns `False` if
 36 | ||| the computation returns a result, and `True` otherwise.
 37 | |||
 38 | ||| This is a version of `isNothing` lifted to work with `MaybeT`.
 39 | public export
 40 | %inline
 41 | isNothingT : Functor m => MaybeT m a -> m Bool
 42 | isNothingT = map isNothing . runMaybeT
 43 |
 44 | ||| Check if a monadic computation returns a result. This returns `True` if
 45 | ||| the computation returns a result, and `False` otherwise.
 46 | |||
 47 | ||| This is a version of `isJust` lifted to work with `MaybeT`.
 48 | public export
 49 | %inline
 50 | isJustT : Functor m => MaybeT m a -> m Bool
 51 | isJustT = map isJust . runMaybeT
 52 |
 53 | ||| Run a `MaybeT` computation, handling the case of a result or no result
 54 | ||| separately.
 55 | |||
 56 | ||| This is a version of `maybe` lifted to work with `MaybeT`.
 57 | public export
 58 | %inline
 59 | maybeT : Monad m => m b -> (a -> m b) -> MaybeT m a -> m b
 60 | maybeT v g x = runMaybeT x >>= maybe v g
 61 |
 62 | ||| Run a `MaybeT` computation providing a default value.
 63 | |||
 64 | ||| This is a version of `fromMaybe` lifted to work with `MaybeT`.
 65 | public export
 66 | %inline
 67 | fromMaybeT : Monad m => m a -> MaybeT m a -> m a
 68 | fromMaybeT v x = runMaybeT x >>= maybe v pure
 69 |
 70 | ||| Return a value if a condition is met, or else no value. The condition
 71 | ||| only affects whether the `Maybe` produces a value; the effect is run
 72 | ||| either way.
 73 | |||
 74 | ||| This is a version of `toMaybe` lifted to work with `MaybeT`.
 75 | public export
 76 | %inline
 77 | toMaybeT : Functor m => Bool -> m a -> MaybeT m a
 78 | toMaybeT b m = MkMaybeT $ map (\a => toMaybe b a) m
 79 |
 80 | ||| Map over the underlying computation.
 81 | public export
 82 | %inline
 83 | mapMaybeT : (m (Maybe a) -> n (Maybe a')) -> MaybeT m a -> MaybeT n a'
 84 | mapMaybeT f = MkMaybeT . f . runMaybeT
 85 |
 86 | ||| A version of `Just` lifted to work with `MaybeT`.
 87 | |||
 88 | ||| This is equivalent to `pure`.
 89 | public export
 90 | %inline
 91 | just : Applicative m => a -> MaybeT m a
 92 | just = MkMaybeT . pure . Just
 93 |
 94 | ||| A version of `Nothing` lifted to work with `MaybeT`.
 95 | |||
 96 | ||| This is equivalent to `throwE ()`.
 97 | public export
 98 | %inline
 99 | nothing : Applicative m => MaybeT m a
100 | nothing = MkMaybeT $ pure Nothing
101 |
102 | -------------------------------------------------
103 | -- Interface Implementations
104 | -------------------------------------------------
105 |
106 | public export
107 | Eq (m (Maybe a)) => Eq (MaybeT m a) where
108 |  (==) = (==) `on` runMaybeT
109 |
110 | public export
111 | Ord (m (Maybe a)) => Ord (MaybeT m a) where
112 |  compare = compare `on` runMaybeT
113 |
114 | public export
115 | Show (m (Maybe a)) => Show (MaybeT m a) where
116 |   showPrec d (MkMaybeT x) = showCon d "MkMaybeT" $ showArg x
117 |
118 | ||| Corresponds to the Semigroup instance of Maybe
119 | |||
120 | ||| Note: This could also be implemented with only an Applicative
121 | ||| prerequisite: `MkMaybeT x <+> MkMaybeT y = MkMaybeT $ [| x <+> y |]`
122 | ||| However, the monadic version is more efficient for long-running effects,
123 | ||| only evaluating the second argument if the first returns `Nothing`.
124 | public export
125 | Monad m => Semigroup (MaybeT m a) where
126 |   MkMaybeT x <+> MkMaybeT y = MkMaybeT $ do
127 |     r@(Just _) <- x | Nothing => y
128 |     pure r
129 |
130 | public export
131 | Monad m => Monoid (MaybeT m a) where
132 |   neutral = nothing
133 |
134 | public export
135 | Functor m => Functor (MaybeT m) where
136 |   map f m = MkMaybeT $ map f <$> runMaybeT m
137 |
138 | public export
139 | Foldable m => Foldable (MaybeT m) where
140 |   foldr f acc (MkMaybeT e)
141 |     = foldr (\x,xs => maybe xs (`f` xs) x) acc e
142 |
143 |   null (MkMaybeT e) = null e
144 |
145 | public export
146 | Traversable m => Traversable (MaybeT m) where
147 |   traverse f (MkMaybeT x)
148 |     = MkMaybeT <$> traverse (maybe (pure Nothing) (map Just . f)) x
149 |
150 | public export
151 | Applicative m => Applicative (MaybeT m) where
152 |   pure = just
153 |   MkMaybeT f <*> MkMaybeT x = MkMaybeT [| f <*> x |]
154 |
155 | public export
156 | Monad m => Monad (MaybeT m) where
157 |   MkMaybeT x >>= k = MkMaybeT $ x >>= maybe (pure Nothing) (runMaybeT . k)
158 |
159 | ||| See note about Monad prerequisite on Semigroup instance.
160 | public export
161 | Monad m => Alternative (MaybeT m) where
162 |   empty = nothing
163 |   MkMaybeT x <|> my = MkMaybeT $ x >>= \case
164 |     r@(Just _) => pure r
165 |     Nothing    => runMaybeT my
166 |
167 | public export
168 | MonadTrans MaybeT where
169 |   lift = MkMaybeT . map Just
170 |
171 | public export
172 | HasIO m => HasIO (MaybeT m) where
173 |   liftIO act = MkMaybeT $ liftIO (io_bind act (pure . Just))
174 |