From 394613432f6e1a66e14c315c95935027cf1b0b6e Mon Sep 17 00:00:00 2001
From: Jeremy <36511199+Jeremy-Stafford@users.noreply.github.com>
Date: Fri, 25 Mar 2022 10:14:25 +0000
Subject: [PATCH] Add documentation for Control.Monad.* (#2365)

Co-authored-by: Zoe Stafford <36511192+Z-snails@users.noreply.github.com>
---
 libs/base/Control/Monad/Error/Either.idr    | 49 +++++++++++++--------
 libs/base/Control/Monad/Identity.idr        |  2 +
 libs/base/Control/Monad/Maybe.idr           | 37 ++++++++++++++--
 libs/base/Control/Monad/RWS/CPS.idr         | 29 ++++++++----
 libs/base/Control/Monad/Reader/Reader.idr   |  9 +++-
 libs/base/Control/Monad/ST.idr              | 19 ++++++++
 libs/base/Control/Monad/State/Interface.idr |  2 +-
 libs/base/Control/Monad/State/State.idr     |  4 +-
 libs/base/Control/Monad/Trans.idr           |  3 ++
 9 files changed, 120 insertions(+), 34 deletions(-)

diff --git a/libs/base/Control/Monad/Error/Either.idr b/libs/base/Control/Monad/Error/Either.idr
index 9c550575e..81bb91775 100644
--- a/libs/base/Control/Monad/Error/Either.idr
+++ b/libs/base/Control/Monad/Error/Either.idr
@@ -1,59 +1,68 @@
+||| Provides a monad transformer `EitherT` that extends an inner monad with the
+||| ability to throw and catch exceptions.
+
 module Control.Monad.Error.Either
 
--------------------------------------------------
--- The monad transformer `EitherT e m a` equips a monad with the ability to
--- return a choice of two values.
-
--- Sequenced actions of `Either e m a` produce a value `a` only if none of the
--- actions in the sequence returned `e`. Because returning `e` exits the
--- computation early, this can be seen as equipping a monad with the ability to
--- throw an exception.
-
--- This is more powerful than MaybeT which instead equips a monad with the
--- ability to not return a result.
--------------------------------------------------
-
 import Control.Monad.Trans
 
 %default total
 
+||| A monad transformer extending an inner monad with the ability to throw and
+||| catch exceptions.
+|||
+||| Sequenced actions produce an exception if either action produces an
+||| exception, with preference for the first exception. If neither produce an
+||| exception, neither does the sequence of actions.
+|||
+||| `MaybeT m a` is equivalent to `EitherT () m a`, that is, an computation
+||| that can only throw a single, information-less exception.
 public export
 data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
   MkEitherT : m (Either e a) -> EitherT e m a
 
+||| Unwrap an `EitherT` computation.
 public export
 %inline
 runEitherT : EitherT e m a -> m (Either e a)
 runEitherT (MkEitherT x) = x
 
+||| Run an `EitherT` computation, handling results and exceptions with seperate
+||| functions.
+|||
+||| This is a version of `either` lifted to work with `EitherT`.
 public export
 eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
 eitherT f g x = runEitherT x >>= either f g
 
-||| map the underlying computation
-||| The basic 'unwrap, apply, rewrap' of this transformer.
+||| Map over the underlying monadic computation.
 public export
 %inline
 mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
 mapEitherT f = MkEitherT . f . runEitherT
 
+||| Map over the result or the exception of a monadic computation.
 public export
 bimapEitherT : Functor m => (a -> c) -> (b -> d)
             -> EitherT a m b -> EitherT c m d
 bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x
 
-||| Analogous to Left, aka throwE
+||| A version of `Left` lifted to work with `EitherT`.
+|||
+||| This is equivalent to `throwE`.
 public export
 %inline
 left : Applicative m => e -> EitherT e m a
 left = MkEitherT . pure . Left
 
-||| Analogous to Right, aka pure for EitherT
+||| A version of `Right` lifted to work with `EitherT`.
+|||
+||| This is equivalent to `pure`.
 public export
 %inline
 right : Applicative m => a -> EitherT e m a
 right = MkEitherT . pure . Right
 
+||| Swap the result and the exception of a monadic computation.
 public export
 swapEitherT : Functor m => EitherT e m a -> EitherT a m e
 swapEitherT = mapEitherT (map (either Right Left))
@@ -62,12 +71,16 @@ swapEitherT = mapEitherT (map (either Right Left))
 -- Methods of the 'exception' theme
 -------------------------------------------------
 
-||| aka `left`
+||| Throw an exception in a monadic computation.
 public export
 %inline
 throwE : Applicative m => e -> EitherT e m a
 throwE = MkEitherT . pure . Left
 
+||| Handle an exception thrown in a monadic computation.
+|||
+||| Since the handler catches all errors thrown in the computation, it may
+||| raise a different exception type.
 public export
 catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
 catchE et f
diff --git a/libs/base/Control/Monad/Identity.idr b/libs/base/Control/Monad/Identity.idr
index f938bad27..2b201c7b6 100644
--- a/libs/base/Control/Monad/Identity.idr
+++ b/libs/base/Control/Monad/Identity.idr
@@ -4,6 +4,8 @@ import Data.Bits
 
 %default total
 
+||| The identity monad. This monad provides no abilities other than pure
+||| computation.
 public export
 record Identity (a : Type) where
   constructor Id
diff --git a/libs/base/Control/Monad/Maybe.idr b/libs/base/Control/Monad/Maybe.idr
index 78c9fed49..a2def4e95 100644
--- a/libs/base/Control/Monad/Maybe.idr
+++ b/libs/base/Control/Monad/Maybe.idr
@@ -16,54 +16,83 @@ import Data.Maybe
 
 %default total
 
+||| A monad transformer extending an inner monad with the ability to not return
+||| a result.
+|||
+||| Sequenced actions produce a result only if both actions return a result.
+|||
+||| `MaybeT m a` is equivalent to `EitherT () m a`, that is, an computation
+||| that can only throw a single, information-less exception.
 public export
 data MaybeT : (m : Type -> Type) -> (a : Type) -> Type where
   MkMaybeT : m (Maybe a) -> MaybeT m a
 
+||| Unwrap a `MaybeT` computation.
 public export
 %inline
 runMaybeT : MaybeT m a -> m (Maybe a)
 runMaybeT (MkMaybeT x) = x
 
+||| Check if a monadic computation returns a result. This returns `False` if
+||| the computation returns a result, and `True` otherwise.
+|||
+||| This is a version of `isNothing` lifted to work with `MaybeT`.
 public export
 %inline
 isNothingT : Functor m => MaybeT m a -> m Bool
 isNothingT = map isNothing . runMaybeT
 
+||| Check if a monadic computation returns a result. This returns `True` if
+||| the computation returns a result, and `False` otherwise.
+|||
+||| This is a version of `isJust` lifted to work with `MaybeT`.
 public export
 %inline
 isJustT : Functor m => MaybeT m a -> m Bool
 isJustT = map isJust . runMaybeT
 
+||| Run a `MaybeT` computation, handling the case of a result or no result
+||| seperately.
+|||
+||| This is a version of `maybe` lifted to work with `MaybeT`.
 public export
 %inline
 maybeT : Monad m => m b -> (a -> m b) -> MaybeT m a -> m b
 maybeT v g x = runMaybeT x >>= maybe v g
 
+||| Run a `MaybeT` computation providing a default value.
+|||
+||| This is a version of `fromMaybe` lifted to work with `MaybeT`.
 public export
 %inline
 fromMaybeT : Monad m => m a -> MaybeT m a -> m a
 fromMaybeT v x = runMaybeT x >>= maybe v pure
 
+||| Return a value if a condition is met, or else no value.
+|||
+||| This is a version of `toMaybe` lifted to work with `MaybeT`.
 public export
 %inline
 toMaybeT : Functor m => Bool -> m a -> MaybeT m a
 toMaybeT b m = MkMaybeT $ map (\a => toMaybe b a) m
 
-||| map the underlying computation
-||| The basic 'unwrap, apply, rewrap' of this transformer.
+||| Map over the underlying computation.
 public export
 %inline
 mapMaybeT : (m (Maybe a) -> n (Maybe a')) -> MaybeT m a -> MaybeT n a'
 mapMaybeT f = MkMaybeT . f . runMaybeT
 
-||| Analogous to Just, aka pure for MaybeT
+||| A version of `Just` lifted to work with `MaybeT`.
+|||
+||| This is equivalent to `pure`.
 public export
 %inline
 just : Applicative m => a -> MaybeT m a
 just = MkMaybeT . pure . Just
 
-||| Analogous to Nothing, aka empty for MaybeT
+||| A version of `Nothing` lifted to work with `MaybeT`.
+|||
+||| This is equivalent to `throwE ()`.
 public export
 %inline
 nothing : Applicative m => MaybeT m a
diff --git a/libs/base/Control/Monad/RWS/CPS.idr b/libs/base/Control/Monad/RWS/CPS.idr
index 009d0991f..f31ff7490 100644
--- a/libs/base/Control/Monad/RWS/CPS.idr
+++ b/libs/base/Control/Monad/RWS/CPS.idr
@@ -9,20 +9,27 @@ import Control.Monad.Trans
 
 %default total
 
-||| A monad transformer adding reading an environment of type `r`,
-||| collecting an output of type `w` and updating a state of type `s`
-||| to an inner monad `m`.
+||| A monad transformer extending an inner monad `m` with the ability to read
+||| an environment of type `r`, collect an output of type `w` and update a
+||| state of type `s`.
+|||
+||| This is equivalent to `ReaderT r (WriterT w (StateT s m)) a`, but fuses the
+||| three layers.
 public export
 record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
   constructor MkRWST
   unRWST : r -> s -> w -> m (a, s, w)
 
-||| Unwrap an RWST computation as a function. (The inverse of `rwsT`.)
+||| Unwrap an RWST computation as a function.
+|||
+||| This is the inverse of `rwsT`.
 public export %inline
 runRWST : Monoid w => RWST r w s m a -> r -> s -> m (a, s, w)
 runRWST m r s = unRWST m r s neutral
 
-||| Construct an RWST computation from a function. (The inverse of `runRWST`.)
+||| Construct an RWST computation from a function.
+|||
+||| This is the inverse of `runRWST`.
 public export %inline
 rwsT : Semigroup w => Functor m => (r -> s -> m (a, s, w)) -> RWST r w s m a
 rwsT f = MkRWST $ \r,s,w => (\(a,s',w') => (a,s',w <+> w')) <$> f r s
@@ -39,7 +46,7 @@ public export %inline
 execRWST : Monoid w => Functor m => RWST r w s m a -> r -> s -> m (s,w)
 execRWST m r s = (\(_,s',w) => (s',w)) <$> runRWST m r s
 
-||| Map the inner computation using the given function.
+||| Map over the inner computation.
 public export %inline
 mapRWST : (Functor n, Monoid w, Semigroup w')
         => (m (a, s, w) -> n (b, s, w')) -> RWST r w s m a -> RWST r w' s n b
@@ -58,16 +65,22 @@ withRWST f m = MkRWST $ \r,s => uncurry (unRWST m) (f r s)
 
 ||| A monad containing an environment of type `r`, output of type `w`
 ||| and an updatable state of type `s`.
+|||
+||| This is `RWST` applied to `Identity`.
 public export
 RWS : (r : Type) -> (w : Type) -> (s : Type) -> (a : Type) -> Type
 RWS r w s = RWST r w s Identity
 
-||| Unwrap an RWS computation as a function. (The inverse of `rws`.)
+||| Unwrap an RWS computation as a function.
+|||
+||| This is the inverse of `rws`.
 public export %inline
 runRWS : Monoid w => RWS r w s a -> r -> s -> (a, s, w)
 runRWS m r s = runIdentity (runRWST m r s)
 
-||| Construct an RWS computation from a function. (The inverse of `runRWS`.)
+||| Construct an RWS computation from a function.
+|||
+||| This is the inverse of `runRWS`.
 public export %inline
 rws : Semigroup w => (r -> s -> (a, s, w)) -> RWS r w s a
 rws f = MkRWST $ \r,s,w => let (a, s', w') = f r s
diff --git a/libs/base/Control/Monad/Reader/Reader.idr b/libs/base/Control/Monad/Reader/Reader.idr
index d05973475..edd73b7e8 100644
--- a/libs/base/Control/Monad/Reader/Reader.idr
+++ b/libs/base/Control/Monad/Reader/Reader.idr
@@ -5,7 +5,10 @@ import Control.Monad.Trans
 
 %default total
 
-||| The transformer on which the Reader monad is based
+||| A monad transformer extending an inner monad with access to an environment.
+|||
+||| The environment is the same for all actions in a sequence, but may be
+||| changed within scopes created by `Control.Monad.Reader.local`.
 public export
 record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
   constructor MkReaderT
@@ -26,7 +29,9 @@ runReaderT s action = runReaderT' action s
 --          Reader
 --------------------------------------------------------------------------------
 
-||| The Reader monad. The ReaderT transformer applied to the Identity monad.
+||| A monad that can access an environment.
+|||
+||| This is `ReaderT` applied to `Identity`.
 public export
 Reader : (stateType : Type) -> (a : Type) -> Type
 Reader s a = ReaderT s Identity a
diff --git a/libs/base/Control/Monad/ST.idr b/libs/base/Control/Monad/ST.idr
index 8f8d03a0f..d43fee54a 100644
--- a/libs/base/Control/Monad/ST.idr
+++ b/libs/base/Control/Monad/ST.idr
@@ -1,17 +1,29 @@
+||| Provides mutable references as described in Lazy Functional State Threads.
 module Control.Monad.ST
 
 import Data.IORef
 
 %default total
 
+||| A mutable reference, bound to a state thread.
+|||
+||| A value of type `STRef s a` contains a mutable `a`, bound to a "thread"
+||| `s`. Any access to the reference must occur in an `ST s` monad with the
+||| same "thread".
 export
 data STRef : Type -> Type -> Type where
      MkSTRef : IORef a -> STRef s a
 
+||| The `ST` monad allows for mutable access to references, but unlike `IO`, it
+||| is "escapable".
+|||
+||| The parameter `s` is a "thread" -- it ensures that access to mutable
+||| references created in each thread must occur in that same thread.
 export
 data ST : Type -> Type -> Type where
      MkST : IO a -> ST s a
 
+||| Run a `ST` computation.
 export
 runST : (forall s . ST s a) -> a
 runST p
@@ -34,22 +46,29 @@ Monad (ST s) where
                   let MkST kp = k p'
                   kp
 
+||| Create a new mutable reference with the given value.
 export
 newSTRef : a -> ST s (STRef s a)
 newSTRef val
     = MkST $ do r <- newIORef val
                 pure (MkSTRef r)
 
+||| Read the value of a mutable reference.
+|||
+||| This occurs within `ST s` to prevent `STRef`s from being usable if they are
+||| "leaked" via `runST`.
 %inline
 export
 readSTRef : STRef s a -> ST s a
 readSTRef (MkSTRef r) = MkST $ readIORef r
 
+||| Write to a mutable reference.
 %inline
 export
 writeSTRef : STRef s a -> (val : a) -> ST s ()
 writeSTRef (MkSTRef r) val = MkST $ writeIORef r val
 
+||| Apply a function to the contents of a mutable reference.
 export
 modifySTRef : STRef s a -> (a -> a) -> ST s ()
 modifySTRef ref f
diff --git a/libs/base/Control/Monad/State/Interface.idr b/libs/base/Control/Monad/State/Interface.idr
index a219fd938..de9f3d57a 100644
--- a/libs/base/Control/Monad/State/Interface.idr
+++ b/libs/base/Control/Monad/State/Interface.idr
@@ -10,7 +10,7 @@ import Control.Monad.Writer.CPS
 
 %default total
 
-||| A computation which runs in a context and produces an output
+||| A monadic computation that has access to state.
 public export
 interface Monad m => MonadState stateType m | m where
     ||| Get the context
diff --git a/libs/base/Control/Monad/State/State.idr b/libs/base/Control/Monad/State/State.idr
index 4f91c614c..c5d73d832 100644
--- a/libs/base/Control/Monad/State/State.idr
+++ b/libs/base/Control/Monad/State/State.idr
@@ -5,7 +5,9 @@ import Control.Monad.Trans
 
 %default total
 
-||| The transformer on which the State monad is based
+||| A monad transformer extending an inner monad `m` with state `stateType`.
+|||
+||| Updates to the state are applied in the order as the sequence of actions.
 public export
 record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
   constructor ST
diff --git a/libs/base/Control/Monad/Trans.idr b/libs/base/Control/Monad/Trans.idr
index 6ace4164c..a142c5e77 100644
--- a/libs/base/Control/Monad/Trans.idr
+++ b/libs/base/Control/Monad/Trans.idr
@@ -2,6 +2,9 @@ module Control.Monad.Trans
 
 %default total
 
+||| A monad transformer is a type that can wrap an inner monad, extending it
+||| with additional abilities.
 public export
 interface MonadTrans t where
+    ||| Lift a computation from the inner monad to the transformed monad.
     lift : Monad m => m a -> t m a