diff --git a/heftia-effects/Example/FileSystemProvider/Main.hs b/heftia-effects/Example/FileSystemProvider/Main.hs
index 2c3f4fd..f16aaea 100644
--- a/heftia-effects/Example/FileSystemProvider/Main.hs
+++ b/heftia-effects/Example/FileSystemProvider/Main.hs
@@ -18,7 +18,7 @@ import Control.Monad.Hefty (
     type (<|),
     type (~>),
  )
-import Control.Monad.Hefty.Provider (Provider_, runProvider_, scope_)
+import Control.Monad.Hefty.Provider (Provide_, runProvider_, scope_)
 
 data FileSystemF a where
     ReadFS :: FilePath -> FileSystemF String
@@ -28,7 +28,7 @@ data FileSystemH m (a :: Type) where
     TransactFS :: m a -> FileSystemH m a
 makeEffect [''FileSystemF] [''FileSystemH]
 
-type FSProvider eh ef = Provider_ FilePath FileSystemH FileSystemF eh ef
+type FSProvider eh ef = Provide_ FilePath FileSystemH FileSystemF eh ef
 
 runDummyFSProvider :: (IO <| ef) => Eff (FSProvider eh ef ': eh) ef ~> Eff eh ef
 runDummyFSProvider =
diff --git a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Parallel.hs b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Parallel.hs
index e1f8e2b..09cfd87 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Parallel.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Parallel.hs
@@ -2,6 +2,13 @@
 
 -- SPDX-License-Identifier: MPL-2.0
 
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+License     :  MPL-2.0 (see the LICENSE file)
+Maintainer  :  ymdfield@outlook.jp
+
+Interpreters for the [Parallel]("Data.Effect.Concurrent.Parallel") effects.
+-}
 module Control.Monad.Hefty.Concurrent.Parallel (
     module Control.Monad.Hefty.Concurrent.Parallel,
     module Data.Effect.Concurrent.Parallel,
diff --git a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Stream.hs b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Stream.hs
index b5776e3..be8db3a 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Stream.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Stream.hs
@@ -1,7 +1,12 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 
--- SPDX-License-Identifier: MPL-2.0
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+License     :  MPL-2.0 (see the LICENSE file)
+Maintainer  :  ymdfield@outlook.jp
 
+Coroutine-based, composable, and resumable concurrent streams.
+-}
 module Control.Monad.Hefty.Concurrent.Stream (
     module Control.Monad.Hefty.Concurrent.Stream,
     module Control.Monad.Hefty.Input,
diff --git a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Subprocess.hs b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Subprocess.hs
index 1f2279d..8564b34 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Subprocess.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Subprocess.hs
@@ -4,9 +4,14 @@
 
 -- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause
 
---  (c) The University of Glasgow 2004-2008
---  (c) Sayo Koyoneda 2024
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+               (c) The University of Glasgow 2004-2008
+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause
+Maintainer  :  ymdfield@outlook.jp
 
+Effects for subprocess.
+-}
 module Control.Monad.Hefty.Concurrent.Subprocess (
     module Control.Monad.Hefty.Concurrent.Subprocess,
     module Control.Monad.Hefty.Provider,
@@ -62,7 +67,7 @@ data Lifecycle = Kill | Wait
 
 makeEffectF [''Subprocess]
 
-type SubprocProvider eh ef = Provider SubprocResult CreateProcess (Const2 LNop) Subprocess eh ef
+type SubprocProvider eh ef = Provide SubprocResult CreateProcess (Const2 LNop) Subprocess eh ef
 
 data SubprocResult p a where
     RaceResult :: Either ExitCode a -> SubprocResult ('SubprocMode i o e 'Kill 'Kill) a
diff --git a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Timer.hs b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Timer.hs
index ecc61b3..eea3285 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Concurrent/Timer.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Concurrent/Timer.hs
@@ -2,6 +2,13 @@
 
 -- SPDX-License-Identifier: MPL-2.0
 
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+License     :  MPL-2.0 (see the LICENSE file)
+Maintainer  :  ymdfield@outlook.jp
+
+Interpreters for the [Timer]("Data.Effect.Concurrent.Timer") effects.
+-}
 module Control.Monad.Hefty.Concurrent.Timer (
     module Control.Monad.Hefty.Concurrent.Timer,
     module Data.Effect.Concurrent.Timer,
@@ -58,6 +65,7 @@ runCyclicTimer a = do
                     Continue () k -> put =<< raise (k delta)
         & evalState timer0
 
+-- | Re-zeros the clock time in the local scope.
 restartClock :: (Timer <| ef) => eh :!! ef ~> eh :!! ef
 restartClock a = do
     t0 <- clock
diff --git a/heftia-effects/src/Control/Monad/Hefty/Coroutine.hs b/heftia-effects/src/Control/Monad/Hefty/Coroutine.hs
index a5483c3..9b2c8e1 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Coroutine.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Coroutine.hs
@@ -1,5 +1,12 @@
 -- SPDX-License-Identifier: MPL-2.0
 
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+License     :  MPL-2.0 (see the LICENSE file)
+Maintainer  :  ymdfield@outlook.jp
+
+Interpreters for the [coroutine]("Data.Effect.Coroutine") effect.
+-}
 module Control.Monad.Hefty.Coroutine (
     module Control.Monad.Hefty.Coroutine,
     module Data.Effect.Coroutine,
@@ -13,14 +20,17 @@ import Data.Effect.Coroutine
 import Data.Effect.Input
 import Data.Effect.Output
 
+-- | Interpret the [coroutine]("Data.Effect.Coroutine")'s t'Yield' effect.
 runCoroutine
     :: forall a b ans ef
      . Eff '[] (Yield a b ': ef) ans
     -> Eff '[] ef (Status (Eff '[] ef) a b ans)
 runCoroutine = interpretBy (pure . Done) (\(Yield a) k -> pure $ Continue a k)
 
