heftia 0.1.0.0 → 0.2.0.0

raw patch · 35 files changed

+2825/−2743 lines, 35 filesdep +data-effectsdep +singletons-basedep +singletons-thdep −classy-effects-basePVP ok

version bump matches the API change (PVP)

Dependencies added: data-effects, singletons-base, singletons-th, unliftio

Dependencies removed: classy-effects-base

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• README.md +177/−51
• heftia.cabal +42/−25
• src/Control/Effect/ExtensibleChurch.hs +43/−0
• src/Control/Effect/ExtensibleFastA.hs +45/−0
• src/Control/Effect/ExtensibleFinal.hs +43/−0
• src/Control/Effect/ExtensibleFinalA.hs +43/−0
• src/Control/Effect/ExtensibleTree.hs +43/−0
• src/Control/Effect/ExtensibleTreeA.hs +46/−0
• src/Control/Effect/Free.hs +85/−0
• src/Control/Effect/Freer.hs +0/−632
• src/Control/Effect/Heftia.hs +0/−760
• src/Control/Effect/Hefty.hs +1114/−0
• src/Control/Freer.hs +127/−23
• src/Control/Freer/Final.hs +115/−0
• src/Control/Freer/Trans.hs +0/−70
• src/Control/Heftia.hs +0/−45
• src/Control/Heftia/Trans.hs +0/−89
• src/Control/Hefty.hs +182/−0
• src/Control/Monad/Freer.hs +21/−0
• src/Control/Monad/Freer/Church.hs +58/−0
• src/Control/Monad/Freer/Tree.hs +74/−0
• src/Control/Monad/Trans/Freer.hs +0/−71
• src/Control/Monad/Trans/Freer/Church.hs +0/−56
• src/Control/Monad/Trans/Freer/Tree.hs +0/−83
• src/Control/Monad/Trans/Heftia.hs +0/−82
• src/Control/Monad/Trans/Heftia/Church.hs +0/−77
• src/Control/Monad/Trans/Heftia/Tree.hs +0/−20
• src/Control/Monad/Trans/Hefty.hs +0/−72
• src/Data/Free/Extensible.hs +0/−92
• src/Data/Free/Sum.hs +7/−89
• src/Data/Free/Union.hs +0/−150
• src/Data/Hefty/Extensible.hs +82/−34
• src/Data/Hefty/Sum.hs +0/−123
• src/Data/Hefty/Union.hs +473/−99

@@ -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.

@@ -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

@@ -1,15 +1,19 @@ cabal-version:      2.4 name:               heftia-version:            0.1.0.0+version:            0.2.0.0  -- A short (one-line) description of the package.-synopsis: Higher-order version of Freer.+synopsis: higher-order effects done right  -- A longer description of the package. description:-    Heftia, a composition of hefty trees and co-Yoneda, is a higher-order-    effects version of Freer.+    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@@ -20,7 +24,7 @@     Hefty trees, proposed by the above paper, are extensions of free monads,     allowing for a straightforward treatment of higher-order effects.     .-    This library provides Heftia monads and Freer monads, encoded into data+    This library provides Hefty monads and Freer monads, encoded into data     types in several ways to enable tuning in pursuit of high performance.     . @@ -35,8 +39,7 @@  -- A copyright notice. copyright:-    2023 Yamada Ryo,-    2023 Casper Bach Poulsen and Cas van der Rest+    2023-2024 Yamada Ryo category: Control, Monads  extra-source-files:@@ -50,31 +53,42 @@ source-repository head     type: git     location: https://github.com/sayo-hs/heftia-    tag: v0.1.0+    tag: v0.2.0     subdir: heftia  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.Trans-        Control.Heftia-        Control.Heftia.Trans-        Control.Monad.Trans.Freer-        Control.Monad.Trans.Freer.Tree-        Control.Monad.Trans.Freer.Church-        Control.Monad.Trans.Heftia-        Control.Monad.Trans.Heftia.Tree-        Control.Monad.Trans.Heftia.Church-        Control.Monad.Trans.Hefty-        Control.Effect.Freer-        Control.Effect.Heftia-        Data.Free.Union-        Data.Free.Extensible-        Data.Free.Sum+        Control.Freer.Final+        Control.Monad.Freer+        Control.Monad.Freer.Church+        Control.Monad.Freer.Tree         Data.Hefty.Union         Data.Hefty.Extensible-        Data.Hefty.Sum+        Data.Free.Sum +    reexported-modules:+        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,+     -- Modules included in this executable, other than Main.     -- other-modules: @@ -82,7 +96,7 @@     -- other-extensions:     build-depends:         base                          ^>= 4.16.4.0,-        classy-effects-base           ^>= 0.1,+        data-effects                ^>= 0.1,         mtl ^>= 2.2.2,         free ^>= 5.2,         kan-extensions ^>= 5.2.5,@@ -91,6 +105,9 @@         transformers ^>= 0.5.6,         extensible ^>= 0.9,         membership == 0.0.1,+        singletons-base ^>= 3.1,+        singletons-th ^>= 3.1,+        unliftio ^>= 0.2,      hs-source-dirs:   src     ghc-options:      -Wall

