diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -3,3 +3,8 @@
 ## 0.1.0.0 -- 2023-09-18
 
 * Initial public release.
+
+## 0.2.0.0 -- 2024-07-17
+
+* Redesign from scratch.
+* Released as a beta version.
diff --git a/Example/Continuation/Main.hs b/Example/Continuation/Main.hs
--- a/Example/Continuation/Main.hs
+++ b/Example/Continuation/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 -- This Source Code Form is subject to the terms of the Mozilla Public
@@ -6,62 +7,64 @@
 
 module Main where
 
-import Control.Effect.Class (sendIns, type (~>))
-import Control.Effect.Class.Machinery.TH (makeEffectF, makeEffectH)
-import Control.Effect.Freer (Fre, interposeK, interpret, runFreerEffects, type (<|))
-import Control.Effect.Heftia (Elaborator, runElaborate)
-import Control.Monad.Trans.Heftia.Church (HeftiaChurchT)
+import Control.Effect (type (~>))
+import Control.Effect.ExtensibleChurch (runEff, type (:!!))
+import Control.Effect.Hefty (interposeK, interpretRec, interpretRecH)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.TH (makeEffectF, makeEffectH)
 import Data.Function ((&))
-import Data.Hefty.Extensible (ExtensibleUnionH)
-import Data.Hefty.Union (UnionH (absurdUnionH, (|+:)))
+import Data.Hefty.Extensible (ForallHFunctor, type (<|))
 
 type ForkID = Int
 