+-- | Converts the t'Input' effect into the [coroutine]("Data.Effect.Coroutine")'s t'Yield' effect.
 inputToYield :: Input i ~> Yield () i
 inputToYield Input = Yield ()
 
+-- | Converts the t'Output' effect into the [coroutine]("Data.Effect.Coroutine")'s t'Yield' effect.
 outputToYield :: Output o ~> Yield o ()
 outputToYield (Output o) = Yield o
diff --git a/heftia-effects/src/Control/Monad/Hefty/Except.hs b/heftia-effects/src/Control/Monad/Hefty/Except.hs
index 955f89e..b06e919 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Except.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Except.hs
@@ -1,14 +1,11 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2023 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
 
-Interpreters for the t'Data.Effect.Except.Throw' / t'Data.Effect.Except.Catch' effects.
+Interpreters for the [Except]("Data.Effect.Except") effects.
 -}
 module Control.Monad.Hefty.Except (
     module Control.Monad.Hefty.Except,
@@ -35,29 +32,36 @@ import Data.Effect.Unlift (UnliftIO)
 import UnliftIO (throwIO)
 import UnliftIO qualified as IO
 
+-- | Interpret the t'Throw'/t'Catch' effects.
 runExcept :: Eff '[Catch e] (Throw e ': r) a -> Eff '[] r (Either e a)
 runExcept = runThrow . runCatch
 
+-- | Interpret the t'Throw' effect.
 runThrow :: Eff '[] (Throw e ': r) a -> Eff '[] r (Either e a)
 runThrow = interpretBy (pure . Right) handleThrow
 
+-- | Interpret the t'Catch' effect.
 runCatch :: (Throw e <| ef) => Eff '[Catch e] ef ~> Eff '[] ef
 runCatch = interpretH elabCatch
 