@@ -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 Church-encoded Freer monad.+-}+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+type (!) ef = EffectfulF ExtensibleUnion FreerChurch ef++infixr 5 !!+infixr 4 !++type ehs :!! efs = Eff ExtensibleUnion FreerChurch ehs efs+type (:!) efs = EffF ExtensibleUnion FreerChurch efs++infixr 4 :!!+infixr 3 :!++runEff :: Monad f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Monad f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -0,0 +1,45 @@+-- 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 fast-encoded free applicative.++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+type (!) ef = EffectfulF ExtensibleUnion Ap ef++infixr 5 !!+infixr 4 !++type ehs :!! efs = Eff ExtensibleUnion Ap ehs efs+type (:!) efs = EffF ExtensibleUnion Ap efs++infixr 4 :!!+infixr 3 :!++runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Applicative f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -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 4 :!!+infixr 3 :!++runEff :: Monad f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Monad f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -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 4 :!!+infixr 3 :!++runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Applicative f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -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 tree-structured encoded Freer monad.+-}+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+type (!) ef = EffectfulF ExtensibleUnion FreerTree ef++infixr 5 !!+infixr 4 !++type ehs :!! efs = Eff ExtensibleUnion FreerTree ehs efs+type (:!) efs = EffF ExtensibleUnion FreerTree efs++infixr 4 :!!+infixr 3 :!++runEff :: Monad f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Monad f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -0,0 +1,46 @@+-- 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 tree-structured encoded free+applicative.++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+type (!) ef = EffectfulF ExtensibleUnion Ap ef++infixr 5 !!+infixr 4 !++type ehs :!! efs = Eff ExtensibleUnion Ap ehs efs+type (:!) efs = EffF ExtensibleUnion Ap efs++infixr 4 :!!+infixr 3 :!++runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f+runEff = H.runEff+{-# INLINE runEff #-}++runEffF :: Applicative f => (:!) '[LiftIns f] ~> f+runEffF = F.runEffF+{-# INLINE runEffF #-}

@@ -0,0 +1,85 @@+{-# LANGUAGE UndecidableInstances #-}++-- 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++A Freer carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+module Control.Effect.Free where++import Control.Effect (type (~>))++import Control.Effect.Hefty (Eff, EffUnion (EffUnion), caseHF)+import Control.Freer (Freer, InjectIns, ViaFreer (ViaFreer), injectIns, interpretFreer, 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 (Member, 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 (U u e)++{- |+A common type for representing first-order extensible effectful programs that can issue effects+belonging to the specified list of effect classes.+-}+type EffF u fr es = ViaFreer fr (EffUnionF u es)++-- | A common wrapper data type for representing first-order extensible effect union.+newtype EffUnionF (u :: [SigClass] -> SigClass) es a = EffUnionF {unEffUnionF :: u es Nop a}++instance Member u e es => InjectIns e (EffUnionF u es) where+    injectIns = EffUnionF . injectRec . LiftIns+    {-# INLINE injectIns #-}++toEffF :: forall es fr u c. (Freer c fr, Union u) => Eff u fr '[] es ~> EffF u fr es+toEffF =+    ViaFreer+        . transformFreer (caseHF exhaust EffUnionF)+        . unHefty+{-# INLINE toEffF #-}++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 fromEffF #-}++{-  all types of interpret-family functions:+        - interpret   :                 e  ~> E r           ->    E (e + r)  ~> E r+        - reinterpret :                 e1 ~> E (e2 + r)    ->    E (e1 + r) ~> E (e2 + r)+        - interpose   :  e <| es  =>    e  ~> E es          ->    E es       ~> E es++        all possible suffix patterns of interpret-family functions:+            - <none>+            - K+            - ContT+            - Fin+            - T++    all types of transform-family functions:+        - transform :                  e1 ~> e2    ->    E (e1 + r) ~> E (e2 + r)+        - translate :  e2 <| r   =>    e1 ~> e2    ->    E (e1 + r) ~> E r+        - rewrite   :  e  <| es  =>    e  ~> e     ->    E es       ~> E es++    todo patterns: all ( 5x3 + 3 = 18 functions )++        + *By (for keyed effects) in interpose/translate/rewrite ( 5 + 2 = 7 functions )+-}++runEffF :: forall f fr u c. (Freer c fr, Union u, c f) => EffF u fr '[LiftIns f] ~> f+runEffF (ViaFreer f) = interpretFreer ((id |+ exhaust) . unEffUnionF) f+{-# INLINE runEffF #-}

@@ -1,632 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE PartialTypeSignatures #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE UndecidableInstances #-}---- 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 Freer carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).--}-module Control.Effect.Freer where--import Control.Applicative (Alternative)-import Control.Effect.Class (-    EffectDataHandler,-    EffectsVia (EffectsVia),-    Instruction,-    SendIns,-    Tag,-    getTag,-    runEffectsVia,-    sendIns,-    type (~>),- )-import Control.Freer.Trans (-    TransFreer,-    hoistFreer,-    interposeLowerT,-    interpretFT,-    liftInsT,-    liftLowerFT,-    reinterpretFT,-    runInterpretF,-    transformT,- )-import Control.Monad (MonadPlus)-import Control.Monad.Cont (ContT (ContT), runContT)-import Control.Monad.IO.Class (MonadIO, liftIO)-import Control.Monad.Trans (MonadTrans, lift)-import Control.Monad.Trans.Freer (MonadTransFreer, interpretMK, interpretMT, reinterpretMK, reinterpretMT)-import Control.Monad.Trans.Freer.Church (FreerChurchT)-import Data.Coerce (Coercible, coerce)-import Data.Free.Extensible (ExtensibleUnion)-import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))-import Data.Free.Union (-    IsMember,-    Member,-    Union (-        absurdUnion,-        bundleUnion2,-        bundleUnion3,-        bundleUnion4,-        decomp,-        flipUnion,-        flipUnion3,-        flipUnionUnder,-        inject,-        inject0,-        project,-        rot3,-        rot3',-        unbundleUnion2,-        unbundleUnion3,-        unbundleUnion4,-        weaken,-        weaken2,-        weaken2Under,-        weaken2Under2,-        weaken3,-        weaken3Under,-        weaken4,-        weakenUnder,-        weakenUnder2,-        weakenUnder3-    ),-    (|+|:),- )-import Data.Function ((&))-import Data.Kind (Type)--{- |-A data type that wraps Freer with any encoding to become an instance of 'SendIns' based on the-`liftInsT` from the `TransFreer` type class.--}-newtype-    FreerUnion-        (fr :: Instruction -> (Type -> Type) -> Type -> Type)-        u-        (es :: [Instruction])-        f-        a = FreerUnion {runFreerUnion :: fr (u es) f a}-    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)-    deriving stock (Foldable, Traversable)--{- |-A Freer carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).--}-type FreerEffects fr u es f = EffectsVia EffectDataHandler (FreerUnion fr u es f)---- | Unwrap the `FreerEffects` wrapper.-unFreerEffects :: FreerEffects fr u es f ~> fr (u es) f-unFreerEffects = runFreerUnion . runEffectsVia-{-# INLINE unFreerEffects #-}---- | Wrap with `FreerEffects`.-freerEffects :: fr (u es) f ~> FreerEffects fr u es f-freerEffects = EffectsVia . FreerUnion-{-# INLINE freerEffects #-}--{- |-A wrapper data type designed to induce instance resolution to delegate the search for effect classes-to a lower carrier @f@ even when there are no target effect classes in the effect class list @es@.--When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it-doesn't exist, it's induced to be @'False@.--}-newtype FreerUnionForSend handleHere fr u es f a = FreerUnionForSend-    {runFreerUnionForSend :: FreerUnion fr u es f a}-    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)-    deriving stock (Foldable, Traversable)--instance-    SendIns e (FreerUnionForSend (e `IsMember` es) fr u es f) =>-    SendIns e (FreerUnion fr u es f)-    where-    sendIns = runFreerUnionForSend @(e `IsMember` es) . sendIns-    {-# INLINE sendIns #-}--instance-    (TransFreer c fr, Union u, Member u e es) =>-    SendIns e (FreerUnionForSend 'True fr u es f)-    where-    sendIns = FreerUnionForSend . FreerUnion . liftInsT . inject-    {-# INLINE sendIns #-}--instance (TransFreer c fr, SendIns e f, c f) => SendIns e (FreerUnionForSend 'False fr u es f) where-    sendIns = FreerUnionForSend . FreerUnion . liftLowerFT . sendIns-    {-# INLINE sendIns #-}---- | Interpret the leading effect class in the effect class list.-interpret ::-    (TransFreer c fr, Union u, c f) =>-    (e ~> FreerEffects fr u es f) ->-    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f-interpret i =-    overFreerEffects $ interpretFT liftLowerFT \u ->-        case decomp u of-            Left e -> unFreerEffects $ i e-            Right e -> liftInsT e---- | Interpret the leading effect class in the effect class list using a monad transformer.-interpretT ::-    forall t fr u e es f.-    (MonadTransFreer fr, Union u, MonadTrans t, Monad f, Monad (t (FreerEffects fr u es f))) =>-    (e ~> t (FreerEffects fr u es f)) ->-    FreerEffects fr u (e ': es) f ~> t (FreerEffects fr u es f)-interpretT i = interpretMT i . splitFreerEffects @_ @fr-{-# INLINE interpretT #-}---- | Interpret the leading effect class in the effect class list using a delimited continuation.-interpretK ::-    (MonadTransFreer fr, Union u, Monad f) =>-    (a -> FreerEffects fr u es f r) ->-    (forall x. (x -> FreerEffects fr u es f r) -> e x -> FreerEffects fr u es f r) ->-    FreerEffects fr u (e ': es) f a ->-    FreerEffects fr u es f r-interpretK k i = (`runContT` k) . interpretContT \e -> ContT (`i` e)-{-# INLINE interpretK #-}--{- |-Interpret the leading effect class in the effect class list using a continuation monad transformer.--}-interpretContT ::-    forall r fr u e es f.-    (MonadTransFreer fr, Union u, Monad f) =>-    (e ~> ContT r (FreerEffects fr u es f)) ->-    FreerEffects fr u (e ': es) f ~> ContT r (FreerEffects fr u es f)-interpretContT i = interpretMK i . splitFreerEffects @_ @fr-{-# INLINE interpretContT #-}--{- |-Interpret not only the leading effect class but also all the remaining effect classes and the-underlying carrier simultaneously, transforming them into any carrier @g@.--}-interpretAll ::-    (TransFreer c fr, Union u, c f, c g) =>-    (f ~> g) ->-    (u es ~> g) ->-    (e ~> g) ->-    FreerEffects fr u (e ': es) f ~> g-interpretAll iLower iOther iTarget a =-    unFreerEffects a & interpretFT iLower \u ->-        case decomp u of-            Left e -> iTarget e-            Right e -> iOther e---- | Reinterpret the leading effect class in the effect class list.-reinterpret ::-    (TransFreer c fr, Union u, c f) =>-    (e ~> FreerEffects fr u (e ': es) f) ->-    FreerEffects fr u (e ': es) f ~> FreerEffects fr u (e ': es) f-reinterpret i =-    overFreerEffects $ reinterpretFT \u ->-        case decomp u of-            Left e -> unFreerEffects $ i e-            Right e -> liftInsT $ weaken e---- | Transform all effect classes in the effect class list into another union of effect classes.-transformAll ::-    (TransFreer c fr, Union u, Union u', c f) =>-    (u es ~> u' es') ->-    FreerEffects fr u es f ~> FreerEffects fr u' es' f-transformAll f = overFreerEffects $ transformT f-{-# INLINE transformAll #-}---- | Transform the leading effect class in the effect class list into another effect class.-transform ::-    forall e' e fr u r f c.-    (TransFreer c fr, Union u, c f) =>-    (e ~> e') ->-    FreerEffects fr u (e ': r) f ~> FreerEffects fr u (e' ': r) f-transform f =-    overFreerEffects $ transformT \u ->-        case decomp u of-            Left e -> inject0 $ f e-            Right e -> weaken e---- | Remove the tag attached to the effect class.-untag ::-    forall tag e fr u r f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (Tag e tag ': r) f ~> FreerEffects fr u (e ': r) f-untag = transform getTag---- | Interpose the effect class that exists within the effect class list.-interpose ::-    forall e fr u es f c.-    (TransFreer c fr, Union u, Member u e es, c f) =>-    (e ~> FreerEffects fr u es f) ->-    FreerEffects fr u es f ~> FreerEffects fr u es f-interpose f =-    overFreerEffects $ reinterpretFT \u ->-        case project @_ @e u of-            Just e -> unFreerEffects $ f e-            Nothing -> liftInsT u---- | Interpose the effect class that exists within the effect class list using a monad transformer.-interposeT ::-    forall e t fr u es m.-    ( MonadTransFreer fr-    , Union u-    , Member u e es-    , Monad m-    , MonadTrans t-    , forall m1 m2 x. Coercible m1 m2 => Coercible (t m1 x) (t m2 x)-    , Monad (t (fr (u es) m))-    ) =>-    (e ~> t (FreerEffects fr u es m)) ->-    FreerEffects fr u es m ~> t (FreerEffects fr u es m)-interposeT f a =-    hoistT @(fr (u es) m) $-        unFreerEffects a & reinterpretMT \u ->-            case project @_ @e u of-                Just e -> hoistT $ f e-                Nothing -> lift $ liftInsT u-  where-    hoistT :: Coercible (t m1 a) (t m2 a) => t m1 a -> t m2 a-    hoistT = coerce-    {-# INLINE hoistT #-}--{- |-Transform all other effect classes in the effect class list and the underlying carrier, along-with the effect class that exists within the effect class list, into any carrier @g@.--}-interposeAll ::-    forall e g fr u es f c.-    ( TransFreer c fr-    , Union u-    , Member u e es-    , c f-    , c g-    ) =>-    (f ~> g) ->-    (u es ~> g) ->-    (e ~> g) ->-    FreerEffects fr u es f ~> g-interposeAll iLower iOther iTarget a =-    unFreerEffects a & interpretFT iLower \u ->-        case project @_ @e u of-            Just e -> iTarget e-            Nothing -> iOther u--{- |-Interpose the effect class that exists within the effect class list using a delimited continuation.--}-interposeK ::-    (MonadTransFreer fr, Union u, Member u e es, Monad m) =>-    (a -> FreerEffects fr u es m r) ->-    (forall x. (x -> FreerEffects fr u es m r) -> e x -> FreerEffects fr u es m r) ->-    FreerEffects fr u es m a ->-    FreerEffects fr u es m r-interposeK k i = (`runContT` k) . interposeContT \e -> ContT (`i` e)-{-# INLINE interposeK #-}--{- |-Interpose the effect class that exists within the effect class list using a continuation monad-transformer.--}-interposeContT ::-    forall e r fr u es m.-    (MonadTransFreer fr, Union u, Member u e es, Monad m) =>-    (e ~> ContT r (FreerEffects fr u es m)) ->-    FreerEffects fr u es m ~> ContT r (FreerEffects fr u es m)-interposeContT f a =-    hoistContT $-        unFreerEffects a & reinterpretMK \u ->-            case project @_ @e u of-                Just e -> hoistContT $ f e-                Nothing -> lift $ liftInsT u-  where-    hoistContT :: Coercible m1 m2 => ContT r m1 a -> ContT r m2 a-    hoistContT = coerce-    {-# INLINE hoistContT #-}---- | Transform the effect of the effect class that exists within the effect class list.-intercept ::-    forall e fr u es f c.-    (TransFreer c fr, Union u, Member u e es, c f) =>-    (e ~> e) ->-    FreerEffects fr u es f ~> FreerEffects fr u es f-intercept f =-    overFreerEffects $ transformT \u ->-        case project @_ @e u of-            Just e -> inject $ f e-            Nothing -> u---- | Insert an arbitrary effect class at the beginning of the effect class list.-raise ::-    forall e es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u es f ~> FreerEffects fr u (e ': es) f-raise = transformAll weaken-{-# INLINE raise #-}---- | Insert two arbitrary effect classes at the beginning of the effect class list.-raise2 ::-    forall e1 e2 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': es) f-raise2 = transformAll weaken2-{-# INLINE raise2 #-}---- | Insert three arbitrary effect classes at the beginning of the effect class list.-raise3 ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f-raise3 = transformAll weaken3-{-# INLINE raise3 #-}---- | Insert four arbitrary effect classes at the beginning of the effect class list.-raise4 ::-    forall e1 e2 e3 e4 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f-raise4 = transformAll weaken4-{-# INLINE raise4 #-}---- | Insert an arbitrary effect class below the leading effect class in the effect class list.-raiseUnder ::-    forall e1 e2 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f-raiseUnder = transformAll weakenUnder-{-# INLINE raiseUnder #-}--{- |-Insert an arbitrary effect class below the first two leading effect classes in the effect class-list.--}-raiseUnder2 ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f-raiseUnder2 = transformAll weakenUnder2-{-# INLINE raiseUnder2 #-}--{- |-Insert an arbitrary effect class below the first three leading effect classes in the effect class list.--}-raiseUnder3 ::-    forall e1 e2 e3 e4 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f-raiseUnder3 = transformAll weakenUnder3-{-# INLINE raiseUnder3 #-}---- | Insert two arbitrary effect classes below the leading effect class in the effect class list.-raise2Under ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f-raise2Under = transformAll weaken2Under-{-# INLINE raise2Under #-}--{- |-Insert two arbitrary effect classes below the first two leading effect classes in the effect class list.--}-raise2Under2 ::-    forall e1 e2 e3 e4 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f-raise2Under2 = transformAll weaken2Under2-{-# INLINE raise2Under2 #-}---- | Inserts three arbitrary effect classes under the top effect class in the effect class list.-raise3Under ::-    forall e1 e2 e3 e4 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f-raise3Under = transformAll weaken3Under-{-# INLINE raise3Under #-}---- | Swaps the top two effect classes in the effect class list.-flipFreer ::-    forall e1 e2 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e2 ': e1 ': es) f-flipFreer = transformAll flipUnion-{-# INLINE flipFreer #-}---- | Reverses the order of the top three effect classes in the effect class list.-flipFreer3 ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e2 ': e1 ': es) f-flipFreer3 = transformAll flipUnion3-{-# INLINE flipFreer3 #-}---- | Swaps the second and third effect classes from the top in the effect class list.-flipFreerUnder ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e3 ': e2 ': es) f-flipFreerUnder = transformAll flipUnionUnder-{-# INLINE flipFreerUnder #-}---- | Rotates the top three effect classes in the effect class list to the left.-rotate3 ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e2 ': e3 ': e1 ': es) f-rotate3 = transformAll rot3-{-# INLINE rotate3 #-}---- | Rotates the top three effect classes in the effect class list to the left twice.-rotate3' ::-    forall e1 e2 e3 es fr u f c.-    (TransFreer c fr, Union u, c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e1 ': e2 ': es) f-rotate3' = transformAll rot3'-{-# INLINE rotate3' #-}---- | Bundles the top two effect classes in the effect class list into any open union.-bundle2 ::-    forall e1 e2 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (u' '[e1, e2] ': es) f-bundle2 = transformAll bundleUnion2-{-# INLINE bundle2 #-}---- | Bundles the top three effect classes in the effect class list into any open union.-bundle3 ::-    forall e1 e2 e3 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3] ': es) f-bundle3 = transformAll bundleUnion3-{-# INLINE bundle3 #-}---- | Bundles the top four effect classes in the effect class list into any open union.-bundle4 ::-    forall e1 e2 e3 e4 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f-bundle4 = transformAll bundleUnion4-{-# INLINE bundle4 #-}---- | Expands the open union at the top of the effect class list.-unbundle2 ::-    forall e1 e2 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (u' '[e1, e2] ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f-unbundle2 = transformAll unbundleUnion2-{-# INLINE unbundle2 #-}---- | Expands the open union at the top of the effect class list.-unbundle3 ::-    forall e1 e2 e3 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (u' '[e1, e2, e3] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f-unbundle3 = transformAll unbundleUnion3-{-# INLINE unbundle3 #-}---- | Expands the open union at the top of the effect class list.-unbundle4 ::-    forall e1 e2 e3 e4 es fr u f c u'.-    (TransFreer c fr, Union u, Union u', c f) =>-    FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f-unbundle4 = transformAll unbundleUnion4-{-# INLINE unbundle4 #-}--{- |-Transforms the lower carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-hoistFreerEffects ::-    (TransFreer c fr, c f, c g) => (f ~> g) -> FreerEffects fr u es f ~> FreerEffects fr u es g-hoistFreerEffects f = overFreerEffects $ hoistFreer f-{-# INLINE hoistFreerEffects #-}---- | Converts the lower carrier to an instruction.-lowerToIns ::-    (TransFreer c fr, c g, c (f + g), Union u) =>-    FreerEffects fr u es (f + g) ~> FreerEffects fr u (f ': es) g-lowerToIns =-    overFreerEffects $-        interpretFT-            (caseF (liftInsT . inject0) liftLowerFT)-            (liftInsT . weaken)-{-# INLINE lowerToIns #-}---- | Converts the instruction to the lower carrier.-insToLower ::-    (TransFreer c fr, c (f + g), c g, Union u) =>-    FreerEffects fr u (f ': es) g ~> FreerEffects fr u es (f + g)-insToLower = overFreerEffects $ interpretFT (liftLowerFT . R1) (liftLowerFT . L1 |+|: liftInsT)-{-# INLINE insToLower #-}--{- |-Interprets the lower carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-interpretLower ::-    (TransFreer c fr, c f, c g) =>-    (f ~> FreerEffects fr u es g) ->-    FreerEffects fr u es f ~> FreerEffects fr u es g-interpretLower f = overFreerEffects $ interposeLowerT (unFreerEffects . f)-{-# INLINE interpretLower #-}---- | Accesses the inside of the 'FreerEffects' wrapper.-overFreerEffects ::-    (fr (u es) f a -> fr' (u' es') g b) ->-    FreerEffects fr u es f a ->-    FreerEffects fr' u' es' g b-overFreerEffects f = freerEffects . f . unFreerEffects-{-# INLINE overFreerEffects #-}---- | Drops a Freer with no effect classes to interpret to the lower carrier.-interpreted :: (TransFreer c fr, c f, Union u) => FreerEffects fr u '[] f ~> f-interpreted = runInterpretF absurdUnion . unFreerEffects-{-# INLINE interpreted #-}---- | Splits the Freer into the lower carrier.-splitFreerEffects ::-    (TransFreer c fr', TransFreer c fr, c f, c (FreerEffects fr u es f), Union u) =>-    FreerEffects fr u (e ': es) f ~> fr' e (FreerEffects fr u es f)-splitFreerEffects a =-    unFreerEffects a & interpretFT (liftLowerFT . freerEffects . liftLowerFT) \u ->-        case decomp u of-            Left e -> liftInsT e-            Right e -> liftLowerFT $ freerEffects $ liftInsT e---- | Transfer the effect to the underlying level.-subsume ::-    (TransFreer c fr, SendIns e (FreerEffects fr u es f), Union u, c f) =>-    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f-subsume = interpret sendIns-{-# INLINE subsume #-}---- | Transfer the effect to the lower carrier.-subsumeLower ::-    (TransFreer c fr, SendIns e f, Union u, c f) =>-    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f-subsumeLower = interpret $ liftLower . sendIns-{-# INLINE subsumeLower #-}---- | Lifts the lower carrier.-liftLower :: (TransFreer c fr, c f) => f ~> FreerEffects fr u es f-liftLower = freerEffects . liftLowerFT-{-# INLINE liftLower #-}---- | Embeds an IO action into a lower carrier that is a `MonadIO`.-runIO :: MonadIO m => Fre (IO ': es) m ~> Fre es m-runIO = interpret $ liftLower . liftIO-{-# INLINE runIO #-}---- | Interprets all effects in the effect class list at once.-runInterpret :: (TransFreer c fr, c f) => (u es ~> f) -> FreerEffects fr u es f ~> f-runInterpret f = runInterpretF f . unFreerEffects-{-# INLINE runInterpret #-}---- | Drops the Freer to the lower carrier.-runFreerEffects ::-    (TransFreer c fr, c f, Union u) =>-    FreerEffects fr u '[f] f ~> f-runFreerEffects = runInterpret $ id |+|: absurdUnion-{-# INLINE runFreerEffects #-}---- | A type synonym for commonly used Monad Freer.-type Fre es f = FreerEffects FreerChurchT ExtensibleUnion es f---- -- | Type synonym for commonly used Applicative Freer.--- type FreA es f = FreerEffects (FreerFinalT Applicative) SumUnion es f---- | An operator representing the membership relationship of the effect class list.-type e <| es = Member ExtensibleUnion e es

@@ -1,760 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE UndecidableInstances #-}---- 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 Heftia carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).--}-module Control.Effect.Heftia where--import Control.Applicative (Alternative)-import Control.Arrow ((>>>))-import Control.Effect.Class (-    EffectDataHandler,-    EffectsVia (EffectsVia),-    LiftIns (LiftIns),-    SendIns,-    SendSig,-    Signature,-    TagH,-    getTagH,-    runEffectsVia,-    sendIns,-    sendSig,-    unliftIns,-    type (~>),- )-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)-import Control.Effect.Freer (FreerEffects, freerEffects, interpose, unFreerEffects)-import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)-import Control.Heftia.Trans (-    TransHeftia,-    elaborateHT,-    hoistHeftia,-    interpretLowerHT,-    liftLowerHT,-    liftSigT,-    reelaborateHT,-    runElaborateH,-    transformHT,-    translateT,- )-import Control.Monad (MonadPlus)-import Control.Monad.Cont (ContT (ContT), MonadTrans, runContT)-import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, elaborateMT)-import Control.Monad.Trans.Heftia.Church (HeftiaChurchT)-import Data.Extensible.Class (Forall)-import Data.Free.Union (Member, Union, project)-import Data.Hefty.Extensible (ExtensibleUnionH)-import Data.Hefty.Union (-    IsMemberH,-    MemberH,-    UnionH (-        absurdUnionH,-        bundleUnion2H,-        bundleUnion3H,-        bundleUnion4H,-        decompH,-        flipUnion3H,-        flipUnionH,-        flipUnionUnderH,-        inject0H,-        injectH,-        projectH,-        rot3H,-        rot3H',-        unbundleUnion2H,-        unbundleUnion3H,-        unbundleUnion4H,-        weaken2H,-        weaken2Under2H,-        weaken2UnderH,-        weaken3H,-        weaken3UnderH,-        weaken4H,-        weakenH,-        weakenUnder2H,-        weakenUnder3H,-        weakenUnderH-    ),-    (|+:),- )-import Data.Kind (Type)--{- |-A data type that wraps Heftia with any encoding to become an instance of 'SendIns'/'SendSig' based-on the `liftInsT` or `liftSigT` from the `TransFreer` or `TransHeftia` type class.--}-newtype-    HeftiaUnion-        (h :: Signature -> (Type -> Type) -> Type -> Type)-        u-        (es :: [Signature])-        f-        a = HeftiaUnion {runHeftiaUnion :: h (u es) f a}-    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)-    deriving stock (Foldable, Traversable)--{- |-A Heftia carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).--}-type HeftiaEffects h u es f = EffectsVia EffectDataHandler (HeftiaUnion h u es f)---- | Unwrap the `HeftiaEffects` wrapper.-unHeftiaEffects :: HeftiaEffects h u es f ~> h (u es) f-unHeftiaEffects = runHeftiaUnion . runEffectsVia-{-# INLINE unHeftiaEffects #-}---- | Wrap with `HeftiaEffects`.-heftiaEffects :: h (u es) f ~> HeftiaEffects h u es f-heftiaEffects = EffectsVia . HeftiaUnion-{-# INLINE heftiaEffects #-}--{- |-A wrapper data type designed to induce instance resolution to delegate the search for first-order-effect classes to a lower carrier @f@ even when there are no target effect classes in the effect-class list @es@.--When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it-doesn't exist, it's induced to be @'False@.--}-newtype HeftiaUnionForSendIns handleHere h u es f a = HeftiaUnionForSendIns-    {runHeftiaUnionForSendIns :: HeftiaUnion h u es f a}-    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)-    deriving stock (Foldable, Traversable)--instance-    SendIns e (HeftiaUnionForSendIns (LiftIns e `IsMemberH` es) h u es f) =>-    SendIns e (HeftiaUnion h u es f)-    where-    sendIns = runHeftiaUnionForSendIns @(LiftIns e `IsMemberH` es) . sendIns-    {-# INLINE sendIns #-}--instance-    (TransHeftia c h, UnionH u, MemberH u (LiftIns e) es, HFunctor (u es)) =>-    SendIns e (HeftiaUnionForSendIns 'True h u es f)-    where-    sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftSigT . injectH . LiftIns-    {-# INLINE sendIns #-}--instance-    (TransHeftia c h, SendIns e f, c f, HFunctor (u es)) =>-    SendIns e (HeftiaUnionForSendIns 'False h u es f)-    where-    sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftLowerHT . sendIns-    {-# INLINE sendIns #-}--instance-    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es)) =>-    SendSig e (HeftiaUnion h u es f)-    where-    sendSig = HeftiaUnion . liftSigT . hfmap runHeftiaUnion . injectH-    {-# INLINE sendSig #-}---- | Elaborate all effects in the effect class list at once.-runElaborate ::-    (TransHeftia c h, HFunctor (u es), c f, UnionH u) =>-    (u es f ~> f) ->-    HeftiaEffects h u es f ~> f-runElaborate f = runElaborateH f . unHeftiaEffects-{-# INLINE runElaborate #-}---- | Elaborate all effects in the effect class list using a delimited continuation.-runElaborateK ::-    (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) =>-    (a -> m r) ->-    (forall x. (x -> m r) -> u es (ContT r m) x -> m r) ->-    HeftiaEffects h u es m a ->-    m r-runElaborateK k f = (`runContT` k) . runElaborateContT \e -> ContT (`f` e)-{-# INLINE runElaborateK #-}--{- |-Elaborate all effects in the effect class list using a continuation monad transformer.--}-runElaborateContT ::-    (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) =>-    (u es (ContT r m) ~> ContT r m) ->-    HeftiaEffects h u es m ~> ContT r m-runElaborateContT f = elaborateMK f . unHeftiaEffects-{-# INLINE runElaborateContT #-}--{- |-Elaborate all effects in the effect class list using a monad transformer.--}-runElaborateT ::-    (MonadTransHeftia h, HFunctor (u es), UnionH u, MonadTrans t, Monad m, Monad (t m)) =>-    (u es (t m) ~> t m) ->-    HeftiaEffects h u es m ~> t m-runElaborateT f = elaborateMT f . unHeftiaEffects-{-# INLINE runElaborateT #-}--{- |-Elaborate all effects in the effect class list and the underlying carrier simultaneously,-transforming them into any carrier @g@.--}-elaborate ::-    (TransHeftia c h, HFunctor (u es), c f, UnionH u, c g) =>-    (f ~> g) ->-    (u es g ~> g) ->-    HeftiaEffects h u es f ~> g-elaborate f g = elaborateHT f g . unHeftiaEffects-{-# INLINE elaborate #-}---- | Elaborate the leading effect class in the effect class list.-interpretH ::-    (TransHeftia c h, UnionH u, HFunctor (u es), HFunctor (u (e : es)), HFunctor e, c f) =>-    (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) ->-    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u es f-interpretH i =-    overHeftiaEffects $ elaborateHT liftLowerHT \u ->-        case decompH u of-            Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e-            Right e -> liftSigT e---- | Re-elaborate the leading effect class in the effect class list.-reinterpretH ::-    (TransHeftia c h, UnionH u, HFunctor (u (e : es)), HFunctor e, c f) =>-    (e (HeftiaEffects h u (e ': es) f) ~> HeftiaEffects h u (e ': es) f) ->-    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u (e ': es) f-reinterpretH i =-    overHeftiaEffects $ reelaborateHT \u ->-        case decompH u of-            Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e-            Right e -> liftSigT $ weakenH e---- | Transform all effect classes in the effect class list into another union of effect classes.-transformAllH ::-    ( TransHeftia c h-    , UnionH u-    , UnionH u'-    , HFunctor (u es)-    , HFunctor (u' es')-    , c f-    ) =>-    (forall g. u es g ~> u' es' g) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f-transformAllH f = overHeftiaEffects $ transformHT f-{-# INLINE transformAllH #-}---- | Transform the leading effect class in the effect class list into another effect class.-transformH ::-    forall e' e h u r f c.-    ( TransHeftia c h-    , UnionH u-    , c f-    , HFunctor (u (e : r))-    , HFunctor (u (e' : r))-    ) =>-    (forall g. e g ~> e' g) ->-    HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f-transformH f = overHeftiaEffects $ translateT \u ->-    case decompH u of-        Left e -> inject0H $ f e-        Right e -> weakenH e---- | Remove the tag attached to the effect class.-untagH ::-    forall tag e h u r f c.-    ( TransHeftia c h-    , UnionH u-    , c f-    , HFunctor (u (e : r))-    , HFunctor (u (TagH e tag : r))-    ) =>-    HeftiaEffects h u (TagH e tag ': r) f ~> HeftiaEffects h u (e ': r) f-untagH = transformH getTagH---- | Transform the leading effect class in the effect class list into another effect class.-translate ::-    forall e' e h u r f c.-    ( TransHeftia c h-    , UnionH u-    , HFunctor (u (e : r))-    , HFunctor (u (e' : r))-    , HFunctor e-    , HFunctor e'-    , c f-    ) =>-    (e (HeftiaEffects h u (e' ': r) f) ~> e' (HeftiaEffects h u (e' ': r) f)) ->-    HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f-translate f =-    overHeftiaEffects $ translateT \u ->-        case decompH u of-            Left e -> inject0H $ hfmap unHeftiaEffects $ f $ hfmap heftiaEffects e-            Right e -> weakenH e---- | Transform all effect classes in the effect class list into another union of effect classes.-translateAll ::-    ( TransHeftia c h-    , UnionH u-    , UnionH u'-    , HFunctor (u es)-    , HFunctor (u' es')-    , c f-    ) =>-    (u es (HeftiaEffects h u' es' f) ~> u' es' (HeftiaEffects h u' es' f)) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f-translateAll f =-    overHeftiaEffects $ translateT (hfmap unHeftiaEffects . f . hfmap heftiaEffects)-{-# INLINE translateAll #-}---- | Interpose the effect class that exists within the effect class list using a monad transformer.-interposeH ::-    forall e h u es f c.-    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), c f) =>-    (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u es f-interposeH f =-    overHeftiaEffects $ reelaborateHT \u ->-        let u' = hfmap (interposeH f . heftiaEffects) u-         in case projectH @_ @e u' of-                Just e -> unHeftiaEffects $ f e-                Nothing -> liftSigT $ hfmap unHeftiaEffects u'---- | Transform the effect of the effect class that exists within the effect class list.-interceptH ::-    forall e h u es f c.-    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), HFunctor e, c f) =>-    (e (HeftiaEffects h u es f) ~> e (HeftiaEffects h u es f)) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u es f-interceptH f =-    overHeftiaEffects $ translateT \u ->-        let u' = hfmap (interceptH f . heftiaEffects) u-         in case projectH @_ @e u' of-                Just e -> injectH $ hfmap unHeftiaEffects $ f e-                Nothing -> hfmap unHeftiaEffects u'---- | Insert an arbitrary effect class at the beginning of the effect class list.-raiseH ::-    forall e hs h u f c.-    ( TransHeftia c h-    , HFunctor (u hs)-    , HFunctor (u (e ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u hs f ~> HeftiaEffects h u (e ': hs) f-raiseH = transformAllH weakenH-{-# INLINE raiseH #-}---- | Insert two arbitrary effect classes at the beginning of the effect class list.-raise2H ::-    forall e1 e2 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u hs)-    , HFunctor (u (e1 ': e2 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': hs) f-raise2H = transformAllH weaken2H-{-# INLINE raise2H #-}---- | Insert three arbitrary effect classes at the beginning of the effect class list.-raise3H ::-    forall e1 e2 e3 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u hs)-    , HFunctor (u (e1 ': e2 ': e3 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f-raise3H = transformAllH weaken3H-{-# INLINE raise3H #-}---- | Insert four arbitrary effect classes at the beginning of the effect class list.-raise4H ::-    forall e1 e2 e3 e4 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u hs)-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f-raise4H = transformAllH weaken4H-{-# INLINE raise4H #-}---- | Insert an arbitrary effect class below the leading effect class in the effect class list.-raiseUnderH ::-    forall e1 e2 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': hs))-    , HFunctor (u (e1 ': e2 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': hs) f-raiseUnderH = transformAllH weakenUnderH-{-# INLINE raiseUnderH #-}--{- |-Insert an arbitrary effect class below the first two leading effect classes in the effect class-list.--}-raiseUnder2H ::-    forall e1 e2 e3 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': hs))-    , HFunctor (u (e1 ': e2 ': e3 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f-raiseUnder2H = transformAllH weakenUnder2H-{-# INLINE raiseUnder2H #-}--{- |-Insert an arbitrary effect class below the first three leading effect classes in the effect class list.--}-raiseUnder3H ::-    forall e1 e2 e3 e4 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': hs))-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f-raiseUnder3H = transformAllH weakenUnder3H-{-# INLINE raiseUnder3H #-}---- | Insert two arbitrary effect classes below the leading effect class in the effect class list.-raise2UnderH ::-    forall e1 e2 e3 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': hs))-    , HFunctor (u (e1 ': e2 ': e3 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f-raise2UnderH = transformAllH weaken2UnderH-{-# INLINE raise2UnderH #-}--{- |-Insert two arbitrary effect classes below the first two leading effect classes in the effect class list.--}-raise2Under2H ::-    forall e1 e2 e3 e4 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': hs))-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f-raise2Under2H = transformAllH weaken2Under2H-{-# INLINE raise2Under2H #-}---- | Inserts three arbitrary effect classes under the top effect class in the effect class list.-raise3UnderH ::-    forall e1 e2 e3 e4 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': hs))-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f-raise3UnderH = transformAllH weaken3UnderH-{-# INLINE raise3UnderH #-}---- | Swaps the top two effect classes in the effect class list.-flipHeftia ::-    forall e1 e2 hs h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': hs))-    , HFunctor (u (e2 ': e1 ': hs))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e2 ': e1 ': hs) f-flipHeftia = transformAllH flipUnionH-{-# INLINE flipHeftia #-}---- | Reverses the order of the top three effect classes in the effect class list.-flipHeftia3 ::-    forall e1 e2 e3 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (e3 : e2 : e1 : es))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e2 ': e1 ': es) f-flipHeftia3 = transformAllH flipUnion3H-{-# INLINE flipHeftia3 #-}---- | Swaps the second and third effect classes from the top in the effect class list.-flipHeftiaUnder ::-    forall e1 e2 e3 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (e1 : e3 : e2 : es))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e1 ': e3 ': e2 ': es) f-flipHeftiaUnder = transformAllH flipUnionUnderH-{-# INLINE flipHeftiaUnder #-}---- | Rotates the top three effect classes in the effect class list to the left.-rotate3H ::-    forall e1 e2 e3 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (e2 : e3 : e1 : es))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e2 ': e3 ': e1 ': es) f-rotate3H = transformAllH rot3H-{-# INLINE rotate3H #-}---- | Rotates the top three effect classes in the effect class list to the left twice.-rotate3H' ::-    forall e1 e2 e3 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (e3 : e1 : e2 : es))-    , c f-    , UnionH u-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e1 ': e2 ': es) f-rotate3H' = transformAllH rot3H'-{-# INLINE rotate3H' #-}---- | Bundles the top two effect classes in the effect class list into any open union.-bundle2H ::-    forall u' e1 e2 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': es))-    , HFunctor (u (u' '[e1, e2] ': es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (e1 ': e2 ': es) f ~> HeftiaEffects h u (u' '[e1, e2] ': es) f-bundle2H = transformAllH bundleUnion2H-{-# INLINE bundle2H #-}---- | Bundles the top three effect classes in the effect class list into any open union.-bundle3H ::-    forall u' e1 e2 e3 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (u' '[e1, e2, e3] : es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (u' '[e1, e2, e3] ': es) f-bundle3H = transformAllH bundleUnion3H-{-# INLINE bundle3H #-}---- | Bundles the top four effect classes in the effect class list into any open union.-bundle4H ::-    forall u' e1 e2 e3 e4 es h u f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))-    , HFunctor (u (u' '[e1, e2, e3, e4] : es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f-        ~> HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f-bundle4H = transformAllH bundleUnion4H-{-# INLINE bundle4H #-}---- | Expands the open union at the top of the effect class list.-unbundle2H ::-    forall e1 e2 es h u u' f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': es))-    , HFunctor (u (u' '[e1, e2] ': es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (u' '[e1, e2] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': es) f-unbundle2H = transformAllH unbundleUnion2H-{-# INLINE unbundle2H #-}---- | Expands the open union at the top of the effect class list.-unbundle3H ::-    forall e1 e2 e3 es h u u' f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': es))-    , HFunctor (u (u' '[e1, e2, e3] ': es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (u' '[e1, e2, e3] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': es) f-unbundle3H = transformAllH unbundleUnion3H-{-# INLINE unbundle3H #-}---- | Expands the open union at the top of the effect class list.-unbundle4H ::-    forall e1 e2 e3 e4 es h u u' f c.-    ( TransHeftia c h-    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))-    , HFunctor (u (u' '[e1, e2, e3, e4] ': es))-    , c f-    , UnionH u-    , UnionH u'-    ) =>-    HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f-        ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f-unbundle4H = transformAllH unbundleUnion4H-{-# INLINE unbundle4H #-}--{- |-Transforms the lower carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-hoistHeftiaEffects ::-    (TransHeftia c h, HFunctor (u es), c f, c g) =>-    (f ~> g) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u es g-hoistHeftiaEffects f = overHeftiaEffects $ hoistHeftia f-{-# INLINE hoistHeftiaEffects #-}---- | Accesses the inside of the 'HeftiaEffects' wrapper.-overHeftiaEffects ::-    (h (u es) f a -> h' (u' es') g b) ->-    HeftiaEffects h u es f a ->-    HeftiaEffects h' u' es' g b-overHeftiaEffects f = heftiaEffects . f . unHeftiaEffects-{-# INLINE overHeftiaEffects #-}--{- |-Interpose the lower Freer carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-hoistInterpose ::-    forall e h u es fr u' es' f c c'.-    ( TransHeftia c h-    , HFunctor (u es)-    , TransFreer c' fr-    , Union u'-    , Member u' e es'-    , c (FreerEffects fr u' es' f)-    , c' f-    ) =>-    (e ~> FreerEffects fr u' es' f) ->-    HeftiaEffects h u es (FreerEffects fr u' es' f)-        ~> HeftiaEffects h u es (FreerEffects fr u' es' f)-hoistInterpose f = hoistHeftiaEffects $ interpose f-{-# INLINE hoistInterpose #-}--{- |-Interpose the lower Freer carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-interposeLower ::-    forall e h u es fr u' es' f c c'.-    ( TransHeftia c h-    , HFunctor (u es)-    , TransFreer c' fr-    , Union u'-    , Member u' e es'-    , c (FreerEffects fr u' es' f)-    , c' f-    , c' (HeftiaEffects h u es (FreerEffects fr u' es' f))-    ) =>-    (e ~> HeftiaEffects h u es (FreerEffects fr u' es' f)) ->-    HeftiaEffects h u es (FreerEffects fr u' es' f)-        ~> HeftiaEffects h u es (FreerEffects fr u' es' f)-interposeLower f =-    interpretLowerH $-        unFreerEffects-            >>> interpretFT-                (liftLowerH . freerEffects . liftLowerFT)-                \u -> case project @_ @e u of-                    Just e -> f e-                    Nothing -> liftLowerH $ freerEffects $ liftInsT u--{- |-Interprets the lower carrier.--__Warning__: The given natural transformation must be a monad morphism-(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).-If not, the result will be ill-behaved.--}-interpretLowerH ::-    (c f, c g, TransHeftia c h, HFunctor (u es)) =>-    (f ~> HeftiaEffects h u es g) ->-    HeftiaEffects h u es f ~> HeftiaEffects h u es g-interpretLowerH f = overHeftiaEffects $ interpretLowerHT (unHeftiaEffects . f)-{-# INLINE interpretLowerH #-}---- | Transfer the higher-order effect to the underlying level.-subsume ::-    ( TransHeftia c h-    , MemberH u e es-    , UnionH u-    , HFunctor e-    , HFunctor (u es)-    , HFunctor (u (e : es))-    , c f-    ) =>-    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u es f-subsume = interpretH $ heftiaEffects . liftSigT . hfmap unHeftiaEffects . injectH-{-# INLINE subsume #-}---- | Lifts the lower carrier.-liftLowerH :: (TransHeftia c h, c f, HFunctor (u es)) => f ~> HeftiaEffects h u es f-liftLowerH = heftiaEffects . liftLowerHT-{-# INLINE liftLowerH #-}---- | Drops a Heftia with no effect classes to elaborate to the lower carrier.-elaborated :: (TransHeftia c h, UnionH u, HFunctor (u '[]), c f) => HeftiaEffects h u '[] f ~> f-elaborated = runElaborateH absurdUnionH . unHeftiaEffects-{-# INLINE elaborated #-}---- | Drops the Heftia to the lower carrier.-runHeftiaEffects ::-    (TransHeftia c h, HFunctor (u '[LiftIns f]), UnionH u, c f) =>-    HeftiaEffects h u '[LiftIns f] f ~> f-runHeftiaEffects = runElaborate $ unliftIns |+: absurdUnionH-{-# INLINE runHeftiaEffects #-}---- | A type synonym for commonly used Monad Heftia.-type Hef es f = HeftiaEffects HeftiaChurchT ExtensibleUnionH es f---- -- | Type synonym for commonly used Applicative Heftia.--- type HefA es f = HeftiaEffects (HeftiaFinalT Applicative) SumUnionH es f---- | An operator representing the membership relationship of the higher-order effect class list.-type e <<| es = MemberH ExtensibleUnionH e es---- | A type synonym for functions that perform the elaboration of higher-order effects.-type Elaborator e f = e f ~> f---- | A type synonym for frequently occurring constraints on a list of effect classes.-type ForallHFunctor = Forall HFunctor

@@ -0,0 +1,1114 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}++-- 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++A Heftia carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+module Control.Effect.Hefty where++import Control.Effect (type (~>))+import Control.Effect.Key (sendInsBy, sendSigBy)+import Control.Freer (Freer, InjectIns, InjectInsBy, injectIns, injectInsBy, interpretFreer, liftIns, transformFreer)+import Control.Hefty (Hefty (Hefty), InjectSig, InjectSigBy, injectSig, injectSigBy, overHefty, unHefty)+import Control.Monad.Cont (Cont, ContT (ContT), lift, runContT)+import Control.Monad.Freer (MonadFreer, interpretFreerK)+import Control.Monad.Identity (Identity (Identity), runIdentity)+import Control.Monad.Trans (MonadTrans)+import Data.Coerce (coerce)+import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)+import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:))+import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>))+import Data.Effect.Tag (Tag (unTag), TagH (unTagH), type (#), type (##))+import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))+import Data.Hefty.Union (+    HFunctorUnion,+    HFunctorUnion_ (ForallHFunctor),+    HeadIns,+    LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),+    Lookup,+    Member,+    MemberBy,+    MemberH,+    MemberHBy,+    MemberRec,+    U,+    UH,+    Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)),+    UnliftIfSingle,+    flipUnion,+    flipUnion3,+    flipUnionUnder,+    inject,+    injectRec,+    projectRec,+    weaken2,+    weaken2Under,+    weaken2Under2,+    weaken3Under,+    weakenUnder2,+    weakenUnder3,+    (|+),+ )+import Data.Kind (Type)+import Data.Maybe.Singletons (FromJust)++{- |+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.+-}+newtype EffUnion (u :: [SigClass] -> SigClass) ehs efs f a = EffUnion+    {unEffUnion :: (u ehs f + u efs Nop) a}++caseHF :: (u ehs f a -> r) -> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r+caseHF f g = caseF f g . unEffUnion++instance HFunctor (u ehs) => HFunctor (EffUnion u ehs efs) where+    hfmap f = EffUnion . caseF (L1 . hfmap f) R1 . unEffUnion+    {-# INLINE hfmap #-}++instance MemberRec u (LiftIns e) efs => InjectIns e (EffUnion u ehs efs f) where+    injectIns = EffUnion . R1 . injectRec . LiftIns+    {-# INLINE injectIns #-}++instance MemberRec u e ehs => InjectSig e (EffUnion u ehs efs) where+    injectSig = EffUnion . L1 . injectRec+    {-# INLINE injectSig #-}++type HasMembershipF u e efs = HasMembership u (LiftIns e) efs++infixr 3 $+infixr 4 $$++-- | Type-level infix applcation for functors.+type (f :: Type -> Type) $ a = f a++-- | Type-level infix applcation for higher-order functors.+type (h :: (Type -> Type) -> Type -> Type) $$ f = h f++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+{-# INLINE injectH #-}++injectF :: Freer c f => u efs Nop ~> Eff u f ehs efs+injectF = Hefty . liftIns . EffUnion . R1+{-# INLINE injectF #-}++{-  all types of interpret-family functions:+        - interpret   :                 e  ~> E r           ->    E (e + r)  ~> E r+        - reinterpret :                 e1 ~> E (e2 + r)    ->    E (e1 + r) ~> E (e2 + r)+        - interpose   :  e <| es  =>    e  ~> E es          ->    E es       ~> E es++        all possible suffix patterns of interpret functions:+            { <none> , K , ContT , Fin , T } x { <none> , H , FH }+            - Rec+            - RecH+            - RecFH++        all possible suffix patterns of interpret-family functions (except 'interpret'):+            - <none>+            - K+            - ContT+            - Fin ('interpose' only)+            - T+            - Rec+            - RecH+            - RecFH++    all types of transform-family functions:+        - transform :                  e1 ~> e2    ->    E (e1 + r) ~> E (e2 + r)+        - translate :  e2 <| r   =>    e1 ~> e2    ->    E (e1 + r) ~> E r+        - rewrite   :  e  <| es  =>    e  ~> e     ->    E es       ~> E es++        all possible suffix patterns of transform-family functions:+            - <none>+            - H+            - FH++    todo patterns:+        - *FH in interpret-family ( (5+1) + 2 = 8 functions )++        + *By (for keyed effects) in interpose/translate/rewrite ( 8 + 2x3 = 14 functions )+-}++-- | Using the provided interpretation function, interpret first-order effects.+interpret ::+    forall e r ehs fr u c.+    (Freer c fr, Union u, HeadIns e) =>+    UnliftIfSingle e ~> Eff u fr ehs r ->+    Eff u fr '[] (e ': r) ~> Eff u fr ehs r+interpret i = interpretAllE $ i . unliftInsIfSingle |+: injectF+{-# INLINE interpret #-}++interpretH ::+    forall eh ehs efs fr u c.+    (Freer c fr, Union u) =>+    eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs ->+    Eff u fr '[eh] efs ~> Eff u fr ehs efs+interpretH i = interpretAllH $ i |+: exhaust+{-# INLINE interpretH #-}++-- | Interpret the leading first-order effect class using delimited continuations.+interpretK ::+    forall e rs r a ehs fr u c.+    (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>+    (a -> Eff u fr ehs rs r) ->+    (forall x. (x -> Eff u fr ehs rs r) -> UnliftIfSingle e x -> Eff u fr ehs rs r) ->+    Eff u fr '[] (e ': rs) a ->+    Eff u fr ehs rs r+interpretK = toInterpretKFromContT interpretContT+{-# INLINE interpretK #-}++interpretKH ::+    forall e r ehs efs a fr u c.+    (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>+    (a -> Eff u fr ehs efs r) ->+    (forall x. (x -> Eff u fr ehs efs r) -> e (Eff u fr '[e] efs) x -> Eff u fr ehs efs r) ->+    Eff u fr '[e] efs a ->+    Eff u fr ehs efs r+interpretKH = toInterpretKFromContT interpretContTH+{-# INLINE interpretKH #-}++-- | Interpret the leading first-order effect class using a continuation monad transformer.+interpretContT ::+    forall e rs r ehs fr u c.+    (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>+    (UnliftIfSingle e ~> ContT r (Eff u fr ehs rs)) ->+    Eff u fr '[] (e ': rs) ~> ContT r (Eff u fr ehs rs)+interpretContT i =+    interpretContTAll $ i . unliftInsIfSingle |+: lift . injectF+{-# INLINE interpretContT #-}++interpretContTH ::+    forall e r ehs efs fr u c.+    (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>+    (e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs)) ->+    Eff u fr '[e] efs ~> ContT r (Eff u fr ehs efs)+interpretContTH i = interpretContTAllH $ i |+: exhaust+{-# INLINE interpretContTH #-}++-- | Interpret the leading first-order effect class into the carrier @f@.+interpretFin ::+    forall e r f fr u c.+    (Freer c fr, Union u, HeadIns e, c f) =>+    (u r Nop ~> f) ->+    UnliftIfSingle e ~> f ->+    Eff u fr '[] (e ': r) ~> f+interpretFin liftFin i = interpretAll $ i . unliftInsIfSingle |+: liftFin+{-# INLINE interpretFin #-}++interpretFinH ::+    forall e f efs fr u c.+    (Freer c fr, Union u, c f) =>+    (u efs Nop ~> f) ->+    e (Eff u fr '[e] efs) ~> f ->+    Eff u fr '[e] efs ~> f+interpretFinH liftFin i = interpretAllFH (i |+: exhaust) liftFin+{-# INLINE interpretFinH #-}++-- | Interpret the leading first-order effect class using a monad transformer.+interpretT ::+    forall e r t ehs fr u c.+    ( Freer c fr+    , Union u+    , MonadTrans t+    , HeadIns e+    , Monad (Eff u fr ehs r)+    , c (t (Eff u fr ehs r))+    ) =>+    UnliftIfSingle e ~> t (Eff u fr ehs r) ->+    Eff u fr '[] (e ': r) ~> t (Eff u fr ehs r)+interpretT = interpretFin $ lift . injectF+{-# INLINE interpretT #-}++interpretTH ::+    forall e t ehs efs fr u c.+    (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs efs), c (t (Eff u fr ehs efs))) =>+    e (Eff u fr '[e] efs) ~> t (Eff u fr ehs efs) ->+    Eff u fr '[e] efs ~> t (Eff u fr ehs efs)+interpretTH = interpretFinH $ lift . injectF+{-# INLINE interpretTH #-}++{- |+Using the provided interpretation function, interpret first-order effects. For actions (scopes)+within higher-order effects that are currently unhandled, interpretation is applied recursively.++Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not+maintained across the scopes.+-}+interpretRec ::+    forall e rs ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>+    UnliftIfSingle e ~> Eff u fr ehs rs ->+    Eff u fr ehs (e ': rs) ~> Eff u fr ehs rs+interpretRec i = interpretAllRec $ i . unliftInsIfSingle |+: injectF+{-# INLINE interpretRec #-}++{- |+Using the provided interpretation function, interpret higher-order effects. For actions (scopes)+within higher-order effects that are currently unhandled, interpretation is applied recursively.++Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not+maintained across the scopes.+-}+interpretRecH ::+    forall e rs efs fr u c.+    (Freer c fr, Union u, HFunctor e, HFunctor (u rs), HFunctor (u (e ': rs))) =>+    e (Eff u fr rs efs) ~> Eff u fr rs efs ->+    Eff u fr (e ': rs) efs ~> Eff u fr rs efs+interpretRecH i = interpretAllRecH $ i |+: injectH+{-# INLINE interpretRecH #-}++reinterpret ::+    forall e2 e1 r ehs fr u c.+    (Freer c fr, Union u, HeadIns e1, HFunctor (u '[])) =>+    UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) ->+    Eff u fr '[] (e1 ': r) ~> Eff u fr ehs (e2 ': r)+reinterpret f = interpret f . raiseUnder+{-# INLINE reinterpret #-}++reinterpretK ::+    forall e2 e1 rs r a ehs fr u c.+    (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) =>+    (a -> Eff u fr ehs (e2 ': rs) r) ->+    ( forall x.+      (x -> Eff u fr ehs (e2 ': rs) r) ->+      UnliftIfSingle e1 x ->+      Eff u fr ehs (e2 ': rs) r+    ) ->+    Eff u fr '[] (e1 ': rs) a ->+    Eff u fr ehs (e2 ': rs) r+reinterpretK = toInterpretKFromContT reinterpretContT+{-# INLINE reinterpretK #-}++reinterpretContT ::+    forall e2 e1 rs r ehs fr u c.+    (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) =>+    (UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 ': rs))) ->+    Eff u fr '[] (e1 ': rs) ~> ContT r (Eff u fr ehs (e2 ': rs))+reinterpretContT i = interpretContT i . raiseUnder+{-# INLINE reinterpretContT #-}++reinterpretT ::+    forall e2 e1 t r ehs fr u c.+    ( Freer c fr+    , Union u+    , MonadTrans t+    , HeadIns e1+    , HFunctor (u '[])+    , Monad (Eff u fr ehs (e2 ': r))+    , c (t (Eff u fr ehs (e2 ': r)))+    ) =>+    UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 ': r)) ->+    Eff u fr '[] (e1 ': r) ~> t (Eff u fr ehs (e2 ': r))+reinterpretT i = interpretT i . raiseUnder+{-# INLINE reinterpretT #-}++reinterpretRec ::+    forall e2 e1 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) =>+    UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) ->+    Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r)+reinterpretRec i = interpretRec i . raiseUnder+{-# INLINE reinterpretRec #-}++reinterpretRecH ::+    forall e2 e1 r efs fr u c.+    (Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2, ForallHFunctor u r) =>+    e1 (Eff u fr (e2 ': r) efs) ~> Eff u fr (e2 ': r) efs ->+    Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs+reinterpretRecH i = interpretRecH i . raiseUnderH+{-# INLINE reinterpretRecH #-}++interpose ::+    forall e efs fr u c.+    (Freer c fr, Union u, Member u e efs) =>+    e ~> Eff u fr '[] efs ->+    Eff u fr '[] efs ~> Eff u fr '[] efs+interpose f =+    interpretAllE+        \u -> case projectRec u of+            Just (LiftIns e) -> f e+            Nothing -> injectF u++interposeK ::+    forall e efs r a fr u c.+    (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>+    (a -> Eff u fr '[] efs r) ->+    (forall x. (x -> Eff u fr '[] efs r) -> e x -> Eff u fr '[] efs r) ->+    Eff u fr '[] efs a ->+    Eff u fr '[] efs r+interposeK = toInterpretKFromContT interposeContT+{-# INLINE interposeK #-}++interposeContT ::+    forall e efs r fr u c.+    (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>+    (e ~> ContT r (Eff u fr '[] efs)) ->+    Eff u fr '[] efs ~> ContT r (Eff u fr '[] efs)+interposeContT f =+    interpretContTAll+        \u -> case projectRec u of+            Just (LiftIns e) -> f e+            Nothing -> lift $ injectF u+{-# INLINE interposeContT #-}++interposeFin ::+    forall e f efs fr u c.+    (Freer c fr, Union u, Member u e efs, c f) =>+    u efs Nop ~> f ->+    e ~> f ->+    Eff u fr '[] efs ~> f+interposeFin liftFin f =+    interpretAll+        \u -> case projectRec u of+            Just (LiftIns e) -> f e+            Nothing -> liftFin u+{-# INLINE interposeFin #-}++interposeT ::+    forall e t efs fr u c.+    ( Freer c fr+    , Union u+    , MonadTrans t+    , Member u e efs+    , Monad (Eff u fr '[] efs)+    , c (t (Eff u fr '[] efs))+    ) =>+    e ~> t (Eff u fr '[] efs) ->+    Eff u fr '[] efs ~> t (Eff u fr '[] efs)+interposeT = interposeFin $ lift . injectF+{-# INLINE interposeT #-}++interposeRec ::+    forall e ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), Member u e efs) =>+    e ~> Eff u fr ehs efs ->+    Eff u fr ehs efs ~> Eff u fr ehs efs+interposeRec f =+    interpretAllRec+        \u -> case projectRec u of+            Just (LiftIns e) -> f e+            Nothing -> injectF u+{-# INLINE interposeRec #-}++interposeRecH ::+    forall e ehs efs fr u c.+    (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u ehs, MemberH u e ehs) =>+    e (Eff u fr ehs efs) ~> Eff u fr ehs efs ->+    Eff u fr ehs efs ~> Eff u fr ehs efs+interposeRecH f =+    interpretAllH+        \u -> case projectRec u of+            Just e -> f e+            Nothing -> injectH u+{-# INLINE interposeRecH #-}++interpretAll ::+    forall g efs fr u c.+    (Freer c fr, Union u, c g) =>+    u efs Nop ~> g ->+    Eff u fr '[] efs ~> g+interpretAll = interpretAllFH exhaust+{-# INLINE interpretAll #-}++interpretAllE ::+    forall ehs' efs' efs fr u c.+    (Freer c fr, Union u) =>+    u efs Nop ~> Eff u fr ehs' efs' ->+    Eff u fr '[] efs ~> Eff u fr ehs' efs'+interpretAllE = interpretAllFHE exhaust+{-# INLINE interpretAllE #-}++interpretAllRecH ::+    forall ehs' ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs+interpretAllRecH fh =+    interpretAllH $ fh . hfmap (interpretAllRecH fh)++interpretAllH ::+    forall ehs' ehs efs fr u c.+    (Freer c fr, Union u) =>+    u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs+interpretAllH fh = interpretAllFHE fh injectF+{-# INLINE interpretAllH #-}++interpretAllRecFH ::+    forall g ehs efs fr u c.+    (Freer c fr, Union u, c g, HFunctor (u ehs)) =>+    u ehs g ~> g ->+    u efs Nop ~> g ->+    Eff u fr ehs efs ~> g+interpretAllRecFH fh ff =+    interpretAllFH (fh . hfmap (interpretAllRecFH fh ff)) ff++interpretAllFH ::+    forall g ehs efs fr u c.+    (Freer c fr, Union u, c g) =>+    u ehs (Eff u fr ehs efs) ~> g ->+    u efs Nop ~> g ->+    Eff u fr ehs efs ~> g+interpretAllFH fh ff = interpretFreer (caseHF fh ff) . unHefty+{-# INLINE interpretAllFH #-}++interpretAllRecFHE ::+    forall ehs' efs' ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs' ->+    u efs Nop ~> Eff u fr ehs' efs' ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs'+interpretAllRecFHE fh ff =+    interpretAllFHE (fh . hfmap (interpretAllRecFHE fh ff)) ff+{-# INLINE interpretAllRecFHE #-}++interpretAllFHE ::+    forall ehs' efs' ehs efs fr u c.+    (Freer c fr, Union u) =>+    u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs' ->+    u efs Nop ~> Eff u fr ehs' efs' ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs'+interpretAllFHE fh ff =+    overHefty $ interpretFreer $ unHefty . caseHF fh ff++interpretKAll ::+    forall r a efs fr u c.+    (MonadFreer c fr, Union u) =>+    (a -> Eff u fr '[] efs r) ->+    (forall x. (x -> Eff u fr '[] efs r) -> u efs Nop x -> Eff u fr '[] efs r) ->+    Eff u fr '[] efs a ->+    Eff u fr '[] efs r+interpretKAll = toInterpretKFromContT interpretContTAll+{-# INLINE interpretKAll #-}++interpretKAllRecH ::+    forall ehs' r a ehs efs fr u c.+    (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) =>+    (a -> Eff u fr ehs' efs r) ->+    ( forall x.+      (x -> Eff u fr ehs' efs r) ->+      u ehs (ContT r (Eff u fr ehs' efs)) x ->+      Eff u fr ehs' efs r+    ) ->+    Eff u fr ehs efs a ->+    Eff u fr ehs' efs r+interpretKAllRecH = toInterpretKFromContT interpretContTAllRecH+{-# INLINE interpretKAllRecH #-}++interpretKAllH ::+    forall ehs' r a ehs efs fr u c.+    (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>+    (a -> Eff u fr ehs' efs r) ->+    ( forall x.+      (x -> Eff u fr ehs' efs r) ->+      u ehs (Eff u fr ehs efs) x ->+      Eff u fr ehs' efs r+    ) ->+    Eff u fr ehs efs a ->+    Eff u fr ehs' efs r+interpretKAllH = toInterpretKFromContT interpretContTAllH+{-# INLINE interpretKAllH #-}++interpretKAllRecFH ::+    forall g r a ehs efs fr u c.+    (MonadFreer c fr, Union u, HFunctor (u ehs)) =>+    (a -> g r) ->+    (forall x. (x -> g r) -> u ehs (ContT r g) x -> g r) ->+    (forall x. (x -> g r) -> u efs Nop x -> g r) ->+    Eff u fr ehs efs a ->+    g r+interpretKAllRecFH = toInterpretKFromContT2 interpretContTAllRecFH+{-# INLINE interpretKAllRecFH #-}++interpretKAllFH ::+    forall g r a ehs efs fr u c.+    (MonadFreer c fr, Union u) =>+    (a -> g r) ->+    (forall x. (x -> g r) -> u ehs (Eff u fr ehs efs) x -> g r) ->+    (forall x. (x -> g r) -> u efs Nop x -> g r) ->+    Eff u fr ehs efs a ->+    g r+interpretKAllFH = toInterpretKFromContT2 interpretContTAllFH+{-# INLINE interpretKAllFH #-}++interpretContTAll ::+    forall g r efs fr u c.+    (MonadFreer c fr, Union u) =>+    u efs Nop ~> ContT r g ->+    Eff u fr '[] efs ~> ContT r g+interpretContTAll f =+    transCont+        . interpretFreerK (caseHF exhaust (detransContT . f))+        . unHefty++interpretContTAllRecH ::+    forall ehs' r ehs efs fr u c.+    (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) =>+    u ehs (ContT r (Eff u fr ehs' efs)) ~> ContT r (Eff u fr ehs' efs) ->+    Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)+interpretContTAllRecH fh = interpretContTAllRecFH fh (lift . injectF)+{-# INLINE interpretContTAllRecH #-}++interpretContTAllH ::+    forall ehs' r ehs efs fr u c.+    (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>+    u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs) ->+    Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)+interpretContTAllH fh = interpretContTAllFH fh (lift . injectF)+{-# INLINE interpretContTAllH #-}++interpretContTAllRecFH ::+    forall g r ehs efs fr u c.+    (MonadFreer c fr, Union u, HFunctor (u ehs)) =>+    u ehs (ContT r g) ~> ContT r g ->+    u efs Nop ~> ContT r g ->+    Eff u fr ehs efs ~> ContT r g+interpretContTAllRecFH fh ff =+    transCont+        . interpretFreerK (detransContT . caseHF (fh . hfmap (interpretContTAllRecFH fh ff)) ff)+        . unHefty++interpretContTAllFH ::+    forall g r ehs efs fr u c.+    (MonadFreer c fr, Union u) =>+    u ehs (Eff u fr ehs efs) ~> ContT r g ->+    u efs Nop ~> ContT r g ->+    Eff u fr ehs efs ~> ContT r g+interpretContTAllFH fh ff =+    transCont+        . interpretFreerK (detransContT . caseHF fh ff)+        . unHefty++transCont :: Cont (m r) ~> ContT r m+transCont (ContT f) = ContT \k -> coerce $ f $ coerce . k+{-# INLINE transCont #-}++detransContT :: ContT r m ~> Cont (m r)+detransContT (ContT f) = ContT \k -> coerce $ f $ coerce . k+{-# INLINE detransContT #-}++toInterpretKFromContT ::+    ((e ~> ContT r m) -> f ~> ContT r m') ->+    (a -> m' r) ->+    (forall x. (x -> m r) -> e x -> m r) ->+    f a ->+    m' r+toInterpretKFromContT intContT k i = (`runContT` k) . intContT \e -> ContT (`i` e)+{-# INLINE toInterpretKFromContT #-}++toInterpretKFromContT2 ::+    ((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m') ->+    (a -> m' r) ->+    (forall x. (x -> m r) -> e1 x -> m r) ->+    (forall x. (x -> m r) -> e2 x -> m r) ->+    f a ->+    m' r+toInterpretKFromContT2 intContT k i1 i2 =+    (`runContT` k) . intContT (\e -> ContT (`i1` e)) (\e -> ContT (`i2` e))+{-# INLINE toInterpretKFromContT2 #-}++interpretTAll ::+    forall t g efs fr u c.+    (Freer c fr, Union u, c (t g)) =>+    u efs Nop ~> t g ->+    Eff u fr '[] efs ~> t g+interpretTAll = interpretAll+{-# INLINE interpretTAll #-}++interpretTAllRecH ::+    forall ehs' t ehs efs fr u c.+    ( Freer c fr+    , Union u+    , MonadTrans t+    , HFunctor (u ehs)+    , Monad (Eff u fr ehs' efs)+    , c (t (Eff u fr ehs' efs))+    ) =>+    u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs) ->+    Eff u fr ehs efs ~> t (Eff u fr ehs' efs)+interpretTAllRecH i = interpretAllRecFH i (lift . injectF)+{-# INLINE interpretTAllRecH #-}++interpretTAllH ::+    forall ehs' t ehs efs fr u c.+    (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs' efs), c (t (Eff u fr ehs' efs))) =>+    u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs) ->+    Eff u fr ehs efs ~> t (Eff u fr ehs' efs)+interpretTAllH i = interpretAllFH i (lift . injectF)+{-# INLINE interpretTAllH #-}++interpretAllRec ::+    forall efs' ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    u efs Nop ~> Eff u fr ehs efs' ->+    Eff u fr ehs efs ~> Eff u fr ehs efs'+interpretAllRec = interpretAllRecFHE injectH+{-# INLINE interpretAllRec #-}++transform ::+    forall e2 e1 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>+    (UnliftIfSingle e1 ~> UnliftIfSingle e2) ->+    Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r)+transform f =+    transformAll $+        inject0 . liftInsIfSingle . f . unliftInsIfSingle |+: weaken+{-# INLINE transform #-}++transformH ::+    forall e2 e1 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e1 ': r))) =>+    (e1 (Eff u fr (e2 ': r) efs) ~> e2 (Eff u fr (e2 ': r) efs)) ->+    Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs+transformH f = transformAllH $ inject0 . f |+: weaken+{-# INLINE transformH #-}++transformFH ::+    forall e2h e2f e1h e1f rh rf fr u c.+    (Freer c fr, Union u, HFunctor (u (e1h ': rh)), HeadIns e1f, HeadIns e2f) =>+    (e1h (Eff u fr (e2h ': rh) (e2f ': rf)) ~> e2h (Eff u fr (e2h ': rh) (e2f ': rf))) ->+    (UnliftIfSingle e1f ~> UnliftIfSingle e2f) ->+    Eff u fr (e1h ': rh) (e1f ': rf) ~> Eff u fr (e2h ': rh) (e2f ': rf)+transformFH fh ff =+    transformAllFH+        (inject0 . fh |+: weaken)+        (inject0 . liftInsIfSingle . ff . unliftInsIfSingle |+: weaken)+{-# INLINE transformFH #-}++translate ::+    forall e2 e1 es ehs fr u c.+    (Freer c fr, Union u, Member u e2 es, HFunctor (u ehs), HeadIns e1) =>+    (UnliftIfSingle e1 ~> e2) ->+    Eff u fr ehs (e1 ': es) ~> Eff u fr ehs es+translate f =+    transformAll $+        injectRec . LiftIns . f . unliftInsIfSingle |+: id+{-# INLINE translate #-}++translateH ::+    forall e2 e1 es efs fr u c.+    (Freer c fr, Union u, MemberH u e2 es, HFunctor (u (e1 ': es))) =>+    (e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs)) ->+    Eff u fr (e1 ': es) efs ~> Eff u fr es efs+translateH f = transformAllH $ injectRec . f |+: id+{-# INLINE translateH #-}++translateFH ::+    forall e2h e2f e1h e1f ehs efs fr u c.+    ( Freer c fr+    , Union u+    , MemberH u e2h ehs+    , Member u e2f efs+    , HFunctor (u (e1h ': ehs))+    , HeadIns e1f+    ) =>+    (e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs)) ->+    (UnliftIfSingle e1f ~> e2f) ->+    Eff u fr (e1h ': ehs) (e1f ': efs) ~> Eff u fr ehs efs+translateFH fh ff =+    transformAllFH+        (injectRec . fh |+: id)+        (injectRec . LiftIns . ff . unliftInsIfSingle |+: id)+{-# INLINE translateFH #-}++rewrite ::+    forall e efs ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), Member 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, Member 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)) =>+    u efs Nop ~> u efs' Nop ->+    Eff u fr ehs efs ~> Eff u fr ehs efs'+transformAll = transformAllFH id+{-# INLINE transformAll #-}++transformAllH ::+    forall ehs' ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs) ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs+transformAllH f = transformAllFH f id+{-# INLINE transformAllH #-}++transformAllFH ::+    forall ehs' efs' ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs') ->+    (u efs Nop ~> u efs' Nop) ->+    Eff u fr ehs efs ~> Eff u fr ehs' efs'+transformAllFH fh ff =+    overHefty $+        transformFreer $+            EffUnion+                . caseHF+                    (L1 . fh . hfmap (transformAllFH fh ff))+                    (R1 . ff)++raise ::+    forall e r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs r ~> Eff u fr ehs (e ': r)+raise = transformAll weaken+{-# INLINE raise #-}++raiseH ::+    forall e r efs fr u c.+    (Freer c fr, Union u, HFunctor (u r)) =>+    Eff u fr r efs ~> Eff u fr (e ': r) efs+raiseH = transformAllH weaken+{-# INLINE raiseH #-}++raise2H ::+    forall e2 e1 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u r)) =>+    Eff u fr r efs ~> Eff u fr (e2 ': e1 ': r) efs+raise2H = transformAllH weaken2+{-# INLINE raise2H #-}++raiseUnder ::+    forall e1 e2 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r)+raiseUnder = transformAll weakenUnder+{-# INLINE raiseUnder #-}++raiseUnder2 ::+    forall e1 e2 e3 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e3 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)+raiseUnder2 = transformAll weakenUnder2+{-# INLINE raiseUnder2 #-}++raiseUnder3 ::+    forall e1 e2 e3 e4 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e4 ': e3 ': e2 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)+raiseUnder3 = transformAll weakenUnder3+{-# INLINE raiseUnder3 #-}++raise2Under2 ::+    forall e1 e2 e3 e4 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e4 ': e3 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)+raise2Under2 = transformAll weaken2Under2+{-# INLINE raise2Under2 #-}++raise2Under ::+    forall e1 e2 e3 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)+raise2Under = transformAll weaken2Under+{-# INLINE raise2Under #-}++raise3Under ::+    forall e1 e2 e3 e4 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e4 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)+raise3Under = transformAll weaken3Under+{-# INLINE raise3Under #-}++raiseUnderH ::+    forall e1 e2 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e2 ': r))) =>+    Eff u fr (e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs+raiseUnderH = transformAllH weakenUnder+{-# INLINE raiseUnderH #-}++raiseUnder2H ::+    forall e1 e2 e3 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e3 ': e2 ': r))) =>+    Eff u fr (e3 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs+raiseUnder2H = transformAllH weakenUnder2+{-# INLINE raiseUnder2H #-}++raiseUnder3H ::+    forall e1 e2 e3 e4 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': e2 ': r))) =>+    Eff u fr (e4 ': e3 ': e2 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs+raiseUnder3H = transformAllH weakenUnder3+{-# INLINE raiseUnder3H #-}++raise2Under2H ::+    forall e1 e2 e3 e4 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': r))) =>+    Eff u fr (e4 ': e3 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs+raise2Under2H = transformAllH weaken2Under2+{-# INLINE raise2Under2H #-}++raise2UnderH ::+    forall e1 e2 e3 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e3 ': r))) =>+    Eff u fr (e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs+raise2UnderH = transformAllH weaken2Under+{-# INLINE raise2UnderH #-}++raise3UnderH ::+    forall e1 e2 e3 e4 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e4 ': r))) =>+    Eff u fr (e4 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs+raise3UnderH = transformAllH weaken3Under+{-# INLINE raise3UnderH #-}++raiseAll ::+    forall ehs efs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs '[] ~> Eff u fr ehs efs+raiseAll = transformAll exhaust+{-# INLINE raiseAll #-}++raiseAllH ::+    forall ehs efs fr u c.+    (Freer c fr, Union u) =>+    Eff u fr '[] efs ~> Eff u fr ehs efs+raiseAllH = overHefty $ transformFreer $ EffUnion . caseHF exhaust R1+{-# INLINE raiseAllH #-}++flipEff ::+    forall e1 e2 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e1 ': e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r)+flipEff = transformAll flipUnion+{-# INLINE flipEff #-}++flipEff3 ::+    forall e1 e2 e3 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e1 ': e2 ': e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)+flipEff3 = transformAll flipUnion3+{-# INLINE flipEff3 #-}++flipEffUnder ::+    forall e1 e2 e3 r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (e3 ': e1 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)+flipEffUnder = transformAll flipUnionUnder+{-# INLINE flipEffUnder #-}++flipEffH ::+    forall e1 e2 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': r))) =>+    Eff u fr (e1 ': e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs+flipEffH = transformAllH flipUnion+{-# INLINE flipEffH #-}++flipEff3H ::+    forall e1 e2 e3 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': e3 ': r))) =>+    Eff u fr (e1 ': e2 ': e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs+flipEff3H = transformAllH flipUnion3+{-# INLINE flipEff3H #-}++flipEffUnderH ::+    forall e1 e2 e3 r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e3 ': e1 ': e2 ': r))) =>+    Eff u fr (e3 ': e1 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs+flipEffUnderH = transformAllH flipUnionUnder+{-# INLINE flipEffUnderH #-}++subsume ::+    forall e r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), HasMembership u e r) =>+    Eff u fr ehs (e ': r) ~> Eff u fr ehs r+subsume = transformAll $ inject |+: id+{-# INLINE subsume #-}++subsumeH ::+    forall e r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembership u e r) =>+    Eff u fr (e ': r) efs ~> Eff u fr r efs+subsumeH = transformAllH $ inject |+: id+{-# INLINE subsumeH #-}++liftInsEff ::+    forall e eh ef fr u c.+    (Freer c fr, Union u, HFunctor (u eh), HFunctor e) =>+    Eff u fr eh (e ': ef) ~> Eff u fr (e ': eh) ef+liftInsEff =+    overHefty $+        transformFreer $+            EffUnion+                . caseHF+                    (L1 . weaken . hfmap liftInsEff)+                    (L1 . inject0 . hfmap \case {} |+: R1)++splitEff ::+    forall fr' e r ehs fr u c.+    (Freer c fr', Freer c fr, Union u, HeadIns e) =>+    Eff u fr '[] (e ': r) ~> fr' (UnliftIfSingle e + Eff u fr ehs r)+splitEff = interpretAll $ liftIns . (L1 . unliftInsIfSingle |+: R1 . injectF)+{-# INLINE splitEff #-}++mergeEff ::+    forall fr' e r ehs fr u c.+    (Freer c fr', Freer c fr, Union u, HeadIns e, c (Eff u fr ehs (e ': r)), HFunctor (u ehs)) =>+    fr' (UnliftIfSingle e + Eff u fr ehs r) ~> Eff u fr ehs (e ': r)+mergeEff = interpretFreer $ caseF send0 raise+{-# INLINE mergeEff #-}++mergeEffH ::+    forall fr' e r efs fr u c.+    ( Freer c fr'+    , Freer c fr+    , Union u+    , c (Eff u fr (e ': r) efs)+    , HFunctor (u r)+    , HFunctor e+    ) =>+    Hefty fr' (e :+: LiftIns (Eff u fr r efs)) ~> Eff u fr (e ': r) efs+mergeEffH =+    interpretFreer+        ( caseH+            (send0H . hfmap mergeEffH)+            (raiseH . unliftIns)+        )+        . unHefty++send0 :: (Freer c fr, Union u, HeadIns e) => UnliftIfSingle e ~> Eff u fr eh (e ': r)+send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle+{-# INLINE send0 #-}++send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r)+send1 = Hefty . liftIns . EffUnion . R1 . weaken . inject0 . liftInsIfSingle+{-# INLINE send1 #-}++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 #-}++send1H :: (Freer c fr, Union u) => e1 (Eff u fr (e2 ': e1 ': r) ef) ~> Eff u fr (e2 ': e1 ': r) ef+send1H = Hefty . liftIns . EffUnion . L1 . weaken . inject0+{-# INLINE send1H #-}++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 #-}++runPure :: forall a fr u c. (Freer c fr, Union u, c Identity) => Eff u fr '[] '[] a -> a+runPure = runIdentity . interpretAll exhaust+{-# INLINE runPure #-}++untagEff ::+    forall tag e r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (LiftIns (e # tag) ': r) ~> Eff u fr ehs (LiftIns e ': r)+untagEff = transform unTag+{-# INLINE untagEff #-}++untagEffH ::+    forall tag e r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (e ## tag ': r))) =>+    Eff u fr (e ## tag ': r) efs ~> Eff u fr (e ': r) efs+untagEffH = transformH unTagH+{-# INLINE untagEffH #-}++-- keyed effects++instance+    (MemberRec u (LiftIns (key #> e)) efs, LiftIns (key #> e) ~ FromJust (Lookup key efs)) =>+    InjectInsBy key e (EffUnion u ehs efs f)+    where+    injectInsBy = EffUnion . R1 . injectRec . LiftIns . Key @key+    {-# INLINE injectInsBy #-}++instance+    (MemberRec u (key ##> e) ehs, key ##> e ~ FromJust (Lookup key ehs)) =>+    InjectSigBy key e (EffUnion u ehs efs)+    where+    injectSigBy = EffUnion . L1 . injectRec . KeyH @key+    {-# INLINE injectSigBy #-}++unkeyEff ::+    forall key e r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs)) =>+    Eff u fr ehs (LiftIns (key #> e) ': r) ~> Eff u fr ehs (LiftIns e ': r)+unkeyEff = transform unKey+{-# INLINE unkeyEff #-}++unkeyEffH ::+    forall key e r efs fr u c.+    (Freer c fr, Union u, HFunctor (u (key ##> e ': r))) =>+    Eff u fr (key ##> e ': r) efs ~> Eff u fr (e ': r) efs+unkeyEffH = transformH unKeyH+{-# INLINE unkeyEffH #-}++keySubsume ::+    forall key e r ehs fr u c.+    (Freer c fr, Union u, HFunctor (u ehs), MemberBy u key e r) =>+    Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs r+keySubsume = interpretRec $ sendInsBy @key+{-# INLINE keySubsume #-}++keySubsumeH ::+    forall key e r efs fr u c.+    (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u r, MemberHBy u key e r) =>+    Eff u fr (e ': r) efs ~> Eff u fr r efs+keySubsumeH = interpretRecH $ sendSigBy @key+{-# INLINE keySubsumeH #-}++end :: Union u => u '[] f a -> x+end = exhaust+{-# INLINE end #-}

@@ -1,4 +1,6 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}  -- 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@@ -15,45 +17,147 @@ -} module Control.Freer where +import Control.Applicative (Alternative, empty, (<|>)) import Control.Applicative.Free (Ap, liftAp, runAp)-import Control.Effect.Class (type (~>))+import Control.Applicative.Free.Fast qualified as Fast+import Control.Effect (SendIns, sendIns, type (~>))+import Control.Effect.Key (SendInsBy, sendInsBy)+import Control.Monad (MonadPlus)+import Control.Monad.Base (MonadBase)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.State.Class (MonadState, get, put)+import Data.Bool (bool)+import Data.Effect (InsClass)+import Data.Effect.Fail (Fail (Fail))+import Data.Effect.NonDet (Choose, Empty, choose)+import Data.Effect.NonDet qualified as NonDet+import Data.Effect.State (State, get'', put'') import Data.Functor.Coyoneda (Coyoneda, hoistCoyoneda, liftCoyoneda, lowerCoyoneda)+import Data.Kind (Type)  -- | A type class to abstract away the encoding details of the Freer carrier.-class (forall ins. c (f ins)) => Freer c f | f -> c where-    {-# MINIMAL liftIns, (interpretF | retract, transformF) #-}+class (forall e. c (f e)) => Freer c f | f -> c where+    {-# MINIMAL liftIns, (interpretFreer | retractFreer, transformFreer) #-}      -- | Lift a /instruction/ into a Freer carrier.-    liftIns :: ins a -> f ins a+    liftIns :: e a -> f e a -    interpretF :: c m => (ins ~> m) -> f ins a -> m a-    interpretF i = retract . transformF i-    {-# INLINE interpretF #-}+    interpretFreer :: c m => (e ~> m) -> f e a -> m a+    interpretFreer i = retractFreer . transformFreer i+    {-# INLINE interpretFreer #-} -    retract :: c m => f m a -> m a-    retract = interpretF id-    {-# INLINE retract #-}+    retractFreer :: c m => f m a -> m a+    retractFreer = interpretFreer id+    {-# INLINE retractFreer #-}      -- | Translate /instruction/s embedded in a Freer carrier.-    transformF ::-        (ins ~> ins') ->-        f ins a ->-        f ins' a-    transformF phi = interpretF $ liftIns . phi-    {-# INLINE transformF #-}+    transformFreer ::+        (e ~> e') ->+        f e a ->+        f e' a+    transformFreer phi = interpretFreer $ liftIns . phi+    {-# INLINE transformFreer #-} -    reinterpretF :: (ins ~> f ins) -> f ins a -> f ins a-    reinterpretF = interpretF-    {-# INLINE reinterpretF #-}+    reinterpretFreer :: (e ~> f e) -> f e a -> f e a+    reinterpretFreer = interpretFreer+    {-# INLINE reinterpretFreer #-}  instance Freer Functor Coyoneda where     liftIns = liftCoyoneda-    interpretF i = lowerCoyoneda . hoistCoyoneda i+    interpretFreer i = lowerCoyoneda . hoistCoyoneda i     {-# INLINE liftIns #-}-    {-# INLINE interpretF #-}+    {-# INLINE interpretFreer #-}  instance Freer Applicative Ap where     liftIns = liftAp-    interpretF = runAp+    interpretFreer = runAp     {-# INLINE liftIns #-}-    {-# INLINE interpretF #-}+    {-# INLINE interpretFreer #-}++instance Freer Applicative Fast.Ap where+    liftIns = Fast.liftAp+    interpretFreer = Fast.runAp+    {-# INLINE liftIns #-}+    {-# INLINE interpretFreer #-}++newtype+    ViaFreer+        (fr :: InsClass -> Type -> Type)+        (e :: InsClass)+        (a :: Type) = ViaFreer+    {viaFreer :: fr e a}++deriving newtype instance Functor (fr e) => Functor (ViaFreer fr e)+deriving newtype instance Applicative (fr e) => Applicative (ViaFreer fr e)+deriving newtype instance Monad (fr e) => Monad (ViaFreer fr e)+deriving newtype instance (MonadBase b (fr e), Monad b) => MonadBase b (ViaFreer fr e)++deriving newtype instance Foldable (fr e) => Foldable (ViaFreer fr e)+deriving stock instance Traversable (fr e) => Traversable (ViaFreer fr e)+deriving newtype instance Eq (fr e a) => Eq (ViaFreer fr e a)+deriving newtype instance Ord (fr e a) => Ord (ViaFreer fr e a)+deriving newtype instance Read (fr e a) => Read (ViaFreer fr e a)+deriving newtype instance Show (fr e a) => Show (ViaFreer fr e a)++deriving newtype instance (Freer c fr, forall e. c (ViaFreer fr e)) => Freer c (ViaFreer fr)++instance (Freer c fr, InjectIns e e') => SendIns e (ViaFreer fr e') where+    sendIns = ViaFreer . liftIns . injectIns+    {-# INLINE sendIns #-}++class InjectIns e (e' :: InsClass) where+    injectIns :: e ~> e'++instance (Freer c fr, InjectInsBy key e e') => SendInsBy key e (ViaFreer fr e') where+    sendInsBy = ViaFreer . liftIns . injectInsBy @key+    {-# INLINE sendInsBy #-}++class InjectInsBy key e (e' :: InsClass) | key e' -> e where+    injectInsBy :: e ~> e'++overFreer :: (fr e a -> fr' e' b) -> ViaFreer fr e a -> ViaFreer fr' e' b+overFreer f = ViaFreer . f . viaFreer+{-# INLINE overFreer #-}++reencodeFreer :: (Freer c fr, Freer c' fr', c (fr' f)) => fr f ~> fr' f+reencodeFreer = interpretFreer liftIns+{-# INLINE reencodeFreer #-}++instance (Freer c fr, InjectInsBy StateKey (State s) e, Monad (fr e)) => MonadState s (ViaFreer fr e) where+    get = get'' @StateKey+    put = put'' @StateKey+    {-# INLINE get #-}+    {-# INLINE put #-}++data StateKey++instance+    ( Freer c fr+    , InjectIns Empty e+    , InjectIns Choose e+    , Monad (fr e)+    ) =>+    Alternative (ViaFreer fr e)+    where+    empty = NonDet.empty+    a <|> b = do+        world <- choose+        bool a b world+    {-# INLINE empty #-}+    {-# INLINE (<|>) #-}++instance+    ( Freer c fr+    , InjectIns Empty e+    , InjectIns Choose e+    , Monad (fr e)+    ) =>+    MonadPlus (ViaFreer fr e)++instance (Freer c fr, InjectIns IO e, Monad (fr e)) => MonadIO (ViaFreer fr e) where+    liftIO = ViaFreer . liftIns . injectIns+    {-# INLINE liftIO #-}++instance (Freer c fr, InjectIns Fail e, Monad (fr e)) => MonadFail (ViaFreer fr e) where+    fail = ViaFreer . liftIns . injectIns . Fail+    {-# INLINE fail #-}

@@ -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 Monad (FreerFinal Monad)

@@ -1,70 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}---- 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 type class to abstract away the encoding details of the Freer carrier transformers.--}-module Control.Freer.Trans where--import Control.Effect.Class (type (~>))-import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)-import Data.Free.Sum (pattern L1, pattern R1, type (+))---- | A type class to abstract away the encoding details of the Freer carrier transformers.-class (forall ins f. c f => c (fr ins f)) => TransFreer c fr | fr -> c where-    {-# MINIMAL liftInsT, liftLowerFT, (hoistFreer, runInterpretF | interpretFT) #-}--    -- | Lift a /instruction/ into a Freer carrier transformer.-    liftInsT :: ins ~> fr ins f--    liftLowerFT :: forall ins f. c f => f ~> fr ins f--    -- | Translate /instruction/s embedded in a Freer carrier transformer.-    transformT :: c f => (ins ~> ins') -> fr ins f ~> fr ins' f-    transformT f = interpretFT liftLowerFT (liftInsT . f)-    {-# INLINE transformT #-}--    -- | Translate an underlying carrier.-    hoistFreer :: (c f, c g) => (f ~> g) -> fr ins f ~> fr ins g-    hoistFreer f = interpretFT (liftLowerFT . f) liftInsT-    {-# INLINE hoistFreer #-}--    interposeLowerT :: (c f, c g) => (f ~> fr ins g) -> fr ins f ~> fr ins g-    interposeLowerT f = interpretFT f liftInsT-    {-# INLINE interposeLowerT #-}--    runInterpretF :: c f => (ins ~> f) -> fr ins f a -> f a-    default runInterpretF :: (c f, c (IdentityT f)) => (ins ~> f) -> fr ins f a -> f a-    runInterpretF f = runIdentityT . interpretFT IdentityT (IdentityT . f)-    {-# INLINE runInterpretF #-}--    interpretFT :: (c f, c g) => (f ~> g) -> (ins ~> g) -> fr ins f ~> g-    interpretFT f i = runInterpretF i . hoistFreer f-    {-# INLINE interpretFT #-}--    reinterpretFT :: c f => (ins ~> fr ins f) -> fr ins f ~> fr ins f-    reinterpretFT = interpretFT liftLowerFT-    {-# INLINE reinterpretFT #-}--mergeFreer ::-    forall fr m ins ins' c.-    (TransFreer c fr, c m) =>-    fr ins (fr ins' m) ~> fr (ins + ins') m-mergeFreer = interpretFT (transformT @c R1) (liftInsT @c . L1)--splitFreer ::-    forall fr m ins ins' c.-    (TransFreer c fr, c m) =>-    fr (ins + ins') m ~> fr ins (fr ins' m)-splitFreer = interpretFT (liftLowerFT . liftLowerFT) \case-    L1 e -> liftInsT e-    R1 e -> liftLowerFT $ liftInsT e

@@ -1,45 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}---- 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 type class to abstract away the encoding details of the Heftia carriers.--}-module Control.Heftia where--import Control.Effect.Class (LiftIns, unliftIns, type (~>))-import Control.Effect.Class.Machinery.HFunctor (HFunctor)---- | A type class to abstract away the encoding details of the Heftia carrier.-class (forall sig. HFunctor sig => c (h sig)) => Heftia c h | h -> c where-    {-# MINIMAL liftSig, interpretHH #-}--    -- | Lift a /signature/ into a Heftia carrier.-    liftSig :: HFunctor sig => sig (h sig) a -> h sig a--    interpretHH :: (c m, HFunctor sig) => (sig m ~> m) -> h sig a -> m a--    -- | Translate /signature/s embedded in a Heftia carrier.-    translateHH ::-        (HFunctor sig, HFunctor sig') =>-        (sig (h sig') ~> sig' (h sig')) ->-        h sig a ->-        h sig' a-    translateHH phi = interpretHH $ liftSig . phi-    {-# INLINE translateHH #-}--    reinterpretHH :: HFunctor sig => (sig (h sig) ~> h sig) -> h sig a -> h sig a-    reinterpretHH = interpretHH-    {-# INLINE reinterpretHH #-}--retractH :: (Heftia c h, c m) => h (LiftIns m) a -> m a-retractH = interpretHH unliftIns-{-# INLINE retractH #-}

@@ -1,89 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}-{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}--{-# HLINT ignore "Eta reduce" #-}---- 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 type class to abstract away the encoding details of the Heftia carrier transformers.--}-module Control.Heftia.Trans where--import Control.Effect.Class (LiftIns (LiftIns), unliftIns, type (~>))-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))-import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)-import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)---- | A type class to abstract away the encoding details of the Heftia carrier transformers.-class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where-    {-# MINIMAL liftSigT, liftLowerHT, (hoistHeftia, runElaborateH | elaborateHT) #-}--    -- | Lift a /signature/ into a Heftia carrier transformer.-    liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a--    transformHT ::-        (c f, HFunctor sig, HFunctor sig') =>-        (forall g. sig g ~> sig' g) ->-        h sig f ~> h sig' f-    transformHT f = translateT f-    {-# INLINE transformHT #-}--    -- | Translate /signature/s embedded in a Heftia carrier transformer.-    translateT ::-        (c f, HFunctor sig, HFunctor sig') =>-        (sig (h sig' f) ~> sig' (h sig' f)) ->-        h sig f ~> h sig' f-    translateT f = elaborateHT liftLowerHT (liftSigT . f)-    {-# INLINE translateT #-}--    liftLowerHT :: forall sig f. (c f, HFunctor sig) => f ~> h sig f--    -- | Translate an underlying monad.-    hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f ~> h sig g-    hoistHeftia phi = elaborateHT (liftLowerHT . phi) liftSigT-    {-# INLINE hoistHeftia #-}--    interpretLowerHT :: (HFunctor sig, c f, c g) => (f ~> h sig g) -> h sig f ~> h sig g-    interpretLowerHT f = elaborateHT f liftSigT-    {-# INLINE interpretLowerHT #-}--    runElaborateH :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f ~> f-    default runElaborateH :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f ~> f-    runElaborateH f = runIdentityT . elaborateHT IdentityT (IdentityT . f . hfmap runIdentityT)-    {-# INLINE runElaborateH #-}--    elaborateHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f ~> g-    elaborateHT f i = runElaborateH i . hoistHeftia f-    {-# INLINE elaborateHT #-}--    reelaborateHT :: (c f, HFunctor sig) => (sig (h sig f) ~> h sig f) -> h sig f ~> h sig f-    reelaborateHT = elaborateHT liftLowerHT-    {-# INLINE reelaborateHT #-}--heftiaToFreer ::-    (TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>-    h (LiftIns ins) f ~> fr ins f-heftiaToFreer = elaborateHT liftLowerFT (liftInsT . unliftIns)-{-# INLINE heftiaToFreer #-}--freerToHeftia ::-    (TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f), c' (h (LiftIns ins) f), c f) =>-    fr ins f ~> h (LiftIns ins) f-freerToHeftia = interpretFT liftLowerHT (liftSigT . LiftIns)-{-# INLINE freerToHeftia #-}--mergeHeftia ::-    forall h m sig sig' a c.-    (HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>-    h sig (h sig' m) a ->-    h (sig :+: sig') m a-mergeHeftia = elaborateHT (translateT @c Inr) (liftSigT @c . Inl)

@@ -0,0 +1,182 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}++-- 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.Hefty where++import Control.Applicative (Alternative, empty, (<|>))+import Control.Effect (SendIns (..), SendSig (..), type (~>))+import Control.Effect.Key (ByKey (ByKey), SendInsBy, SendSigBy, key, sendInsBy, sendSigBy)+import Control.Freer (Freer (liftIns), InjectIns, InjectInsBy, StateKey, injectIns, injectInsBy)+import Control.Monad (MonadPlus)+import Control.Monad.Base (MonadBase)+import Control.Monad.Fix (MonadFix, mfix)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.RWS.Class (MonadRWS)+import Control.Monad.Reader.Class (MonadReader, ask, local)+import Control.Monad.State.Class (MonadState, get, put)+import Control.Monad.Writer.Class (MonadWriter, listen, pass, tell)+import Data.Effect (InsClass, SigClass)+import Data.Effect.Fail (Fail)+import Data.Effect.Fail qualified as E+import Data.Effect.Fix (Fix)+import Data.Effect.Fix qualified as E+import Data.Effect.NonDet (ChooseH, Empty, chooseH)+import Data.Effect.NonDet qualified as NonDet+import Data.Effect.Reader (Ask, Local, ask'', local'')+import Data.Effect.State (State, get'', put'')+import Data.Effect.Unlift (UnliftIO, pattern WithRunInIO)+import Data.Effect.Writer (Tell, WriterH, listen'', tell'')+import Data.Function ((&))+import Data.Kind (Type)+import Data.Tuple (swap)+import UnliftIO (MonadUnliftIO, withRunInIO)++newtype+    Hefty+        (f :: InsClass -> Type -> Type)+        (e :: SigClass)+        (a :: Type) = Hefty+    {unHefty :: f (e (Hefty f e)) a}++deriving newtype instance Functor (f (e (Hefty f e))) => Functor (Hefty f e)+deriving newtype instance Applicative (f (e (Hefty f e))) => Applicative (Hefty f e)+deriving newtype instance Monad (f (e (Hefty f e))) => Monad (Hefty f e)+deriving newtype instance (MonadBase b (f (e (Hefty f e))), Monad b) => MonadBase b (Hefty f e)++deriving newtype instance Foldable (f (e (Hefty f e))) => Foldable (Hefty f e)+deriving stock instance Traversable (f (e (Hefty f e))) => Traversable (Hefty f e)+deriving newtype instance Eq (f (e (Hefty f e)) a) => Eq (Hefty f e a)+deriving newtype instance Ord (f (e (Hefty f e)) a) => Ord (Hefty f e a)+deriving newtype instance Read (f (e (Hefty f e)) a) => Read (Hefty f e a)+deriving newtype instance Show (f (e (Hefty f e)) a) => Show (Hefty f e a)++overHefty ::+    (f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b) ->+    Hefty f e a ->+    Hefty f' e' b+overHefty f = Hefty . f . unHefty+{-# INLINE overHefty #-}++instance (Freer c fr, InjectIns e (e' (Hefty fr e'))) => SendIns e (Hefty fr e') where+    sendIns = Hefty . liftIns . injectIns+    {-# INLINE sendIns #-}++instance (Freer c fr, InjectSig e e') => SendSig e (Hefty fr e') where+    sendSig = Hefty . liftIns . injectSig+    {-# INLINE sendSig #-}++class InjectSig e (e' :: SigClass) where+    injectSig :: e f ~> e' f++instance (Freer c fr, InjectInsBy key e (e' (Hefty fr e'))) => SendInsBy key e (Hefty fr e') where+    sendInsBy = Hefty . liftIns . injectInsBy @key+    {-# INLINE sendInsBy #-}++instance (Freer c fr, InjectSigBy key e e') => SendSigBy key e (Hefty fr e') where+    sendSigBy = Hefty . liftIns . injectSigBy @key+    {-# INLINE sendSigBy #-}++class InjectSigBy key e (e' :: SigClass) | key e' -> e where+    injectSigBy :: e f ~> e' f++instance+    ( Freer c fr+    , InjectInsBy ReaderKey (Ask r) (e (Hefty fr e))+    , InjectSigBy ReaderKey (Local r) e+    , Monad (fr (e (Hefty fr e)))+    ) =>+    MonadReader r (Hefty fr e)+    where+    ask = ask'' @ReaderKey+    local = local'' @ReaderKey+    {-# INLINE ask #-}+    {-# INLINE local #-}++data ReaderKey++instance+    ( Freer c fr+    , InjectInsBy WriterKey (Tell w) (e (Hefty fr e))+    , InjectSigBy WriterKey (WriterH w) e+    , Monoid w+    , Monad (fr (e (Hefty fr e)))+    ) =>+    MonadWriter w (Hefty fr e)+    where+    tell = tell'' @WriterKey+    listen = fmap swap . listen'' @WriterKey+    pass m = pass (ByKey m) & key @WriterKey+    {-# INLINE tell #-}+    {-# INLINE listen #-}++data WriterKey++instance+    (Freer c fr, InjectInsBy StateKey (State s) (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) =>+    MonadState s (Hefty fr e)+    where+    get = get'' @StateKey+    put = put'' @StateKey+    {-# INLINE get #-}+    {-# INLINE put #-}++instance+    ( Freer c fr+    , InjectInsBy ReaderKey (Ask r) (e (Hefty fr e))+    , InjectSigBy ReaderKey (Local r) e+    , InjectInsBy WriterKey (Tell w) (e (Hefty fr e))+    , InjectSigBy WriterKey (WriterH w) e+    , InjectInsBy StateKey (State s) (e (Hefty fr e))+    , Monoid w+    , Monad (fr (e (Hefty fr e)))+    ) =>+    MonadRWS r w s (Hefty fr e)++instance+    ( Freer c fr+    , InjectIns Empty (e (Hefty fr e))+    , InjectSig ChooseH e+    , Applicative (fr (e (Hefty fr e)))+    ) =>+    Alternative (Hefty fr e)+    where+    empty = NonDet.empty+    a <|> b = chooseH a b+    {-# INLINE empty #-}+    {-# INLINE (<|>) #-}++instance+    ( Freer c fr+    , InjectIns Empty (e (Hefty fr e))+    , InjectSig ChooseH e+    , Monad (fr (e (Hefty fr e)))+    ) =>+    MonadPlus (Hefty fr e)++instance (Freer c fr, InjectIns IO (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) => MonadIO (Hefty fr e) where+    liftIO = sendIns+    {-# INLINE liftIO #-}++instance (Freer c fr, InjectIns Fail (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) => MonadFail (Hefty fr e) where+    fail = E.fail+    {-# INLINE fail #-}++instance (Freer c fr, InjectSig Fix e, Monad (fr (e (Hefty fr e)))) => MonadFix (Hefty fr e) where+    mfix = E.mfix+    {-# INLINE mfix #-}++instance+    ( Freer c fr+    , InjectIns IO (e (Hefty fr e))+    , InjectSig UnliftIO e+    , Monad (fr (e (Hefty fr e)))+    ) =>+    MonadUnliftIO (Hefty fr e)+    where+    withRunInIO f = Hefty . liftIns . injectSig $ WithRunInIO f+    {-# INLINE withRunInIO #-}

@@ -0,0 +1,21 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Eta reduce" #-}++-- 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.Monad.Freer where++import Control.Effect (type (~>))+import Control.Freer (Freer, interpretFreer)+import Control.Monad.Cont (Cont)++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 #-}

@@ -0,0 +1,58 @@+-- 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 Church-encoded Freer monad.+-}+module Control.Monad.Freer.Church where++import Control.Effect (type (~>))+import Control.Freer (Freer, interpretFreer, liftIns, retractFreer, transformFreer)+import Control.Monad.Cont (Cont, ContT (ContT), runCont)+import Control.Monad.Freer (MonadFreer, interpretFreerK)+import Control.Monad.Identity (Identity (Identity), runIdentity)+import Control.Monad.Trans.Free.Church (FT (FT), retract, transFT)++-- | A Church encoded Freer monad.+newtype FreerChurch f a = FreerChurch {unFreerChurch :: FT f Identity a}+    deriving newtype+        ( Functor+        , Applicative+        , Monad+        , Eq+        , Ord+        )+    deriving stock (Foldable, Traversable)++liftInsChurch :: ins a -> FreerChurch ins a+liftInsChurch e = FreerChurch $ FT \k f -> f k e+{-# INLINE liftInsChurch #-}++interpretChurch :: Monad m => (ins ~> m) -> FreerChurch ins a -> m a+interpretChurch i = retract . transFT i . unFreerChurch+{-# INLINE interpretChurch #-}++interpretChurchK :: (e ~> Cont r) -> FreerChurch e ~> Cont r+interpretChurchK i (FreerChurch (FT f)) =+    ContT \k -> f k \k' e -> Identity $ runCont (i e) (runIdentity . k')++instance Freer Monad FreerChurch where+    liftIns = liftInsChurch+    interpretFreer = interpretChurch+    retractFreer = retract . unFreerChurch+    transformFreer phi = FreerChurch . transFT phi . unFreerChurch+    {-# INLINE liftIns #-}+    {-# INLINE interpretFreer #-}+    {-# INLINE retractFreer #-}+    {-# INLINE transformFreer #-}++instance MonadFreer Monad FreerChurch where+    interpretFreerK = interpretChurchK+    {-# INLINE interpretFreerK #-}

@@ -0,0 +1,74 @@+{-# LANGUAGE DerivingVia #-}++-- 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 tree-structured encoded Freer monad.+-}+module Control.Monad.Freer.Tree where++import Control.Applicative (Alternative)+import Control.Effect (type (~>))+import Control.Freer (Freer, interpretFreer, liftIns, transformFreer)+import Control.Monad (MonadPlus)+import Control.Monad.Cont (Cont, ContT (ContT), runCont)+import Control.Monad.Free (Free (Free, Pure), hoistFree, liftF)+import Control.Monad.Freer (MonadFreer, interpretFreerK)+import Control.Monad.Identity (Identity (Identity), runIdentity)+import Data.Functor.Coyoneda (Coyoneda (Coyoneda), hoistCoyoneda, liftCoyoneda)++-- | A tree-structured encoded Freer monad.+newtype FreerTree f a = FreerTree {unFreerTree :: Free (Coyoneda f) a}+    deriving newtype+        ( Functor+        , Applicative+        , Monad+        , Alternative+        , MonadPlus+        , Eq+        , Ord+        , Read+        , Show+        )+    deriving stock (Foldable, Traversable)++liftInsTree :: ins a -> FreerTree ins a+liftInsTree = FreerTree . liftF . liftCoyoneda+{-# INLINE liftInsTree #-}++interpretTree :: Monad m => (ins ~> m) -> FreerTree ins a -> m a+interpretTree i (FreerTree m) =+    case m of+        Pure x -> pure x+        Free (Coyoneda f e) -> i e >>= interpretTree i . FreerTree . f++interpretTreeK :: (e ~> Cont r) -> FreerTree e ~> Cont r+interpretTreeK i (FreerTree m) =+    case m of+        Pure x -> pure x+        Free (Coyoneda f e) ->+            ContT \k ->+                Identity $+                    runCont+                        (i e)+                        ((`runCont` runIdentity . k) . interpretTreeK i . FreerTree . f)++instance Freer Monad FreerTree where+    liftIns = liftInsTree+    interpretFreer = interpretTree+    transformFreer phi = FreerTree . hoistFree (hoistCoyoneda phi) . unFreerTree+    {-# INLINE liftIns #-}+    {-# INLINE interpretFreer #-}+    {-# INLINE transformFreer #-}++instance MonadFreer Monad FreerTree where+    interpretFreerK = interpretTreeK+    {-# INLINE interpretFreerK #-}

@@ -1,71 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}---- 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 type class to abstract away the encoding details of the Freer monad transformers.--}-module Control.Monad.Trans.Freer where--import Control.Effect.Class (Instruction, type (~>))-import Control.Freer.Trans (TransFreer, hoistFreer, interpretFT, liftLowerFT)-import Control.Monad.Cont (ContT)-import Control.Monad.Trans (MonadTrans, lift)-import Data.Coerce (Coercible, coerce)-import Data.Kind (Type)---- | A type class to abstract away the encoding details of the Freer monad transformers.-class-    (TransFreer Monad fr, forall ins. MonadTrans (fr ins)) =>-    MonadTransFreer fr-    where-    interpretMK :: Monad m => (ins ~> ContT r m) -> fr ins m ~> ContT r m-    interpretMK = interpretMT-    {-# INLINE interpretMK #-}--    reinterpretMK :: Monad m => (ins ~> ContT r (fr ins m)) -> fr ins m ~> ContT r (fr ins m)-    reinterpretMK = reinterpretMT-    {-# INLINE reinterpretMK #-}--    interpretMT :: (Monad m, MonadTrans t, Monad (t m)) => (ins ~> t m) -> fr ins m ~> t m-    interpretMT = interpretFT lift-    {-# INLINE interpretMT #-}--    reinterpretMT ::-        forall m t n ins.-        (Monad m, MonadTrans t, Coercible n (fr ins m), Monad (t n), Monad n) =>-        (ins ~> t n) ->-        fr ins m ~> t n-    reinterpretMT f = interpretMT f . hoistFreer (coerce . liftLowerFT @Monad @fr @ins)-    {-# INLINE reinterpretMT #-}--reinterpretTTViaFinal ::-    forall fr m t n ins.-    ( MonadTransFreer fr-    , Monad m-    , MonadTrans t-    , Coercible n (fr ins m)-    , Monad (t n)-    , Monad n-    ) =>-    (ins ~> t n) ->-    fr ins m ~> t n-reinterpretTTViaFinal = interpretFT $ lift . coerce . liftLowerFT @Monad @fr @ins-{-# INLINE reinterpretTTViaFinal #-}--newtype ViaLiftLower (fr :: Instruction -> (Type -> Type) -> Type -> Type) ins m a = ViaLiftLower-    {runViaLiftLower :: fr ins m a}-    deriving newtype (Functor, Applicative, Monad)-    deriving stock (Foldable, Traversable)--instance TransFreer Monad h => MonadTrans (ViaLiftLower h ins) where-    lift = ViaLiftLower . liftLowerFT-    {-# INLINE lift #-}

@@ -1,56 +0,0 @@-{-# LANGUAGE DerivingVia #-}---- 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 Church-encoded Freer transformer.--}-module Control.Monad.Trans.Freer.Church where--import Control.Effect.Class (Instruction, LiftIns (..))-import Control.Freer.Trans (TransFreer (hoistFreer, liftInsT, liftLowerFT, runInterpretF))-import Control.Heftia.Trans (TransHeftia (..), liftSigT)-import Control.Monad.Trans (MonadTrans)-import Control.Monad.Trans.Freer (-    MonadTransFreer (interpretMK, reinterpretMK),-    ViaLiftLower (ViaLiftLower),- )-import Control.Monad.Trans.Heftia.Church (HeftiaChurchT (HeftiaChurchT))---- | A Church-encoded Freer transformer.-newtype FreerChurchT (ins :: Instruction) f a = FreerChurchT-    {unFreerChurchT :: HeftiaChurchT (LiftIns ins) f a}--deriving newtype instance Functor (FreerChurchT ins m)-deriving newtype instance Applicative (FreerChurchT ins m)-deriving newtype instance Monad (FreerChurchT ins m)--instance TransFreer Monad FreerChurchT where-    liftInsT = FreerChurchT . liftSigT . LiftIns-    {-# INLINE liftInsT #-}--    liftLowerFT = FreerChurchT . liftLowerHT-    {-# INLINE liftLowerFT #-}--    runInterpretF i = runElaborateH (i . unliftIns) . unFreerChurchT-    {-# INLINE runInterpretF #-}--    hoistFreer phi = FreerChurchT . hoistHeftia phi . unFreerChurchT-    {-# INLINE hoistFreer #-}--deriving via ViaLiftLower FreerChurchT ins instance MonadTrans (FreerChurchT ins)--instance MonadTransFreer FreerChurchT where-    interpretMK f (FreerChurchT (HeftiaChurchT g)) = g $ f . unliftIns-    {-# INLINE interpretMK #-}--    reinterpretMK f = interpretMK f . hoistFreer liftLowerFT-    {-# INLINE reinterpretMK #-}

@@ -1,83 +0,0 @@-{-# LANGUAGE DerivingVia #-}---- 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 tree-structured encoded Freer transformer.--}-module Control.Monad.Trans.Freer.Tree where--import Control.Applicative (Alternative)-import Control.Effect.Class (type (~>))-import Control.Freer (Freer, interpretF, liftIns)-import Control.Monad (MonadPlus)-import Control.Monad.Base (MonadBase)-import Control.Monad.Identity (Identity, runIdentity)-import Control.Monad.Trans (MonadIO, MonadTrans)-import Control.Monad.Trans.Free (FreeF (Free, Pure), FreeT (FreeT), MonadFree, liftF)-import Data.Functor.Coyoneda (Coyoneda (Coyoneda), liftCoyoneda)---- | A tree-structured encoded Freer transformer.-newtype FreerTreeT f m a = FreerTreeT {unFreerTreeT :: FreeT (Coyoneda f) m a}-    deriving newtype-        ( Functor-        , Applicative-        , Monad-        , Alternative-        , MonadPlus-        , MonadBase b-        , MonadIO-        , MonadFail-        , Eq-        , Ord-        , Read-        , Show-        , MonadTrans-        )-    deriving stock (Foldable, Traversable)--newtype FreerTreeMonad m f a = FreerTreeMonad {unFreerTreeMonad :: FreerTreeT f m a}-    deriving newtype-        ( Functor-        , Applicative-        , Alternative-        , Monad-        , MonadPlus-        , MonadBase b-        , MonadIO-        , MonadFail-        , Eq-        , Ord-        , Read-        , Show-        )-    deriving stock (Foldable, Traversable)-    deriving (MonadFree (Coyoneda f)) via FreeT (Coyoneda f) m--liftInsTree :: Monad m => ins a -> FreerTreeT ins m a-liftInsTree = FreerTreeT . liftF . liftCoyoneda-{-# INLINE liftInsTree #-}--interpretTTree :: Monad n => (m ~> n) -> (ins ~> n) -> FreerTreeT ins m a -> n a-interpretTTree iLower i (FreerTreeT (FreeT m)) =-    iLower m >>= \case-        Pure x -> pure x-        Free (Coyoneda f e) -> i e >>= interpretTTree iLower i . FreerTreeT . f--type FreerTree = FreerTreeMonad Identity--instance Freer Monad FreerTree where-    liftIns = FreerTreeMonad . liftInsTree-    interpretF i = interpretTTree (pure . runIdentity) i . unFreerTreeMonad-    {-# INLINE liftIns #-}-    {-# INLINE interpretF #-}---- todo: MonadTransFreer instance

@@ -1,82 +0,0 @@-{-# LANGUAGE QuantifiedConstraints #-}---- 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 type class to abstract away the encoding details of the Heftia monad transformers.--}-module Control.Monad.Trans.Heftia where--import Control.Effect.Class (Signature, type (~>))-import Control.Effect.Class.Machinery.HFunctor (HFunctor)-import Control.Heftia.Trans (TransHeftia, elaborateHT, hoistHeftia, liftLowerHT)-import Control.Monad.Cont (ContT)-import Control.Monad.Trans (MonadTrans, lift)-import Data.Coerce (Coercible, coerce)-import Data.Kind (Type)---- | A type class to abstract away the encoding details of the Heftia monad transformers.-class-    (TransHeftia Monad h, forall sig. HFunctor sig => MonadTrans (h sig)) =>-    MonadTransHeftia h-    where-    elaborateMK ::-        (Monad m, HFunctor sig) =>-        (sig (ContT r m) ~> ContT r m) ->-        h sig m ~> ContT r m-    elaborateMK = elaborateMT-    {-# INLINE elaborateMK #-}--    reelaborateMK ::-        (Monad m, HFunctor sig) =>-        (sig (ContT r (h sig m)) ~> ContT r (h sig m)) ->-        h sig m ~> ContT r (h sig m)-    reelaborateMK = reelaborateMT-    {-# INLINE reelaborateMK #-}--    elaborateMT ::-        (Monad m, MonadTrans t, Monad (t m), HFunctor sig) =>-        (sig (t m) ~> t m) ->-        h sig m ~> t m-    elaborateMT = elaborateHT lift-    {-# INLINE elaborateMT #-}--    reelaborateMT ::-        forall m t n sig.-        (Monad m, MonadTrans t, Coercible n (h sig m), Monad (t n), Monad n, HFunctor sig) =>-        (sig (t n) ~> t n) ->-        h sig m ~> t n-    reelaborateMT f = elaborateMT f . hoistHeftia (coerce . liftLowerHT @Monad @h @sig)-    {-# INLINE reelaborateMT #-}--reinterpretHTTViaFinal ::-    forall h m t n sig.-    ( MonadTransHeftia h-    , Monad m-    , MonadTrans t-    , Coercible n (h sig m)-    , Monad (t n)-    , Monad n-    , HFunctor sig-    ) =>-    (sig (t n) ~> t n) ->-    h sig m ~> t n-reinterpretHTTViaFinal = elaborateHT $ lift . coerce . liftLowerHT @Monad @h @sig-{-# INLINE reinterpretHTTViaFinal #-}--newtype ViaLiftLowerH (h :: Signature -> (Type -> Type) -> Type -> Type) sig m a = ViaLiftLowerH-    {runViaLiftLowerH :: h sig m a}-    deriving newtype (Functor, Applicative, Monad)-    deriving stock (Foldable, Traversable)--instance (TransHeftia Monad h, HFunctor sig) => MonadTrans (ViaLiftLowerH h sig) where-    lift = ViaLiftLowerH . liftLowerHT-    {-# INLINE lift #-}

@@ -1,77 +0,0 @@--- 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 Church-encoded Heftia transformer.--}-module Control.Monad.Trans.Heftia.Church where--import Control.Effect.Class (type (~>))-import Control.Effect.Class.Machinery.HFunctor (hfmap)-import Control.Heftia.Trans (TransHeftia (..))-import Control.Monad (join)-import Control.Monad.Trans (MonadTrans, lift)-import Control.Monad.Trans.Cont (ContT (ContT), runContT)-import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, reelaborateMK)---- | A Church-encoded Heftia transformer.-newtype HeftiaChurchT h f a = HeftiaChurchT-    {unHeftiaChurchT :: forall r. (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a}-    deriving stock (Functor)--runHeftiaChurchT :: (h (HeftiaChurchT h f) ~> ContT r f) -> HeftiaChurchT h f b -> ContT r f b-runHeftiaChurchT i (HeftiaChurchT f) = f i--instance Applicative (HeftiaChurchT h f) where-    pure x = HeftiaChurchT \_ -> pure x-    {-# INLINE pure #-}--    HeftiaChurchT f <*> HeftiaChurchT g = HeftiaChurchT \i -> f i <*> g i-    {-# INLINE (<*>) #-}--instance Monad (HeftiaChurchT h f) where-    HeftiaChurchT f >>= k =-        HeftiaChurchT \i -> f i >>= runHeftiaChurchT i . k-    {-# INLINE (>>=) #-}--instance TransHeftia Monad HeftiaChurchT where-    liftSigT e = HeftiaChurchT \i -> i e-    {-# INLINE liftSigT #-}--    translateT phi (HeftiaChurchT f) =-        HeftiaChurchT \i ->-            f $ i . phi . hfmap (translateT phi)--    liftLowerHT a = HeftiaChurchT \_ -> lift a-    {-# INLINE liftLowerHT #-}--    hoistHeftia phi (HeftiaChurchT f) =-        HeftiaChurchT \i ->-            ContT \k ->-                join . phi $-                    runContT-                        ( f \e -> ContT \k' ->-                            pure $ runContT (i $ hfmap (hoistHeftia phi) e) (join . phi . k')-                        )-                        (pure . k)--    runElaborateH g (HeftiaChurchT f) =-        runContT (f $ lift . g . hfmap (runElaborateH g)) pure--instance MonadTrans (HeftiaChurchT h) where-    lift m = HeftiaChurchT \_ -> lift m-    {-# INLINE lift #-}--instance MonadTransHeftia HeftiaChurchT where-    elaborateMK f (HeftiaChurchT g) = g $ f . hfmap (elaborateMK f)-    {-# INLINE elaborateMK #-}--    reelaborateMK f = elaborateMK f . hoistHeftia liftLowerHT-    {-# INLINE reelaborateMK #-}

@@ -1,20 +0,0 @@--- 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 tree-structured encoded Heftia transformer.--}-module Control.Monad.Trans.Heftia.Tree where--import Data.Functor.Coyoneda (Coyoneda)--newtype HCoyoneda h f a = HCoyoneda {unHCoyoneda :: Coyoneda (h f) a}---- todo

@@ -1,72 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- 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) 2023 Casper Bach Poulsen and Cas van der Rest-    License : MPL-2.0 (see the file LICENSE)--    Maintainer : ymdfield@outlook.jp-    Stability : experimental-    Portability : portable--    The data structure of hefty trees.--}-module Control.Monad.Trans.Hefty where--import Control.Monad (ap)-import Control.Monad.Identity (Identity (Identity), runIdentity)-import Control.Monad.Trans (MonadTrans, lift)-import Control.Monad.Trans.Free (FreeF (Free, Pure))-import Data.Functor ((<&>))---- | A hefty monad transformer.-newtype HeftyT h m a = HeftyT {runHeftyT :: m (FreeF (h (HeftyT h m)) a (HeftyT h m a))}--instance (Functor m, Functor (h (HeftyT h m))) => Functor (HeftyT h m) where-    fmap f (HeftyT m) =-        HeftyT $-            m <&> \case-                Pure x -> Pure $ f x-                Free h -> Free $ fmap f <$> h--instance (Monad m, Functor (h (HeftyT h m))) => Applicative (HeftyT h m) where-    pure = HeftyT . pure . Pure-    (<*>) = ap--    {-# INLINE pure #-}-    {-# INLINE (<*>) #-}--instance (Monad m, Functor (h (HeftyT h m))) => Monad (HeftyT h m) where-    HeftyT m >>= k =-        HeftyT $-            m >>= \case-                Pure x -> runHeftyT $ k x-                Free h -> return $ Free $ (k =<<) <$> h--instance MonadTrans (HeftyT h) where-    lift = liftHefty-    {-# INLINE lift #-}--{- | Lift a computation to a hefty monad.--     Note that this is less constrained than MonadTrans's lift (this one only-    requires a Functor for underlying monad).--}-liftHefty :: Functor m => m a -> HeftyT h m a-liftHefty = HeftyT . fmap Pure-{-# INLINE liftHefty #-}---- | A hefty monad.-type Hefty h = HeftyT h Identity--hefty :: FreeF (h (Hefty h)) a (Hefty h a) -> Hefty h a-hefty = HeftyT . Identity-{-# INLINE hefty #-}--runHefty :: Hefty h a -> FreeF (h (Hefty h)) a (Hefty h a)-runHefty = runIdentity . runHeftyT-{-# INLINE runHefty #-}

@@ -1,92 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- 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--An implementation of an open union for first-order effects using-the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.--}-module Data.Free.Extensible where--import Control.Effect.Class (Instruction)-import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)-import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))-import Data.Free.Union (-    Union (-        HasMembership,-        absurdUnion,-        inject,-        inject0,-        project,-        weaken,-        (|+|:)-    ),- )-import Data.Proxy (Proxy (Proxy))-import GHC.TypeNats (KnownNat, Nat, natVal, type (+))-import Type.Membership (Membership, nextMembership)-import Unsafe.Coerce (unsafeCoerce)--{- |-An implementation of an open union for first-order effects using-the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.--}-newtype ExtensibleUnion fs a = ExtensibleUnion {unExtensibleUnion :: fs :/ FieldApp a}--newtype FieldApp a (f :: Instruction) = FieldApp {unFieldApp :: f a}--instance Forall Functor fs => Functor (ExtensibleUnion fs) where-    fmap f =-        ExtensibleUnion-            . match-                ( htabulateFor @Functor Proxy \w ->-                    Match \e -> EmbedAt w $ FieldApp $ f <$> unFieldApp e-                )-            . unExtensibleUnion-    {-# INLINE fmap #-}--{- todo:-instance Forall Foldable fs => Foldable (ExtensibleUnion fs) where-instance Forall Traversable fs => Traversable (ExtensibleUnion fs) where--}--instance Union ExtensibleUnion where-    type HasMembership _ f fs = KnownNat (TypeIndex fs f)--    inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp-    {-# INLINE inject #-}--    project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u-    {-# INLINE project #-}--    absurdUnion = exhaust . unExtensibleUnion-    {-# INLINE absurdUnion #-}--    inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp-    {-# INLINE inject0 #-}--    weaken (ExtensibleUnion (EmbedAt w e)) =-        ExtensibleUnion $ EmbedAt (nextMembership w) e-    {-# INLINE weaken #-}--    f |+|: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion-    {-# INLINE (|+|:) #-}--findFirstMembership :: forall xs x. KnownNat (TypeIndex xs x) => Membership xs x-findFirstMembership = unsafeMkMembership $ fromIntegral $ natVal @(TypeIndex xs x) Proxy-  where-    -- This hack may break if the membership package version gets updated.-    unsafeMkMembership :: Int -> Membership xs x-    unsafeMkMembership = unsafeCoerce--type family TypeIndex (xs :: [k]) (x :: k) :: Nat where-    TypeIndex (x ': xs) x = 0-    TypeIndex (y ': xs) x = 1 + TypeIndex xs x

@@ -1,32 +1,24 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE UndecidableInstances #-}- -- 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/. --- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest.- {- |-Copyright   :  (c) 2023 Yamada Ryo-               (c) 2023 Casper Bach Poulsen and Cas van der Rest+Copyright   :  (c) 2023-2024 Yamada Ryo License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp Stability   :  experimental Portability :  portable -An implementation of an open union for first-order effects using recursively nested binary sums.+Binary sums for first-order effects. -} module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1) where -import Control.Effect.Class (Instruction, NopI, type (~>))-import Data.Free.Union (HasMembership, Union, absurdUnion, comp, decomp, inject, project)+import Control.Effect (type (~>))+import Data.Effect (Nop) import GHC.Generics (type (:+:) (L1, R1)) -infixr 6 +---- | A type synonym for disambiguation to the sum on the higher-order side. type (+) = (:+:)+infixr 5 +  caseF :: (f a -> r) -> (g a -> r) -> (f + g) a -> r caseF f g = \case@@ -34,88 +26,14 @@     R1 x -> g x {-# INLINE caseF #-} -absurdL :: (NopI + f) ~> f+absurdL :: Nop + f ~> f absurdL = caseF \case {} id {-# INLINE absurdL #-} -absurdR :: (f + NopI) ~> f+absurdR :: f + Nop ~> f absurdR = caseF id \case {} {-# INLINE absurdR #-}  swapSum :: (f + g) a -> (g + f) a swapSum = caseF R1 L1 {-# INLINE swapSum #-}--type family Sum fs where-    Sum '[] = NopI-    Sum (f ': fs) = f :+: Sum fs--{- |-An implementation of an open union for first-order effects using recursively nested binary sums.--}-newtype SumUnion fs a = SumUnion {unSumUnion :: Sum fs a}--deriving newtype instance Functor (SumUnion '[])-deriving newtype instance (Functor f, Functor (Sum fs)) => Functor (SumUnion (f ': fs))--deriving newtype instance Foldable (SumUnion '[])-deriving newtype instance (Foldable f, Foldable (Sum fs)) => Foldable (SumUnion (f ': fs))--deriving stock instance Traversable (SumUnion '[])-deriving stock instance (Traversable f, Traversable (Sum fs)) => Traversable (SumUnion (f ': fs))--instance Union SumUnion where-    type HasMembership _ f fs = f < Sum fs--    inject sig = SumUnion $ inj sig-    project (SumUnion sig) = proj sig--    absurdUnion = \case {}--    comp =-        SumUnion . \case-            Left x -> L1 x-            Right (SumUnion x) -> R1 x--    decomp (SumUnion sig) = case sig of-        L1 x -> Left x-        R1 x -> Right (SumUnion x)--    {-# INLINE inject #-}-    {-# INLINE project #-}-    {-# INLINE absurdUnion #-}--class isHead ~ f `IsHeadInsOf` g => SumMember isHead (f :: Instruction) g where-    injSum :: f a -> g a-    projSum :: g a -> Maybe (f a)--type family (f :: Instruction) `IsHeadInsOf` g where-    f `IsHeadInsOf` f + g = 'True-    _ `IsHeadInsOf` _ = 'False--type f < g = SumMember (IsHeadInsOf f g) f g--inj :: forall f g. f < g => f ~> g-inj = injSum @(IsHeadInsOf f g)--proj :: forall f g a. f < g => g a -> Maybe (f a)-proj = projSum--instance SumMember 'True f (f + g) where-    injSum = L1--    projSum = \case-        L1 x -> Just x-        R1 _ -> Nothing--    {-# INLINE injSum #-}-    {-# INLINE projSum #-}--instance (f `IsHeadInsOf` (g + h) ~ 'False, f < h) => SumMember 'False f (g + h) where-    injSum = R1 . inj-    projSum = \case-        L1 _ -> Nothing-        R1 x -> projSum x--    {-# INLINE injSum #-}-    {-# INLINE projSum #-}

@@ -1,150 +0,0 @@--- 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 type class representing a general open union for first-order effects, independent of the internal-implementation.--}-module Data.Free.Union where--import Control.Effect.Class (Instruction, type (~>))-import Data.Kind (Constraint)--{- |-A type class representing a general open union for first-order effects, independent of the internal-implementation.--}-class Union (u :: [Instruction] -> Instruction) where-    {-# MINIMAL inject, project, absurdUnion, (comp | (inject0, weaken), decomp | (|+|:)) #-}--    type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint--    inject :: HasMembership u f fs => f ~> u fs-    project :: HasMembership u f fs => u fs a -> Maybe (f a)--    absurdUnion :: u '[] a -> x--    comp :: Either (f a) (u fs a) -> u (f ': fs) a-    comp = \case-        Left x -> inject0 x-        Right x -> weaken x-    {-# INLINE comp #-}--    decomp :: u (f ': fs) a -> Either (f a) (u fs a)-    decomp = Left |+|: Right-    {-# INLINE decomp #-}--    infixr 5 |+|:-    (|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r-    (f |+|: g) u = case decomp u of-        Left x -> f x-        Right x -> g x-    {-# INLINE (|+|:) #-}--    inject0 :: f ~> u (f ': fs)-    inject0 = comp . Left-    {-# INLINE inject0 #-}--    injectUnder :: f2 ~> u (f1 ': f2 ': fs)-    injectUnder = weaken . inject0-    {-# INLINE injectUnder #-}--    injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs)-    injectUnder2 = weaken2 . inject0-    {-# INLINE injectUnder2 #-}--    injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs)-    injectUnder3 = weaken3 . inject0-    {-# INLINE injectUnder3 #-}--    weaken :: u fs a -> u (f ': fs) a-    weaken = comp . Right-    {-# INLINE weaken #-}--    weaken2 :: u fs a -> u (f1 ': f2 ': fs) a-    weaken2 = weaken . weaken-    {-# INLINE weaken2 #-}--    weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a-    weaken3 = weaken2 . weaken-    {-# INLINE weaken3 #-}--    weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a-    weaken4 = weaken3 . weaken-    {-# INLINE weaken4 #-}--    weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs)-    weakenUnder = inject0 |+|: weaken2--    weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs)-    weakenUnder2 = inject0 |+|: injectUnder |+|: weaken3--    weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)-    weakenUnder3 = inject0 |+|: injectUnder |+|: injectUnder2 |+|: weaken4--    weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs)-    weaken2Under = inject0 |+|: weaken3--    weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)-    weaken2Under2 = inject0 |+|: injectUnder |+|: weaken4--    weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)-    weaken3Under = inject0 |+|: weaken4--    flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs)-    flipUnion = injectUnder |+|: inject0 |+|: weaken2--    flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs)-    flipUnion3 = injectUnder2 |+|: injectUnder |+|: inject0 |+|: weaken3--    flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs)-    flipUnionUnder = inject0 |+|: injectUnder2 |+|: injectUnder |+|: weaken3--    rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs)-    rot3 = injectUnder2 |+|: inject0 |+|: injectUnder |+|: weaken3--    rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs)-    rot3' = injectUnder |+|: injectUnder2 |+|: inject0 |+|: weaken3--    bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs)-    bundleUnion2 = inject0 . inject0 |+|: inject0 . injectUnder |+|: weaken--    bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs)-    bundleUnion3 =-        (inject0 . inject0)-            |+|: (inject0 . injectUnder)-            |+|: (inject0 . injectUnder2)-            |+|: weaken--    bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs)-    bundleUnion4 =-        (inject0 . inject0)-            |+|: (inject0 . injectUnder)-            |+|: (inject0 . injectUnder2)-            |+|: (inject0 . injectUnder3)-            |+|: weaken--    unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs)-    unbundleUnion2 = (inject0 |+|: injectUnder |+|: absurdUnion) |+|: weaken2--    unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs)-    unbundleUnion3 = (inject0 |+|: injectUnder |+|: injectUnder2 |+|: absurdUnion) |+|: weaken3--    unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)-    unbundleUnion4 =-        (inject0 |+|: injectUnder |+|: injectUnder2 |+|: injectUnder3 |+|: absurdUnion)-            |+|: weaken4--type family IsMember (f :: Instruction) fs where-    IsMember f (f ': fs) = 'True-    IsMember f (_ ': fs) = IsMember f fs-    IsMember _ '[] = 'False--type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True)

@@ -1,3 +1,4 @@+{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE UndecidableInstances #-}  -- This Source Code Form is subject to the terms of the Mozilla Public@@ -14,66 +15,113 @@ An implementation of an open union for higher-order effects using the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. -}-module Data.Hefty.Extensible where+module Data.Hefty.Extensible (+    module Data.Hefty.Extensible,+    Forall,+) where -import Control.Effect.Class (Signature)-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)-import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)-import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))-import Data.Free.Extensible (TypeIndex, findFirstMembership)+import Data.Effect (SigClass)+import Data.Effect.HFunctor (HFunctor, hfmap)+import Data.Extensible (Forall, Match (Match), htabulateFor, match)+import Data.Extensible.Sum (strikeAt, (<:|), type (:/) (EmbedAt))+import Data.Extensible.Sum qualified as E import Data.Hefty.Union (-    UnionH (-        HasMembershipH,-        absurdUnionH,-        inject0H,-        injectH,-        projectH,-        weakenH,+    ClassIndex,+    HFunctorUnion_ (ForallHFunctor),+    Union (+        HasMembership,+        exhaust,+        inject,+        inject0,+        project,+        weaken,         (|+:)     ),  )+import Data.Hefty.Union qualified as U+import Data.Hefty.Union qualified as Union import Data.Proxy (Proxy (Proxy))+import Data.Type.Equality ((:~:) (Refl)) import GHC.TypeNats (KnownNat)-import Type.Membership (nextMembership)+import Type.Membership.Internal (+    Elaborate,+    Elaborated (Expecting),+    FindType,+    Membership,+    leadership,+    membership,+    nextMembership,+ )+import Unsafe.Coerce (unsafeCoerce)  {- | An implementation of an open union for higher-order effects using the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. -}-newtype ExtensibleUnionH hs f a = ExtensibleUnionH {unExtensibleUnionH :: hs :/ FieldAppH f a}+newtype ExtensibleUnion es f a = ExtensibleUnion {unExtensibleUnion :: es :/ FieldApp f a} -newtype FieldAppH f a (h :: Signature) = FieldAppH {unFieldAppH :: h f a}+newtype FieldApp f a (e :: SigClass) = FieldApp {unFieldApp :: e f a} -instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where+instance Forall HFunctor es => HFunctor (ExtensibleUnion es) where     hfmap f =-        ExtensibleUnionH+        ExtensibleUnion             . match                 ( htabulateFor @HFunctor Proxy \w ->-                    Match $ EmbedAt w . FieldAppH . hfmap f . unFieldAppH+                    Match $ EmbedAt w . FieldApp . hfmap f . unFieldApp                 )-            . unExtensibleUnionH+            . unExtensibleUnion     {-# INLINE hfmap #-}  -- todo: Functor, Foldable, Traversable instances -instance UnionH ExtensibleUnionH where-    type HasMembershipH _ h hs = KnownNat (TypeIndex hs h)+instance Union ExtensibleUnion where+    type HasMembership _ e es = KnownNat (ClassIndex es e) -    injectH = ExtensibleUnionH . EmbedAt findFirstMembership . FieldAppH-    {-# INLINE injectH #-}+    inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp+    {-# INLINE inject #-} -    projectH (ExtensibleUnionH u) = unFieldAppH <$> strikeAt findFirstMembership u-    {-# INLINE projectH #-}+    project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u+    {-# INLINE project #-} -    absurdUnionH = exhaust . unExtensibleUnionH-    {-# INLINE absurdUnionH #-}+    exhaust = E.exhaust . unExtensibleUnion+    {-# INLINE exhaust #-} -    inject0H = ExtensibleUnionH . EmbedAt leadership . FieldAppH-    {-# INLINE inject0H #-}+    inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp+    {-# INLINE inject0 #-} -    weakenH (ExtensibleUnionH (EmbedAt w e)) =-        ExtensibleUnionH $ EmbedAt (nextMembership w) e-    {-# INLINE weakenH #-}+    weaken (ExtensibleUnion (EmbedAt w e)) =+        ExtensibleUnion $ EmbedAt (nextMembership w) e+    {-# INLINE weaken #-} -    f |+: g = (f . unFieldAppH <:| g . ExtensibleUnionH) . unExtensibleUnionH+    f |+: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion     {-# INLINE (|+:) #-}++findFirstMembership :: forall xs x. KnownNat (ClassIndex xs x) => Membership xs x+findFirstMembership = unsafeMkMembership @(ClassIndex xs x) Proxy+  where+    -- This hack may break if the membership package version gets updated.+    unsafeMkMembership :: forall pos. Proxy pos -> KnownNat pos => Membership xs x+    unsafeMkMembership _ = case hackedEquality of Refl -> membership+      where+        hackedEquality :: Elaborate x (FindType x xs) :~: 'Expecting pos+        hackedEquality = unsafeCoerce Refl++instance HFunctorUnion_ (Forall HFunctor) ExtensibleUnion where+    type ForallHFunctor _ = Forall HFunctor++type e <| es = U.Member ExtensibleUnion e es+type e <<| es = U.MemberH ExtensibleUnion e es++type MemberBy key e efs = U.MemberBy ExtensibleUnion key e efs+type MemberHBy key e ehs = U.MemberHBy ExtensibleUnion key e ehs++infix 3 <|+infix 3 <<|++type ForallHFunctor = Forall HFunctor++type U ef = Union.U ExtensibleUnion ef+type UH eh = Union.UH ExtensibleUnion eh++type S ef = Union.S ExtensibleUnion ef+type SH eh = Union.SH ExtensibleUnion eh

@@ -1,123 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- 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/.---- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest.--{- |-Copyright   :  (c) 2023 Yamada Ryo-               (c) 2023 Casper Bach Poulsen and Cas van der Rest-License     :  MPL-2.0 (see the file LICENSE)-Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--An implementation of an open union for higher-order effects using recursively nested binary sums.--}-module Data.Hefty.Sum where--import Control.Effect.Class (NopS, Signature, type (~>))-import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))-import Data.Hefty.Union (HasMembershipH, UnionH, absurdUnionH, compH, decompH, injectH, projectH)--absurdLH :: (NopS :+: h) f ~> h f-absurdLH = caseH \case {} id-{-# INLINE absurdLH #-}--absurdRH :: (h :+: NopS) f ~> h f-absurdRH = caseH id \case {}-{-# INLINE absurdRH #-}--swapSumH :: (h1 :+: h2) f a -> (h2 :+: h1) f a-swapSumH = caseH Inr Inl-{-# INLINE swapSumH #-}--type family SumH hs where-    SumH '[] = NopS-    SumH (h ': hs) = h :+: SumH hs--{- |-An implementation of an open union for higher-order effects using recursively nested binary sums.--}-newtype SumUnionH hs f a = SumUnionH {unSumUnionH :: SumH hs f a}--deriving newtype instance Functor (SumUnionH '[] f)-deriving newtype instance Foldable (SumUnionH '[] f)-deriving stock instance Traversable (SumUnionH '[] f)--{- Lack of instances of 'Data.Comp.Multi.Ops.:+:'.- - Should we create a pullreq on the compdata package side?- -}-{--deriving newtype instance-    (Functor (h f), Functor (SumH hs f)) =>-    Functor (SumUnionH (h ': hs) f)--deriving newtype instance-    (Foldable (h f), Foldable (SumH hs f)) =>-    Foldable (SumUnionH (h ': hs) f)--deriving stock instance-    (Traversable (h f), Traversable (SumH hs f)) =>-    Traversable (SumUnionH (h ': hs) f)--}--deriving newtype instance HFunctor (SumH hs) => HFunctor (SumUnionH hs)--instance UnionH SumUnionH where-    type HasMembershipH _ h hs = h << SumH hs--    injectH sig = SumUnionH $ injH sig-    projectH (SumUnionH sig) = projH sig--    absurdUnionH = \case {}--    compH =-        SumUnionH . \case-            Left x -> Inl x-            Right (SumUnionH x) -> Inr x--    decompH (SumUnionH sig) = case sig of-        Inl x -> Left x-        Inr x -> Right (SumUnionH x)--    {-# INLINE injectH #-}-    {-# INLINE projectH #-}-    {-# INLINE absurdUnionH #-}--class isHead ~ h1 `IsHeadSigOf` h2 => SumMemberH isHead (h1 :: Signature) h2 where-    injSumH :: h1 f a -> h2 f a-    projSumH :: h2 f a -> Maybe (h1 f a)--type family (h1 :: Signature) `IsHeadSigOf` h2 where-    f `IsHeadSigOf` f :+: g = 'True-    _ `IsHeadSigOf` _ = 'False--type h1 << h2 = SumMemberH (IsHeadSigOf h1 h2) h1 h2--injH :: forall h1 h2 f. h1 << h2 => h1 f ~> h2 f-injH = injSumH @(IsHeadSigOf h1 h2)--projH :: forall h1 h2 f a. h1 << h2 => h2 f a -> Maybe (h1 f a)-projH = projSumH--instance SumMemberH 'True f (f :+: g) where-    injSumH = Inl--    projSumH = \case-        Inl x -> Just x-        Inr _ -> Nothing--    {-# INLINE injSumH #-}-    {-# INLINE projSumH #-}--instance (f `IsHeadSigOf` (g :+: h) ~ 'False, f << h) => SumMemberH 'False f (g :+: h) where-    injSumH = Inr . injH-    projSumH = \case-        Inl _ -> Nothing-        Inr x -> projSumH x--    {-# INLINE injSumH #-}-    {-# INLINE projSumH #-}

@@ -1,11 +1,16 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}  -- 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+Copyright   :  (c) 2023-2024 Yamada Ryo License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp Stability   :  experimental@@ -16,142 +21,511 @@ -} module Data.Hefty.Union where -import Control.Effect.Class (Signature, type (~>))+import Control.Effect (type (~>))+import Control.Monad ((<=<))+import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)+import Data.Effect.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))+import Data.Effect.Key (type (##>), type (#>))+import Data.Free.Sum (type (+)) import Data.Kind (Constraint)+import Data.Singletons (SingI, sing)+import Data.Singletons.TH (singletons)+import Data.Type.Bool (If)+import Data.Type.Equality ((:~:) (Refl))+import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), Nat, TypeError)+import GHC.TypeNats qualified as N  {- | A type class representing a general open union for higher-order effects, independent of the internal implementation. -}-class UnionH (u :: [Signature] -> Signature) where-    {-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-}+class Union (u :: [SigClass] -> SigClass) where+    {-# MINIMAL inject, project, exhaust, (comp | (inject0, weaken), decomp | (|+:)) #-} -    type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint+    type HasMembership u (e :: SigClass) (es :: [SigClass]) :: Constraint -    injectH :: HasMembershipH u h hs => h f ~> u hs f-    projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)+    inject :: HasMembership u e es => e f ~> u es f+    project :: HasMembership u e es => u es f a -> Maybe (e f a) -    absurdUnionH :: u '[] f a -> x+    exhaust :: u '[] f a -> x -    compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a-    compH = \case-        Left x -> inject0H x-        Right x -> weakenH x-    {-# INLINE compH #-}+    comp :: Either (e f a) (u es f a) -> u (e ': es) f a+    comp = \case+        Left x -> inject0 x+        Right x -> weaken x+    {-# INLINE comp #-} -    decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)-    decompH = Left |+: Right-    {-# INLINE decompH #-}+    decomp :: u (e ': es) f a -> (e :+: u es) f a+    decomp = Inl |+: Inr+    {-# INLINE decomp #-}      infixr 5 |+:-    (|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r-    (f |+: g) u = case decompH u of-        Left x -> f x-        Right x -> g x+    (|+:) :: (e f a -> r) -> (u es f a -> r) -> u (e ': es) f a -> r+    f |+: g = caseH f g . decomp     {-# INLINE (|+:) #-} -    inject0H :: h f ~> u (h ': hs) f-    inject0H = compH . Left-    {-# INLINE inject0H #-}+    inject0 :: e f ~> u (e ': es) f+    inject0 = comp . Left+    {-# INLINE inject0 #-} -    injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f-    injectUnderH = weakenH . inject0H-    {-# INLINE injectUnderH #-}+    injectUnder :: h2 f ~> u (h1 ': h2 ': es) f+    injectUnder = weaken . inject0+    {-# INLINE injectUnder #-} -    injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f-    injectUnder2H = weaken2H . inject0H-    {-# INLINE injectUnder2H #-}+    injectUnder2 :: h3 f ~> u (h1 ': h2 ': h3 ': es) f+    injectUnder2 = weaken2 . inject0+    {-# INLINE injectUnder2 #-} -    injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    injectUnder3H = weaken3H . inject0H-    {-# INLINE injectUnder3H #-}+    injectUnder3 :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': es) f+    injectUnder3 = weaken3 . inject0+    {-# INLINE injectUnder3 #-} -    weakenH :: u hs f ~> u (h ': hs) f-    weakenH = compH . Right-    {-# INLINE weakenH #-}+    weaken :: u es f ~> u (e ': es) f+    weaken = comp . Right+    {-# INLINE weaken #-} -    weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f-    weaken2H = weakenH . weakenH-    {-# INLINE weaken2H #-}+    weaken2 :: u es f ~> u (e1 ': e2 ': es) f+    weaken2 = weaken . weaken+    {-# INLINE weaken2 #-} -    weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f-    weaken3H = weaken2H . weakenH-    {-# INLINE weaken3H #-}+    weaken3 :: u es f ~> u (e1 ': e2 ': e3 ': es) f+    weaken3 = weaken2 . weaken+    {-# INLINE weaken3 #-} -    weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    weaken4H = weaken3H . weakenH-    {-# INLINE weaken4H #-}+    weaken4 :: u es f ~> u (e1 ': e2 ': e3 ': e4 ': es) f+    weaken4 = weaken3 . weaken+    {-# INLINE weaken4 #-} -    weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f-    weakenUnderH = inject0H |+: weaken2H+    weakenUnder :: u (e1 ': es) f ~> u (e1 ': e2 ': es) f+    weakenUnder = inject0 |+: weaken2 -    weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f-    weakenUnder2H = inject0H |+: injectUnderH |+: weaken3H+    weakenUnder2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': es) f+    weakenUnder2 = inject0 |+: injectUnder |+: weaken3 -    weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    weakenUnder3H = inject0H |+: injectUnderH |+: injectUnder2H |+: weaken4H+    weakenUnder3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f+    weakenUnder3 = inject0 |+: injectUnder |+: injectUnder2 |+: weaken4 -    weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f-    weaken2UnderH = inject0H |+: weaken3H+    weaken2Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': es) f+    weaken2Under = inject0 |+: weaken3 -    weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    weaken2Under2H = inject0H |+: injectUnderH |+: weaken4H+    weaken2Under2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f+    weaken2Under2 = inject0 |+: injectUnder |+: weaken4 -    weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    weaken3UnderH = inject0H |+: weaken4H+    weaken3Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f+    weaken3Under = inject0 |+: weaken4 -    flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f-    flipUnionH = injectUnderH |+: inject0H |+: weaken2H+    flipUnion :: u (e1 ': e2 ': es) f ~> u (e2 ': e1 ': es) f+    flipUnion = injectUnder |+: inject0 |+: weaken2 -    flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f-    flipUnion3H = injectUnder2H |+: injectUnderH |+: inject0H |+: weaken3H+    flipUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e2 ': e1 ': es) f+    flipUnion3 = injectUnder2 |+: injectUnder |+: inject0 |+: weaken3 -    flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f-    flipUnionUnderH = inject0H |+: injectUnder2H |+: injectUnderH |+: weaken3H+    flipUnionUnder :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e3 ': e2 ': es) f+    flipUnionUnder = inject0 |+: injectUnder2 |+: injectUnder |+: weaken3 -    rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f-    rot3H = injectUnder2H |+: inject0H |+: injectUnderH |+: weaken3H+    rot3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e2 ': e3 ': e1 ': es) f+    rot3 = injectUnder2 |+: inject0 |+: injectUnder |+: weaken3 -    rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f-    rot3H' = injectUnderH |+: injectUnder2H |+: inject0H |+: weaken3H+    rot3' :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e1 ': e2 ': es) f+    rot3' = injectUnder |+: injectUnder2 |+: inject0 |+: weaken3 -    bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f-    bundleUnion2H = inject0H . inject0H |+: inject0H . injectUnderH |+: weakenH+    bundleUnion2 :: u (e1 ': e2 ': es) f ~> u (u '[e1, e2] ': es) f+    bundleUnion2 = inject0 . inject0 |+: inject0 . injectUnder |+: weaken -    bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f-    bundleUnion3H =-        (inject0H . inject0H)-            |+: (inject0H . injectUnderH)-            |+: (inject0H . injectUnder2H)-            |+: weakenH+    bundleUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (u '[e1, e2, e3] ': es) f+    bundleUnion3 =+        (inject0 . inject0)+            |+: (inject0 . injectUnder)+            |+: (inject0 . injectUnder2)+            |+: weaken -    bundleUnion4H ::-        UnionH u' =>-        u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f-    bundleUnion4H =-        (inject0H . inject0H)-            |+: (inject0H . injectUnderH)-            |+: (inject0H . injectUnder2H)-            |+: (inject0H . injectUnder3H)-            |+: weakenH+    bundleUnion4 ::+        u (e1 ': e2 ': e3 ': e4 ': es) f ~> u (u '[e1, e2, e3, e4] ': es) f+    bundleUnion4 =+        (inject0 . inject0)+            |+: (inject0 . injectUnder)+            |+: (inject0 . injectUnder2)+            |+: (inject0 . injectUnder3)+            |+: weaken -    unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f-    unbundleUnion2H = (inject0H |+: injectUnderH |+: absurdUnionH) |+: weaken2H+    unbundleUnion2 :: u (u '[e1, e2] ': es) f ~> u (e1 ': e2 ': es) f+    unbundleUnion2 = (inject0 |+: injectUnder |+: exhaust) |+: weaken2 -    unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f-    unbundleUnion3H = (inject0H |+: injectUnderH |+: injectUnder2H |+: absurdUnionH) |+: weaken3H+    unbundleUnion3 :: u (u '[e1, e2, e3] ': es) f ~> u (e1 ': e2 ': e3 ': es) f+    unbundleUnion3 = (inject0 |+: injectUnder |+: injectUnder2 |+: exhaust) |+: weaken3 -    unbundleUnion4H ::-        UnionH u' =>-        u (u' '[h1, h2, h3, h4] ': hs) f-            ~> u (h1 ': h2 ': h3 ': h4 ': hs) f-    unbundleUnion4H =-        (inject0H |+: injectUnderH |+: injectUnder2H |+: injectUnder3H |+: absurdUnionH)-            |+: weaken4H+    unbundleUnion4 ::+        u (u '[e1, e2, e3, e4] ': es) f+            ~> u (e1 ': e2 ': e3 ': e4 ': es) f+    unbundleUnion4 =+        (inject0 |+: injectUnder |+: injectUnder2 |+: injectUnder3 |+: exhaust)+            |+: weaken4 -type family IsMemberH (h :: Signature) hs where-    IsMemberH h (h ': hs) = 'True-    IsMemberH h (_ ': hs) = IsMemberH h hs-    IsMemberH _ '[] = 'False+type HFunctorUnion u = HFunctorUnion_ (ForallHFunctor u) u -type MemberH u h hs = (HasMembershipH u h hs, IsMemberH h hs ~ 'True)+-- A hack to avoid the "Quantified predicate must have a class or type variable head" error.+class+    ( Union u+    , forall e es. (HFunctor e, forallHFunctor es) => forallHFunctor (e ': es)+    , forall es. forallHFunctor es => HFunctor (u es)+    , forallHFunctor ~ ForallHFunctor u+    , forallHFunctor '[]+    ) =>+    HFunctorUnion_ forallHFunctor u+        | u -> forallHFunctor+    where+    type ForallHFunctor u :: [SigClass] -> Constraint++$( singletons+    [d|+        data SearchResult = FoundIn FoundLevel | NotFound++        data FoundLevel = CurrentLevel | LowerLevel+        |]+ )++type family FoundLevelOf found :: FoundLevel where+    FoundLevelOf ( 'FoundIn l) = l++type MemberH u e ehs = HasMembershipRec u e ehs+type Member u e efs = MemberH u (LiftIns e) efs++class MemberRec (u :: [SigClass] -> SigClass) e es where+    injectRec :: e f ~> u es f+    projectRec :: u es f a -> Maybe (e f a)++type HasMembershipRec u e es =+    ( SearchMemberRec es u e es+    , HasMembershipRec1_ u e es (Search u es e)+    )++type HasMembershipRec1_ u e es searchResult =+    ( HasMembershipRec2_ u e es (CurrentLevelSearchResult searchResult)+    , SingI (HeadLowerSearchResult searchResult)+    )+type HasMembershipRec2_ u e es found = HasMembershipRec3_ u e es found (FoundLevelOf found)+type HasMembershipRec3_ u e es found lvl =+    ( found ~ 'FoundIn lvl+    , SingI lvl+    , HasMembershipWhenCurrentLevel lvl u e es+    , SearchMemberRecWhenLowerLevel lvl es u e+    )++instance+    ( SearchMemberRec es u e es+    , MemberFound e es (CurrentLevelSearchResult searchResult)+    , searchResult ~ Search u es e+    , SingI (HeadLowerSearchResult searchResult)+    , found ~ CurrentLevelSearchResult searchResult+    ) =>+    MemberRec u e es+    where+    injectRec = withFound @e @es @found $ injectSMR @es Refl sing sing+    projectRec = withFound @e @es @found $ projectSMR @es Refl sing sing+    {-# INLINE injectRec #-}+    {-# INLINE projectRec #-}++class MemberFound e es found where+    withFound :: (forall lvl. (found ~ 'FoundIn lvl, SingI lvl) => a) -> a++instance SingI lvl => MemberFound e es ( 'FoundIn lvl) where+    withFound a = a+    {-# INLINE withFound #-}++-- A stopgap until upgrading to base-4.19.+-- https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeError.html#t:Unsatisfiable+instance+    TypeError+        ( 'Text "The effect class: " ':<>: 'ShowType e+            ':$$: 'Text " was not found in the union:"+            ':$$: 'Text "    " ':<>: 'ShowType es+        ) =>+    MemberFound e es 'NotFound+    where+    withFound _ = error "unreachable"++type SearchMemberRec rest u e = SearchMemberRec_ (NextSearchMemberRecAction rest u e) rest u e++class+    SearchMemberRec_+        (act :: SearchMemberRecAction)+        (rest :: [SigClass])+        (u :: [SigClass] -> SigClass)+        (e :: SigClass)+        (es :: [SigClass])+    where+    type Search_ act u rest e :: SearchResults++    injectSMR_ ::+        searchResult ~ Search_ act u rest e =>+        CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->+        SSearchResult ( 'FoundIn lvl) ->+        SSearchResult (HeadLowerSearchResult searchResult) ->+        e f ~> u es f++    projectSMR_ ::+        searchResult ~ Search_ act u rest e =>+        CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->+        SSearchResult ( 'FoundIn lvl) ->+        SSearchResult (HeadLowerSearchResult searchResult) ->+        u es f a ->+        Maybe (e f a)++type Search u rest e = Search_ (NextSearchMemberRecAction rest u e) u rest e++injectSMR ::+    forall rest u e es searchResult lvl f.+    (SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>+    CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->+    SSearchResult ( 'FoundIn lvl) ->+    SSearchResult (HeadLowerSearchResult searchResult) ->+    e f ~> u es f+injectSMR = injectSMR_ @(NextSearchMemberRecAction rest u e) @rest+{-# INLINE injectSMR #-}++projectSMR ::+    forall rest u e es searchResult lvl f a.+    (SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>+    CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->+    SSearchResult ( 'FoundIn lvl) ->+    SSearchResult (HeadLowerSearchResult searchResult) ->+    u es f a ->+    Maybe (e f a)+projectSMR = projectSMR_ @(NextSearchMemberRecAction rest u e) @rest+{-# INLINE projectSMR #-}++data SearchResults = SearchResults SearchResult SearchResult+type family CurrentLevelSearchResult a where+    CurrentLevelSearchResult ( 'SearchResults a _) = a++type family HeadLowerSearchResult a where+    HeadLowerSearchResult ( 'SearchResults _ a) = a++data SearchMemberRecAction = SmrStop | SmrRight | SmrDown++type family NextSearchMemberRecAction rest (u :: [SigClass] -> SigClass) e where+    NextSearchMemberRecAction (e ': _) u e = 'SmrStop+    NextSearchMemberRecAction (u _ ': _) u e = 'SmrDown+    NextSearchMemberRecAction _ _ _ = 'SmrRight++instance+    (HasMembership u e es, Union u) =>+    SearchMemberRec_ 'SmrStop (e ': _tail) u e es+    where+    type Search_ _ _ (e ': _tail) e = 'SearchResults ( 'FoundIn 'CurrentLevel) 'NotFound++    injectSMR_ _ _ _ = inject+    projectSMR_ _ _ _ = project+    {-# INLINE injectSMR_ #-}+    {-# INLINE projectSMR_ #-}++type family IsFound found where+    IsFound ( 'FoundIn _) = 'True+    IsFound 'NotFound = 'False++instance+    ( SearchMemberRec es' u e es'+    , headSearchResults ~ Search u es' e+    , tailSearchResults ~ Search u tail e+    , isFoundInHead ~ IsFound (CurrentLevelSearchResult headSearchResults)+    , If isFoundInHead (HasMembership u (u es') es) (() :: Constraint)+    , SearchMemberRec (If isFoundInHead '[] tail) u e es+    , Union u+    , SingI (HeadLowerSearchResult headSearchResults)+    , SingI (HeadLowerSearchResult tailSearchResults)+    ) =>+    SearchMemberRec_ 'SmrDown (u es' ': tail) u e es+    where+    type+        Search_ _ _ (u es' ': tail) e =+            SearchResultsOnSmrDown+                u+                es'+                tail+                e+                (CurrentLevelSearchResult (Search u es' e))+                (CurrentLevelSearchResult (Search u tail e))++    injectSMR_ Refl found = \case+        SFoundIn lvl -> inject . injectSMR @es' @u @_ @es' Refl (SFoundIn lvl) sing+        SNotFound -> injectSMR @tail Refl found sing++    projectSMR_ Refl found = \case+        SFoundIn lvl -> projectSMR @es' @u @_ @es' Refl (SFoundIn lvl) sing <=< project+        SNotFound -> projectSMR @tail Refl found sing++    {-# INLINE injectSMR_ #-}+    {-# INLINE projectSMR_ #-}++type SearchResultsOnSmrDown u es' tail e foundInHead foundInTail =+    'SearchResults+        (If (IsFound foundInHead) ( 'FoundIn 'LowerLevel) foundInTail)+        foundInHead++instance+    ( HasMembershipWhenCurrentLevel lvl u e (_e ': rest)+    , SearchMemberRecWhenLowerLevel lvl rest u e+    , SingI (HeadLowerSearchResult searchResult)+    , Union u+    , searchResult ~ Search u rest e+    , lvl ~ FoundLevelOf (CurrentLevelSearchResult searchResult)+    ) =>+    SearchMemberRec_ 'SmrRight (_e ': rest) u e (_e ': rest)+    where+    type Search_ _ u (_ ': rest) e = 'SearchResults (CurrentLevelSearchResult (Search u rest e)) 'NotFound++    injectSMR_ Refl (SFoundIn lvl) _ = case lvl of+        SCurrentLevel -> inject+        SLowerLevel -> weaken . injectSMR @rest Refl sing sing++    projectSMR_ Refl (SFoundIn lvl) _ = case lvl of+        SCurrentLevel -> project+        SLowerLevel -> const Nothing |+: projectSMR @rest Refl sing sing++    {-# INLINE injectSMR_ #-}+    {-# INLINE projectSMR_ #-}++instance SearchMemberRec_ act '[] u e es where+    type Search_ _ _ _ _ = 'SearchResults 'NotFound 'NotFound+    injectSMR_ = \case {}+    projectSMR_ = \case {}+    {-# INLINE injectSMR_ #-}+    {-# INLINE projectSMR_ #-}++-- A hack to avoid the "Quantified predicate must have a class or type variable head" error.++type HasMembershipWhenCurrentLevel lvl u e es =+    HasMembershipWhenCurrentLevel_ (HasMembership u e es) lvl u e es+class+    (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) =>+    HasMembershipWhenCurrentLevel_ c lvl u e es+        | u e es -> c+instance+    (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) =>+    HasMembershipWhenCurrentLevel_ c lvl u e es++type SearchMemberRecWhenLowerLevel lvl rest u e =+    SearchMemberRecWhenLowerLevel_ (SearchMemberRec rest u e rest) lvl rest u e+class+    (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) =>+    SearchMemberRecWhenLowerLevel_ c lvl rest u e+        | rest u e -> c+instance+    (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) =>+    SearchMemberRecWhenLowerLevel_ c lvl rest u e++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 #-}++type family ClassIndex (es :: [SigClass]) (e :: SigClass) :: Nat where+    ClassIndex (e ': es) e = 0+    ClassIndex (_ ': es) e = 1 N.+ ClassIndex es e+    ClassIndex '[] e =+        TypeError+            ( 'Text "The effect class ‘" ':<>: 'ShowType e ':<>: 'Text "’ was not found in the list.")++-- keyed effects++type MemberBy u key e efs = (Member u (key #> e) efs, Lookup key efs ~ 'Just (LiftIns (key #> e)))+type MemberHBy u key e ehs = (MemberH u (key ##> e) ehs, Lookup key ehs ~ 'Just (key ##> e))++type family Lookup (key :: k) es :: Maybe SigClass where+    Lookup key (key ##> e ': _) = 'Just (key ##> e)+    Lookup key (LiftIns (key #> e) ': _) = 'Just (LiftIns (key #> e))+    Lookup key (u es ': es') = Lookup key es `OrElse` Lookup key es'+    Lookup key (_ ': es) = Lookup key es+    Lookup key '[] = 'Nothing++type family OrElse (a :: Maybe k) (b :: Maybe k) :: Maybe k where+    OrElse ( 'Just a) _ = 'Just a+    OrElse 'Nothing a = a