[add] final-encoded generic Freer carrier.

heftia-effects/Example/Writer/Main.hs

@@ -4,46 +4,34 @@
 
 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 (sendIns, type (<:), type (<<:))
+import Control.Effect.ExtensibleFinal (runEff)
+import Control.Effect.Handler.Heftia.Writer (elaborateWriter, elaborateWriterTransactional, interpretTell)
+import Control.Effect.Hefty (interpretH)
+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)
         hello
 
 main :: IO ()
-main = runFreerEffects do
+main = runEff do
     (s :: String, _) <-
         interpretTell
-            . runElaborate' (elaborateWriterT @String)
+            . interpretH (elaborateWriter @String)
             $ censorHello
 
     (sTransactional :: String, _) <-
         interpretTell
-            . runElaborate' (elaborateWriterTransactionalT @String)
+            . interpretH (elaborateWriterTransactional @String)
             $ censorHello
 
     sendIns $ putStrLn $ "Normal: " <> s
     sendIns $ putStrLn $ "Transactional: " <> sTransactional
-
-runElaborate' ::
-    (HFunctor e, Monad f) =>
-    Elaborator e f ->
-    Hef '[e] f ~> f
-runElaborate' f = runElaborate $ f |+: absurdUnionH

heftia-effects/src/Control/Effect/Handler/Heftia/Except.hs