+-- | A handler function for the t'Throw' effect.
 handleThrow :: Interpreter (Throw e) (Eff '[] r) (Either e a)
 handleThrow (Throw e) _ = pure $ Left e
 {-# INLINE handleThrow #-}
 
+-- | A elaborator function for the t'Catch' effect.
 elabCatch :: (Throw e <| ef) => Catch e ~~> Eff '[] ef
 elabCatch (Catch action hdl) = action & interposeWith \(Throw e) _ -> hdl e
 {-# INLINE elabCatch #-}
 
+-- | Interpret the t'Throw' effect based on an IO-fused semantics using IO-level exceptions.
 runThrowIO
     :: forall e eh ef
      . (IO <| ef, Exception e)
     => Eff eh (Throw e ': ef) ~> Eff eh ef
 runThrowIO = interpret \(Throw e) -> throwIO e
 
+-- | Interpret the t'Catch' effect based on an IO-fused semantics using IO-level exceptions.
 runCatchIO
     :: forall e eh ef
      . (UnliftIO <<| eh, IO <| ef, Exception e)
diff --git a/heftia-effects/src/Control/Monad/Hefty/Input.hs b/heftia-effects/src/Control/Monad/Hefty/Input.hs
index 49895cc..1173c25 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Input.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Input.hs
@@ -1,12 +1,11 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2024 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
+
+Interpreters for the t'Input' effect.
 -}
 module Control.Monad.Hefty.Input (
     module Control.Monad.Hefty.Input,
@@ -21,18 +20,25 @@ import Data.Effect.Input
 import Data.Effect.State (gets, put)
 import Data.List (uncons)
 
+-- | Interprets the t'Input' effect by executing the given input handler each time an input is required.
 runInputEff
     :: forall i ef eh
      . Eff eh ef i
     -> Eff eh (Input i ': ef) ~> Eff eh ef
 runInputEff a = interpret \Input -> a
 
+-- | Interprets the t'Input' effect by providing the given constant as input.
 runInputConst
     :: forall i ef eh
      . i
     -> Eff eh (Input i ': ef) ~> Eff eh ef
 runInputConst i = interpret \Input -> pure i
 
+{- |
+Interprets the t'Input' effect by using the given list as a series of inputs.
+
+Each time 'input' is called, it retrieves elements from the list one by one from the beginning, and after all elements are consumed, 'Nothing' is returned indefinitely.
+-}
 runInputList :: forall i r. [i] -> Eff '[] (Input (Maybe i) ': r) ~> Eff '[] r
 runInputList is =
     raiseUnder
diff --git a/heftia-effects/src/Control/Monad/Hefty/NonDet.hs b/heftia-effects/src/Control/Monad/Hefty/NonDet.hs
index 6c5e4f9..d1f2f46 100644
--- a/heftia-effects/src/Control/Monad/Hefty/NonDet.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/NonDet.hs
@@ -2,15 +2,14 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2024 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
+
+Interpreters for the [non-determinism]("Data.Effect.NonDet") effects.
 -}
 module Control.Monad.Hefty.NonDet (
     module Control.Monad.Hefty.NonDet,
@@ -42,7 +41,7 @@ import Data.Effect.NonDet
 import Data.Effect.Unlift (UnliftIO)
 import UnliftIO (Exception, SomeException, throwIO, try)
 
--- | 'NonDet' effects handler for alternative answer type.
+-- | [NonDet]("Data.Effect.NonDet") effects handler for alternative answer type.
 runNonDet
     :: forall f ef a
      . (Alternative f)
@@ -57,7 +56,7 @@ runNonDet =
                 !+ nil
             )
 
--- | 'NonDet' effects handler for monoidal answer type.
+-- | [NonDet]("Data.Effect.NonDet") effects handler for monoidal answer type.
 runNonDetMonoid
     :: forall ans ef a
      . (Monoid ans)
@@ -73,7 +72,7 @@ runNonDetMonoid f =
                 !+ nil
             )
 
--- | 'Choose' effect handler for alternative answer type.
+-- | t'Choose' effect handler for alternative answer type.
 runChoose
     :: forall f ef a
      . (Alternative f)
@@ -83,7 +82,7 @@ runChoose =
     interpretBy (pure . pure) \Choose k ->
         liftA2 (<|>) (k False) (k True)
 
--- | 'Choose' effect handler for monoidal answer type.
+-- | t'Choose' effect handler for monoidal answer type.
 runChooseMonoid
     :: forall ans ef a
      . (Semigroup ans)
@@ -94,14 +93,14 @@ runChooseMonoid f =
     interpretBy f \Choose k ->
         liftA2 (<>) (k False) (k True)
 
--- | 'Empty' effect handler.
+-- | t'Empty' effect handler.
 runEmpty :: forall a ef. Eff '[] (Empty ': ef) a -> Eff '[] ef (Maybe a)
 runEmpty =
     interpretBy
         (pure . Just)
         \Empty _ -> pure Nothing
 
-{- | 'ChooseH' effect elaborator.
+{- | t'ChooseH' effect elaborator.
 
     Convert a higher-order effect of the form
 
@@ -125,16 +124,25 @@ branch a b = do
 
 infixl 3 `branch`
 
+-- | Selects one element from the list nondeterministically, branching the control as many times as the number of elements.
 choice :: (Choose <| ef, Empty <| ef) => [a] -> Eff eh ef a
 choice = \case
     [] -> empty
     x : xs -> pure x `branch` choice xs
 
+-- | Selects one element from the list nondeterministically, branching the control as many times as the number of elements. Uses t'ChooseH'.
 choiceH :: (ChooseH <<| eh, Empty <| ef) => [a] -> Eff eh ef a
 choiceH = \case
     [] -> empty
     x : xs -> pure x <|> choiceH xs
 
+{- |
+Interprets the [NonDet]("Data.Effect.NonDet") effects using IO-level exceptions.
+
+When 'empty' occurs, an 'EmptyException' is thrown, and unless all branches from
+ 'chooseH' fail due to IO-level exceptions, only the leftmost result is returned
+ as the final result.
+-}
 runNonDetIO
     :: (UnliftIO <<| eh, IO <| ef)
     => Eff (ChooseH ': eh) (Empty ': ef) a
@@ -149,6 +157,7 @@ runNonDetIO m = try do
             )
         & interpret (\Empty -> throwIO EmptyException)
 
+-- | Exception thrown when 'empty' occurs in 'runNonDetIO'.
 data EmptyException = EmptyException
     deriving stock (Show)
     deriving anyclass (Exception)
diff --git a/heftia-effects/src/Control/Monad/Hefty/Output.hs b/heftia-effects/src/Control/Monad/Hefty/Output.hs
index 4bfef72..191e1b5 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Output.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Output.hs
@@ -1,12 +1,11 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2024 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
+
+Interpreters for the t'Output' effect.
 -}
 module Control.Monad.Hefty.Output (
     module Control.Monad.Hefty.Output,
@@ -22,17 +21,20 @@ import Data.Effect.Output
 import Data.Effect.State (modify)
 import Data.Effect.Writer (Tell (Tell))
 
+-- | Interprets the t'Output' effect using the given output handler.
 runOutputEff
     :: forall o ef eh
      . (o -> Eff eh ef ())
     -> Eff eh (Output o ': ef) ~> Eff eh ef
 runOutputEff f = interpret \(Output o) -> f o
 
+-- | Interprets the t'Output' effect by ignoring the outputs.
 ignoreOutput
     :: forall o ef eh
      . Eff eh (Output o ': ef) ~> Eff eh ef
 ignoreOutput = runOutputEff $ const $ pure ()
 
+-- | Interprets the t'Output' effect by accumulating the outputs into a list.
 runOutputList
     :: forall o a ef
      . Eff '[] (Output o ': ef) a
@@ -42,7 +44,7 @@ runOutputList =
         >>> interpret (\(Output o) -> modify (o :))
         >>> runState []
 
--- | Run an `Output` effect by transforming into a monoid.
+-- | Interprets the t'Output' effect by accumulating the outputs into a monoid.
 runOutputMonoid
     :: forall o w a ef
      . ( Monoid w
diff --git a/heftia-effects/src/Control/Monad/Hefty/Provider.hs b/heftia-effects/src/Control/Monad/Hefty/Provider.hs
index 89dd69a..6c44f15 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Provider.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Provider.hs
@@ -4,6 +4,8 @@
 Copyright   :  (c) 2024 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
+
+Interpreters for the [Provider]("Data.Effect.Provider") effects.
 -}
 module Control.Monad.Hefty.Provider (
     module Control.Monad.Hefty.Provider,
@@ -30,48 +32,52 @@ import Control.Monad.Hefty (
     type (~>),
  )
 import Data.Effect.HFunctor (hfmap)
-import Data.Effect.Provider hiding (Provider, Provider_)
-import Data.Effect.Provider qualified as D
+import Data.Effect.Provider
 import Data.Functor.Const (Const (Const))
 import Data.Functor.Identity (Identity (Identity))
 
-type Provider ctx i sh sf eh ef = D.Provider ctx i (ProviderEff ctx i sh sf eh ef)
+type Provide ctx i sh sf eh ef = Provider ctx i (ProviderEff ctx i sh sf eh ef)
 
 newtype ProviderEff ctx i sh sf eh ef p a
-    = ProviderEff {unProviderEff :: Eff (sh p ': Provider ctx i sh sf eh ef ': eh) (sf p ': ef) a}
+    = ProviderEff {unProviderEff :: Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) a}
 
-type Provider_ i sh sf eh ef =
-    D.Provider (Const1 Identity) (Const i :: () -> Type) (Const1 (ProviderEff_ i sh sf eh ef))
+type Provide_ i sh sf eh ef =
+    Provider (Const1 Identity) (Const i :: () -> Type) (Const1 (ProviderEff_ i sh sf eh ef))
 
 newtype ProviderEff_ i sh sf eh ef a
-    = ProviderEff_ {unProviderEff_ :: Eff (sh ': Provider_ i sh sf eh ef ': eh) (sf ': ef) a}
+    = ProviderEff_ {unProviderEff_ :: Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) a}
 
 newtype Const2 ff x f a = Const2 {getConst2 :: ff f a}
 instance (HFunctor ff) => HFunctor (Const2 ff x) where
     hfmap phi (Const2 ff) = Const2 $ hfmap phi ff
 
+-- | Interpret the t'Provider' effect using the given effect interpreter.
 runProvider
     :: forall ctx i sh sf eh ef
      . ( forall p x
           . i p
-         -> Eff (sh p ': Provider ctx i sh sf eh ef ': eh) (sf p ': ef) x
-         -> Eff (Provider ctx i sh sf eh ef ': eh) ef (ctx p x)
+         -> Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) x
+         -> Eff (Provide ctx i sh sf eh ef ': eh) ef (ctx p x)
        )
-    -> Eff (Provider ctx i sh sf eh ef ': eh) ef ~> Eff eh ef
+    -> Eff (Provide ctx i sh sf eh ef ': eh) ef ~> Eff eh ef
 runProvider run =
     interpretH \(KeyH (Provide i f)) ->
         runProvider run $
             run i (unProviderEff $ f $ ProviderEff . transEffHF (weakenNH @2) weaken)
 
+{- |
+Interpret the t'Provider' effect using the given effect interpreter.
+A version of 'runProvider' where the type of t'Provider' is simpler.
+-}
 runProvider_
     :: forall i sh sf eh ef
      . (HFunctor sh)
     => ( forall x
           . i
-         -> Eff (sh ': Provider_ i sh sf eh ef ': eh) (sf ': ef) x
-         -> Eff (Provider_ i sh sf eh ef ': eh) ef x
+         -> Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) x
+         -> Eff (Provide_ i sh sf eh ef ': eh) ef x
        )
-    -> Eff (Provider_ i sh sf eh ef ': eh) ef ~> Eff eh ef
+    -> Eff (Provide_ i sh sf eh ef ': eh) ef ~> Eff eh ef
 runProvider_ run =
     interpretH \(KeyH (Provide (Const i) f)) ->
         runProvider_ run $
@@ -86,6 +92,7 @@ runProvider_ run =
                         . transEffHF (weakenNH @2) weaken
                 )
 
+-- | Introduces a new local scope that provides effects @sh p@ and @sf p@ parameterized by @i p@ value and with results wrapped in @ctx p@.
 scope
     :: forall key ctx i p eh ef a sh sf bh bf
      . ( MemberHBy
@@ -95,14 +102,15 @@ scope
        , HFunctor (sh p)
        )
     => i p
-    -> ( Eff eh ef ~> Eff (key ##> sh p ': Provider ctx i sh sf bh bf ': bh) (key #> sf p ': bf)
-         -> Eff (key ##> sh p ': Provider ctx i sh sf bh bf ': bh) (key #> sf p ': bf) a
+    -> ( Eff eh ef ~> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf)
+         -> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf) a
        )
     -> Eff eh ef (ctx p a)
 scope i f =
     i ..! \runInScope ->
         ProviderEff $ unkeyH . unkey $ f (keyH . key . unProviderEff . runInScope)
 
+-- | Introduces a new local scope that provides effects @sh@ and @sf@ parameterized by @i@ value.
 scope_
     :: forall key i eh ef a sh sf bh bf
      . ( MemberHBy
@@ -116,8 +124,8 @@ scope_
        , HFunctor sh
        )
     => i
-    -> ( Eff eh ef ~> Eff (key ##> sh ': Provider_ i sh sf bh bf ': bh) (key #> sf ': bf)
-         -> Eff (key ##> sh ': Provider_ i sh sf bh bf ': bh) (key #> sf ': bf) a
+    -> ( Eff eh ef ~> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf)
+         -> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf) a
        )
     -> Eff eh ef a
 scope_ i f =
diff --git a/heftia-effects/src/Control/Monad/Hefty/Reader.hs b/heftia-effects/src/Control/Monad/Hefty/Reader.hs
index 16b41e8..30f6784 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Reader.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Reader.hs
@@ -1,14 +1,11 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2023 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
 
-Interpreters for the t'Ask' / t'Local' effects.
+Interpreters for the [Reader]("Data.Effect.Reader") effects.
 -}
 module Control.Monad.Hefty.Reader (
     module Control.Monad.Hefty.Reader,
@@ -28,19 +25,21 @@ import Control.Monad.Hefty (
  )
 import Data.Effect.Reader
 
+-- | Interpret the t'Ask'/t'Local' effects.
 runReader
     :: forall r eh ef
      . r
     -> Eff (Local r ': eh) (Ask r ': ef) ~> Eff eh ef
 runReader r = runAsk r . runLocal
 
--- | Elaborate the t'Local' effect.
+-- | Interpret the t'Local' effect.
 runLocal
     :: forall r eh ef
      . (Ask r <| ef)
     => Eff (Local r ': eh) ef ~> Eff eh ef
 runLocal = interpretH elabLocal
 
+-- | A elaborator function for the t'Local' effect.
 elabLocal
     :: forall r eh ef
      . (Ask r <| ef)
diff --git a/heftia-effects/src/Control/Monad/Hefty/State.hs b/heftia-effects/src/Control/Monad/Hefty/State.hs
index 79c003c..3e9d5e8 100644
--- a/heftia-effects/src/Control/Monad/Hefty/State.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/State.hs
@@ -6,7 +6,6 @@
 Copyright   :  (c) 2023 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
 
 Interpreter for the t'Data.Effect.State.State' effect.
 -}
@@ -38,25 +37,35 @@ import Data.Effect.State
 import Data.Functor ((<&>))
 import UnliftIO (newIORef, readIORef, writeIORef)
 
--- | Interpret the 'Get'/'Put' effects.
+-- | Interpret the 'State' effect.
 runState :: forall s ef a. s -> Eff '[] (State s ': ef) a -> Eff '[] ef (s, a)
 runState s0 = interpretStateBy s0 (curry pure) handleState
 
+-- | Interpret the 'State' effect. Do not include the final state in the return value.
 evalState :: forall s ef a. s -> Eff '[] (State s ': ef) a -> Eff '[] ef a
 evalState s0 = interpretStateBy s0 (const pure) handleState
 
+-- | Interpret the 'State' effect. Do not include the final result in the return value.
 execState :: forall s ef a. s -> Eff '[] (State s ': ef) a -> Eff '[] ef s
 execState s0 = interpretStateBy s0 (\s _ -> pure s) handleState
 
+{- |
+Interpret the 'State' effect.
+
+Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.
+Note that the state is reset and does not persist beyond the scopes.
+-}
 evalStateRec :: forall s ef eh. s -> Eff eh (State s ': ef) ~> Eff eh ef
 evalStateRec s0 = interpretStateRecWith s0 handleState
 
+-- | A handler function for the 'State' effect.
 handleState :: StateInterpreter s (State s) (Eff eh r) ans
 handleState = \case
     Put s -> \_ k -> k s ()
     Get -> \s k -> k s s
 {-# INLINE handleState #-}
 
+-- | Interpret the 'State' effect based on an IO-fused semantics using t'Data.IORef.IORef'.
 runStateIORef
     :: forall s ef eh a
      . (IO <| ef)
@@ -71,6 +80,10 @@ runStateIORef s0 m = do
             Put s -> writeIORef ref s
     readIORef ref <&> (,a)
 
+{- |
+Interpret the 'State' effect based on an IO-fused semantics using t'Data.IORef.IORef'.
+Do not include the final state in the return value.
+-}
 evalStateIORef
     :: forall s ef eh a
      . (IO <| ef)
@@ -83,6 +96,7 @@ evalStateIORef s0 m = do
         Get -> readIORef ref
         Put s -> writeIORef ref s
 
+-- | Within the given scope, make the state roll back to the beginning of the scope in case of exceptions, etc.
 transactState :: forall s ef. (State s <| ef) => Eff '[] ef ~> Eff '[] ef
 transactState m = do
     pre <- get @s
diff --git a/heftia-effects/src/Control/Monad/Hefty/Unlift.hs b/heftia-effects/src/Control/Monad/Hefty/Unlift.hs
index c86dd35..31637ac 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Unlift.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Unlift.hs
@@ -1,12 +1,11 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2024 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
+
+Interpreters for the [Unlift]("Data.Effect.Unlift") effects.
 -}
 module Control.Monad.Hefty.Unlift (
     module Control.Monad.Hefty.Unlift,
diff --git a/heftia-effects/src/Control/Monad/Hefty/Writer.hs b/heftia-effects/src/Control/Monad/Hefty/Writer.hs
index 65b123c..a5b13e8 100644
--- a/heftia-effects/src/Control/Monad/Hefty/Writer.hs
+++ b/heftia-effects/src/Control/Monad/Hefty/Writer.hs
@@ -1,17 +1,11 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2023 Sayo Koyoneda
 License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Portability :  portable
 
-Interpreter and elaborator for the t'Data.Effect.Writer.Writer' effect class.
-See [README.md](https://github.com/sayo-hs/heftia/blob/master/README.md).
+Interpreters for the [Writer]("Data.Effect.Writer") effects.
 -}
 module Control.Monad.Hefty.Writer (
     module Control.Monad.Hefty.Writer,
@@ -32,26 +26,30 @@ import Control.Monad.Hefty (
  )
 import Data.Effect.Writer
 
--- | 'Writer' effect handler with post-applying censor semantics.
+-- | Interpret the [Writer]("Data.Effect.Writer") effects with post-applying censor semantics.
 runWriterPost :: (Monoid w) => Eff '[WriterH w] (Tell w ': ef) a -> Eff '[] ef (w, a)
 runWriterPost = runTell . runWriterHPost
 
--- | 'Writer' effect handler with pre-applying censor semantics.
+-- | Interpret the [Writer]("Data.Effect.Writer") effects with pre-applying censor semantics.
 runWriterPre :: (Monoid w) => Eff '[WriterH w] (Tell w ': ef) a -> Eff '[] ef (w, a)
 runWriterPre = runTell . runWriterHPre
 
+-- | Interpret the t'Tell' effect.
 runTell :: (Monoid w) => Eff '[] (Tell w ': ef) a -> Eff '[] ef (w, a)
 runTell = interpretStateBy mempty (curry pure) handleTell
 
+-- | A handler function for the 'Tell' effect.
 handleTell :: (Monoid w) => StateInterpreter w (Tell w) (Eff '[] ef) (w, a)
 handleTell (Tell w') w k = k (w <> w') ()
 {-# INLINE handleTell #-}
 
+-- | Interpret the 'WriterH' effect with post-applying censor semantics.
 runWriterHPost :: (Monoid w, Tell w <| ef) => Eff '[WriterH w] ef ~> Eff '[] ef
 runWriterHPost = interpretH \case
     Listen m -> intercept m
     Censor f m -> censorPost f m
 
+-- | Interpret the 'WriterH' effect with pre-applying censor semantics.
 runWriterHPre :: (Monoid w, Tell w <| ef) => Eff '[WriterH w] ef ~> Eff '[] ef
 runWriterHPre = interpretH \case
     Listen m -> intercept m
@@ -83,6 +81,7 @@ confiscate
     -> Eff '[] ef (w, a)
 confiscate = interposeStateBy mempty (curry pure) handleTell
 
+-- | 'censor' with post-applying semantics.
 censorPost
     :: forall w ef
      . (Tell w <| ef, Monoid w)
@@ -93,6 +92,7 @@ censorPost f m = do
     tell $ f w
     pure a
 
+-- | 'censor' with pre-applying semantics.
 censorPre
     :: forall w eh ef
      . (Tell w <| ef, Monoid w)