-class Fork f where
-    fork :: f ForkID
-
-makeEffectF ''Fork
-
-runForkSingle :: Monad m => Fre (ForkI ': r) m ~> Fre r m
-runForkSingle = interpret \Fork -> pure 0
+data Fork a where
+    Fork :: Fork ForkID
+makeEffectF [''Fork]
 
-class DelimitFork f where
-    delimitFork :: Monoid w => f w -> f w
+runForkSingle :: ForallHFunctor eh => eh :!! LFork ': r ~> eh :!! r
+runForkSingle = interpretRec \Fork -> pure 0
 
-makeEffectH ''DelimitFork
+data ResetFork f a where
+    ResetFork :: Monoid w => f w -> ResetFork f w
+makeEffectH [''ResetFork]
 
-applyDelimitFork :: (ForkI <| es, Monad m) => Int -> Elaborator DelimitForkS (Fre es m)
-applyDelimitFork numberOfFork (DelimitFork m) =
+applyResetFork :: Fork <| r => Int -> ResetFork ('[] :!! r) ~> '[] :!! r
+applyResetFork numberOfFork (ResetFork m) =
     m & interposeK pure \k Fork -> do
         r <- mapM k [1 .. numberOfFork]
         pure $ mconcat r
 
-{-
--- In the `mconcat` section, we utilize the fact that `w` in `delimitFork` is a `Monoid`.
--- However, `hoistHeftiaEffects` quantifies `w` into any type, so we can't make use of
--- it being a `Monoid`. Thus, writing it this way results in a type error.
-
-runDelimitFork ::
-    (ForkI <| es, ForallHFunctor r, Monad m) =>
-    Int ->
-    Hef (DelimitForkS ': r) (Fre es m) ~> Hef r (Fre es m)
-runDelimitFork numberOfFork =
-    interpretH \(DelimitFork m) ->
-        ($ m) $ hoistHeftiaEffects $ interposeK pure \k Fork -> do
-            r <- mapM k [1 .. numberOfFork]
-            pure $ mconcat r -- Here's where the type error occurs
--}
-
 main :: IO ()
 main =
-    runFreerEffects
+    runEff
         . runForkSingle
-        . runElaborate @_ @HeftiaChurchT @ExtensibleUnionH (applyDelimitFork 4 |+: absurdUnionH)
+        . interpretRecH (applyResetFork 4)
         $ do
-            sendIns . putStrLn . (("[out of scope] " ++) . show) =<< fork
-            s <- delimitFork do
+            liftIO . putStrLn . (("[out of scope] " ++) . show) =<< fork
+            s <- resetFork do
                 fid1 <- fork
                 fid2 <- fork
-                sendIns $ putStrLn $ "[delimited continuation of `fork`] Fork ID: " ++ show (fid1, fid2)
+                liftIO $ putStrLn $ "[delimited continuation of `fork`] Fork ID: " ++ show (fid1, fid2)
                 pure $ show (fid1, fid2)
-            sendIns $ putStrLn $ "scope exited. result: " ++ s
+            liftIO $ putStrLn $ "scope exited. result: " ++ s
+
+{-
+[out of scope] 0
+[delimited continuation of `fork`] Fork ID: (1,1)
+[delimited continuation of `fork`] Fork ID: (1,2)
+[delimited continuation of `fork`] Fork ID: (1,3)
+[delimited continuation of `fork`] Fork ID: (1,4)
+[delimited continuation of `fork`] Fork ID: (2,1)
+[delimited continuation of `fork`] Fork ID: (2,2)
+[delimited continuation of `fork`] Fork ID: (2,3)
+[delimited continuation of `fork`] Fork ID: (2,4)
+[delimited continuation of `fork`] Fork ID: (3,1)
+[delimited continuation of `fork`] Fork ID: (3,2)
+[delimited continuation of `fork`] Fork ID: (3,3)
+[delimited continuation of `fork`] Fork ID: (3,4)
+[delimited continuation of `fork`] Fork ID: (4,1)
+[delimited continuation of `fork`] Fork ID: (4,2)
+[delimited continuation of `fork`] Fork ID: (4,3)
+[delimited continuation of `fork`] Fork ID: (4,4)
+scope exited. result: (1,1)(1,2)(1,3)(1,4)(2,1)(2,2)(2,3)(2,4)(3,1)(3,2)(3,3)(3,4)(4,1)(4,2)(4,3)(4,4)
+-}
diff --git a/Example/Continuation2/Main.hs b/Example/Continuation2/Main.hs
new file mode 100644
--- /dev/null
+++ b/Example/Continuation2/Main.hs
@@ -0,0 +1,105 @@
+-- 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/.
+
+module Main where
+
+import Control.Arrow ((>>>))
+import Control.Effect.ExtensibleChurch (runEff, type (!!))
+import Control.Effect.Handler.Heftia.Reader (runAsk, runLocal)
+import Control.Effect.Handler.Heftia.ShiftReset (evalShift, runShift_)
+import Control.Effect.Handler.Heftia.State (evalState)
+import Control.Effect.Hefty (send1, unkeyEff, type ($))
+import Control.Effect.Key (key)
+import Control.Monad.Extra (whenM)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.HFunctor ((:+:))
+import Data.Effect.Key (type (#>))
+import Data.Effect.Reader (Ask, Local, ask, local)
+import Data.Effect.ShiftReset (Shift, Shift_, getCC, getCC_)
+import Data.Effect.State (State, get'', modify)
+import Data.Free.Sum (type (+))
+import Data.Function ((&))
+import Data.Functor ((<&>))
+
+main :: IO ()
+main = do
+    putStrLn "[handleReaderThenShift]"
+    handleReaderThenShift
+
+    putStrLn ""
+    putStrLn "[handleShiftThenReader]"
+    handleShiftThenReader
+
+{-
+===== result =====
+
+[handleReaderThenShift]
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 1
+
+[handleShiftThenReader]
+[local scope outer] env = 1
+[local scope inner] env = 2
+[local scope outer] env = 2
+[local scope inner] env = 4
+[local scope outer] env = 4
+[local scope inner] env = 8
+[local scope outer] env = 8
+[local scope inner] env = 16
+[local scope outer] env = 16
+[local scope inner] env = 32
+[local scope outer] env = 32
+-}
+
+handleReaderThenShift :: IO ()
+handleReaderThenShift =
+    prog
+        & runLocal
+        & runAsk 1
+        & runEff
+        & evalShift
+        & (unkeyEff >>> evalState 0)
+        & runEff
+  where
+    prog :: Local Int !! Ask Int + Shift () !! "counter" #> State Int + IO $ ()
+    prog = do
+        k <- send1 getCC
+        env <- ask @Int
+        send1 $ liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
+        local @Int (* 2) do
+            whenM (send1 (get'' @"counter") <&> (< 5)) do
+                send1 $ modify (+ 1) & key @"counter"
+                env' <- ask @Int
+                send1 $ liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
+                send1 k
+
+handleShiftThenReader :: IO ()
+handleShiftThenReader = do
+    prog
+        & runShift_
+        & runLocal
+        & runAsk 1
+        & (unkeyEff >>> evalState 0)
+        & runEff
+  where
+    prog :: Shift_ :+: Local Int !! Ask Int + "counter" #> State Int + IO $ ()
+    prog = do
+        k <- getCC_
+        env <- ask @Int
+        liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
+        local @Int (* 2) do
+            whenM (get'' @"counter" <&> (< 5)) do
+                modify (+ 1) & key @"counter"
+                env' <- ask @Int
+                liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
+                k
diff --git a/Example/KeyedEffects/Main.hs b/Example/KeyedEffects/Main.hs
new file mode 100644
--- /dev/null
+++ b/Example/KeyedEffects/Main.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+-- 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/.
+
+module Main where
+
+import Control.Effect (type (~>))
+import Control.Effect.ExtensibleChurch (runEff, type (:!!))
+import Control.Effect.Hefty (interposeRec, interpretRec, unkeyEff)
+import Control.Effect.Key (SendInsBy)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.Key (unKey, type (#>))
+import Data.Effect.TH (makeEffectF)
+import Data.Hefty.Extensible (ForallHFunctor, MemberBy, type (<|))
+
+data Teletype a where
+    ReadTTY :: Teletype String
+    WriteTTY :: String -> Teletype ()
+
+makeEffectF [''Teletype]
+
+teletypeToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LTeletype ': r ~> eh :!! r
+teletypeToIO = interpretRec \case
+    ReadTTY -> liftIO getLine
+    WriteTTY msg -> liftIO $ putStrLn msg
+
+echo :: (SendInsBy "tty1" Teletype m, Monad m) => m ()
+echo = do
+    i <- readTTY'' @"tty1"
+    case i of
+        "" -> pure ()
+        _ -> writeTTY'' @"tty1" i >> echo
+
+strong :: (MemberBy "tty1" Teletype ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
+strong =
+    interposeRec @("tty1" #> _) \e -> case unKey e of
+        ReadTTY -> readTTY'' @"tty1"
+        WriteTTY msg -> writeTTY'' @"tty1" $ msg <> "!"
+
+main :: IO ()
+main = runEff do
+    liftIO $ putStrLn "Please enter something..."
+    teletypeToIO . unkeyEff @"tty1" . strong . strong $ echo
diff --git a/Example/Logging/Main.hs b/Example/Logging/Main.hs
--- a/Example/Logging/Main.hs
+++ b/Example/Logging/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 
@@ -7,189 +8,171 @@
 
 module Main where
 
-import Control.Effect.Class (SendIns (sendIns), type (<:), type (~>))
-import Control.Effect.Class.Machinery.TH (makeEffectF, makeEffectH)
-import Control.Effect.Class.Reader (Ask (ask), AskI, Local (local), LocalS)
-import Control.Effect.Class.State (State (get), StateI, modify)
-import Control.Effect.Freer (
-    Fre,
-    flipFreer,
-    interpose,
-    interpret,
-    interpreted,
-    liftLower,
-    raise,
-    raise2,
-    runFreerEffects,
-    subsume,
-    type (<|),
- )
-import Control.Effect.Handler.Heftia.Reader (interpretReader, liftReader)
+import Control.Arrow ((>>>))
+import Control.Effect (type (<:), type (<<:), type (~>))
+import Control.Effect.ExtensibleChurch (runEff, type (:!!))
+import Control.Effect.Handler.Heftia.Reader (runReader)
 import Control.Effect.Handler.Heftia.State (evalState)
-import Control.Effect.Heftia (
-    ForallHFunctor,
-    Hef,
-    elaborated,
-    flipHeftia,
-    hoistHeftiaEffects,
-    hoistInterpose,
-    interpretH,
-    liftLowerH,
-    runElaborate,
-    type (<<|),
- )
+import Control.Effect.Hefty (interposeRec, interposeRecH, interpretRec, interpretRecH, raise, raiseH)
 import Control.Monad (when)
-import Control.Monad.Trans.Heftia.Church (HeftiaChurchT)
+import Control.Monad.IO.Class (MonadIO, liftIO)
+import Data.Effect.Reader (ask, local)
+import Data.Effect.State (get, modify)
+import Data.Effect.TH (makeEffectF, makeEffectH)
 import Data.Function ((&))
-import Data.Hefty.Extensible (ExtensibleUnionH)
-import Data.Hefty.Union (absurdUnionH, (|+:))
+import Data.Hefty.Extensible (ForallHFunctor, type (<<|), type (<|))
+import Data.Kind (Type)
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
 import Data.Time (UTCTime, getCurrentTime)
 import Data.Time.Format.ISO8601 (iso8601Show)
-import Prelude hiding (log)
 
-class Log f where
-    log :: Text -> f ()
+data Log a where
+    Logging :: Text -> Log ()
 
-makeEffectF ''Log
+makeEffectF [''Log]
 
-logToIO :: (IO <: Fre r m, Monad m) => Fre (LogI ': r) m ~> Fre r m
-logToIO = interpret \(Log msg) -> sendIns $ T.putStrLn msg
+logToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LLog ': r ~> eh :!! r
+logToIO = interpretRec \(Logging msg) -> liftIO $ T.putStrLn msg
 
-class Time f where
-    currentTime :: f UTCTime
+data Time a where
+    CurrentTime :: Time UTCTime
 
-makeEffectF ''Time
+makeEffectF [''Time]
 
-timeToIO :: (IO <: Fre r m, Monad m) => Fre (TimeI ': r) m ~> Fre r m
-timeToIO = interpret \case
-    CurrentTime -> sendIns getCurrentTime
+timeToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LTime ': r ~> eh :!! r
+timeToIO = interpretRec \CurrentTime -> liftIO getCurrentTime
 
-logWithTime :: (LogI <| es, Time (Fre es m), Monad m) => Fre es m ~> Fre es m
-logWithTime = interpose \(Log msg) -> do
+logWithTime :: (Log <| ef, Time <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
+logWithTime = interposeRec \(Logging msg) -> do
     t <- currentTime
-    log $ "[" <> T.pack (show t) <> "] " <> msg
+    logging $ "[" <> T.pack (show t) <> "] " <> msg
 
 -- | An effect that introduces a scope that represents a chunk of logs.
-class LogChunk f where
-    logChunk :: f a -> f a
+data LogChunk f (a :: Type) where
+    LogChunk ::
+        -- | chunk name
+        Text ->
+        f a ->
+        LogChunk f a
 
-makeEffectH ''LogChunk
+makeEffectH [''LogChunk]
 
--- | Output logs in log chunks as they are.
-passthroughLogChunk ::
-    (Monad m, ForallHFunctor r) =>
-    Hef (LogChunkS ': r) m ~> Hef r m
-passthroughLogChunk = interpretH \(LogChunk m) -> m
+-- | Ignore chunk names and output logs in log chunks as they are.
+runLogChunk :: ForallHFunctor eh => LogChunk ': eh :!! ef ~> eh :!! ef
+runLogChunk = interpretRecH \(LogChunk _ m) -> m
 
 -- | Limit the number of logs in a log chunk to the first @n@ logs.
 limitLogChunk ::
-    forall m.
-    (LogChunk m, Log m, Monad m) =>
+    forall eh ef.
+    (LogChunk <<| eh, Log <| ef) =>
     Int ->
-    LogChunkS (Fre '[LogI] m) ~> m
-limitLogChunk n (LogChunk a) =
-    logChunk
-        . interpreted
-        . evalState 0
-        . interpretLog
-        . flipFreer
-        . raise
-        $ a
-  where
-    interpretLog :: Fre '[LogI, StateI Int] m ~> Fre '[StateI Int] m
-    interpretLog =
-        interpret \(Log msg) -> do
+    LogChunk ('[] :!! ef) ~> LogChunk ('[] :!! ef)
+limitLogChunk n (LogChunk chunkName a) =
+    LogChunk chunkName . evalState @Int 0 $
+        raise a & interposeRec \(Logging msg) -> do
             count <- get
             when (count <= n) do
-                liftLower $
-                    if count == n
-                        then log "LOG OMITTED..."
-                        else log msg
+                if count == n
+                    then logging "LOG OMITTED..."
+                    else logging msg
 
                 modify @Int (+ 1)
 
-class FileSystem f where
-    mkdir :: FilePath -> f ()
-    writeFS :: FilePath -> String -> f ()
+data FileSystem a where
+    Mkdir :: FilePath -> FileSystem ()
+    WriteToFile :: FilePath -> String -> FileSystem ()
 
-makeEffectF ''FileSystem
+makeEffectF [''FileSystem]
 
-runDummyFS :: (IO <: Fre r m, Monad m) => Fre (FileSystemI ': r) m ~> Fre r m
-runDummyFS = interpret \case
-    Mkdir path -> sendIns $ putStrLn $ "<runDummyFS> mkdir " <> path
-    WriteFS path content -> sendIns $ putStrLn $ "<runDummyFS> writeFS " <> path <> " : " <> content
+runDummyFS :: (IO <| r, ForallHFunctor eh) => eh :!! LFileSystem ': r ~> eh :!! r
+runDummyFS = interpretRec \case
+    Mkdir path ->
+        liftIO $ putStrLn $ "<runDummyFS> mkdir " <> path
+    WriteToFile path content ->
+        liftIO $ putStrLn $ "<runDummyFS> writeToFile " <> path <> " : " <> content
 
 -- | Create directories according to the log-chunk structure and save one log in one file.
 saveLogChunk ::
-    forall es es' m.
-    ( LogChunkS <<| es
-    , LogI <| es'
-    , FileSystem (Fre es' m)
-    , Time (Fre es' m)
-    , Monad m
-    , ForallHFunctor es
-    ) =>
-    Hef (LogChunkS ': es) (Fre (LogI ': es') m) ~> Hef es (Fre (LogI ': es') m)
+    forall eh ef.
+    (LogChunk <<| eh, Log <| ef, FileSystem <| ef, Time <| ef, ForallHFunctor eh) =>
+    eh :!! ef ~> eh :!! ef
 saveLogChunk =
-    interpretReader ("./log_chunks/" :: FilePath)
-        . hoistHeftiaEffects flipFreer
-        . interpretLogChunk
-        . hoistHeftiaEffects flipFreer
-        . flipHeftia
-        . liftReader
-  where
-    interpretLogChunk ::
-        Hef (LogChunkS ': LocalS FilePath ': es) (Fre (LogI ': AskI FilePath ': es') m)
-            ~> Hef (LocalS FilePath ': es) (Fre (LogI ': AskI FilePath ': es') m)
-    interpretLogChunk =
-        interpretH \(LogChunk a) -> logChunk do
-            chunkBeginAt <- currentTime & raise2 & liftLowerH
-            local @FilePath (++ iso8601Show chunkBeginAt ++ "/") do
-                newLogChunkDir <- ask & liftLowerH
-                mkdir newLogChunkDir & raise2 & liftLowerH
-                a & hoistInterpose \(Log msg) -> do
-                    logAt <- currentTime & raise2
-                    saveDir <- ask
-                    log msg & raise2
-                    writeFS (saveDir ++ iso8601Show logAt ++ ".log") (show msg) & raise2
+    raise >>> raiseH
+        >>> ( interposeRecH \(LogChunk chunkName a) -> do
+                chunkBeginAt <- currentTime
+                let dirName = iso8601Show chunkBeginAt ++ "-" ++ T.unpack chunkName
+                local @FilePath (++ dirName ++ "/") do
+                    logChunkPath <- ask
+                    mkdir logChunkPath
+                    a & interposeRec \(Logging msg) -> do
+                        logAt <- currentTime
+                        logging msg
+                        writeToFile (logChunkPath ++ iso8601Show logAt ++ ".log") (show msg)
+            )
+        >>> runReader @FilePath "./log/"
 
-logs :: (LogChunk m, Log m, IO <: m, Monad m) => m ()
-logs =
-    logChunk do
-        log "foo"
-        log "bar"
-        log "baz"
-        log "qux"
+logExample :: (LogChunk <<: m, Log <: m, MonadIO m) => m ()
+logExample =
+    logChunk "scope1" do
+        logging "foo"
+        logging "bar"
+        logging "baz"
+        logging "qux"
 
-        sendIns $ putStrLn "------"
+        liftIO $ putStrLn "------"
 
-        logChunk do
-            log "hoge"
-            log "piyo"
-            log "fuga"
-            log "hogera"
+        logChunk "scope2" do
+            logging "hoge"
+            logging "piyo"
+            logging "fuga"
+            logging "hogera"
 
-        sendIns $ putStrLn "------"
+        liftIO $ putStrLn "------"
 
-        log "quux"
-        log "foobar"
+        logging "quux"
+        logging "foobar"
 
 main :: IO ()
 main =
-    runFreerEffects
+    runEff
         . logToIO
         . timeToIO
         . logWithTime
         . runDummyFS
-        . subsume
-        . elaborated
-        . passthroughLogChunk
+        . runLogChunk
         . saveLogChunk
-        . interpreted
-        . subsume
-        . runElaborate @_ @HeftiaChurchT @ExtensibleUnionH
-            (liftLower . limitLogChunk 2 |+: absurdUnionH)
-        $ logs
+        $ do
+            logExample
+
+{-
+<runDummyFS> mkdir ./log/2024-07-06T13:56:23.447829919Z-scope1/
+[2024-07-06 13:56:23.448628515 UTC] foo
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.448625419Z.log : "foo"
+[2024-07-06 13:56:23.448932798 UTC] bar
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.448930113Z.log : "bar"
+[2024-07-06 13:56:23.448989065 UTC] baz
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.448986289Z.log : "baz"
+[2024-07-06 13:56:23.449036674 UTC] qux
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449035743Z.log : "qux"
+------
+<runDummyFS> mkdir ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449090566Z-scope2/
+[2024-07-06 13:56:23.44913009 UTC] hoge
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449127986Z.log : "hoge"
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449090566Z-scope2/2024-07-06T13:56:23.449125371Z.log : "hoge"
+[2024-07-06 13:56:23.449215892 UTC] piyo
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449213508Z.log : "piyo"
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449090566Z-scope2/2024-07-06T13:56:23.449210612Z.log : "piyo"
+[2024-07-06 13:56:23.449303087 UTC] fuga
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449300221Z.log : "fuga"
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449090566Z-scope2/2024-07-06T13:56:23.449298909Z.log : "fuga"
+[2024-07-06 13:56:23.449383799 UTC] hogera
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449380502Z.log : "hogera"
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449090566Z-scope2/2024-07-06T13:56:23.44937926Z.log : "hogera"
+------
+[2024-07-06 13:56:23.449513012 UTC] quux
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449510688Z.log : "quux"
+[2024-07-06 13:56:23.449560241 UTC] foobar
+<runDummyFS> writeToFile ./log/2024-07-06T13:56:23.447829919Z-scope1/2024-07-06T13:56:23.449558087Z.log : "foobar"
+-}
diff --git a/Example/SemanticsZoo/Main.hs b/Example/SemanticsZoo/Main.hs
new file mode 100644
--- /dev/null
+++ b/Example/SemanticsZoo/Main.hs
@@ -0,0 +1,112 @@
+-- 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/.
+
+{- |
+[lexi-lambda's semantics-zoo.md](https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md).
+
+It can be confirmed that Heftia also realizes continuation-based semantics equivalent to eff.
+-}
+module Main where
+
+import Control.Applicative ((<|>))
+import Control.Effect.ExtensibleChurch ((:!!))
+import Control.Effect.Handler.Heftia.Except (runCatch, runThrow)
+import Control.Effect.Handler.Heftia.NonDet (runChooseH, runNonDet)
+import Control.Effect.Handler.Heftia.State (evalState)
+import Control.Effect.Handler.Heftia.Writer (elaborateWriterPre, runTell)
+import Control.Effect.Hefty (runPure, type ($))
+import Data.Effect.Except (Catch, Throw, catch, throw)
+import Data.Effect.NonDet (ChooseH, Empty)
+import Data.Effect.State (State, get, put)
+import Data.Effect.Writer (Tell, WriterH, listen, tell)
+import Data.Functor (($>))
+import Data.Hefty.Extensible (type (<<|), type (<|))
+import Data.Monoid (Sum (Sum))
+
+statePlusExcept :: IO ()
+statePlusExcept = do
+    let action :: (State Bool <| ef, Throw () <| ef, Catch () <<| eh) => (eh :!! ef) Bool
+        action = do
+            (put True *> throw ()) `catch` \() -> pure ()
+            get
+
+    putStr "( evalState . runThrow . runCatch $ action ) = "
+    print . runPure $ evalState False . runThrow @() . runCatch @() $ action
+    putStr "( runThrow . evalState . runCatch $ action ) = "
+    print . runPure $ runThrow @() . evalState False . runCatch @() $ action
+
+nonDetPlusExcept :: IO ()
+nonDetPlusExcept = do
+    let action1
+            , action2 ::
+                (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh) => eh :!! ef $ Bool
+        action1 = (pure True <|> throw ()) `catch` \() -> pure False
+        action2 = (throw () <|> pure True) `catch` \() -> pure False
+
+        testAllPattern ::
+            ( forall eh ef.
+              (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh) =>
+              (eh :!! ef) Bool
+            ) ->
+            String ->
+            IO ()
+        testAllPattern action name = do
+            putStr $ "( runNonDet . runThrow . runCatch . runChooseH $ " <> name <> " ) = "
+            print . runPure $
+                runNonDet @[] . runThrow @() . runCatch @() . runChooseH $ action
+
+            putStr $ "( runThrow . runNonDet . runCatch . runChooseH $ " <> name <> " ) = "
+            print . runPure $
+                runThrow @() . runNonDet @[] . runCatch @() . runChooseH $ action
+
+    testAllPattern action1 "action1"
+    testAllPattern action2 "action2"
+
+nonDetPlusWriter :: IO ()
+nonDetPlusWriter = do
+    let action ::
+            (Empty <| ef, ChooseH <<| eh, Tell (Sum Int) <| ef, WriterH (Sum Int) <<| eh) =>
+            eh :!! ef $ (Sum Int, Bool)
+        action = listen $ add 1 *> (add 2 $> True <|> add 3 $> False)
+          where
+            add = tell . Sum @Int
+
+    putStr "( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = "
+    print . map (\(Sum m, (Sum n, b)) -> (m, (n, b))) . runPure $
+        runNonDet @[] . runTell @(Sum Int) . elaborateWriterPre @(Sum Int) . runChooseH $ action
+
+    putStr "( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = "
+    print . (\(Sum m, xs) -> (m, map (\(Sum n, b) -> (n, b)) xs)) . runPure $
+        runTell @(Sum Int) . runNonDet @[] . elaborateWriterPre @(Sum Int) . runChooseH $ action
+
+main :: IO ()
+main = do
+    putStrLn "# State + Except"
+    statePlusExcept
+
+    putStrLn "\n# NonDet + Except"
+    nonDetPlusExcept
+
+    putStrLn "\n# NonDet + Writer"
+    nonDetPlusWriter
+
+    putStrLn "\n[Note] All other permutations will cause type errors."
+
+{-
+# State + Except
+( evalState . runThrow . runCatch $ action ) = Right True
+( runThrow . evalState . runCatch $ action ) = Right True
+
+# NonDet + Except
+( runNonDet . runThrow . runCatch . runChooseH $ action1 ) = [Right True,Right False]
+( runThrow . runNonDet . runCatch . runChooseH $ action1 ) = Right [True,False]
+( runNonDet . runThrow . runCatch . runChooseH $ action2 ) = [Right False,Right True]
+( runThrow . runNonDet . runCatch . runChooseH $ action2 ) = Right [False,True]
+
+# NonDet + Writer
+( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = [(3,(3,True)),(4,(4,False))]
+( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = (6,[(3,True),(4,False)])
+
+[Note] All other permutations will cause type errors.
+-}
diff --git a/Example/Teletype/Main.hs b/Example/Teletype/Main.hs
--- a/Example/Teletype/Main.hs
+++ b/Example/Teletype/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 -- This Source Code Form is subject to the terms of the Mozilla Public
@@ -10,38 +11,39 @@
 -}
 module Main where
 
-import Control.Effect.Class (Taggable, getTag, sendIns, tag, type (#), type (<:), type (@#), type (~>))
-import Control.Effect.Class.Machinery.TH (makeEffectF)
-import Control.Effect.Freer (Fre, interpose, interpret, runFreerEffects, untag, type (<|))
-import Data.Function ((&))
-
-class Teletype f where
-    readTTY :: f String
-    writeTTY :: String -> f ()
+import Control.Effect (type (<:), type (~>))
+import Control.Effect.ExtensibleChurch (runEff, type (:!!))
+import Control.Effect.Hefty (interposeRec, interpretRec, untagEff)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.TH (makeEffectF)
+import Data.Effect.Tag (Tag (unTag), type (#))
+import Data.Hefty.Extensible (ForallHFunctor, type (<|))
 
-makeEffectF ''Teletype
+data Teletype a where
+    ReadTTY :: Teletype String
+    WriteTTY :: String -> Teletype ()
 
-teletypeToIO :: (IO <: Fre es m, Monad m) => Fre (TeletypeI ': es) m ~> Fre es m
-teletypeToIO = interpret \case
-    ReadTTY -> sendIns getLine
-    WriteTTY msg -> sendIns $ putStrLn msg
+makeEffectF [''Teletype]
 
-data TTY1
+teletypeToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LTeletype ': r ~> eh :!! r
+teletypeToIO = interpretRec \case
+    ReadTTY -> liftIO getLine
+    WriteTTY msg -> liftIO $ putStrLn msg
 
-echo :: (Teletype (m @# TTY1), Monad m, Taggable m) => m ()
+echo :: (Teletype # "tty1" <: m, Monad m) => m ()
 echo = do
-    i <- readTTY & tag @TTY1
+    i <- readTTY' @"tty1"
     case i of
         "" -> pure ()
-        _ -> (writeTTY i & tag @TTY1) >> echo
+        _ -> writeTTY' @"tty1" i >> echo
 
-strong :: (TeletypeI # TTY1 <| es, Monad m) => Fre es m ~> Fre es m
+strong :: (Teletype # "tty1" <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
 strong =
-    interpose @(_ # TTY1) \e -> case getTag e of
-        ReadTTY -> readTTY & tag @TTY1
-        WriteTTY msg -> writeTTY (msg <> "!") & tag @TTY1
+    interposeRec @(_ # "tty1") \e -> case unTag e of
+        ReadTTY -> readTTY' @"tty1"
+        WriteTTY msg -> writeTTY' @"tty1" $ msg <> "!"
 
 main :: IO ()
-main = runFreerEffects $ do
-    sendIns $ putStrLn "Please enter something..."
-    teletypeToIO . untag @TTY1 . strong . strong $ echo
+main = runEff do
+    liftIO $ putStrLn "Please enter something..."
+    teletypeToIO . untagEff @"tty1" . strong . strong $ echo
diff --git a/Example/Writer/Main.hs b/Example/Writer/Main.hs
--- a/Example/Writer/Main.hs
+++ b/Example/Writer/Main.hs
@@ -4,46 +4,47 @@
 
 module Main where
 
-import Control.Effect.Class (sendIns, type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor)
-import Control.Effect.Class.Writer (Writer, censor, tell)
-import Control.Effect.Freer (runFreerEffects)
-import Control.Effect.Handler.Heftia.Writer (
-    elaborateWriterT,
-    elaborateWriterTransactionalT,
-    interpretTell,
- )
-import Control.Effect.Heftia (Elaborator, Hef, runElaborate)
-import Data.Hefty.Union (absurdUnionH, (|+:))
+import Control.Effect (type (<:), type (<<:))
+import Control.Effect.ExtensibleChurch (runEff)
+import Control.Effect.Handler.Heftia.Writer (elabWriterPost, elabWriterPre, runTell)
+import Control.Effect.Hefty (interpretRecH)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.Writer (Tell, WriterH, censor, tell)
 
-hello :: (Writer String m, Monad m) => m ()
+hello :: (Tell String <: m, Monad m) => m ()
 hello = do
     tell "Hello"
     tell " world!"
 
-censorHello :: (Writer String m, Monad m) => m ()
+censorHello :: (Tell String <: m, WriterH String <<: m, Monad m) => m ()
 censorHello =
     censor
-        (\s -> if s == "Hello" then "Goodbye" else s)
+        ( \s ->
+            if s == "Hello"
+                then "Goodbye"
+                else
+                    if s == "Hello world!"
+                        then "Hello world!!"
+                        else s
+        )
         hello
 
 main :: IO ()
-main = runFreerEffects do
-    (s :: String, _) <-
-        interpretTell
-            . runElaborate' (elaborateWriterT @String)
+main = runEff do
+    (sPre, _) <-
+        runTell
+            . interpretRecH (elabWriterPre @String)
             $ censorHello
 
-    (sTransactional :: String, _) <-
-        interpretTell
-            . runElaborate' (elaborateWriterTransactionalT @String)
+    (sPost, _) <-
+        runTell
+            . interpretRecH (elabWriterPost @String)
             $ censorHello
 
-    sendIns $ putStrLn $ "Normal: " <> s
-    sendIns $ putStrLn $ "Transactional: " <> sTransactional
+    liftIO $ putStrLn $ "Pre-applying: " <> sPre
+    liftIO $ putStrLn $ "Post-applying: " <> sPost
 
-runElaborate' ::
-    (HFunctor e, Monad f) =>
-    Elaborator e f ->
-    Hef '[e] f ~> f
-runElaborate' f = runElaborate $ f |+: absurdUnionH
+{-
+Pre-applying: Goodbye world!
+Post-applying: Hello world!!
+-}
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,13 @@
-# Heftia
-Heftia, a composition of hefty trees and co-Yoneda, is a higher-order effects
-version of Freer.
+# Heftia: higher-order effects done right for Haskell
 
+[![Hackage](https://img.shields.io/hackage/v/heftia.svg?logo=haskell&label=heftia)](https://hackage.haskell.org/package/heftia)
+[![Hackage](https://img.shields.io/hackage/v/heftia-effects.svg?logo=haskell&label=heftia-effects)](https://hackage.haskell.org/package/heftia-effects)
+
+Heftia is a higher-order effects version of Freer.
+
+This library provides "[continuation-based semantics](https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md)" for higher-order effects, the same as [lexi-lambda's eff](https://github.com/lexi-lambda/eff).
+Instead of using the `IO` monad to implement delimited continuations for effects, Heftia internally uses `Freer` monad.
+
 The paper
 * Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular
     Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7,
@@ -11,85 +17,205 @@
 Hefty trees, proposed by the above paper, are extensions of free monads,
 allowing for a straightforward treatment of higher-order effects.
 
-This library offers Heftia monads and Freer monads, encoded into data
+This library offers Hefty monads and Freer monads, encoded into data
 types in several ways to enable tuning in pursuit of high performance.
 
-Additionally, it's designed to operate as a handler system based
-on [`classy-effects`](https://github.com/sayo-hs/classy-effects), which aims to
-standardize and unify the definitions of effects in Haskell.
+## Status
 
+This library is currently in the beta stage.
+There may be significant changes and potential bugs.
+
+**We are looking forward to your feedback!**
+
+## Getting Started
+To run the [SemanticsZoo example](heftia-effects/Example/SemanticsZoo/Main.hs):
+```console
+$ git clone https://github.com/sayo-hs/heftia
+$ cd heftia/heftia-effects
+$ cabal run exe:SemanticsZoo
+...
+# State + Except
+( evalState . runThrow . runCatch $ action ) = Right True
+( runThrow . evalState . runCatch $ action ) = Right True
+
+# NonDet + Except
+( runNonDet . runThrow . runCatch . runChooseH $ action1 ) = [Right True,Right False]
+( runThrow . runNonDet . runCatch . runChooseH $ action1 ) = Right [True,False]
+( runNonDet . runThrow . runCatch . runChooseH $ action2 ) = [Right False,Right True]
+( runThrow . runNonDet . runCatch . runChooseH $ action2 ) = Right [False,True]
+
+# NonDet + Writer
+( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = [(3,(3,True)),(4,(4,False))]
+( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = (6,[(3,True),(4,False)])
+
+[Note] All other permutations will cause type errors.
+$
+```
+
+## Example
+
 Compared to existing Effect System libraries in Haskell that handle higher-order effects, this
 library's approach allows for a more effortless and flexible handling of higher-order effects. Here
 are some examples:
 
-* Two interpretations of the `censor` effect for Writer
+### Extracting Multi-shot Delimited Continuations
 
-    Let's consider the following Writer effectful program:
+In handling higher-order effects, it's easy to work with **multi-shot delimited continuations**.
+This enables an almost complete emulation of "Algebraic Effects and Handlers".
+For more details, please refer to
+the [example code](heftia-effects/Example/Continuation/Main.hs).
 
-    ```hs
-    hello :: (Writer String m, Monad m) => m ()
-    hello = do
-        tell "Hello"
-        tell " world!"
+### Two interpretations of the `censor` effect for Writer
 
-    censorHello :: (Writer String m, Monad m) => m ()
-    censorHello =
-        censor
-            (\s -> if s == "Hello" then "Goodbye" else s)
-            hello
-    ```
+Let's consider the following Writer effectful program:
 
-    For `censorHello`, should the final written string be `"Goodbye world!"`? Or should it be `"Hello world!"`?
-    With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use.
+```hs
+hello :: (Tell String <: m, Monad m) => m ()
+hello = do
+    tell "Hello"
+    tell " world!"
 
-    ```hs
-    main :: IO ()
-    main = runFreerEffects do
-        (s :: String, _) <-
-            interpretTell
-                . runElaborate' (elaborateWriterT @String)
-                $ censorHello
+censorHello :: (Tell String <: m, WriterH String <<: m, Monad m) => m ()
+censorHello =
+    censor
+        ( \s ->
+            if s == "Hello" then
+                "Goodbye"
+            else if s == "Hello world!" then
+                "Hello world!!"
+            else
+                s
+        )
+        hello
+```
 
-        (sTransactional :: String, _) <-
-            interpretTell
-                . runElaborate' (elaborateWriterTransactionalT @String)
-                $ censorHello
+For `censorHello`, should the final written string be `"Goodbye world!"` (Pre-applying behavior) ?
+Or should it be `"Hello world!!"` (Post-applying behavior) ?
+With Heftia, **you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use**.
 
-        sendIns $ putStrLn $ "Normal: " <> s
-        sendIns $ putStrLn $ "Transactional: " <> sTransactional
-    ```
+```hs
+main :: IO ()
+main = runEff do
+    (sPre, _) <-
+        runTell
+            . interpretRecH (elabWriterPre @String)
+            $ censorHello
 
-    Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!".
-    For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
+    (sPost, _) <-
+        runTell
+            . interpretRecH (elabWriterPost @String)
+            $ censorHello
 
-* Extracting Multi-shot Delimited Continuations
+    liftIO $ putStrLn $ "Pre-applying: " <> sPre
+    liftIO $ putStrLn $ "Post-applying: " <> sPost
+```
 
-    In handling higher-order effects, it's easy to work with multi-shot delimited continuations.
-    This enables an almost complete emulation of "Algebraic Effects and Handlers".
-    For more details, please refer to
-    [Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/master/docs/examples/03%20Delimited%20Continuation.md>) .
+Using the `elabWriterPre` elaborator, you'll get "Goodbye world!", whereas with the `elabWriterPost` elaborator, you'll get "Hello world!!".
+```
+Pre-applying: Goodbye world!
+Post-applying: Hello world!!
+```
 
+For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
+
 Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
 eliminated.
 
-Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).
+Additionally, Heftia supports not only monadic effectful programs but also **applicative effectful programs**.
+This may be useful when writing concurrent effectful code.
 
+Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs).
+
 ## Documentation
-Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.
+The example codes are located in the [heftia-effects/Example/](heftia-effects/Example/) directory.
+Also, the following *HeftWorld* example: https://github.com/sayo-hs/HeftWorld
 
+~~Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.~~ Documents have become outdated.
+Please wait for the documentation for the new version to be written.
+
+## Limitation and how to avoid it
+### The *reset* behavior of the scopes held by unhandled higher-order effects
+When attempting to interpret an effect while there are unhandled higher-order effects present, you cannot obtain delimited continuations beyond the action scope held by these unhandled higher-order effects.
+It appears as if a *reset* (in the sense of *shift/reset*) is applied to each of the scopes still held by the remaining unhandled higher-order effects.
+
+In other words, to obtain delimited continuations beyond their scope, it is necessary to first handle and eliminate all higher-order effects that hold those scopes,
+and then handle the effect targeted for stateful interpretation in that order.
+For this purpose, it might sometimes be possible to use *multi-layering*. For an example of multi-layering,
+see `handleReaderThenShift` defined in [Example/Continuation2](https://github.com/sayo-hs/heftia/blob/8f71a2d4e6125018b64cbbacd32151565a29046d/heftia-effects/Example/Continuation2/Main.hs)
+(particularly, the type signature of `prog` within it).
+For more details, please refer to the documentation of the `interpretRec` family of functions.
+
+## Comparison
+
+* Higher-Order Effects: Does it support higher-order effects?
+* Delimited Continuation: The ability to manipulate delimited continuations.
+* Statically Typed Set of Effects: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce?
+* Purely Monadic: Is an effectful program represented as a transparent data structure that is a monad, and can it be interpreted into other data types using only pure operations without side effects or `unsafePerformIO`?
+* Dynamic Effect Rewriting: Can an effectful program have its internal effects altered afterwards (by functions typically referred to as `handle with`, `intercept`, `interpose`, `transform`, `translate`, or `rewrite`) ?
+* Performance: Time complexity or space complexity.
+
+| Library or Language | Higher-Order Effects | Delimited Continuation | Statically Typed Set of Effects                 | Purely Monadic                    | Dynamic Effect Rewriting | Performance (TODO) |
+| ------------------- | -------------------- | ---------------------- | ----------------------------------------------- | --------------------------------- | ------------------------ | ------------------ |
+| Heftia              | Yes [^1]             | Multi-shot             | Yes                                             | Yes (also Applicative and others) | Yes                      | ?                  |
+| freer-simple        | No                   | Multi-shot             | Yes                                             | Yes                               | Yes                      | ?                  |
+| Polysemy            | Yes                  | No                     | Yes                                             | Yes                               | Yes                      | ?                  |
+| Effectful           | Yes                  | No                     | Yes                                             | No (based on the `IO` monad)      | Yes                      | ?                  |
+| eff                 | Yes                  | Multi-shot?            | Yes                                             | No (based on the `IO` monad)      | Yes                      | Fast               |
+| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes                                             | Yes                               | No                       | ?                  |
+| fused-effects       | Yes                  | No?                    | Yes                                             | Yes                               | No                       | ?                  |
+| koka-lang           | No?                  | Multi-shot             | Yes                                             | No (language built-in)            | ?                        | ?                  |
+| OCaml-lang 5        | Yes                  | One-shot               | No [^2]                                         | No (language built-in)            | ?                        | ?                  |
+
+[^1]: limitation: https://github.com/sayo-hs/heftia?tab=readme-ov-file#the-reset-behavior-of-the-scopes-held-by-unhandled-higher-order-effects
+[^2]: potential for 'unhandled' runtime errors
+
+Heftia can simply be described as a higher-order version of freer-simple.
+This is indeed true in terms of its internal mechanisms as well.
+
+### Compatibility with other libraries
+#### Representation of effects
+* Heftia Effects relies on [data-effects](https://github.com/sayo-hs/data-effects) for the definitions of standard effects such as `Reader`, `Writer`, and `State`.
+
+* It is generally recommended to use effects defined with automatic derivation provided by [data-effects-th](https://github.com/sayo-hs/data-effects/tree/develop/data-effects-th).
+
+* The representation of first-order effects is compatible with freer-simple.
+    Therefore, effects defined for freer-simple can be used as is in this library.
+    However, to avoid confusion between redundantly defined effects,
+    it is recommended to use the effects defined in [data-effects](https://github.com/sayo-hs/data-effects).
+
+* GADTs for higher-order effects need to be instances of the [HFunctor](https://hackage.haskell.org/package/compdata-0.13.1/docs/Data-Comp-Multi-HFunctor.html#t:HFunctor) type class for convenient usage.
+    While it is still possible to use them without being instances of `HFunctor`,
+    the `interpretRec` family of functions cannot be used when higher-order effects that are not `HFunctor` are unhandled.
+    If this issue is not a concern, the GADT representation of higher-order effects is compatible with Polysemy and fused-effects.
+    It is not compatible with Effectful and eff.
+
+#### About mtl
+* Since the representation of effectful programs in Heftia is simply a monad (`Eff`), it can be used as the base monad for transformers.
+    This means you can stack any transformer on top of it.
+
+* The `Eff` monad is an instance of `MonadIO`, `MonadError`, `MonadRWS`, etc., and these behave as the senders for the embedded `IO` or the effect GADTs defined in [data-effects](https://github.com/sayo-hs/data-effects).
+
 ## Future Plans
-* Benchmarking
-* Enriching the documentation
+* Enriching the documentation and tests
 * Completing missing definitions such as
-    * the Heftia monad transformer encoded in tree structure
-    * handlers for the `Accum`, `Coroutine`, `Fresh`, `Input`, `Output` effect classes
+    * `raise`, `raiseUnder`, and `subsume` for arbitrary numbers of effects by type classes.
+    * more patterns of interpret & transform function-families.
+    * handlers for the `Accum` and others effect classes
 
     and others.
+* Benchmarking
 
 ## License
-The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/master/NOTICE).
+The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/develop/NOTICE).
 Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed
 under CC BY-SA 4.0.
 
 ## Your contributions are welcome!
-Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/master/CONTRIBUTING.md).
+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md).
+
+## Credits
+Parts of this project have been inspired by the following resources:
+
+* **[Hefty Algebras -- The Artifact](https://github.com/heft-lang/POPL2023)**
+    * **Copyright** (c) 2023 Casper Bach Poulsen and Cas van der Rest
+    * **License**: MIT
diff --git a/heftia-effects.cabal b/heftia-effects.cabal
--- a/heftia-effects.cabal
+++ b/heftia-effects.cabal
@@ -1,17 +1,14 @@
 cabal-version:      2.4
 name:               heftia-effects
-version:            0.1.0.0
+version:            0.2.0.0
 
 -- A short (one-line) description of the package.
-synopsis: Handlers for standard effects using Heftia.
+synopsis: higher-order effects done right
 
 -- A longer description of the package.
 description:
-    This library provides interpreters based
-    on [Heftia](https://hackage.haskell.org/package/heftia) for the standard effect classes
-    compliant with [CEPs](https://github.com/sayo-hs/classy-effects/blob/master/CEPs/README.md),
-    offered by
-    the [classy-effects](https://hackage.haskell.org/package/classy-effects) package.
+    This library is the battery-included version of the [heftia](https://hackage.haskell.org/package/heftia) package,
+    providing interpreters for standard effects.
 
 -- A URL where users can report bugs.
 bug-reports: https://github.com/sayo-hs/heftia
@@ -37,7 +34,7 @@
 source-repository head
     type: git
     location: https://github.com/sayo-hs/heftia
-    tag: v0.1.0
+    tag: v0.2.0
     subdir: heftia-effects
 
 common common-base
@@ -55,6 +52,14 @@
         DefaultSignatures,
         PatternSynonyms
 
+    build-depends:
+        base ^>= 4.16,
+        ghc-typelits-knownnat ^>= 0.7,
+        data-effects ^>= 0.1,
+        heftia ^>= 0.2,
+
+    ghc-options: -Wall -fplugin GHC.TypeLits.KnownNat.Solver
+
 library
     import: common-base
 
@@ -63,20 +68,77 @@
         Control.Effect.Handler.Heftia.Writer
         Control.Effect.Handler.Heftia.State
         Control.Effect.Handler.Heftia.Except
+        Control.Effect.Handler.Heftia.ShiftReset
+        Control.Effect.Handler.Heftia.NonDet
+        Control.Effect.Handler.Heftia.Coroutine
+        Control.Effect.Handler.Heftia.Input
+        Control.Effect.Handler.Heftia.Output
         Control.Effect.Handler.Heftia.Provider
+        Control.Effect.Handler.Heftia.Provider.Implicit
+        Control.Effect.Handler.Heftia.Resource
+        Control.Effect.Handler.Heftia.Unlift
+        Control.Effect.Handler.Heftia.KVStore
+        Control.Effect.Handler.Heftia.Fresh
+        Control.Effect.Handler.Heftia.Fail
 
+    reexported-modules:
+        Control.Effect.Hefty,
+        Control.Effect.Free,
+        Control.Effect.ExtensibleFinal,
+        Control.Effect.ExtensibleChurch,
+        Control.Effect.ExtensibleTree,
+        Control.Effect.ExtensibleFinalA,
+        Control.Effect.ExtensibleTreeA,
+        Control.Effect.ExtensibleFastA,
+        Control.Hefty,
+        Control.Freer,
+        Control.Freer.Final,
+        Control.Monad.Freer,
+        Control.Monad.Freer.Church,
+        Control.Monad.Freer.Tree,
+        Data.Hefty.Union,
+        Data.Hefty.Extensible,
+        Data.Free.Sum,
+        Data.Effect,
+        Data.Effect.TH,
+        Data.Effect.Tag,
+        Data.Effect.Key,
+        Data.Effect.Key.TH,
+        Data.Effect.HFunctor,
+        Data.Effect.HFunctor.HCont,
+        Data.Effect.HFunctor.TH,
+        Control.Effect,
+        Control.Effect.Tag,
+        Control.Effect.Key,
+        Data.Effect.Reader,
+        Data.Effect.Writer,
+        Data.Effect.State,
+        Data.Effect.Except,
+        Data.Effect.ShiftReset,
+        Data.Effect.NonDet,
+        Data.Effect.Coroutine,
+        Data.Effect.Input,
+        Data.Effect.Output,
+        Data.Effect.Provider,
+        Data.Effect.Provider.Implicit,
+        Data.Effect.Resource,
+        Data.Effect.Unlift,
+        Data.Effect.KVStore,
+        Data.Effect.Fresh,
+        Data.Effect.Fail,
+
     -- Modules included in this executable, other than Main.
     -- other-modules:
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:
     build-depends:
-        base                          ^>= 4.16.4.0,
-        heftia                        ^>= 0.1,
-        classy-effects                ^>= 0.1,
         mtl                           ^>= 2.2.2,
         transformers                  ^>= 0.5.6,
         extensible                    ^>= 0.9,
+        unliftio                      ^>= 0.2.0,
+        free                          ^>= 5.2,
+        containers                    ^>= 0.6.5,
 
     hs-source-dirs:   src
 
@@ -87,9 +149,6 @@
     hs-source-dirs: test
     build-depends:
         heftia-effects,
-        classy-effects,
-        heftia,
-        base,
         tasty                         ^>= 1.4,
         tasty-hunit                   ^>= 0.10,
 
@@ -105,27 +164,27 @@
     main-is: Main.hs
     hs-source-dirs: Example/Teletype
     build-depends:
-        classy-effects,
-        heftia,
         heftia-effects,
-        base,
 
+executable KeyedEffects
+    import: common-base
+
+    main-is: Main.hs
+    hs-source-dirs: Example/KeyedEffects
+    build-depends:
+        heftia-effects,
+
 executable Logging
     import: common-base
 
     main-is: Main.hs
     hs-source-dirs: Example/Logging
-    ghc-options: -Wall -fplugin GHC.TypeLits.KnownNat.Solver
     build-depends:
-        classy-effects,
-        heftia,
         heftia-effects,
-        base,
         text ^>= 1.2.5,
         time ^>= 1.11.1,
         loglevel ^>= 0.1.0,
         extra ^>= 1.7.14,
-        ghc-typelits-knownnat ^>= 0.7,
 
 executable Continuation
     import: common-base
@@ -133,18 +192,29 @@
     main-is: Main.hs
     hs-source-dirs: Example/Continuation
     build-depends:
-        classy-effects,
-        heftia,
         heftia-effects,
-        base,
 
+executable Continuation2
+    import: common-base
+
+    main-is: Main.hs
+    hs-source-dirs: Example/Continuation2
+    build-depends:
+        heftia-effects,
+        extra ^>= 1.7.14,
+
 executable Writer
     import: common-base
 
     main-is: Main.hs
     hs-source-dirs: Example/Writer
     build-depends:
-        classy-effects,
-        heftia,
         heftia-effects,
-        base,
+
+executable SemanticsZoo
+    import: common-base
+
+    main-is: Main.hs
+    hs-source-dirs: Example/SemanticsZoo
+    build-depends:
+        heftia-effects,
diff --git a/src/Control/Effect/Handler/Heftia/Coroutine.hs b/src/Control/Effect/Handler/Heftia/Coroutine.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Coroutine.hs
@@ -0,0 +1,17 @@
+-- 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/.
+
+module Control.Effect.Handler.Heftia.Coroutine where
+
+import Control.Effect.Hefty (Eff, interpretK)
+import Control.Monad.Freer (MonadFreer)
+import Data.Effect.Coroutine (LYield, Status (Coroutine, Done), Yield (Yield))
+import Data.Hefty.Union (Union)
+
+runCoroutine ::
+    forall a b r er fr u c.
+    (MonadFreer c fr, Union u, c (Eff u fr '[] er)) =>
+    Eff u fr '[] (LYield a b ': er) r ->
+    Eff u fr '[] er (Status (Eff u fr '[] er) a b r)
+runCoroutine = interpretK (pure . Done) (\kk (Yield a) -> pure $ Coroutine a kk)
diff --git a/src/Control/Effect/Handler/Heftia/Except.hs b/src/Control/Effect/Handler/Heftia/Except.hs
--- a/src/Control/Effect/Handler/Heftia/Except.hs
+++ b/src/Control/Effect/Handler/Heftia/Except.hs
@@ -9,44 +9,106 @@
 Stability   :  experimental
 Portability :  portable
 
-Interpreter and elaborator for the t'Control.Effect.Class.Except.Except' effect class.
+Interpreter and elaborator for the t'Data.Effect.Except.Throw' / t'Data.Effect.Except.Catch' effect
+classes.
 -}
 module Control.Effect.Handler.Heftia.Except where
 
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Except (CatchS (Catch), ThrowI (Throw))
-import Control.Effect.Freer (Fre, interposeK, interposeT, interpretK, interpretT, type (<|))
-import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT, throwE)
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (
+    Eff,
+    Elab,
+    interposeK,
+    interposeT,
+    interpretK,
+    interpretRecH,
+    interpretT,
+ )
+import Control.Monad.Freer (MonadFreer)
+import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
+import Data.Effect.Except (Catch (Catch), LThrow, Throw (Throw))
+import Data.Effect.HFunctor (HFunctor)
 import Data.Function ((&))
+import Data.Hefty.Union (Member, Union)
 
--- | Elaborate the 'Catch' effect using the 'ExceptT' monad transformer.
-elaborateExceptT ::
-    (ThrowI e <| es, Monad m) =>
-    CatchS e (Fre es m) ~> Fre es m
-elaborateExceptT (Catch action (hdl :: e -> Fre es m a)) = do
-    r <- runExceptT $ action & interposeT \(Throw (e :: e)) -> throwE e
+-- | Interpret the "Data.Effect.Except" effects using the 'ExceptT' monad transformer internally.
+runExcept ::
+    forall e a ef fr u c.
+    ( Member u (Throw e) (LThrow e ': ef)
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] (LThrow e ': ef))
+    , c (ExceptT e (Eff u fr '[] (LThrow e ': ef)))
+    , HFunctor (u '[Catch e])
+    , c (Eff u fr '[] ef)
+    , c (ExceptT e (Eff u fr '[] ef))
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[Catch e] (LThrow e ': ef) a ->
+    Eff u fr '[] ef (Either e a)
+runExcept = runCatch >>> runThrow
+{-# INLINE runExcept #-}
+
+-- | Elaborate the t'Catch' effect using the 'ExceptT' monad transformer internally.
+runCatch ::
+    forall e ef fr u c.
+    ( Member u (Throw e) ef
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    , c (ExceptT e (Eff u fr '[] ef))
+    , HFunctor (u '[Catch e])
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[Catch e] ef ~> Eff u fr '[] ef
+runCatch = interpretRecH elabCatch
+{-# INLINE runCatch #-}
+
+elabCatch ::
+    forall e ef fr u c.
+    ( Member u (Throw e) ef
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    , c (ExceptT e (Eff u fr '[] ef))
+    ) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elabCatch (Catch action hdl) = do
+    r <- runExceptT $ action & interposeT \(Throw e) -> throwE e
     case r of
         Left e -> hdl e
         Right a -> pure a
 
-{- |
-Elaborate the 'Catch' effect using the t'Control.Monad.Trans.Cont.ContT' continuation monad
-transformer.
--}
-elaborateExceptK ::
-    (ThrowI e <| es, Monad m) =>
-    CatchS e (Fre es m) ~> Fre es m
-elaborateExceptK (Catch action (hdl :: e -> Fre es m a)) =
-    action & interposeK pure \_ (Throw (e :: e)) -> hdl e
+-- | Elaborate the 'Catch' effect using a delimited continuation.
+elabCatchK ::
+    forall e ef fr u c.
+    (Member u (Throw e) ef, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elabCatchK (Catch action hdl) =
+    action & interposeK pure \_ (Throw e) -> hdl e
 
 -- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
-interpretThrowT :: Monad m => Fre (ThrowI e ': es) m ~> ExceptT e (Fre es m)
-interpretThrowT = interpretT \(Throw e) -> throwE e
-{-# INLINE interpretThrowT #-}
+runThrow ::
+    forall e r a fr u c.
+    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+runThrow = runExceptT . runThrowT
+{-# INLINE runThrow #-}
 
-{- |
-Interpret the 'Throw' effect using the t'Control.Monad.Trans.Cont.ContT' continuation monad
-transformer.
--}
-interpretThrowK :: Monad m => Fre (ThrowI e ': es) m a -> Fre es m (Either e a)
-interpretThrowK = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
+-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
+runThrowT ::
+    forall e r fr u c.
+    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
+    Eff u fr '[] (LThrow e ': r) ~> ExceptT e (Eff u fr '[] r)
+runThrowT = interpretT \(Throw e) -> throwE e
+{-# INLINE runThrowT #-}
+
+-- | Interpret the 'Throw' effect using a delimited continuation.
+runThrowK ::
+    forall e r a fr u c.
+    (MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+runThrowK = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
diff --git a/src/Control/Effect/Handler/Heftia/Fail.hs b/src/Control/Effect/Handler/Heftia/Fail.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Fail.hs
@@ -0,0 +1,26 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.Fail where
+
+import Control.Effect (sendIns, type (~>))
+import Control.Effect.Hefty (Eff, interpret)
+import Control.Freer (Freer)
+import Data.Effect.Fail (Fail (Fail), LFail)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Hefty.Union (Member, Union)
+
+runFailAsIO ::
+    forall r fr u c.
+    (Freer c fr, Union u, HFunctor (u '[]), Member u IO r) =>
+    Eff u fr '[] (LFail ': r) ~> Eff u fr '[] r
+runFailAsIO = interpret \(Fail s) -> sendIns @IO $ fail s
+{-# INLINE runFailAsIO #-}
diff --git a/src/Control/Effect/Handler/Heftia/Fresh.hs b/src/Control/Effect/Handler/Heftia/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Fresh.hs
@@ -0,0 +1,54 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.Fresh where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.State (runState)
+import Control.Effect.Hefty (Eff, interpret, raiseUnder)
+import Control.Freer (Freer)
+import Control.Monad.State (StateT)
+import Data.Effect.Fresh (Fresh (Fresh), LFresh)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.State (LState, State, get, modify)
+import Data.Hefty.Union (Member, Union)
+import Numeric.Natural (Natural)
+
+runFreshNatural ::
+    ( Freer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Member u (State Natural) (LState Natural ': r)
+    , c (Eff u fr '[] r)
+    , c (StateT Natural (Eff u fr '[] r))
+    , Monad (Eff u fr '[] r)
+    , Monad (Eff u fr '[] (LState Natural ': r))
+    ) =>
+    Eff u fr '[] (LFresh Natural ': r) a ->
+    Eff u fr '[] r (Natural, a)
+runFreshNatural =
+    raiseUnder
+        >>> runFreshNaturalAsState
+        >>> runState 0
+{-# INLINE runFreshNatural #-}
+
+runFreshNaturalAsState ::
+    forall r fr u c.
+    ( Freer c fr
+    , Union u
+    , Member u (State Natural) r
+    , Monad (Eff u fr '[] r)
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[] (LFresh Natural ': r) ~> Eff u fr '[] r
+runFreshNaturalAsState =
+    interpret \Fresh -> get @Natural <* modify @Natural (+ 1)
diff --git a/src/Control/Effect/Handler/Heftia/Input.hs b/src/Control/Effect/Handler/Heftia/Input.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Input.hs
@@ -0,0 +1,62 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.Input where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.State (evalState)
+import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder)
+import Control.Freer (Freer)
+import Control.Monad.State (StateT)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Input (Input (Input), LInput)
+import Data.Effect.State (LState, State, gets, put)
+import Data.Hefty.Union (Member, Union)
+import Data.List (uncons)
+
+runInputEff ::
+    forall i r eh fr u c.
+    (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh)) =>
+    Eff u fr eh r i ->
+    Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
+runInputEff a = interpretRec \Input -> a
+{-# INLINE runInputEff #-}
+
+runInputConst ::
+    forall i r eh fr u c.
+    (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh)) =>
+    i ->
+    Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
+runInputConst i = interpretRec \Input -> pure i
+{-# INLINE runInputConst #-}
+
+runInputList ::
+    forall i r fr u c.
+    ( Freer c fr
+    , Union u
+    , Applicative (Eff u fr '[] r)
+    , Monad (Eff u fr '[] (LState [i] ': r))
+    , c (Eff u fr '[] r)
+    , c (StateT [i] (Eff u fr '[] r))
+    , Member u (State [i]) (LState [i] ': r)
+    , HFunctor (u '[])
+    ) =>
+    [i] ->
+    Eff u fr '[] (LInput (Maybe i) ': r) ~> Eff u fr '[] r
+runInputList is =
+    raiseUnder
+        >>> ( interpret \Input -> do
+                is' <- gets @[i] uncons
+                mapM_ (put . snd) is'
+                pure $ fst <$> is'
+            )
+        >>> evalState is
diff --git a/src/Control/Effect/Handler/Heftia/KVStore.hs b/src/Control/Effect/Handler/Heftia/KVStore.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/KVStore.hs
@@ -0,0 +1,65 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+This module provides handlers for the t`KVStore` effect, comes
+from [@Polysemy.KVStore@](https://hackage.haskell.org/package/polysemy-kvstore-0.1.3.0/docs/Polysemy-KVStore.html)
+in the @polysemy-kvstore@ package.
+-}
+module Control.Effect.Handler.Heftia.KVStore where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.State (runState)
+import Control.Effect.Hefty (Eff, interpret, raiseUnder)
+import Control.Freer (Freer)
+import Control.Monad.State (StateT)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.KVStore (KVStore (LookupKV, UpdateKV), LKVStore)
+import Data.Effect.State (LState, State, get, modify)
+import Data.Functor ((<&>))
+import Data.Hefty.Union (Member, Union)
+import Data.Map (Map)
+import Data.Map qualified as Map
+
+runKVStorePure ::
+    forall k v r a fr u c.
+    ( Ord k
+    , Freer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Member u (State (Map k v)) (LState (Map k v) ': r)
+    , c (Eff u fr '[] r)
+    , c (StateT (Map k v) (Eff u fr '[] r))
+    , Monad (Eff u fr '[] r)
+    , Monad (Eff u fr '[] (LState (Map k v) ': r))
+    ) =>
+    Map k v ->
+    Eff u fr '[] (LKVStore k v ': r) a ->
+    Eff u fr '[] r (Map k v, a)
+runKVStorePure initial =
+    raiseUnder
+        >>> runKVStoreAsState
+        >>> runState initial
+{-# INLINE runKVStorePure #-}
+
+runKVStoreAsState ::
+    forall k v r fr u c.
+    ( Ord k
+    , Freer c fr
+    , Union u
+    , Member u (State (Map k v)) r
+    , Monad (Eff u fr '[] r)
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[] (LKVStore k v ': r) ~> Eff u fr '[] r
+runKVStoreAsState = interpret \case
+    LookupKV k -> get <&> Map.lookup k
+    UpdateKV k v -> modify $ Map.update (const v) k
diff --git a/src/Control/Effect/Handler/Heftia/NonDet.hs b/src/Control/Effect/Handler/Heftia/NonDet.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/NonDet.hs
@@ -0,0 +1,158 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.NonDet where
+
+import Control.Applicative (Alternative ((<|>)), empty, liftA2, (<|>))
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (Eff, injectF, interpretFin, interpretFinH, interpretK, interpretRecH)
+import Control.Freer (Freer)
+import Control.Monad.Freer (MonadFreer)
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
+import Data.Bool (bool)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.NonDet (Choose (Choose), ChooseH (ChooseH), Empty (Empty), LChoose, LEmpty, choose)
+import Data.Functor.Compose (Compose (Compose), getCompose)
+import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Member, Union)
+
+-- | 'NonDet' effects handler for Monad use.
+runNonDet ::
+    forall f ef a fr u c.
+    ( Alternative f
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    , c (Eff u fr '[] (LEmpty : ef))
+    ) =>
+    Eff u fr '[] (LChoose ': LEmpty ': ef) a ->
+    Eff u fr '[] ef (f a)
+runNonDet =
+    runChoose >>> interpretK pure \_ Empty -> pure empty
+{-# INLINE runNonDet #-}
+
+-- | 'NonDet' effects handler for Monad use.
+runNonDetK ::
+    forall r ef a fr u c.
+    ( Monoid r
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    , c (Eff u fr '[] (LEmpty ': ef))
+    , HFunctor (u '[])
+    ) =>
+    (a -> Eff u fr '[] (LEmpty ': ef) r) ->
+    Eff u fr '[] (LChoose ': LEmpty ': ef) a ->
+    Eff u fr '[] ef r
+runNonDetK f =
+    runChooseK f >>> interpretK pure \_ Empty -> pure mempty
+{-# INLINE runNonDetK #-}
+
+-- | 'Choose' effect handler for Monad use.
+runChoose ::
+    forall f ef a fr u c.
+    ( Alternative f
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    ) =>
+    Eff u fr '[] (LChoose ': ef) a ->
+    Eff u fr '[] ef (f a)
+runChoose =
+    interpretK (pure . pure) \k Choose ->
+        liftA2 (<|>) (k False) (k True)
+
+-- | 'Choose' effect handler for Monad use.
+runChooseK ::
+    forall r ef a fr u c.
+    ( Semigroup r
+    , MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] ef)
+    ) =>
+    (a -> Eff u fr '[] ef r) ->
+    Eff u fr '[] (LChoose ': ef) a ->
+    Eff u fr '[] ef r
+runChooseK f =
+    interpretK f \k Choose ->
+        liftA2 (<>) (k False) (k True)
+
+-- | 'Empty' effect handler for Monad use.
+runEmpty ::
+    forall a r fr u c.
+    ( Freer c fr
+    , Union u
+    , Applicative (Eff u fr '[] r)
+    , c (MaybeT (Eff u fr '[] r))
+    ) =>
+    Eff u fr '[] (LEmpty ': r) a ->
+    Eff u fr '[] r (Maybe a)
+runEmpty =
+    runMaybeT . interpretFin
+        (MaybeT . fmap Just . injectF)
+        \Empty -> MaybeT $ pure Nothing
+
+{- | 'ChooseH' effect handler for Monad use.
+
+    Convert a higher-order effect of the form
+
+        @chooseH :: m a -> m a -> m a@
+
+    into a first-order effect of the form:
+
+        @choose :: m Bool@
+-}
+runChooseH ::
+    ( Freer c fr
+    , HFunctorUnion u
+    , Member u Choose ef
+    , ForallHFunctor u eh
+    , Monad (Eff u fr eh ef)
+    ) =>
+    Eff u fr (ChooseH ': eh) ef ~> Eff u fr eh ef
+runChooseH =
+    interpretRecH \(ChooseH a b) -> do
+        world <- choose
+        bool a b world
+
+-- | 'NonDet' effect handler for Applicative use.
+runNonDetA ::
+    forall f ef a fr u c.
+    ( Alternative f
+    , Freer c fr
+    , Union u
+    , Applicative (Eff u fr '[] ef)
+    , c (Compose (Eff u fr '[] ef) f)
+    ) =>
+    Eff u fr '[ChooseH] (LEmpty ': ef) a ->
+    Eff u fr '[] ef (f a)
+runNonDetA =
+    getCompose
+        . interpretFinH
+            (Compose . runEmptyA . injectF)
+            (\(ChooseH a b) -> Compose $ liftA2 (<|>) (runNonDetA a) (runNonDetA b))
+
+-- | 'Empty' effect handler for Applicative use.
+runEmptyA ::
+    forall f a r fr u c.
+    ( Alternative f
+    , Freer c fr
+    , Union u
+    , Applicative (Eff u fr '[] r)
+    , c (Compose (Eff u fr '[] r) f)
+    ) =>
+    Eff u fr '[] (LEmpty ': r) a ->
+    Eff u fr '[] r (f a)
+runEmptyA =
+    getCompose
+        . interpretFin
+            (Compose . fmap pure . injectF)
+            \Empty -> Compose $ pure empty
diff --git a/src/Control/Effect/Handler/Heftia/Output.hs b/src/Control/Effect/Handler/Heftia/Output.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Output.hs
@@ -0,0 +1,98 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.Output where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.State (runState)
+import Control.Effect.Handler.Heftia.Writer (runTell, runTellA)
+import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder, send0)
+import Control.Freer (Freer)
+import Control.Monad.Trans.State (StateT)
+import Control.Monad.Trans.Writer.CPS qualified as CPS
+import Control.Monad.Trans.Writer.Strict qualified as Strict
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Output (LOutput, Output (Output))
+import Data.Effect.State (LState, State, modify)
+import Data.Effect.Writer (Tell (Tell))
+import Data.Hefty.Union (Member, Union)
+
+runOutputEff ::
+    (Freer c fr, Union u, HFunctor (u eh)) =>
+    (o -> Eff u fr eh r ()) ->
+    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
+runOutputEff f = interpretRec \(Output o) -> f o
+{-# INLINE runOutputEff #-}
+
+ignoreOutput ::
+    (Freer c fr, Union u, HFunctor (u eh), Applicative (Eff u fr eh r)) =>
+    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
+ignoreOutput = runOutputEff $ const $ pure ()
+{-# INLINE ignoreOutput #-}
+
+runOutputList ::
+    forall o a r fr u c.
+    ( Freer c fr
+    , Union u
+    , c (Eff u fr '[] r)
+    , c (StateT [o] (Eff u fr '[] r))
+    , Applicative (Eff u fr '[] r)
+    , Monad (Eff u fr '[] (LState [o] ': r))
+    , Member u (State [o]) (LState [o] ': r)
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[] (LOutput o ': r) a ->
+    Eff u fr '[] r ([o], a)
+runOutputList =
+    raiseUnder
+        >>> interpret (\(Output o) -> modify (o :))
+        >>> runState []
+
+{- | Run an `Output` effect by transforming into a monoid.
+     The carrier is required to be a monad.
+-}
+runOutputMonoid ::
+    forall o m a r fr u c.
+    ( Monoid m
+    , Freer c fr
+    , Union u
+    , Monad (Eff u fr '[] r)
+    , c (CPS.WriterT m (Eff u fr '[] r))
+    , HFunctor (u '[])
+    ) =>
+    (o -> m) ->
+    Eff u fr '[] (LOutput o ': r) a ->
+    Eff u fr '[] r (m, a)
+runOutputMonoid f =
+    raiseUnder
+        >>> interpret (\(Output o) -> send0 $ Tell $ f o)
+        >>> runTell
+
+{- | Strict version of `runOutputMonoid`.
+     The constraint on the carrier has been weakened to applicative.
+-}
+runOutputMonoidA ::
+    forall o m a r fr u c.
+    ( Monoid m
+    , Freer c fr
+    , Union u
+    , Applicative (Eff u fr '[] r)
+    , c (Strict.WriterT m (Eff u fr '[] r))
+    , HFunctor (u '[])
+    ) =>
+    (o -> m) ->
+    Eff u fr '[] (LOutput o ': r) a ->
+    Eff u fr '[] r (m, a)
+runOutputMonoidA f =
+    raiseUnder
+        >>> interpret (\(Output o) -> send0 $ Tell $ f o)
+        >>> runTellA
diff --git a/src/Control/Effect/Handler/Heftia/Provider.hs b/src/Control/Effect/Handler/Heftia/Provider.hs
--- a/src/Control/Effect/Handler/Heftia/Provider.hs
+++ b/src/Control/Effect/Handler/Heftia/Provider.hs
@@ -13,27 +13,27 @@
 -}
 module Control.Effect.Handler.Heftia.Provider where
 
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Provider (ProviderS (Provide))
-import Control.Effect.Heftia (Elaborator)
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (Elab)
 import Control.Monad.Trans (MonadTrans, lift)
+import Data.Effect.Provider (Provider' (Provide))
 
 -- | Elaborate the t'Control.Effect.Class.Provider.Provider' effect using the given interpreter.
-elaborateProvider ::
-    (c h, e h) =>
-    (f ~> h) ->
-    (forall x. i -> h x -> f (g x)) ->
-    Elaborator (ProviderS c e i g) f
-elaborateProvider iLower run (Provide i a) = run i $ a iLower
-{-# INLINE elaborateProvider #-}
+runProvider ::
+    (c g, e g) =>
+    (f ~> g) ->
+    (i -> forall x. g x -> f (ctx x)) ->
+    Elab (Provider' c i ctx e) f
+runProvider iLower run (Provide i f) = run i $ f iLower
+{-# INLINE runProvider #-}
 
 {- |
 Elaborate the t'Control.Effect.Class.Provider.Provider' effect using the given interpreter for some
 monad transformer.
 -}
-elaborateProviderT ::
+runProviderT ::
     (Monad m, MonadTrans t, c (t m), e (t m)) =>
-    (forall x. i -> t m x -> m (g x)) ->
-    Elaborator (ProviderS c e i g) m
-elaborateProviderT = elaborateProvider lift
-{-# INLINE elaborateProviderT #-}
+    (i -> forall x. t m x -> m (ctx x)) ->
+    Elab (Provider' c i ctx e) m
+runProviderT = runProvider lift
+{-# INLINE runProviderT #-}
diff --git a/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs b/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs
@@ -0,0 +1,44 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2023 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Elaborator for the t'Control.Effect.Class.Provider.Implicit.ImplicitProvider' effect class.
+-}
+module Control.Effect.Handler.Heftia.Provider.Implicit where
+
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.Reader (runAsk)
+import Control.Effect.Hefty (Eff, Elab, raise)
+import Control.Freer (Freer)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Provider.Implicit (ImplicitProvider' (WithImplicit))
+import Data.Effect.Reader (LAsk)
+import Data.Hefty.Union (Union)
+
+-- | Elaborate the t'ImplicitProvider'' effect using the given interpreter.
+elaborateImplicitProvider ::
+    (c g, e g) =>
+    (f ~> g) ->
+    (i -> forall x. g x -> f x) ->
+    Elab (ImplicitProvider' c i e) f
+elaborateImplicitProvider iLower run (WithImplicit i f) = run i $ f iLower
+{-# INLINE elaborateImplicitProvider #-}
+
+runImplicitProvider ::
+    ( e (Eff u fr eh (LAsk i ': ef))
+    , c (Eff u fr eh (LAsk i ': ef))
+    , Freer c fr
+    , Union u
+    , HFunctor (u eh)
+    , Applicative (Eff u fr eh ef)
+    ) =>
+    Elab (ImplicitProvider' c i e) (Eff u fr eh ef)
+runImplicitProvider (WithImplicit i f) = runAsk i $ f raise
+{-# INLINE runImplicitProvider #-}
diff --git a/src/Control/Effect/Handler/Heftia/Reader.hs b/src/Control/Effect/Handler/Heftia/Reader.hs
--- a/src/Control/Effect/Handler/Heftia/Reader.hs
+++ b/src/Control/Effect/Handler/Heftia/Reader.hs
@@ -9,42 +9,64 @@
 Stability   :  experimental
 Portability :  portable
 
-Interpreter and elaborator for the t'Control.Effect.Class.Reader.Reader' effect class.
+Interpreter and elaborator for the t'Data.Effect.Reader.Local' / t'Data.Effect.Reader.Catch' effect
+classes.
 -}
 module Control.Effect.Handler.Heftia.Reader where
 
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Reader (AskI (Ask), LocalS (Local), ask)
-import Control.Effect.Freer (Fre, interpose, interpret, raise, type (<|))
-import Control.Effect.Heftia (ForallHFunctor, Hef, hoistHeftiaEffects, hoistInterpose, interpretH, raiseH)
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (
+    Eff,
+    Elab,
+    interposeRec,
+    interpretRec,
+    interpretRecH,
+ )
+import Control.Freer (Freer)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Reader (Ask (..), LAsk, Local (..), ask)
 import Data.Function ((&))
+import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Member, Union)
 
-interpretReader ::
-    (Monad m, ForallHFunctor es) =>
+runReader ::
+    forall r rh rf fr u c.
+    ( Freer c fr
+    , HFunctorUnion u
+    , ForallHFunctor u rh
+    , Member u (Ask r) (LAsk r ': rf)
+    , Functor (Eff u fr rh (LAsk r ': rf))
+    , Applicative (Eff u fr rh rf)
+    ) =>
     r ->
-    Hef (LocalS r ': es) (Fre (AskI r ': es') m) ~> Hef es (Fre es' m)
-interpretReader r = hoistHeftiaEffects (interpretAsk r) . interpretReaderH
-{-# INLINE interpretReader #-}
-
-interpretReaderH ::
-    (AskI r <| es', ForallHFunctor es, Monad m) =>
-    Hef (LocalS r ': es) (Fre es' m) ~> Hef es (Fre es' m)
-interpretReaderH =
-    interpretH \(Local (f :: r -> r) a) ->
-        a & hoistInterpose @(AskI r) \Ask -> f <$> ask
+    Eff u fr (Local r ': rh) (LAsk r ': rf) ~> Eff u fr rh rf
+runReader r = runLocal >>> runAsk r
+{-# INLINE runReader #-}
 
-elaborateReader ::
-    (AskI r <| es, Monad m) =>
-    LocalS r (Fre es m) ~> Fre es m
-elaborateReader (Local (f :: r -> r) a) =
-    a & interpose @(AskI r) \Ask -> f <$> ask
+-- | Elaborate the t'Local' effect.
+runLocal ::
+    forall r rh ef fr u c.
+    ( Freer c fr
+    , HFunctorUnion u
+    , ForallHFunctor u rh
+    , Member u (Ask r) ef
+    , Functor (Eff u fr rh ef)
+    ) =>
+    Eff u fr (Local r ': rh) ef ~> Eff u fr rh ef
+runLocal = interpretRecH elabLocal
+{-# INLINE runLocal #-}
 
-interpretAsk :: Monad m => r -> Fre (AskI r ': es) m ~> Fre es m
-interpretAsk r = interpret \Ask -> pure r
-{-# INLINE interpretAsk #-}
+elabLocal ::
+    forall r eh ef fr u c.
+    (Member u (Ask r) ef, Freer c fr, Union u, HFunctor (u eh), Functor (Eff u fr eh ef)) =>
+    Elab (Local r) (Eff u fr eh ef)
+elabLocal (Local f a) = a & interposeRec @(Ask r) \Ask -> f <$> ask
 
-liftReader ::
-    (ForallHFunctor es, Monad m) =>
-    Hef es (Fre es' m) ~> Hef (LocalS FilePath ': es) (Fre (AskI FilePath ': es') m)
-liftReader = raiseH . hoistHeftiaEffects raise
-{-# INLINE liftReader #-}
+-- | Interpret the t'Ask' effect.
+runAsk ::
+    forall r rs eh fr u c.
+    (Freer c fr, Union u, Applicative (Eff u fr eh rs), HFunctor (u eh)) =>
+    r ->
+    Eff u fr eh (LAsk r ': rs) ~> Eff u fr eh rs
+runAsk r = interpretRec \Ask -> pure r
+{-# INLINE runAsk #-}
diff --git a/src/Control/Effect/Handler/Heftia/Resource.hs b/src/Control/Effect/Handler/Heftia/Resource.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Resource.hs
@@ -0,0 +1,26 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2023 Yamada Ryo
+               (c) 2017 FP Complete
+               (c) 2022 Fumiaki Kinoshita
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+An elaborator for the t'Control.Effect.Class.Resource.Resource' effect class.
+-}
+module Control.Effect.Handler.Heftia.Resource where
+
+import Control.Effect.Hefty (Elab)
+import Data.Effect.Resource (Resource (Bracket, BracketOnExcept))
+import UnliftIO (MonadUnliftIO, bracket, bracketOnError)
+
+-- | Elaborates the `Resource` effect under the `MonadUnliftIO` context.
+resourceToIO :: MonadUnliftIO m => Elab Resource m
+resourceToIO = \case
+    Bracket acquire release thing -> bracket acquire release thing
+    BracketOnExcept acquire onError thing -> bracketOnError acquire onError thing
diff --git a/src/Control/Effect/Handler/Heftia/ShiftReset.hs b/src/Control/Effect/Handler/Heftia/ShiftReset.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/ShiftReset.hs
@@ -0,0 +1,70 @@
+-- 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/.
+
+module Control.Effect.Handler.Heftia.ShiftReset where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (
+    Eff,
+    injectH,
+    interpretKAllH,
+    interpretKH,
+    interpretRecH,
+    raiseH,
+    runEff,
+ )
+import Control.Freer (Freer)
+import Control.Monad ((<=<))
+import Control.Monad.Freer (MonadFreer)
+import Data.Effect (LiftIns)
+import Data.Effect.HFunctor (HFunctor, hfmap)
+import Data.Effect.Key (KeyH (KeyH))
+import Data.Effect.ShiftReset (Reset (Reset), Shift, Shift' (Shift), Shift_ (Shift_))
+import Data.Hefty.Union (HFunctorUnion, HFunctorUnion_ (ForallHFunctor), Union ((|+:)))
+
+evalShift ::
+    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
+    Eff u fr '[Shift r] ef r ->
+    Eff u fr '[] ef r
+evalShift = runShift pure
+{-# INLINE evalShift #-}
+
+runShift ::
+    forall r a ef fr u c.
+    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
+    (a -> Eff u fr '[] ef r) ->
+    Eff u fr '[Shift r] ef a ->
+    Eff u fr '[] ef r
+runShift f =
+    interpretKH f \k ->
+        let k' = raiseH . k
+         in evalShift . \case
+                KeyH (Shift g) -> g k'
+
+withShift ::
+    ( MonadFreer c fr
+    , Union u
+    , c (Eff u fr '[] '[LiftIns (Eff u fr eh ef)])
+    , c (Eff u fr eh ef)
+    , HFunctor (u '[])
+    ) =>
+    Eff u fr '[Shift r] '[LiftIns (Eff u fr eh ef)] r ->
+    Eff u fr eh ef r
+withShift = evalShift >>> runEff
+{-# INLINE withShift #-}
+
+runShift_ ::
+    (MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
+    Eff u fr (Shift_ ': eh) ef ~> Eff u fr eh ef
+runShift_ =
+    interpretKAllH pure \k ->
+        (\(Shift_ f) -> runShift_ $ f $ raiseH . k)
+            |+: (k <=< injectH . hfmap runShift_)
+
+runReset ::
+    (Freer c fr, HFunctorUnion u, ForallHFunctor u eh) =>
+    Eff u fr (Reset ': eh) ef ~> Eff u fr eh ef
+runReset = interpretRecH \(Reset a) -> a
+{-# INLINE runReset #-}
diff --git a/src/Control/Effect/Handler/Heftia/State.hs b/src/Control/Effect/Handler/Heftia/State.hs
--- a/src/Control/Effect/Handler/Heftia/State.hs
+++ b/src/Control/Effect/Handler/Heftia/State.hs
@@ -1,3 +1,5 @@
+{-# 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/.
@@ -13,30 +15,106 @@
 -}
 module Control.Effect.Handler.Heftia.State where
 
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.State (StateI (Get, Put))
-import Control.Effect.Freer (Fre, interpretT)
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Handler.Heftia.Reader (runAsk)
+import Control.Effect.Hefty (Eff, injectF, interpose, interposeT, interpret, interpretFin, interpretK, raiseUnder)
+import Control.Freer (Freer)
+import Control.Monad.Freer (MonadFreer)
 import Control.Monad.State (StateT)
-import Control.Monad.Trans.State (runStateT)
 import Control.Monad.Trans.State qualified as T
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Reader (Ask (Ask), LAsk, ask)
+import Data.Effect.State (LState, State (Get, Put), get, put)
+import Data.Function ((&))
+import Data.Functor ((<&>))
+import Data.Hefty.Union (Member, Union)
 import Data.Tuple (swap)
+import UnliftIO (MonadIO, newIORef, readIORef, writeIORef)
 
 -- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-interpretState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m (s, a)
-interpretState s a = swap <$> runStateT (interpretStateT a) s
-{-# INLINE interpretState #-}
+runState ::
+    forall s r a fr u c.
+    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
+runState s a = swap <$> T.runStateT (runStateT a) s
+{-# INLINE runState #-}
 
-evalState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m a
-evalState s a = snd <$> interpretState s a
+evalState ::
+    forall s r fr u c.
+    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) ~> Eff u fr '[] r
+evalState s a = snd <$> runState s a
 {-# INLINE evalState #-}
 
-execState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m s
-execState s a = fst <$> interpretState s a
+execState ::
+    forall s r a fr u c.
+    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r s
+execState s a = fst <$> runState s a
 {-# INLINE execState #-}
 
 -- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-interpretStateT :: forall s es m. Monad m => Fre (StateI s ': es) m ~> StateT s (Fre es m)
-interpretStateT = interpretT \case
-    Get -> T.get
-    Put s -> T.put s
-{-# INLINE interpretStateT #-}
+runStateT ::
+    forall s r fr u c.
+    (Freer c fr, Union u, c (StateT s (Eff u fr '[] r)), c (Eff u fr '[] r), Applicative (Eff u fr '[] r)) =>
+    Eff u fr '[] (LState s ': r) ~> StateT s (Eff u fr '[] r)
+runStateT =
+    interpretFin (\u -> T.StateT \s -> (,s) <$> injectF u) fuseStateEffect
+
+-- | Interpret the 'Get'/'Put' effects using delimited continuations.
+runStateK ::
+    forall s r a fr u c.
+    ( MonadFreer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Member u (Ask s) (LAsk s ': r)
+    , c (Eff u fr '[] (LAsk s ': r))
+    , Applicative (Eff u fr '[] r)
+    ) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
+runStateK initialState =
+    raiseUnder
+        >>> interpretK
+            (\a -> ask <&> (,a))
+            ( \k -> \case
+                Get -> k =<< ask
+                Put s -> k () & interpose @(Ask s) \Ask -> pure s
+            )
+        >>> runAsk initialState
+
+runStateIORef ::
+    forall s r a fr u c.
+    (Freer c fr, Union u, MonadIO (Eff u fr '[] r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
+runStateIORef s m = do
+    ref <- newIORef s
+    a <-
+        m & interpret \case
+            Get -> readIORef ref
+            Put s' -> writeIORef ref s'
+    readIORef ref <&> (,a)
+
+transactState ::
+    forall s r fr u c.
+    (Freer c fr, Union u, Member u (State s) r, Monad (Eff u fr '[] r), c (StateT s (Eff u fr '[] r))) =>
+    Eff u fr '[] r ~> Eff u fr '[] r
+transactState m = do
+    pre <- get @s
+    (a, post) <- T.runStateT (interposeT fuseStateEffect m) pre
+    put post
+    pure a
+
+fuseStateEffect :: Applicative f => State s ~> StateT s f
+fuseStateEffect = \case
+    Get -> T.StateT \s -> pure (s, s)
+    Put s -> T.StateT \_ -> pure ((), s)
diff --git a/src/Control/Effect/Handler/Heftia/Unlift.hs b/src/Control/Effect/Handler/Heftia/Unlift.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Handler/Heftia/Unlift.hs
@@ -0,0 +1,34 @@
+-- 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/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Control.Effect.Handler.Heftia.Unlift where
+
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (Eff, interpretH, runEff, send0)
+import Control.Freer (Freer)
+import Data.Effect (LiftIns)
+import Data.Effect.Unlift (UnliftBase (WithRunInBase), UnliftIO)
+import Data.Hefty.Union (Union)
+
+runUnliftBase ::
+    forall b fr u c.
+    (Freer c fr, Union u, c b) =>
+    Eff u fr '[UnliftBase b] '[LiftIns b] ~> b
+runUnliftBase =
+    runEff . interpretH \(WithRunInBase f) ->
+        send0 $ f runUnliftBase
+
+runUnliftIO ::
+    forall fr u c.
+    (Freer c fr, Union u, c IO) =>
+    Eff u fr '[UnliftIO] '[LiftIns IO] ~> IO
+runUnliftIO = runUnliftBase
+{-# INLINE runUnliftIO #-}
diff --git a/src/Control/Effect/Handler/Heftia/Writer.hs b/src/Control/Effect/Handler/Heftia/Writer.hs
--- a/src/Control/Effect/Handler/Heftia/Writer.hs
+++ b/src/Control/Effect/Handler/Heftia/Writer.hs
@@ -16,61 +16,304 @@
 -}
 module Control.Effect.Handler.Heftia.Writer where
 
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Writer (Tell (tell), TellI (Tell), WriterS (Censor, Listen))
-import Control.Effect.Freer (Fre, intercept, interposeT, interpretK, interpretT, type (<|))
-import Control.Monad.Trans.Writer.CPS (WriterT, runWriterT)
-import Control.Monad.Trans.Writer.CPS qualified as T
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Effect.Hefty (
+    Eff,
+    Elab,
+    injectF,
+    interposeFin,
+    interposeT,
+    interpretFin,
+    interpretK,
+    interpretRecH,
+    interpretT,
+    rewrite,
+ )
+import Control.Freer (Freer)
+import Control.Monad.Freer (MonadFreer)
+import Control.Monad.Trans (lift)
+import Control.Monad.Trans.Writer.CPS qualified as CPS
+import Control.Monad.Trans.Writer.Strict qualified as Strict
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Writer (LTell, Tell (Tell), WriterH (Censor, Listen), tell)
 import Data.Function ((&))
+import Data.Hefty.Union (Member, Union)
 import Data.Tuple (swap)
 
-elaborateWriterT ::
-    forall w m es.
-    (Monad m, Monoid w, TellI w <| es) =>
-    WriterS w (Fre es m) ~> Fre es m
-elaborateWriterT = \case
+-- | 'Writer' effect handler with post-applying censor semantics for Monad use.
+runWriterPost ::
+    forall w a r fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] r)
+    , c (CPS.WriterT w (Eff u fr '[] r))
+    , Member u (Tell w) (LTell w ': r)
+    , Monad (Eff u fr '[] (LTell w ': r))
+    , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runWriterPost = elaborateWriterPost >>> runTell
+{-# INLINE runWriterPost #-}
+
+elaborateWriterPost ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] ef)
+    , c (CPS.WriterT w (Eff u fr '[] ef))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPost = interpretRecH elabWriterPost
+{-# INLINE elaborateWriterPost #-}
+
+elabWriterPost ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] ef)
+    , c (CPS.WriterT w (Eff u fr '[] ef))
+    ) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPost = \case
     Listen m -> listenT m
-    Censor f m -> m & intercept @(TellI w) \(Tell w) -> Tell $ f w
+    Censor f m -> postCensor f m
 
-elaborateWriterTransactionalT ::
-    forall w m es.
-    (Monad m, Monoid w, TellI w <| es) =>
-    WriterS w (Fre es m) ~> Fre es m
-elaborateWriterTransactionalT = \case
+postCensor ::
+    forall w es fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Member u (Tell w) es
+    , Union u
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] es)
+    , c (CPS.WriterT w (Eff u fr '[] es))
+    ) =>
+    (w -> w) ->
+    Eff u fr '[] es ~> Eff u fr '[] es
+postCensor f m = do
+    (a, w) <- CPS.runWriterT $ confiscateT m
+    tell $ f w
+    pure a
+
+-- | 'Writer' effect handler with pre-applying censor semantics for Monad use.
+runWriterPre ::
+    forall w a r fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] r)
+    , c (CPS.WriterT w (Eff u fr '[] r))
+    , Member u (Tell w) (LTell w ': r)
+    , Monad (Eff u fr '[] (LTell w ': r))
+    , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runWriterPre = elaborateWriterPre >>> runTell
+{-# INLINE runWriterPre #-}
+
+elaborateWriterPre ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] ef)
+    , c (CPS.WriterT w (Eff u fr '[] ef))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPre = interpretRecH elabWriterPre
+{-# INLINE elaborateWriterPre #-}
+
+elabWriterPre ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] ef)
+    , c (CPS.WriterT w (Eff u fr '[] ef))
+    ) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPre = \case
     Listen m -> listenT m
-    Censor f m -> do
-        (a, w) <- confiscateT m
-        tell $ f w
-        pure a
+    Censor f m -> preCensor f m
 
+-- | 'Writer' effect handler with pre-applying censor semantics for Applicative use.
+runWriterPreA ::
+    forall w a r fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , HFunctor (u '[])
+    , Monad (Eff u fr '[] r)
+    , c (Strict.WriterT w (Eff u fr '[] r))
+    , Member u (Tell w) (LTell w ': r)
+    , Monad (Eff u fr '[] (LTell w ': r))
+    , c (Strict.WriterT w (Eff u fr '[] (LTell w ': r)))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runWriterPreA = elaborateWriterPreA >>> runTellA
+{-# INLINE runWriterPreA #-}
+
+elaborateWriterPreA ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Applicative (Eff u fr '[] ef)
+    , c (Strict.WriterT w (Eff u fr '[] ef))
+    , HFunctor (u '[WriterH w])
+    ) =>
+    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPreA = interpretRecH elabWriterPre'
+{-# INLINE elaborateWriterPreA #-}
+
+elabWriterPre' ::
+    forall w ef fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) ef
+    , HFunctor (u '[])
+    , Applicative (Eff u fr '[] ef)
+    , c (Strict.WriterT w (Eff u fr '[] ef))
+    ) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPre' = \case
+    Listen m -> listenTA m
+    Censor f m -> preCensor f m
+
+preCensor ::
+    forall w es fr u c.
+    (Freer c fr, Member u (Tell w) es, Union u, HFunctor (u '[])) =>
+    (w -> w) ->
+    Eff u fr '[] es ~> Eff u fr '[] es
+preCensor f = rewrite @(Tell w) \(Tell w) -> Tell $ f w
+
 listenT ::
-    (Monoid w, Monad m, TellI w <| es) =>
-    Fre es m a ->
-    Fre es m (a, w)
-listenT m = do
-    (a, w) <- confiscateT m
-    tell w
-    pure (a, w)
-{-# INLINE listenT #-}
+    forall w es a fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) es
+    , Monad (Eff u fr '[] es)
+    , c (CPS.WriterT w (Eff u fr '[] es))
+    ) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (w, a)
+listenT m =
+    swap <$> CPS.runWriterT do
+        m & interposeT @(Tell w) \(Tell w) -> do
+            lift $ tell w
+            CPS.tell w
 
-confiscateT ::
-    forall w m es a.
-    (Monoid w, Monad m, TellI w <| es) =>
-    Fre es m a ->
-    Fre es m (a, w)
-confiscateT = runWriterT . interposeT @(TellI w) \(Tell w) -> T.tell w
-{-# INLINE confiscateT #-}
+listenTA ::
+    forall w es a fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) es
+    , Applicative (Eff u fr '[] es)
+    , c (Strict.WriterT w (Eff u fr '[] es))
+    ) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (w, a)
+listenTA m =
+    swap <$> Strict.runWriterT do
+        m & interposeFin @(Tell w) (liftStrictWriterT . injectF) \(Tell w) -> do
+            liftStrictWriterT (tell w) *> tellStrictWriterT w
 
-interpretTell :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
-interpretTell = fmap swap . runWriterT . interpretTellT
-{-# INLINE interpretTell #-}
+runTell ::
+    (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r))) =>
+    Eff u fr '[] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runTell = fmap swap . CPS.runWriterT . runTellT
+{-# INLINE runTell #-}
 
-interpretTellT :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> WriterT w (Fre es m) a
-interpretTellT = interpretT \(Tell w) -> T.tell w
-{-# INLINE interpretTellT #-}
+runTellT ::
+    (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r))) =>
+    Eff u fr '[] (LTell w ': r) ~> CPS.WriterT w (Eff u fr '[] r)
+runTellT = interpretT \(Tell w) -> CPS.tell w
+{-# INLINE runTellT #-}
 
-interpretTellK :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
-interpretTellK =
+runTellA ::
+    (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r))) =>
+    Eff u fr '[] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runTellA = fmap swap . Strict.runWriterT . runTellTA
+{-# INLINE runTellA #-}
+
+runTellTA ::
+    (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r))) =>
+    Eff u fr '[] (LTell w ': r) ~> Strict.WriterT w (Eff u fr '[] r)
+runTellTA = interpretFin (liftStrictWriterT . injectF) \(Tell w) -> tellStrictWriterT w
+{-# INLINE runTellTA #-}
+
+runTellK ::
+    (Monoid w, MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
+    Eff u fr '[] (LTell w ': r) a ->
+    Eff u fr '[] r (w, a)
+runTellK =
     interpretK (pure . (mempty,)) \k (Tell w) -> do
         (w', r) <- k ()
         pure (w <> w', r)
+
+liftStrictWriterT :: forall w f. (Monoid w, Functor f) => f ~> Strict.WriterT w f
+liftStrictWriterT = Strict.WriterT . ((,mempty) <$>)
+{-# INLINE liftStrictWriterT #-}
+
+tellStrictWriterT :: forall w f. Applicative f => w -> Strict.WriterT w f ()
+tellStrictWriterT = Strict.WriterT . pure . ((),)
+{-# INLINE tellStrictWriterT #-}
+
+transactWriter ::
+    forall w es a fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) es
+    , Monad (Eff u fr '[] es)
+    , c (CPS.WriterT w (Eff u fr '[] es))
+    ) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es a
+transactWriter m = do
+    (a, w) <- CPS.runWriterT $ confiscateT m
+    tell @w w
+    pure a
+
+confiscateT ::
+    forall w es a fr u c.
+    ( Monoid w
+    , Freer c fr
+    , Union u
+    , Member u (Tell w) es
+    , Monad (Eff u fr '[] es)
+    , c (CPS.WriterT w (Eff u fr '[] es))
+    ) =>
+    Eff u fr '[] es a ->
+    CPS.WriterT w (Eff u fr '[] es) a
+confiscateT m =
+    m & interposeT @(Tell w) \(Tell w) -> CPS.tell w