@@ -16,7 +16,8 @@ module Control.Effect.Handler.Heftia.Except where
 
 import Control.Effect (type (~>))
 import Control.Effect.Hefty (
-    Effectful,
+    Eff,
+    Elab,
     MemberF,
     interposeK,
     interposeT,
@@ -25,39 +26,50 @@ import Control.Effect.Hefty (
  )
 import Control.Monad.Freer (MonadFreer)
 import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
-import Data.Effect (LNop)
-import Data.Effect.Except (Catch (Catch), Throw (Throw))
-import Data.Free.Sum (type (+))
+import Data.Effect.Except (Catch (Catch), LThrow, Throw (Throw))
 import Data.Function ((&))
 import Data.Hefty.Union (Union)
 
--- | Elaborate the 'Catch' effect using a delimited continuation.
+-- | Elaborate the t'Catch' effect using the 'ExceptT' monad transformer.
 elaborateCatch ::
-    (MemberF u (Throw e) ef, MonadFreer f, Union u) =>
-    Catch e (Effectful u f LNop ef) ~> Effectful u f LNop ef
-elaborateCatch (Catch action hdl) =
-    action & interposeK pure \_ (Throw e) -> hdl e
-
--- | Elaborate the 'Catch' effect using the 'ExceptT' monad transformer.
-elaborateCatchT ::
-    (MemberF u (Throw e) ef, MonadFreer f, Union u) =>
-    Catch e (Effectful u f LNop ef) ~> Effectful u f LNop ef
-elaborateCatchT (Catch action hdl) = do
+    forall e ef fr u.
+    (MemberF u (Throw e) ef, MonadFreer fr, Union u) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elaborateCatch (Catch action hdl) = do
     r <- runExceptT $ action & interposeT \(Throw e) -> throwE e
     case r of
         Left e -> hdl e
         Right a -> pure a
 
--- | Interpret the 'Throw' effect using a delimited continuation.
+-- | Elaborate the 'Catch' effect using a delimited continuation.
+elaborateCatchK ::
+    forall e ef fr u.
+    (MemberF u (Throw e) ef, MonadFreer fr, Union u) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elaborateCatchK (Catch action hdl) =
+    action & interposeK pure \_ (Throw e) -> hdl e
+
+-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
 interpretThrow ::
-    (MonadFreer f, Union u) =>
-    Effectful u f LNop (Throw e + es) a ->
-    Effectful u f LNop es (Either e a)
-interpretThrow = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
+    forall e r a fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+interpretThrow = runExceptT . interpretThrowT
+{-# INLINE interpretThrow #-}
 
 -- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
 interpretThrowT ::
-    (MonadFreer f, Union u) =>
-    Effectful u f LNop (Throw e + es) ~> ExceptT e (Effectful u f LNop es)
+    forall e r fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) ~> ExceptT e (Eff u fr '[] r)
 interpretThrowT = interpretT \(Throw e) -> throwE e
 {-# INLINE interpretThrowT #-}
+
+-- | Interpret the 'Throw' effect using a delimited continuation.
+interpretThrowK ::
+    forall e r a fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+interpretThrowK = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e

heftia-effects/src/Control/Effect/Handler/Heftia/Provider.hs

@@ -14,16 +14,16 @@ Elaborator for the t'Control.Effect.Class.Provider.Provider' effect class.
 module Control.Effect.Handler.Heftia.Provider where
 
 import Control.Effect (type (~>))
-import Control.Effect.Class.Provider (ProviderS (Provide))
-import Control.Effect.Heftia (Elaborator)
+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 g, e g) =>
     (f ~> g) ->
     (i -> forall x. g x -> f (ctx x)) ->
-    Elaborator (ProviderS c i ctx e) f
+    Elab (Provider' c i ctx e) f
 elaborateProvider iLower run (Provide i f) = run i $ f iLower
 {-# INLINE elaborateProvider #-}
 
@@ -34,6 +34,6 @@ monad transformer.
 elaborateProviderT ::
     (Monad m, MonadTrans t, c (t m), e (t m)) =>
     (i -> forall x. t m x -> m (ctx x)) ->
-    Elaborator (ProviderS c i ctx e) m
+    Elab (Provider' c i ctx e) m
 elaborateProviderT = elaborateProvider lift
 {-# INLINE elaborateProviderT #-}

heftia-effects/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs

@@ -14,26 +14,30 @@ Elaborator for the t'Control.Effect.Class.Provider.Implicit.ImplicitProvider' ef
 module Control.Effect.Handler.Heftia.Provider.Implicit where
 
 import Control.Effect (type (~>))
-import Control.Effect.Class.Provider.Implicit (ImplicitProviderS (WithImplicit))
-import Control.Effect.Class.Reader (AskI)
-import Control.Effect.Freer (Fre, raise)
 import Control.Effect.Handler.Heftia.Reader (interpretAsk)
-import Control.Effect.Heftia (Elaborator)
+import Control.Effect.Hefty (Eff, Elab, raise)
+import Control.Monad.Freer (MonadFreer)
+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'Control.Effect.Class.Provider.Implicit.ImplicitProvider' effect using the given
-interpreter.
--}
+-- | Elaborate the t'ImplicitProvider'' effect using the given interpreter.
 elaborateImplicitProvider ::
     (c g, e g) =>
     (f ~> g) ->
     (i -> forall x. g x -> f x) ->
-    Elaborator (ImplicitProviderS c i e) f
+    Elab (ImplicitProvider' c i e) f
 elaborateImplicitProvider iLower run (WithImplicit i f) = run i $ f iLower
 {-# INLINE elaborateImplicitProvider #-}
 
--- todo: make the 'classy-effects-static' handler system and use the static Reader carrier here.
 runImplicitProvider ::
-    (c (Fre (AskI i ': r) m), e (Fre (AskI i ': r) m), Monad m) =>
-    Elaborator (ImplicitProviderS c i e) (Fre r m)
+    ( e (Eff u fr eh (LAsk i ': ef))
+    , c (Eff u fr eh (LAsk i ': ef))
+    , MonadFreer fr
+    , Union u
+    , HFunctor (u eh)
+    ) =>
+    Elab (ImplicitProvider' c i e) (Eff u fr eh ef)
 runImplicitProvider (WithImplicit i f) = interpretAsk i $ f raise
+{-# INLINE runImplicitProvider #-}

heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs

@@ -1,8 +1,6 @@
 -- 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/.
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 {- |
 Copyright   :  (c) 2023 Yamada Ryo
@@ -19,53 +17,45 @@ module Control.Effect.Handler.Heftia.Reader where
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
 import Control.Effect.Hefty (
-    Effectful,
-    HFunctors,
+    Eff,
+    Elab,
     MemberF,
-    TailHFunctor,
     interposeRec,
     interpretRec,
     interpretRecH,
  )
 import Control.Freer (Freer)
-import Data.Effect.HFunctor (type (:+:))
-import Data.Effect.Reader (Ask (..), Local (..), ask)
-import Data.Free.Sum (type (+))
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Reader (Ask (..), LAsk, Local (..), ask)
 import Data.Function ((&))
-import Data.Hefty.Union (HFunctorUnion, Union)
+import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Union)
 
 interpretReader ::
-    ( Freer c f
-    , forall f'. c f' => Applicative f'
+    forall r rh rf fr u c.
+    ( Freer c fr
     , HFunctorUnion u
-    , TailHFunctor u eh
-    , Applicative (Effectful u f eh ef)
-    , MemberF u (Ask r) (Ask r + ef)
-    , c (Effectful u f eh ef)
-    , c (Effectful u f eh (Ask r + ef))
+    , ForallHFunctor u rh
+    , MemberF u (Ask r) (LAsk r ': rf)
+    , Functor (Eff u fr rh (LAsk r ': rf))
+    , Applicative (Eff u fr rh rf)
     ) =>
     r ->
-    Effectful u f (Local r :+: eh) (Ask r + ef) ~> Effectful u f eh ef
+    Eff u fr (Local r ': rh) (LAsk r ': rf) ~> Eff u fr rh rf
 interpretReader r = interpretRecH elaborateLocal >>> interpretAsk r
 {-# INLINE interpretReader #-}
 
 -- | Elaborate the t'Local' effect.
 elaborateLocal ::
-    forall r eh ef f u c.
-    ( MemberF u (Ask r) ef
-    , Freer c f
-    , Union u
-    , HFunctors u eh
-    , Functor (Effectful u f eh ef)
-    ) =>
-    Local r (Effectful u f eh ef) ~> Effectful u f eh ef
+    forall r eh ef fr u c.
+    (MemberF 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)
 elaborateLocal (Local f a) = a & interposeRec @(Ask r) \Ask -> f <$> ask
 
 -- | Interpret the t'Ask' effect.
 interpretAsk ::
-    forall r eh ef f u c.
-    (Freer c f, Union u, Applicative (Effectful u f eh ef), HFunctors u eh) =>
+    forall r rs eh fr u c.
+    (Freer c fr, Union u, Applicative (Eff u fr eh rs), HFunctor (u eh)) =>
     r ->
-    Effectful u f eh (Ask r + ef) ~> Effectful u f eh ef
+    Eff u fr eh (LAsk r ': rs) ~> Eff u fr eh rs
 interpretAsk r = interpretRec \Ask -> pure r
 {-# INLINE interpretAsk #-}

heftia-effects/src/Control/Effect/Handler/Heftia/Resource.hs

@@ -15,12 +15,12 @@ An elaborator for the t'Control.Effect.Class.Resource.Resource' effect class.
 -}
 module Control.Effect.Handler.Heftia.Resource where
 
-import Control.Effect.Class.Resource (ResourceS (Bracket, BracketOnExcept))
-import Control.Effect.Heftia (Elaborator)
+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 => Elaborator ResourceS m
+resourceToIO :: MonadUnliftIO m => Elab Resource m
 resourceToIO = \case
     Bracket acquire release thing -> bracket acquire release thing
     BracketOnExcept acquire onError thing -> bracketOnError acquire onError thing

heftia-effects/src/Control/Effect/Handler/Heftia/State.hs

@@ -15,49 +15,72 @@ module Control.Effect.Handler.Heftia.State where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Class.Reader (AskI (Ask), ask)
-import Control.Effect.Class.State (StateI (Get, Put))
-import Control.Effect.Freer (Fre, interpose, interpretK, interpretT, raiseUnder)
 import Control.Effect.Handler.Heftia.Reader (interpretAsk)
+import Control.Effect.Hefty (Eff, MemberF, interpose, interpretK, interpretT, raiseUnder)
+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))
 import Data.Function ((&))
 import Data.Functor ((<&>))
+import Data.Hefty.Union (Union)
 import Data.Tuple (swap)
 
 -- | 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 ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
 interpretState s a = swap <$> runStateT (interpretStateT a) s
 {-# INLINE interpretState #-}
 
-evalState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m a
+evalState ::
+    forall s r fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) ~> Eff u fr '[] r
 evalState s a = snd <$> interpretState s a
 {-# INLINE evalState #-}
 
-execState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m s
+execState ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r s
 execState s a = fst <$> interpretState 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
+interpretStateT ::
+    forall s r fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LState s ': r) ~> StateT s (Eff u fr '[] r)
+interpretStateT =
+    interpretT \case
+        Get -> T.get
+        Put s -> T.put s
 {-# INLINE interpretStateT #-}
 
-{- |
-Interpret the 'Get'/'Put' effects using the t'Control.Monad.Trans.Cont.ContT' continuation monad
-transformer.
--}
-interpretStateK :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m (s, a)
+-- | Interpret the 'Get'/'Put' effects using delimited continuations.
+interpretStateK ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u, HFunctor (u '[]), MemberF u (Ask s) (LAsk s ': r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
 interpretStateK initialState =
     raiseUnder
         >>> interpretK
             (\a -> ask <&> (,a))
             ( \k -> \case
                 Get -> k =<< ask
-                Put s -> k () & interpose @(AskI s) \Ask -> pure s
+                Put s -> k () & interpose @(Ask s) \Ask -> pure s
             )
         >>> interpretAsk initialState
 {-# INLINE interpretStateK #-}

heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs

@@ -17,26 +17,29 @@ See [README.md](https://github.com/sayo-hs/heftia/blob/master/README.md).
 module Control.Effect.Handler.Heftia.Writer where
 
 import Control.Effect (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.Effect.Hefty (Eff, Elab, MemberF, interposeT, interpretK, interpretT, rewrite)
+import Control.Monad.Freer (MonadFreer)
 import Control.Monad.Trans.Writer.CPS (WriterT, runWriterT)
 import Control.Monad.Trans.Writer.CPS qualified as T
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Writer (LTell, Tell (Tell), WriterH (Censor, Listen), tell)
 import Data.Function ((&))
+import Data.Hefty.Union (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
+elaborateWriter ::
+    forall w ef fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) ef, HFunctor (u '[])) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elaborateWriter = \case
     Listen m -> listenT m
-    Censor f m -> m & intercept @(TellI w) \(Tell w) -> Tell $ f w
+    Censor f m -> m & rewrite @(Tell w) \(Tell w) -> Tell $ f w
 
-elaborateWriterTransactionalT ::
-    forall w m es.
-    (Monad m, Monoid w, TellI w <| es) =>
-    WriterS w (Fre es m) ~> Fre es m
-elaborateWriterTransactionalT = \case
+elaborateWriterTransactional ::
+    forall w ef fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) ef) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elaborateWriterTransactional = \case
     Listen m -> listenT m
     Censor f m -> do
         (a, w) <- confiscateT m
@@ -44,9 +47,10 @@ elaborateWriterTransactionalT = \case
         pure a
 
 listenT ::
-    (Monoid w, Monad m, TellI w <| es) =>
-    Fre es m a ->
-    Fre es m (a, w)
+    forall w es a fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) es) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (a, w)
 listenT m = do
     (a, w) <- confiscateT m
     tell w
@@ -54,22 +58,22 @@ listenT m = do
 {-# INLINE listenT #-}
 
 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
+    forall w es a fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) es) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (a, w)
+confiscateT = runWriterT . interposeT @(Tell w) \(Tell w) -> T.tell w
 {-# INLINE confiscateT #-}
 
-interpretTell :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
+interpretTell :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) a -> Eff u fr '[] r (w, a)
 interpretTell = fmap swap . runWriterT . interpretTellT
 {-# INLINE interpretTell #-}
 
-interpretTellT :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> WriterT w (Fre es m) a
+interpretTellT :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) ~> WriterT w (Eff u fr '[] r)
 interpretTellT = interpretT \(Tell w) -> T.tell w
 {-# INLINE interpretTellT #-}
 
-interpretTellK :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
+interpretTellK :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) a -> Eff u fr '[] r (w, a)
 interpretTellK =
     interpretK (pure . (mempty,)) \k (Tell w) -> do
         (w', r) <- k ()

heftia/heftia.cabal

@@ -56,12 +56,15 @@ library
     exposed-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

heftia/src/Control/Effect/ExtensibleChurch.hs

@@ -13,9 +13,13 @@ Type operators for extensible effectful programs based on the Church-encoded Fre
 -}
 module Control.Effect.ExtensibleChurch where
 
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
 import Control.Monad.Freer.Church (FreerChurch)
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion FreerChurch eh ef
@@ -29,3 +33,11 @@ type (:!) efs = EffF ExtensibleUnion FreerChurch efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/ExtensibleFastA.hs

@@ -16,8 +16,12 @@ See "Control.Applicative.Free.Fast".
 module Control.Effect.ExtensibleFastA where
 
 import Control.Applicative.Free.Fast (Ap)
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion Ap eh ef
@@ -31,3 +35,11 @@ type (:!) efs = EffF ExtensibleUnion Ap efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/ExtensibleFinal.hs

@@ -0,0 +1,43 @@
+-- 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-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the final-encoded Freer monad.
+-}
+module Control.Effect.ExtensibleFinal where
+
+import Control.Effect (type (~>))
+import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
+import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Control.Freer.Final (FreerFinal)
+import Data.Effect (LiftIns)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+type eh !! ef = Effectful ExtensibleUnion (FreerFinal Monad) eh ef
+type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Monad) ef
+
+infixr 5 !!
+infixr 4 !
+
+type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Monad) ehs efs
+type (:!) efs = EffF ExtensibleUnion (FreerFinal Monad) efs
+
+infixr 5 :!!
+infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/ExtensibleFinalA.hs

@@ -0,0 +1,43 @@
+-- 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-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the final-encoded Freer applicative.
+-}
+module Control.Effect.ExtensibleFinalA where
+
+import Control.Effect (type (~>))
+import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
+import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Control.Freer.Final (FreerFinal)
+import Data.Effect (LiftIns)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+type eh !! ef = Effectful ExtensibleUnion (FreerFinal Applicative) eh ef
+type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Applicative) ef
+
+infixr 5 !!
+infixr 4 !
+
+type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Applicative) ehs efs
+type (:!) efs = EffF ExtensibleUnion (FreerFinal Applicative) efs
+
+infixr 5 :!!
+infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/ExtensibleTree.hs

@@ -13,9 +13,13 @@ Type operators for extensible effectful programs based on the tree-structured en
 -}
 module Control.Effect.ExtensibleTree where
 
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
 import Control.Monad.Freer.Tree (FreerTree)
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion FreerTree eh ef
@@ -29,3 +33,11 @@ type (:!) efs = EffF ExtensibleUnion FreerTree efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/ExtensibleTreeA.hs

@@ -17,8 +17,12 @@ See "Control.Applicative.Free".
 module Control.Effect.ExtensibleTreeA where
 
 import Control.Applicative.Free (Ap)
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion Ap eh ef
@@ -32,3 +36,11 @@ type (:!) efs = EffF ExtensibleUnion Ap efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/Free.hs

@@ -18,18 +18,18 @@ module Control.Effect.Free where
 
 import Control.Effect (type (~>))
 
-import Control.Effect.Hefty (Eff, EffUnion (EffUnion), MemberF, SumToUnionListNF, caseHF)
+import Control.Effect.Hefty (Eff, EffUnion (EffUnion), MemberF, caseHF)
 import Control.Freer (Freer, InjectIns, ViaFreer (ViaFreer), injectIns, transformFreer, viaFreer)
 import Control.Hefty (Hefty (Hefty), unHefty)
 import Data.Effect (LiftIns (LiftIns), Nop, SigClass)
 import Data.Free.Sum (pattern R1)
-import Data.Hefty.Union (Union, exhaust, injectRec)
+import Data.Hefty.Union (U, Union, exhaust, injectRec)
 
 {- |
 A common type for representing first-order extensible effectful programs that can issue effects
 belonging to the specified sum of effect classes.
 -}
-type EffectfulF u fr e = EffF u fr (SumToUnionListNF u e)
+type EffectfulF u fr e = EffF u fr (U u e)
 
 {- |
 A common type for representing first-order extensible effectful programs that can issue effects
@@ -51,12 +51,12 @@ toEffF =
         . unHefty
 {-# INLINE toEffF #-}
 
-fromEffectfulF :: forall es fr u c. Freer c fr => EffF u fr es ~> Eff u fr '[] es
-fromEffectfulF =
+fromEffF :: forall es fr u c. Freer c fr => EffF u fr es ~> Eff u fr '[] es
+fromEffF =
     Hefty
         . transformFreer (EffUnion . R1 . unEffUnionF)
         . viaFreer
-{-# INLINE fromEffectfulF #-}
+{-# INLINE fromEffF #-}
 
 {-  all types of interpret-family functions:
         - interpret   :                 e  ~> E r           ->    E (e + r)  ~> E r
@@ -76,3 +76,7 @@ fromEffectfulF =
 
     todo patterns: all ( 4x3 + 3 = 16 functions )
 -}
+
+runEffF :: forall f fr u c. (Freer c fr, Union u, c f) => EffF u fr '[LiftIns f] ~> f
+runEffF = undefined
+{-# INLINE runEffF #-}

heftia/src/Control/Effect/Hefty.hs

@@ -24,37 +24,37 @@ import Control.Monad.Freer (MonadFreer, interpretFreerK)
 import Control.Monad.Identity (Identity (Identity))
 import Control.Monad.Trans (MonadTrans)
 import Data.Coerce (coerce)
-import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)
+import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)
 import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:))
 import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
 import Data.Hefty.Union (
-    ForallHFunctor,
     HFunctorUnion,
-    HasMembership,
+    HFunctorUnion_ (ForallHFunctor),
+    HeadIns,
+    LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),
     MemberRec,
-    Union,
-    exhaust,
-    inject0,
+    U,
+    UH,
+    Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)),
+    UnliftIfSingle,
     injectRec,
     projectRec,
-    weaken,
-    weakenUnder,
-    (|+:),
+    (|+),
  )
 import Data.Kind (Type)
 
-{- |
-A common type for representing first-order and higher-order extensible effectful programs that can
-issue effects belonging to the specified sum of effect classes.
--}
-type Effectful u fr eh ef = Eff u fr (SumToUnionListNH u eh) (SumToUnionListNF u ef)
-
 {- |
 A common type for representing first-order and higher-order extensible effectful programs that can
 issue effects belonging to the specified list of effect classes.
 -}
 type Eff u fr ehs efs = Hefty fr (EffUnion u ehs efs)
 
+{- |
+A common type for representing first-order and higher-order extensible effectful programs that can
+issue effects belonging to the specified sum of effect classes.
+-}
+type Effectful u fr eh ef = Eff u fr (UH u eh) (U u ef)
+
 {- |
 A common wrapper data type for representing first-order and higher-order extensible effect union.
 -}
@@ -90,75 +90,7 @@ type (f :: Type -> Type) $ a = f a
 -- | Type-level infix applcation for higher-order functors.
 type (h :: (Type -> Type) -> Type -> Type) $$ f = h f
 
-{- |
-Recursively decompose the sum of higher-order effects into a list, following the direction of right
-association, with normalization.
--}
-type SumToUnionListNH u eh = SumToUnionList u (NormalizeSig eh)
-
-{- |
-Recursively decompose the sum of first-order effects into a list, following the direction of right
-association, with normalization.
--}
-type SumToUnionListNF u ef = SumToUnionListNH u (LiftIns ef)
-
-{- |
-Recursively decompose the sum of higher-order effects into a list, following the direction of right
-association.
--}
-type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where
-    SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2
-    SumToUnionList u LNop = '[]
-    SumToUnionList u (SingleSig e) = '[e]
-
-{- |
-Convert a given list of higher-order effect classes into a suitable representation type for each
-case of being empty, single, or multiple.
--}
-type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
-    MultiListToUnion u '[] = LNop
-    MultiListToUnion u '[e] = e
-    MultiListToUnion u es = u es
-
-{- |
-Normalization in preparation for decomposing the sum of effect classes into a list.
-
-In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it.
--}
-type family NormalizeSig e where
-    NormalizeSig (LiftIns Nop) = LiftIns Nop
-    NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)
-    NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2
-    NormalizeSig e = SingleSig e
-
-{- |
-A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as
-a sum.
--}
-newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
-    deriving newtype (HFunctor)
-
-type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le
-
-type family UnliftIfSingle e where
-    UnliftIfSingle (LiftIns e) = e
-    UnliftIfSingle e = e Nop
-
-class LiftInsIfSingle e le where
-    liftInsIfSingle :: e ~> le Nop
-    unliftInsIfSingle :: le Nop ~> e
-
-instance LiftInsIfSingle (e Nop) e where
-    liftInsIfSingle = id
-    unliftInsIfSingle = id
-    {-# INLINE liftInsIfSingle #-}
-    {-# INLINE unliftInsIfSingle #-}
-
-instance LiftInsIfSingle e (LiftIns e) where
-    liftInsIfSingle = LiftIns
-    unliftInsIfSingle = unliftIns
-    {-# INLINE liftInsIfSingle #-}
-    {-# INLINE unliftInsIfSingle #-}
+type Elab e f = e f ~> f
 
 injectH :: (Freer c f, HFunctor (u ehs)) => u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
 injectH = Hefty . liftIns . EffUnion . L1
@@ -199,7 +131,7 @@ injectF = Hefty . liftIns . EffUnion . R1
             - FH
 
     todo patterns:
-        - translate*, rewrite* in tramsform-family ( 2x3 = 6 functions )
+        - translate* in tramsform-family ( 3 functions )
         - *{FH,FH_} in interpret-family ( (4x2+1) + 2 = 11 functions )
 -}
 
@@ -228,7 +160,7 @@ interpretH_ ::
 interpretH_ i = interpretAllH_ $ i |+: exhaust
 {-# INLINE interpretH_ #-}
 
--- | Interpret the leading first-order effect class using a delimited continuation.
+-- | Interpret the leading first-order effect class using delimited continuations.
 interpretK ::
     forall e rs r a ehs fr u.
     (MonadFreer fr, Union u, HeadIns e) =>
@@ -755,6 +687,48 @@ transformFH fh ff =
         (inject0 . (liftInsIfSingle . ff . unliftInsIfSingle) |+: weaken)
 {-# INLINE transformFH #-}
 
+rewrite ::
+    forall e efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberF u e efs) =>
+    (e ~> e) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewrite f =
+    transformAll
+        \u -> case projectRec u of
+            Just (LiftIns e) -> injectRec $ LiftIns $ f e
+            Nothing -> u
+{-# INLINE rewrite #-}
+
+rewriteH ::
+    forall e efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberH u e ehs) =>
+    (e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewriteH f =
+    transformAllH
+        \u -> case projectRec u of
+            Just e -> injectRec $ f e
+            Nothing -> u
+{-# INLINE rewriteH #-}
+
+rewriteFH ::
+    forall eh ef efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberH u eh ehs, MemberF u ef efs) =>
+    (eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)) ->
+    (ef ~> ef) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewriteFH fh ff =
+    transformAllFH
+        ( \u -> case projectRec u of
+            Just e -> injectRec $ fh e
+            Nothing -> u
+        )
+        ( \u -> case projectRec u of
+            Just (LiftIns e) -> injectRec $ LiftIns $ ff e
+            Nothing -> u
+        )
+{-# INLINE rewriteFH #-}
+
 transformAll ::
     forall efs' efs ehs fr u c.
     (Freer c fr, Union u, HFunctor (u ehs)) =>
@@ -852,3 +826,7 @@ send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle
 send0H :: (Freer c fr, Union u) => e (Eff u fr (e ': r) ef) ~> Eff u fr (e ': r) ef
 send0H = Hefty . liftIns . EffUnion . L1 . inject0
 {-# INLINE send0H #-}
+
+runEff :: forall f fr u c. (Freer c fr, Union u, c f) => Eff u fr '[] '[LiftIns f] ~> f
+runEff = interpretAll $ id |+ exhaust
+{-# INLINE runEff #-}

heftia/src/Control/Freer.hs

@@ -18,6 +18,7 @@ module Control.Freer where
 
 import Control.Applicative (Alternative)
 import Control.Applicative.Free (Ap, liftAp, runAp)
+import Control.Applicative.Free.Fast qualified as Fast
 import Control.Effect (SendIns, sendIns, type (~>))
 import Control.Monad (MonadPlus)
 import Control.Monad.Base (MonadBase)
@@ -65,6 +66,12 @@ instance Freer Applicative Ap where
     {-# INLINE liftIns #-}
     {-# INLINE interpretFreer #-}
 
+instance Freer Applicative Fast.Ap where
+    liftIns = Fast.liftAp
+    interpretFreer = Fast.runAp
+    {-# INLINE liftIns #-}
+    {-# INLINE interpretFreer #-}
+
 newtype
     ViaFreer
         (fr :: InsClass -> Type -> Type)

heftia/src/Control/Freer/Final.hs

@@ -0,0 +1,115 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Use fmap" #-}
+{-# HLINT ignore "Use const" #-}
+{-# HLINT ignore "Avoid lambda" #-}
+
+-- 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
+
+A final-encoded generic Freer carrier.
+-}
+module Control.Freer.Final where
+
+import Control.Applicative (Alternative, empty, liftA2, many, some, (<|>))
+import Control.Effect (type (~>))
+import Control.Freer (Freer, interpretFreer, liftIns)
+import Control.Monad (MonadPlus, mplus, mzero)
+import Control.Monad.Freer (MonadFreer)
+
+-- | A final-encoded generic Freer carrier.
+newtype FreerFinal c f a = FreerFinal {unFreerFinal :: forall m. c m => (f ~> m) -> m a}
+
+deriving stock instance (forall f. c f => Functor f) => Functor (FreerFinal c e)
+
+instance
+    (forall f. c f => Applicative f, Functor (FreerFinal c e)) =>
+    Applicative (FreerFinal c e)
+    where
+    pure x = FreerFinal \_ -> pure x
+
+    FreerFinal f <*> FreerFinal g =
+        FreerFinal \i -> f i <*> g i
+
+    liftA2 f (FreerFinal fa) (FreerFinal fb) =
+        FreerFinal \i -> liftA2 f (fa i) (fb i)
+
+    FreerFinal f *> FreerFinal g =
+        FreerFinal \i -> f i *> g i
+
+    FreerFinal f <* FreerFinal g =
+        FreerFinal \i -> f i <* g i
+
+    {-# INLINE pure #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+
+instance
+    (forall f. c f => Alternative f, Applicative (FreerFinal c e)) =>
+    Alternative (FreerFinal c e)
+    where
+    empty = FreerFinal \_ -> empty
+
+    FreerFinal f <|> FreerFinal g =
+        FreerFinal \i -> f i <|> g i
+
+    some (FreerFinal f) = FreerFinal \i -> some (f i)
+    many (FreerFinal f) = FreerFinal \i -> many (f i)
+
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
+    {-# INLINE some #-}
+    {-# INLINE many #-}
+
+instance (forall m. c m => Monad m, Applicative (FreerFinal c f)) => Monad (FreerFinal c f) where
+    FreerFinal f >>= k =
+        FreerFinal \i ->
+            f i >>= interpretFreerFinal i . k
+
+    (>>) = (*>)
+    return = pure
+
+    {-# INLINE (>>=) #-}
+    {-# INLINE (>>) #-}
+    {-# INLINE return #-}
+
+instance
+    (forall m. c m => MonadPlus m, Alternative (FreerFinal c f), Monad (FreerFinal c f)) =>
+    MonadPlus (FreerFinal c f)
+    where
+    mzero = FreerFinal \_ -> mzero
+
+    FreerFinal f `mplus` FreerFinal g =
+        FreerFinal \i -> f i `mplus` g i
+
+    {-# INLINE mzero #-}
+    {-# INLINE mplus #-}
+
+interpretFreerFinal :: c f => (e ~> f) -> FreerFinal c e a -> f a
+interpretFreerFinal i (FreerFinal f) = f i
+{-# INLINE interpretFreerFinal #-}
+
+liftInsFinal :: ins a -> FreerFinal c ins a
+liftInsFinal e = FreerFinal \i -> i e
+{-# INLINE liftInsFinal #-}
+
+instance (forall e. c (FreerFinal c e)) => Freer c (FreerFinal c) where
+    liftIns = liftInsFinal
+    interpretFreer = interpretFreerFinal
+    {-# INLINE liftIns #-}
+    {-# INLINE interpretFreer #-}
+
+instance MonadFreer (FreerFinal Monad)

heftia/src/Control/Hefty.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- This Source Code Form is subject to the terms of the Mozilla Public

heftia/src/Control/Monad/Freer.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
 {-# HLINT ignore "Eta reduce" #-}
@@ -12,7 +14,15 @@ import Control.Effect (type (~>))
 import Control.Freer (Freer, interpretFreer)
 import Control.Monad.Cont (Cont)
 
-class Freer Monad f => MonadFreer f where
-    interpretFreerK :: (e ~> Cont r) -> f e ~> Cont r
+class Freer Monad fr => MonadFreer fr where
+    interpretFreerK :: (e ~> Cont r) -> fr e ~> Cont r
     interpretFreerK i = interpretFreer i
     {-# INLINE interpretFreerK #-}
+
+{-
+class (Freer c fr, forall f. c f => Monad f) => MonadFreer c fr where
+    interpretFreerK :: (e ~> Cont r) -> fr e ~> Cont r
+    default interpretFreerK :: c (Cont r) => (e ~> Cont r) -> fr e ~> Cont r
+    interpretFreerK i = interpretFreer i
+    {-# INLINE interpretFreerK #-}
+-}

heftia/src/Data/Hefty/Union.hs

@@ -22,9 +22,9 @@ module Data.Hefty.Union where
 import Control.Effect (type (~>))
 import Control.Monad ((<=<))
 import Data.Bool.Singletons (SBool (SFalse, STrue))
-import Data.Coerce (Coercible)
-import Data.Effect (LiftIns, SigClass, unliftIns)
+import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)
 import Data.Effect.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))
+import Data.Free.Sum (type (+))
 import Data.Kind (Constraint)
 import Data.Singletons (SingI, sing)
 import Data.Type.Bool (If, type (||))
@@ -305,3 +305,91 @@ infixr 5 |+
 (|+) :: Union u => (e a -> r) -> (u es f a -> r) -> u (LiftIns e ': es) f a -> r
 f |+ g = f . unliftIns |+: g
 {-# INLINE (|+) #-}
+
+{- |
+Recursively decompose the sum of first-order effects into a list, following the direction of right
+association, with normalization.
+-}
+type U u ef = UH u (LiftIns ef)
+
+{- |
+Recursively decompose the sum of higher-order effects into a list, following the direction of right
+association, with normalization.
+-}
+type UH u eh = SumToUnionList u (NormalizeSig eh)
+
+{- |
+Recursively decompose the sum of higher-order effects into a list, following the direction of right
+association.
+-}
+type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where
+    SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2
+    SumToUnionList u LNop = '[]
+    SumToUnionList u (SingleSig e) = '[e]
+
+{- |
+Convert a given list of higher-order effect classes into a suitable representation type for each
+case of being empty, single, or multiple.
+-}
+type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
+    MultiListToUnion u '[] = LNop
+    MultiListToUnion u '[e] = e
+    MultiListToUnion u es = u es
+
+{- |
+Normalization in preparation for decomposing the sum of effect classes into a list.
+
+In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it.
+-}
+type family NormalizeSig e where
+    NormalizeSig LNop = LNop
+    NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)
+    NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2
+    NormalizeSig e = SingleSig e
+
+{- |
+A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as
+a sum.
+-}
+newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
+    deriving newtype (HFunctor)
+
+type family UnionListToSum (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
+    UnionListToSum u '[e] = UnionToSum u e
+    UnionListToSum u '[] = LNop
+    UnionListToSum u (e ': r) = UnionToSum u e :+: UnionListToSum u r
+
+type family UnionToSum (u :: [SigClass] -> SigClass) (e :: SigClass) :: SigClass where
+    UnionToSum u (u es) = UnionListToSum u es
+    UnionToSum u e = e
+
+type S u es = UnionListToSum u es Nop
+type SH u es = UnionListToSum u es
+
+type NormalFormUnionList u es = U u (S u es) ~ es
+type NormalFormUnionListH u es = UH u (SH u es) ~ es
+
+type NFU u es = NormalFormUnionList u es
+type NFUH u es = NormalFormUnionListH u es
+
+type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le
+
+type family UnliftIfSingle e where
+    UnliftIfSingle (LiftIns e) = e
+    UnliftIfSingle e = e Nop
+
+class LiftInsIfSingle e le where
+    liftInsIfSingle :: e ~> le Nop
+    unliftInsIfSingle :: le Nop ~> e
+
+instance LiftInsIfSingle (e Nop) e where
+    liftInsIfSingle = id
+    unliftInsIfSingle = id
+    {-# INLINE liftInsIfSingle #-}
+    {-# INLINE unliftInsIfSingle #-}
+
+instance LiftInsIfSingle e (LiftIns e) where
+    liftInsIfSingle = LiftIns
+    unliftInsIfSingle = unliftIns
+    {-# INLINE liftInsIfSingle #-}
+    {-# INLINE unliftInsIfSingle #-}