heftia 0.3.1.0 → 0.4.0.0

raw patch · 32 files changed

+3739/−3235 lines, 32 filesdep +freer-simpledep −constraintsdep −extensibledep −freedep ~basedep ~data-effectsdep ~mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: freer-simple

Dependencies removed: constraints, extensible, free, kan-extensions, membership, singletons-base, singletons-th, transformers, transformers-base

Dependency ranges changed: base, data-effects, mtl, tasty

API changes (from Hackage documentation)

Files

• ChangeLog.md +12/−0
• README.md +120/−100
• heftia.cabal +41/−54
• src/Control/Effect/ExtensibleChurch.hs +0/−43
• src/Control/Effect/ExtensibleFastA.hs +0/−45
• src/Control/Effect/ExtensibleFinal.hs +0/−43
• src/Control/Effect/ExtensibleFinalA.hs +0/−43
• src/Control/Effect/ExtensibleTree.hs +0/−43
• src/Control/Effect/ExtensibleTreeA.hs +0/−46
• src/Control/Effect/Free.hs +0/−85
• src/Control/Effect/Hefty.hs +0/−1306
• src/Control/Freer.hs +0/−163
• src/Control/Freer/Final.hs +0/−115
• src/Control/Hefty.hs +0/−182
• src/Control/Monad/Freer.hs +0/−21
• src/Control/Monad/Freer/Church.hs +0/−58
• src/Control/Monad/Freer/Tree.hs +0/−74
• src/Control/Monad/Hefty.hs +790/−0
• src/Control/Monad/Hefty/Interpret.hs +578/−0
• src/Control/Monad/Hefty/Interpret/State.hs +119/−0
• src/Control/Monad/Hefty/Transform.hs +616/−0
• src/Control/Monad/Hefty/Types.hs +292/−0
• src/Data/Effect/OpenUnion.hs +121/−0
• src/Data/Effect/OpenUnion/Internal.hs +187/−0
• src/Data/Effect/OpenUnion/Internal/FO.hs +445/−0
• src/Data/Effect/OpenUnion/Internal/HO.hs +387/−0
• src/Data/Effect/OpenUnion/Sum.hs +31/−0
• src/Data/Free/Sum.hs +0/−39
• src/Data/Hefty/Extensible.hs +0/−132
• src/Data/Hefty/Union.hs +0/−531
• src/Data/Hefty/Union/Strengthen.hs +0/−56
• src/Data/Hefty/Union/Weaken.hs +0/−56

@@ -15,3 +15,15 @@ * Fixed #8: bug on `subsume`. https://github.com/sayo-hs/heftia/issues/8 * Added effect list manipulation functions such as `raiseNUnderM`. https://github.com/sayo-hs/heftia/issues/4 * Update the data-effects version to 0.1.1.++## 0.4.0.0 -- 2024-10-10++* Rewrote the codebase to improve performance.+    * Achieved similar speed by using techniques from freer-simple.+    * Optimized by making the open union of higher-order effects a Free HFunctor, avoiding the passing of HFunctor dictionaries.+        * Dropped support for higher-order effects that are not HFunctor.+    * Applied loopbreaker techniques to various inline functions.+    * Simplified the API by eliminating excessive generalization.+        * The interface is largely the same as before, but names have been changed throughout.+* Dropped support for GHC 9.2.8, now supporting GHC 9.4.1 and later.+* Added detailed explanations on how to use Heftia and its semantics to the Haddock documentation of the `Control.Monad.Hefty` module.

@@ -3,22 +3,26 @@ [![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.+Heftia is an extensible effects library that generalizes "Algebraic Effects and Handlers" to higher-order effects, providing users with maximum flexibility and delivering standard and reasonable speed.+In its generalization, the focus is on ensuring predictable results based on simple, consistent semantics, while preserving soundness. -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.+Please refer to the [Haddock documentation](https://hackage.haskell.org/package/heftia-0.4.0.0/docs/Control-Monad-Hefty.html) for usage and semantics.+For information on performance, please refer to [performance.md](https://github.com/sayo-hs/heftia/blob/v0.4.0/benchmark/performance.md). -The paper+The library allows the following effects with well-defined semantics:++* Coroutines+* Non-deterministic computations+* `MonadUnliftIO`++This library is inspired by 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,     POPL, Article 62 (January 2023), 31 pages. <https://doi.org/10.1145/3571255> -inspires this library.-Hefty trees, proposed by the above paper, are extensions of free monads,-allowing for a straightforward treatment of higher-order effects.+The *elaboration* approach proposed in the above paper allows for a straightforward treatment of higher-order effects. -This library offers Hefty monads and Freer monads, encoded into data-types in several ways to enable tuning in pursuit of high performance.+Heftia's data structure is an extension of the Freer monad, designed to be theoretically straightforward by eliminating ad-hoc elements.  ## Status @@ -27,12 +31,12 @@  **We are looking forward to your feedback!** -## Installation+## Getting Started 1.     ```console     $ cabal update     ```-2. Add `heftia-effects ^>= 0.2` and `ghc-typelits-knownnat ^>= 0.7` to the build dependencies. Enable the [ghc-typelits-knownnat](https://hackage.haskell.org/package/ghc-typelits-knownnat) plugin, `GHC2021`, and the following language extensions as needed:+2. Add `heftia-effects ^>= 0.4` and `ghc-typelits-knownnat ^>= 0.7` to the build dependencies. Enable the [ghc-typelits-knownnat](https://hackage.haskell.org/package/ghc-typelits-knownnat) plugin, `GHC2021`, and the following language extensions as needed:      * `LambdaCase`     * `DerivingStrategies`@@ -50,7 +54,7 @@ ...     build-depends:         ...-        heftia-effects ^>= 0.2,+        heftia-effects ^>= 0.4,         ghc-typelits-knownnat ^>= 0.7,      default-language: GHC2021@@ -74,33 +78,11 @@ ... ``` -This library has been tested to work with GHC 9.2.8.+The supported versions are GHC 9.4.1 and later.+This library has been tested with GHC 9.8.2 and 9.4.1.  ## Getting Started-To run the [SemanticsZoo example](https://github.com/sayo-hs/heftia/blob/v0.3.0/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@@ -110,9 +92,8 @@ ### Extracting Multi-shot Delimited Continuations  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](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/Continuation/Main.hs).+the [example code](https://github.com/sayo-hs/heftia/blob/v0.4.0/heftia-effects/Example/Continuation/Main.hs).  ### Two interpretations of the `censor` effect for Writer @@ -147,12 +128,12 @@ main = runEff do     (sPre, _) <-         runTell-            . interpretRecH (elabWriterPre @String)+            . runWriterHPre @String             $ censorHello      (sPost, _) <-         runTell-            . interpretRecH (elabWriterPost @String)+            . runWriterHPost @String             $ censorHello      liftIO $ putStrLn $ "Pre-applying: " <> sPre@@ -165,21 +146,43 @@ Post-applying: Hello world!! ``` -For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs).+For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/v0.4.0/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/v0.4.0/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs). -Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being-eliminated.+### Semantics Zoo+To run the [SemanticsZoo example](https://github.com/sayo-hs/heftia/blob/v0.4.0/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 -Additionally, Heftia supports not only monadic effectful programs but also **applicative effectful programs**.-This may be useful when writing concurrent effectful code.+# 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] -Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs).+# NonDet & Writer+( runNonDet . runTell . runWriterH . runChooseH $ action ) = [(3,(3,True)),(4,(4,False))]+( runTell . runNonDet . runWriterH . runChooseH $ action ) = (6,[(3,True),(4,False)]) +# https://github.com/hasura/eff/issues/12+interpret SomeEff then runCatch : ( runThrow . runCatch . runSomeEff $ action ) = Right "caught"+runCatch then interpret SomeEff : ( runThrow . runSomeEff . runCatch $ action ) = Left "not caught"++[Note] All other permutations will cause type errors.+$+```+ ## Documentation-The example codes are located in the [heftia-effects/Example/](https://github.com/sayo-hs/heftia/tree/v0.3.0/heftia-effects/Example) directory.-Also, the following *HeftWorld* example: https://github.com/sayo-hs/HeftWorld+A detailed explanation of usage and semantics is available in [Haddock](https://hackage.haskell.org/package/heftia-0.4.0.0/docs/Control-Monad-Hefty.html).+The example codes are located in the [heftia-effects/Example/](https://github.com/sayo-hs/heftia/tree/v0.4.0/heftia-effects/Example) directory.+Also, the following *HeftWorld* example (outdated): https://github.com/sayo-hs/HeftWorld -Examples with explanations in Japanese can be found in the [docs-ja/examples/](https://github.com/sayo-hs/heftia/tree/v0.3.0/docs-ja/examples) directory.+About the internal *elaboration* mechanism: https://sayo-hs.github.io/jekyll/update/2024/09/04/how-the-heftia-extensible-effects-library-works.html  ## Comparison @@ -193,34 +196,35 @@  * Semantics: Classification of behaviors resulting from the interpretation of effects. -    * continuation-based: The same as Algebraic Effects and Handlers.-    * IO-based: IO + Reader pattern.-    * carrier dependent: The behavior depends on the specific type inference result of the monad. Tagless-final style.--* Performance: Time complexity or space complexity.+    * Algebraic Effects: The same as Algebraic Effects and Handlers.+    * IO-fused: IO + ReaderT pattern.+    * Carrier dependent: The behavior depends on the specific type inference result of the monad. Tagless-final style. -| Library or Language | Higher-Order Effects | Delimited Continuation | Effect System | Purely Monadic                    | Dynamic Effect Rewriting | Semantics                        | Performance (TODO) |-| ------------------- | -------------------- | ---------------------- | --------------| --------------------------------- | ------------------------ | -------------------------------- | ------------------ |-| Heftia              | Yes                  | Multi-shot             | Yes           | Yes (also Applicative and others) | Yes                      | continuation-based               | ?                  |-| freer-simple        | No                   | Multi-shot             | Yes           | Yes                               | Yes                      | continuation-based               | ?                  |-| Polysemy            | Yes                  | No                     | Yes           | Yes                               | Yes                      | weaving-based (functorial state) | ?                  |-| Effectful           | Yes                  | No                     | Yes           | No (based on the `IO` monad)      | Yes                      | IO-based                         | ?                  |-| eff                 | Yes                  | Multi-shot?            | Yes           | No (based on the `IO` monad)      | Yes                      | continuation-based (IO-fused)    | ?                  |-| in-other-words      | Yes                  | Multi-shot?            | Yes           | Yes                               | No?                      | carrier dependent                | ?                  |-| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes           | Yes                               | No                       | carrier dependent                | ?                  |-| fused-effects       | Yes                  | No?                    | Yes           | Yes                               | No                       | carrier dependent & weaving-based (functorial state) | ?                  |-| koka-lang           | No [^2]              | Multi-shot             | Yes           | No (language built-in)            | Yes                      | continuation-based               | ?                  |-| OCaml-lang 5        | ?                    | One-shot               | No [^3]       | No (language built-in)            | ?                        | continuation-based?              | ?                  |+| Library or Language | Higher-Order Effects | Delimited Continuation | Effect System | Purely Monadic                    | Dynamic Effect Rewriting | Semantics                        |+| ------------------- | -------------------- | ---------------------- | --------------| --------------------------------- | ------------------------ | -------------------------------- |+| `heftia`            | Yes                  | Multi-shot             | Yes           | Yes                               | Yes                      | Algebraic Effects                |+| `freer-simple`      | No                   | Multi-shot             | Yes           | Yes                               | Yes                      | Algebraic Effects                |+| `polysemy`          | Yes                  | No                     | Yes           | Yes                               | Yes                      | Weaving-based (functorial state) |+| `effectful`         | Yes                  | No                     | Yes           | No (based on the `IO` monad)      | Yes                      | IO-fused                         |+| `eff`               | Yes                  | Multi-shot             | Yes           | No (based on the `IO` monad)      | Yes                      | Algebraic Effects & IO-fused [^6]|+| `speff`             | Yes                  | Multi-shot (restriction: [^4]) | Yes   | No (based on the `IO` monad)      | Yes                      | Algebraic Effects & IO-fused     |+| `in-other-words`    | Yes                  | Multi-shot?            | Yes           | Yes                               | No?                      | Carrier dependent                |+| `mtl`               | Yes                  | Multi-shot (`ContT`)   | Yes           | Yes                               | No                       | Carrier dependent                |+| `fused-effects`     | Yes                  | No?                    | Yes           | Yes                               | No                       | Carrier dependent & Weaving-based (functorial state) |+| Koka-lang           | No                   | Multi-shot             | Yes           | No (language built-in)            | Yes                      | Algebraic Effects                |+| OCaml-lang 5        | ?                    | One-shot               | No [^3]       | No (language built-in)            | ?                        | Algebraic Effects?               | -[^2]: https://gist.github.com/ymdryo/6fb2f7f4020c6fcda98ccc67c090dc75 [^3]: Effects do not appear in the type signature and can potentially cause unhandled errors at runtime+[^4]: Scoped Resumption only. e.g. Coroutines are not supported.+[^5]: https://github.com/sayo-hs/heftia/issues/12+[^6]: https://github.com/hasura/eff/issues/12  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. -Additionally, this library provides a consistent *continuation-based* semantics that is independent of carriers and effects.-On the other hand, in libraries like in-other-words, mtl, and fused-effects, the semantics of the code depend on the effect and, in part, the carrier inferred by type inference.-Fixing the semantics to a *continuation-based* model helps improve the predictability of the behavior (interpretation result) of the code.+Additionally, this library provides a consistent algebraic effects semantics that is independent of carriers and effects.+On the other hand, in libraries like `in-other-words`, `mtl`, and `fused-effects`, the semantics of the code depend on the effect and, in part, the carrier inferred by type inference.+Fixing the semantics to a algebraic effects model helps improve the predictability of the behavior (interpretation result) of the code without losing flexibility.  Carrier-dependent semantics can lead to unexpected behavior for code readers, particularly in situations where the types become implicit. Particularly, attention should be given to the fact that due to type inference, semantic changes may propagate beyond the blocks enclosed by `interpret` or `interpose`.@@ -228,49 +232,65 @@ Instead, they function as traditional functions, simply transforming the content of the data structure. This results in minimal surprise to the mental model of the code reader. -### 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`.+### Performance -* 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).+Overall, the performance of this library is positioned roughly in the middle between the fast (`effectful`, `eveff`, etc.) and slow (`polysemy`, `fused-effects`, etc.) libraries, and can be considered average.+In all benchmarks, the speed is nearly equivalent to `freer-simple`, only slightly slower. -* 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).+For more details, please refer to [performance.md](https://github.com/sayo-hs/heftia/blob/v0.4.0/benchmark/performance.md). -* 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 unelaborated.-    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.+### Compatibility with other libraries  #### 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).+* The `Eff` monad is an instance of `MonadIO`, `MonadError`, `MonadRWS`, `MonadUnliftIO`, `Alternative`, 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-* Enriching the documentation and tests-* Completing missing definitions such as-    * more patterns of interpret & transform function-families.-    * interpreters for the `Accum` and others effect classes+#### Representation of effects+* Heftia relies on [data-effects](https://hackage.haskell.org/package/data-effects) for the definitions of standard effects such as `Reader`, `Writer`, and `State`. -    and others.-* Benchmarking+* It is generally recommended to use effects defined with automatic derivation provided by [data-effects-th](https://hackage.haskell.org/package/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`.++* GADTs for higher-order effects are formally similar to Polysemy and fused-effects,+    but they 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.+    While it's not impossible to manually derive `HFunctor` for effect types based on these libraries and use them,+    it's inconvenient, so it's better to use `data-effects`.+    Also, it is not compatible with Effectful and eff.++## Future Plans+* Support for Applicative effects+* Completing lacking definitions such as+    * interpreters for the `Accum` and others effects+ ## License-The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/v0.3.0/NOTICE).-Additionally, this README.md and the documents under the `docs-ja` directory are licensed-under CC BY-SA 4.0.+The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/v0.4.0/NOTICE).+Additionally, the code from `freer-simple` has been modified and used internally within this library.+Therefore, some modules are licensed under both `MPL-2.0 AND BSD-3-Clause`.+For details on licenses and copyrights, please refer to the module's Haddock documentation.  ## Your contributions are welcome!-Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/v0.3.0/CONTRIBUTING.md).+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/v0.4.0/CONTRIBUTING.md). -## Credits-Parts of this project have been inspired by the following resources:+## Acknowledgements, citations, and related work+The following is a non-exhaustive list of people and works that have had a significant impact, directly or indirectly, on Heftia’s design and implementation: -* **[Hefty Algebras -- The Artifact](https://github.com/heft-lang/POPL2023)**-    * **Copyright** (c) 2023 Casper Bach Poulsen and Cas van der Rest-    * **License**: MIT+- Oleg Kiselyov, Amr Sabry, and Cameron Swords — [Extensible Effects: An alternative to monad transfomers][oleg:exteff]+- Oleg Kiselyov and Hiromi Ishii — [Freer Monads, More Extensible Effects][oleg:more]+- Rob Rix, Patrick Thomson, and other contributors — [`fused-effects`][gh:fused-effects]+- Sandy Maguire and other contributors — [`polysemy`][gh:polysemy]+- Alexis King and other contributors — [`freer-simple`][gh:freer-simple], [`eff`][gh:eff]+- Casper Bach Poulsen and Cas van der Rest — [Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects][casper:hefty]++[gh:fused-effects]: https://github.com/fused-effects/fused-effects+[gh:polysemy]: https://github.com/polysemy-research/polysemy+[oleg:exteff]: http://okmij.org/ftp/Haskell/extensible/exteff.pdf+[oleg:more]: http://okmij.org/ftp/Haskell/extensible/more.pdf+[casper:hefty]: https://dl.acm.org/doi/10.1145/3571255+[gh:freer-simple]: https://github.com/lexi-lambda/freer-simple+[gh:eff]: https://github.com/lexi-lambda/eff

@@ -1,82 +1,77 @@ cabal-version:      2.4 name:               heftia-version:            0.3.1.0+version:            0.4.0.0  -- A short (one-line) description of the package. synopsis: higher-order effects done right  -- A longer description of the package. description:-    Heftia is a higher-order effects version of Freer.+    Heftia is an extensible effects library that generalizes "Algebraic Effects and Handlers" to higher-order effects, providing users with maximum flexibility and delivering standard and reasonable speed.+    In its generalization, the focus is on ensuring predictable results based on simple, consistent semantics, while preserving soundness.     .-    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.+    Please refer to the [Haddock documentation](https://hackage.haskell.org/package/heftia-0.4.0.0/docs/Control-Monad-Hefty.html) for usage and semantics.+    For information on performance, please refer to [performance.md](https://github.com/sayo-hs/heftia/blob/v0.4.0/benchmark/performance.md).     .-    The paper+    The library allows the following effects with well-defined semantics:     .-    * Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular-    Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7,-    POPL, Article 62 (January 2023), 31 pages. <https://doi.org/10.1145/3571255>+    * Coroutines+    * Non-deterministic computations+    * `MonadUnliftIO`     .-    inspires this library.-    Hefty trees, proposed by the above paper, are extensions of free monads,-    allowing for a straightforward treatment of higher-order effects.+    This library is inspired by the paper:     .-    This library provides Hefty monads and Freer monads, encoded into data-    types in several ways to enable tuning in pursuit of high performance.+    * Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular+        Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7,+        POPL, Article 62 (January 2023), 31 pages. <https://doi.org/10.1145/3571255>     .+    The /elaboration/ approach proposed in the above paper allows for a straightforward treatment of higher-order effects.+    .+    Heftia's data structure is an extension of the Freer monad, designed to be theoretically straightforward by eliminating ad-hoc elements. + -- A URL where users can report bugs. bug-reports: https://github.com/sayo-hs/heftia  -- The license under which the package is released. license:            MPL-2.0 license-file:       LICENSE-author:             Yamada Ryo <ymdfield@outlook.jp>-maintainer:         Yamada Ryo <ymdfield@outlook.jp>+author:             Sayo Koyoneda <ymdfield@outlook.jp>+maintainer:         Sayo Koyoneda <ymdfield@outlook.jp>  -- A copyright notice. copyright:-    2023-2024 Yamada Ryo+    2023-2024 Sayo Koyoneda+    2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King category: Control, Monads -extra-source-files:+extra-doc-files:     ChangeLog.md     NOTICE     README.md  tested-with:-    GHC == 9.2.8+    GHC == 9.8.2+    GHC == 9.4.1  source-repository head     type: git     location: https://github.com/sayo-hs/heftia-    tag: v0.2.0+    tag: v0.4.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.Final-        Control.Monad.Freer-        Control.Monad.Freer.Church-        Control.Monad.Freer.Tree-        Data.Hefty.Union-        Data.Hefty.Union.Weaken-        Data.Hefty.Union.Strengthen-        Data.Hefty.Extensible-        Data.Free.Sum+        Control.Monad.Hefty+        Control.Monad.Hefty.Types+        Control.Monad.Hefty.Interpret+        Control.Monad.Hefty.Interpret.State+        Control.Monad.Hefty.Transform+        Data.Effect.OpenUnion+        Data.Effect.OpenUnion.Internal+        Data.Effect.OpenUnion.Internal.FO+        Data.Effect.OpenUnion.Internal.HO+        Data.Effect.OpenUnion.Sum      reexported-modules:         Data.Effect,@@ -97,19 +92,11 @@     -- LANGUAGE extensions used by modules in this package.     -- other-extensions:     build-depends:-        base                          ^>= 4.16.4.0,-        data-effects                ^>= 0.1.2,-        mtl ^>= 2.2.2,-        free ^>= 5.2,-        kan-extensions ^>= 5.2.5,-        constraints ^>= 0.13.4,-        transformers-base ^>= 0.4.6,-        transformers ^>= 0.5.6,-        extensible ^>= 0.9,-        membership == 0.0.1,-        singletons-base ^>= 3.1,-        singletons-th ^>= 3.1,-        unliftio ^>= 0.2,+        base                          >= 4.17 && < 4.21,+        data-effects                  ^>= 0.2,+        freer-simple                  ^>= 1.2.1.2,+        mtl                           >= 2.2.2 && < 2.4,+        unliftio                      ^>= 0.2,      hs-source-dirs:   src     ghc-options:      -Wall@@ -133,7 +120,7 @@     build-depends:         heftia,         base,-        tasty                         ^>= 1.4,+        tasty                         >= 1.4 && < 1.6,         tasty-hunit                   ^>= 0.10,      type: exitcode-stdio-1.0

@@ -1,43 +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-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 #-}

@@ -1,45 +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-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 #-}

@@ -1,43 +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-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 #-}

@@ -1,43 +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-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 #-}

@@ -1,43 +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-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 #-}

@@ -1,46 +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-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 #-}

@@ -1,85 +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-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 [@data-effects@](https://hackage.haskell.org/package/data-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,1306 +0,0 @@-{-# 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 Hefty carrier that can be used as a handler for effect systems based-on [@data-effects@](https://hackage.haskell.org/package/data-effects).--}-module Control.Effect.Hefty where--import Control.Arrow ((>>>))-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, (:+:) (Inl, Inr))-import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>))-import Data.Effect.Tag (Tag (Tag, unTag), TagH (TagH, unTagH), type (#), type (##))-import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))-import Data.Hefty.Union (-    HFunctorUnion,-    HFunctorUnion_ (ForallHFunctor),-    HasMembershipRec,-    HeadIns,-    LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),-    Lookup,-    Member,-    MemberBy,-    MemberH,-    MemberHBy,-    MemberRec,-    U,-    UH,-    Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)),-    UnliftIfSingle,-    flipUnion,-    flipUnion3,-    flipUnionUnder,-    injectRec,-    projectRec,-    weaken2,-    weaken2Under,-    weaken2Under2,-    weaken3,-    weaken3Under,-    weaken4,-    weakenUnder2,-    weakenUnder3,-    (|+),- )-import Data.Hefty.Union.Strengthen (Strengthen, StrengthenUnder, strengthenN, strengthenNUnderM)-import Data.Hefty.Union.Weaken (Weaken, WeakenUnder, weakenN, weakenNUnderM)-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 =-    interpretAllRecH-        \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)--raiseN ::-    forall n ef' eh fr u c ef.-    (Weaken n ef ef', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh ef'-raiseN = transformAll $ weakenN @n--raiseNH ::-    forall n eh' ef fr u c eh.-    (Weaken n eh eh', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh' ef-raiseNH = transformAllH $ weakenN @n--raiseNUnderM ::-    forall n m ef' eh fr u c ef.-    (WeakenUnder n m ef ef', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh ef'-raiseNUnderM = transformAll $ weakenNUnderM @n @m--raiseNUnderMH ::-    forall n m eh' ef fr u c eh.-    (WeakenUnder n m eh eh', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh' ef-raiseNUnderMH = transformAllH $ weakenNUnderM @n @m--subsumeN ::-    forall n ef' eh fr u c ef.-    (Strengthen n u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh ef'-subsumeN = transformAll $ strengthenN @n--subsumeNH ::-    forall n eh' ef fr u c eh.-    (Strengthen n u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh' ef-subsumeNH = transformAllH $ strengthenN @n--subsumeNUnderM ::-    forall n m ef' eh fr u c ef.-    (StrengthenUnder n m u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh ef'-subsumeNUnderM = transformAll $ strengthenNUnderM @n @m--subsumeNUnderMH ::-    forall n m eh' ef fr u c eh.-    (StrengthenUnder n m u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>-    Eff u fr eh ef ~> Eff u fr eh' ef-subsumeNUnderMH = transformAllH $ strengthenNUnderM @n @m--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 #-}--raise2 ::-    forall e2 e1 r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs r ~> Eff u fr ehs (e2 ': e1 ': r)-raise2 = transformAll weaken2-{-# INLINE raise2 #-}--raise3 ::-    forall e3 e2 e1 r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs r ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)-raise3 = transformAll weaken3-{-# INLINE raise3 #-}--raise4 ::-    forall e4 e3 e2 e1 r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs r ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)-raise4 = transformAll weaken4-{-# INLINE raise4 #-}--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 #-}--raise3H ::-    forall e3 e2 e1 r efs fr u c.-    (Freer c fr, Union u, HFunctor (u r)) =>-    Eff u fr r efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs-raise3H = transformAllH weaken3-{-# INLINE raise3H #-}--raise4H ::-    forall e4 e3 e2 e1 r efs fr u c.-    (Freer c fr, Union u, HFunctor (u r)) =>-    Eff u fr r efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs-raise4H = transformAllH weaken4-{-# INLINE raise4H #-}--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), HasMembershipRec u e r) =>-    Eff u fr ehs (e ': r) ~> Eff u fr ehs r-subsume = transformAll $ injectRec |+: id-{-# INLINE subsume #-}--subsumeH ::-    forall e r efs fr u c.-    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembershipRec u e r) =>-    Eff u fr (e ': r) efs ~> Eff u fr r efs-subsumeH = transformAllH $ injectRec |+: id-{-# INLINE subsumeH #-}--copyEff ::-    forall e r ehs fr u c.-    ( Freer c fr-    , Union u-    , HFunctor (u ehs)-    , Applicative (Eff u fr ehs (e ': r))-    , HeadIns e-    , HasMembershipRec u e r-    ) =>-    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': r)-copyEff = reinterpretRec \e ->-    send0 e *> liftEff (weaken $ injectRec $ liftInsIfSingle @_ @e e)--copyEffH ::-    forall e r ef fr u c.-    ( Freer c fr-    , Union u-    , HFunctorUnion u-    , HFunctor e-    , ForallHFunctor u r-    , Applicative (Eff u fr (e ': r) ef)-    , HasMembershipRec u e r-    ) =>-    Eff u fr (e ': r) ef ~> Eff u fr (e ': r) ef-copyEffH = reinterpretRecH \e -> send0H e *> liftEffH (weaken $ injectRec e)--dupEff ::-    forall e r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs), Applicative (Eff u fr ehs (e ': e ': r)), HeadIns e) =>-    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': e ': r)-dupEff = raiseUnder >>> reinterpretRec \e -> send0 e *> send1 e-{-# INLINE dupEff #-}--dupEffH ::-    forall e r ef fr u c.-    ( Freer c fr-    , Union u-    , Applicative (Eff u fr (e ': e ': r) ef)-    , HFunctorUnion u-    , HFunctor e-    , ForallHFunctor u r-    ) =>-    Eff u fr (e ': r) ef ~> Eff u fr (e ': e ': r) ef-dupEffH = raiseUnderH >>> reinterpretRecH \e -> send0H e *> send1H e-{-# INLINE dupEffH #-}--bundle ::-    forall e r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs (e ': r) ~> Eff u fr ehs (u '[e] ': r)-bundle = transformAll $ inject0 . inject0 |+: weaken--unbundle ::-    forall e r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs (u '[e] ': r) ~> Eff u fr ehs (e ': r)-unbundle = transformAll $ inject0 . (id |+: end) |+: weaken--pushBundle ::-    forall e r1 r2 ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs (u r1 ': e ': r2) ~> Eff u fr ehs (u (e ': r1) ': r2)-pushBundle = transformAll $ inject0 . weaken |+: inject0 . inject0 |+: weaken--popBundle ::-    forall e r1 r2 ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs (u (e ': r1) ': r2) ~> Eff u fr ehs (u r1 ': e ': r2)-popBundle = transformAll $ (weaken . inject0 |+: inject0) |+: weaken2--enqueSum ::-    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 (e1 :+: e2 ': r)-enqueSum = transformAll $ inject0 . Inl |+: inject0 . Inr |+: weaken--dequeSum ::-    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 (e1 ': e2 ': r)-dequeSum = transformAll $ caseH inject0 (weaken . inject0) |+: weaken2--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 = liftEff . inject0 . liftInsIfSingle-{-# INLINE send0 #-}--send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r)-send1 = liftEff . 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 = liftEffH . 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 = liftEffH . weaken . inject0-{-# INLINE send1H #-}--liftEff :: (Freer c fr, Union u) => u ef Nop ~> Eff u fr eh ef-liftEff = Hefty . liftIns . EffUnion . R1-{-# INLINE liftEff #-}--liftEffH :: (Freer c fr, Union u) => u eh (Eff u fr eh ef) ~> Eff u fr eh ef-liftEffH = Hefty . liftIns . EffUnion . L1-{-# INLINE liftEffH #-}--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 #-}--tagEff ::-    forall tag e r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs)) =>-    Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs (LiftIns (e # tag) ': r)-tagEff = transform Tag-{-# INLINE tagEff #-}--tagEffH ::-    forall tag e r efs fr u c.-    (Freer c fr, Union u, HFunctor (u (e ': r))) =>-    Eff u fr (e ': r) efs ~> Eff u fr (e ## tag ': r) efs-tagEffH = transformH TagH-{-# INLINE tagEffH #-}--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,163 +0,0 @@-{-# 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/.--{- |-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 carriers.--}-module Control.Freer where--import Control.Applicative (Alternative, empty, (<|>))-import Control.Applicative.Free (Ap, liftAp, runAp)-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 e. c (f e)) => Freer c f | f -> c where-    {-# MINIMAL liftIns, (interpretFreer | retractFreer, transformFreer) #-}--    -- | Lift a /instruction/ into a Freer carrier.-    liftIns :: e a -> f e a--    interpretFreer :: c m => (e ~> m) -> f e a -> m a-    interpretFreer i = retractFreer . transformFreer i-    {-# INLINE interpretFreer #-}--    retractFreer :: c m => f m a -> m a-    retractFreer = interpretFreer id-    {-# INLINE retractFreer #-}--    -- | Translate /instruction/s embedded in a Freer carrier.-    transformFreer ::-        (e ~> e') ->-        f e a ->-        f e' a-    transformFreer phi = interpretFreer $ liftIns . phi-    {-# INLINE transformFreer #-}--    reinterpretFreer :: (e ~> f e) -> f e a -> f e a-    reinterpretFreer = interpretFreer-    {-# INLINE reinterpretFreer #-}--instance Freer Functor Coyoneda where-    liftIns = liftCoyoneda-    interpretFreer i = lowerCoyoneda . hoistCoyoneda i-    {-# INLINE liftIns #-}-    {-# INLINE interpretFreer #-}--instance Freer Applicative Ap where-    liftIns = liftAp-    interpretFreer = runAp-    {-# INLINE liftIns #-}-    {-# INLINE interpretFreer #-}--instance Freer Applicative Fast.Ap where-    liftIns = Fast.liftAp-    interpretFreer = Fast.runAp-    {-# INLINE liftIns #-}-    {-# INLINE interpretFreer #-}--newtype-    ViaFreer-        (fr :: InsClass -> Type -> Type)-        (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 #-}

@@ -1,115 +0,0 @@-{-# 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,182 +0,0 @@-{-# 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 #-}

@@ -1,21 +0,0 @@-{-# 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 #-}

@@ -1,58 +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 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 #-}

@@ -1,74 +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 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 #-}

@@ -0,0 +1,790 @@+{-# OPTIONS_GHC -Wno-duplicate-exports #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file)+Maintainer  :  ymdfield@outlook.jp++Heftia is an extensible effects library that generalizes "Algebraic Effects and+Handlers" to higher-order effects, providing users with maximum flexibility and+delivering standard and reasonable speed.+In its generalization, the focus is on ensuring predictable results based on+simple, consistent semantics, while preserving soundness.++= Basic Usage++The following is an example of defining, using, and interpreting the first-order+effect @Log@ for logging and the higher-order effect @Span@ for representing+named spans in a program.++@+import "Control.Monad.Hefty"+import Prelude hiding (log, span)++data Log a where+    Log :: String -> Log ()+'makeEffectF' [''Log]++data Span m (a :: Type) where+    Span :: String -> m a -> Span m a+'makeEffectH' [''Span]++runLog :: ('IO' t'Data.Effect.OpenUnion.<|' ef) => 'Eff' eh (Log ': ef) t'Control.Effect.~>' 'Eff' eh ef+runLog = 'interpret' \\(Log msg) -> liftIO $ putStrLn $ "[LOG] " <> msg++runSpan :: ('IO' t'Data.Effect.OpenUnion.<|' ef) => 'Eff' (Span ': eh) ef t'Control.Effect.~>' 'Eff' eh ef+runSpan = 'interpretH' \\(Span name m) -> do+    'liftIO' $ 'putStrLn' $ "[Start span '" <> name <> "']"+    r <- m+    'liftIO' $ 'putStrLn' $ "[End span '" <> name <> "']"+    'pure' r++prog :: 'IO' ()+prog = 'runEff' . runLog . runSpan $ do+    span "example program" do+        log "foo"++        span "greeting" do+            log "hello"+            log "world"++        log "bar"++>>> prog+[Start span \'example program\']+[LOG] foo+[Start span \'greeting\']+[LOG] hello+[LOG] world+[End span \'greeting\']+[LOG] bar+[End span \'example program\']+@+++* When defining effects, you use the Template Haskell functions 'makeEffectF' and 'makeEffectH'.+* The first 'Eff' type parameter is a type-level list of higher-order effects, the second is for first-order effects.++= Glossary++[Handler]: Interpreter for first-order effects.++[Elaborator]:+    Interpreter for higher-order effects.++    Elaboration is generally performed by editing first-order (or higher-order) effectful operations within the computation held by the higher-order effect being elaborated.++    @+    [runCatch](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:runCatch) :: (@t'Data.Effect.Except.Throw'@ e t'Data.Effect.OpenUnion.<|' ef) => 'Eff' '[@t'Data.Effect.Except.Catch'@ e] ef t'Control.Effect.~>' 'Eff' '[] ef+    runCatch = 'interpretH' elabCatch++    [elabCatch](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:elabCatch) :: (@t'Data.Effect.Except.Throw'@ e t'Data.Effect.OpenUnion.<|' ef) => t'Data.Effect.Except.Catch' e t'Control.Monad.Hefty.~~>' 'Eff' '[] ef+    elabCatch (@v'Data.Effect.Except.Catch'@ action hdl) = action & 'interposeWith' \\(@v'Data.Effect.Except.Throw'@ e) _ -> hdl e+    @++    Here, @elabCatch@ is the elaborator for the t'Data.Effect.Except.Catch' effect.++[Interpretation \/ Handling \/ Elaboration]:+    The act of performing interpretation, or the process thereof.++    Also, an /interpreter function/ refers to a function represented by a natural transformation t'Control.Effect.~>' or of type 'Interpreter', that is, one that takes an effectful operation as an argument.+    On the other hand, when we say /interpretation function/, we mean a function of the form @'Eff' eh ef ~> 'Eff' eh' ef'@, that is, one that takes the 'Eff' monad as an argument.+    In the previous example, @elabCatch@ is the /interpreter function/ for the t'Data.Effect.Except.Catch' effect, and @runCatch@ is the /interpretation function/ for the t'Data.Effect.Except.Catch' effect.++    The interpretation function may also be called an /interpreter/.++[Continuational stateful interpreter]:+    An interpreter function that realizes features related to the continuation in algebraic effects.++    It is a function that takes two arguments: an effectful operation and a continuation, which is the continuation of the computation from that operation, and returns the computation up to the end of the computation being interpreted.++    By ignoring the continuation argument, it allows for global escapes like the 'Data.Effect.Except.Throw' effect.++    @+    [runThrow](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:runThrow) :: 'Eff' '[] (@t'Data.Effect.Except.Throw'@ e ': r) a -> 'Eff' '[] r ('Either' e a)+    runThrow = 'interpretBy' ('pure' '.' 'Right') handleThrow++    [handleThrow](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:handleThrow) :: 'Interpreter' (@t'Data.Effect.Except.Throw'@ e) ('Eff' '[] r) ('Either' e a)+    handleThrow (@v'Data.Effect.Except.Throw'@ e) _ = 'pure' $ 'Left' e+    @++    Here, @handleThrow@ is the continuational stateful handler for the t'Data.Effect.Except.Throw' effect.++    By calling the continuation argument multiple times, it allows for non-deterministic computations like the "Data.Effect.NonDet" effect.++    @+    [runNonDet](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-NonDet.html#v:runNonDet)+        :: forall f ef a+        . ('Alternative' f)+        => 'Eff' '[] (@t'Data.Effect.NonDet.Choose'@ ': t'Data.Effect.NonDet.Empty' ': ef) a+        -> 'Eff' '[] ef (f a)+    runNonDet =+        'bundleN' \@2+            '>>>' 'interpretBy'+                ('pure' . 'pure')+                ( (\\@v'Data.Effect.NonDet.Choose'@ k -> 'liftA2' ('<|>') (k 'False') (k 'True'))+                    '!+' (\\@v'Data.Effect.NonDet.Empty'@ _ -> 'pure' 'empty')+                    '!+' 'nil'+                )+    @++    The function passed as the second argument to 'interpretBy' is the continuational stateful handler.++    Additionally, what is passed as the first argument to 'interpretBy' is called a /value handler/.+    This extends the continuation in the computation being interpreted.++[Continuational state]:+    The state of the computation that appears through interpretation, behaving based on [continuation-based semantics](https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md).++= Naming Rules for Interpretation Functions++* Functions with an @H@, such as 'interpretH', are for higher-order effects, while those without are for first-order effects.++    @+    'interpret' :: e t'Control.Effect.~>' 'Eff' eh ef -> 'Eff' (e ': eh) ef ~> 'Eff' eh ef+    'interpretH' :: e ('Eff' eh ef) t'Control.Effect.~>' 'Eff' eh ef -> 'Eff' (e ': eh) ef t'Control.Effect.~>' 'Eff' eh ef+    @++    Note: t'Control.Effect.~>' binds more tightly than @->@.++* Functions may additionally have @With@ or @By@ at the end of their names.++    * These provide functionality equivalent to "Algebraic Effects and Handlers," meaning they offer access to delimited continuations during interpretation.++    * Functions in the @By@ family take two arguments: a value handler and a continuational stateful effect interpreter. They are the most generalized form.++    * Functions in the @With@ family omit the value handler and take only the effect interpreter as an argument.++    * The difference between @interpretBy ret f m@ and @interpretWith f m >>= ret@ is that, during interpretation,+        the delimited continuation passed as the second argument @k@ to @f@ in the former extends up to when @ret@ finishes,+        whereas in the latter, it only goes until @m@ finishes (just before @ret@), so @ret@ is not included in @k@.++    * Functions without @With@ or @By@ cannot manipulate continuations;+        therefore, you cannot maintain internal state or perform behaviors like+        global escapes or non-deterministic computations during interpretation.++* Functions that perform recursive continuational stateful interpretation have @Rec@ additionally added.++    * Non-recursive continuational stateful interpretation functions like 'interpretWith' cannot be used unless the higher-order effects are empty:++        @+        'interpretWith' :: e ~> Eff '[] ef => 'Eff' '[] (e ': ef) ~> 'Eff' '[] ef+        @++    * The @Rec@ versions can be used even when @eh@ is not empty.++        @+        'interpretRecWith' :: e ~> 'Eff' eh (e ': ef) ~> 'Eff' eh ef+        @++    * When using this type of function, pay attention to their /reset semantics/. This is discussed later.++    * In principle, they cannot take value handlers, so there is no combination with @By@.++Function names combine the above three attributes.+Examples of complex combinations include 'interpretHBy' and 'interpretRecHWith'.++= Semantics of effects++Consider the following example.++@+data SomeEff a where+    SomeAction :: SomeEff String+'makeEffectF' [''SomeEff]++-- | Throws an exception when \'SomeAction\' is encountered+runSomeEff :: (@t'Data.Effect.Except.Throw'@ String t'Data.Effect.OpenUnion.<|' ef) => 'Eff' eh (SomeEff ': ef) ~> 'Eff' eh ef+runSomeEff = 'interpret' \\SomeAction -> v'Data.Effect.Except.throw' "not caught"++-- | Catches the exception if \'someAction\' results in one+action :: (SomeEff t'Data.Effect.OpenUnion.<|' ef, t'Data.Effect.Except.Catch' String t'Data.Effect.OpenUnion.<<|' eh, t'Data.Effect.Except.Throw' String '<|' ef) => Eff eh ef+action = someAction \`@v'Data.Effect.Except.catch'@\` \\(_ :: String) -> 'pure' "caught"++prog1 :: IO ()+prog1 = 'runPure' . runThrow @String . runCatch @String . runSomeEff $ action++>>> prog1+Right "caught"++prog2 :: IO ()+prog2 = 'runPure' . runThrow @String . runSomeEff . runCatch @String $ action++>>> prog2+Left "not caught"+@++When applying @runCatch@ after @runSomeEff@ in @prog1@, the exception is caught, but in the reverse order, it is not caught.+We will now explain this behavior to understand it.++In Heftia, the behavior of higher-order effects is based on reduction semantics—that is, term rewriting semantics similar to those in "Algebraic Effects and Handlers."+By properly understanding and becoming familiar with this semantics, users can quickly and easily predict execution results.++Let's revisit the definition of @runCatch@:++@+[runCatch](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:runCatch) :: (@t'Data.Effect.Except.Throw'@ e t'Data.Effect.OpenUnion.<|' ef) => 'Eff' '[@t'Data.Effect.Except.Catch'@ e] ef t'Control.Effect.~>' 'Eff' '[] ef+runCatch = 'interpretH' elabCatch++[elabCatch](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-Except.html#v:elabCatch) :: (@t'Data.Effect.Except.Throw'@ e t'Data.Effect.OpenUnion.<|' ef) => t'Data.Effect.Except.Catch' e t'Control.Monad.Hefty.~~>' 'Eff' '[] ef+elabCatch (@v'Data.Effect.Except.Catch'@ action hdl) = action & 'interposeWith' \\(@v'Data.Effect.Except.Throw'@ e) _ -> hdl e+@++When @runCatch@ encounters code like @... (action \`catch\` hdl) ...@ in the program, it rewrites that part to @... ('interposeWith' (\\(@v'Data.Effect.Except.Throw'@ e) _ -> hdl e) action) ...@.+In general, functions like 'interpretH' and 'interposeH' behave this way—they recursively rewrite the target higher-order effects according to the given elaborator.+Rewriting proceeds from the deepest scope toward the outer scopes.++The same applies to first-order effects. Handling an effect means rewriting the effects that appear in the program.++With this in mind, let's follow the rewriting step by step.++Looking at @prog1@.+First, when @runSomeEff@ is applied to @action@:++@+    runSomeEff action+ =  'interpret' (\\SomeAction -> v'Data.Effect.Except.throw' "not caught") $ someAction \`@v'Data.Effect.Except.catch'@\` \\(_ :: String) -> 'pure' "caught"+==> v'Data.Effect.Except.throw' "not caught" \`@v'Data.Effect.Except.catch'@\` \\(_ :: String) -> 'pure' "caught"+@++The program is rewritten into a program like the above.++Next, when @runCatch@ is applied to this, it evaluates to:++@+    runCatch \@String $ v'Data.Effect.Except.throw' "not caught" \`@v'Data.Effect.Except.catch'@\` \\(_ :: String) -> 'pure' "caught"+==> 'interposeWith' (\\(@v'Data.Effect.Except.Throw'@ e) _ -> 'pure' "caught") $ v'Data.Effect.Except.throw' "not caught"+==> 'pure' "caught"+@++In this way, the exception is caught.++On the other hand, in @prog2@, when @runCatch@ is applied to @action@:++@+    runCatch \@String action+ =  runCatch \@String $ someAction \`@v'Data.Effect.Except.catch'@\` \\(_ :: String) -> 'pure' "caught"+==> 'interposeWith' (\\(@v'Data.Effect.Except.Throw' e) _ -> 'pure' "caught") $ someAction+@++At this point, since there is no v'Data.Effect.Except.throw' in the computation+that is the target of 'interposeWith' (only @someAction@ appears, which is not+ v'Data.Effect.Except.throw'!), 'interposeWith' does nothing because there is no+ v'Data.Effect.Except.throw' to rewrite:++@+==> someAction+@++Therefore, when @runSomeEff@ is applied:++@+    runSomeEff someAction+==> v'Data.Effect.Except.throw' "not caught"+@++Thus, the exception remains as is.++In other words, in @prog2@, at the point of @runCatch@, /it is impossible for @runCatch@ to know that @someAction@ will later be rewritten into @throw@/.+__Interpreters decide what to do based only on the current state of the program's rewriting__. They do not change the result based on any other information.++This is all there is to the reduction semantics of algebraic effects.++== Independence from IO Semantics++As seen in the initial example with logs and spans, 'IO' operations are embedded as effects.+Not limited to 'IO', any monad can be embedded as an effect.++Embedded 'IO' can be viewed as instruction scripts, and to avoid confusion when using Heftia, it should be regarded as such.+Rather than thinking "Haskell represents side effects via a type-level tag called 'IO'", it's better to think:++* Haskell is a purely functional language where you cannot write anything other than pure functions.+* 'IO' is just an opaque algebraic data type whose definition you cannot see, no different from others.+* The runtime system treats the value @main@ as a sequence of instructions to be executed on the CPU.+* Programming with side effects in Haskell is meta-programming where you write a pure function program that outputs 'IO' type instruction scripts.++In fact, the semantics of effects in Heftia are completely isolated from the level of 'IO'.+Considerations at the 'IO' level, such as "asynchronous exceptions might be thrown",+"what is the current state of exception masking", or+"this state/environment value is local and not shared between threads", have no influence on effect interpretation and need not be considered.+ 'IO' is just a data type representing programs with side effects, and we are merely meta-programming it.+The consistent semantics of algebraic effects prevent leaks of abstraction from the 'IO' level.++This is a significant difference from 'IO'-fused effect system libraries like [effectful](https://hackage.haskell.org/package/effectful) and [cleff](https://hackage.haskell.org/package/cleff).++= Reset Semantics in Recursive Continuational Stateful Interpretation++When performing recursive continuational stateful interpretation, that is, when using functions with @Rec@, it's necessary to understand their semantics.+If you are not using @Rec@ functions, you don't need to pay particular attention to this section.++[@runStateRec@](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-State.html#v:runStateRec) is a variant of+ [@runState@](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-State.html#v:runState),+a handler for the @State@ effect that can be used even when higher-order effects are unelaborated:++@+[@runStateRec@](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-State.html#v:runStateRec) :: 'Eff' eh (@t'Data.Effect.State.State'@ s ': ef) t'Control.Effect.~>' 'Eff' eh ef+[@runState@](https://hackage.haskell.org/package/heftia-effects-0.4.0.0/docs/Control-Monad-Hefty-State.html#v:runState) :: 'Eff' '[] (@t'Data.Effect.State.State'@ s ': ef) t'Control.Effect.~>' 'Eff' '[] ef+@++@runStateRec@ uses @Rec@ functions internally. When a function uses @Rec@ functions internally, it's best to reflect that in its naming.++Now, if you perform @runStateRec@ before elaborating higher-order effects, the following occurs.+Note that we are using the @Log@ and @Span@ effects introduced in the first example.++@+import Prelude hiding (log, span)++prog :: IO ()+prog = 'runEff' do+    runLog . runSpan . runStateRec \@[Int] [] $ do++        v'Data.Effect.State.modify' \@[Int] (++ [1])+        log . show =<< v'Data.Effect.State.get' \@[Int]++        span \"A\" do+            v'Data.Effect.State.modify' \@[Int] (++ [2])+            log . show =<< v'Data.Effect.State.get' \@[Int]++        v'Data.Effect.State.modify' \@[Int] (++ [3])+        log . show =<< v'Data.Effect.State.get' \@[Int]++    'pure' ()++>>> prog+[LOG] [1]+[Start span 'A']+[LOG] [1,2]+[End span 'A']+[LOG] [1,3]+@++After exiting span @A@, the added @2@ has disappeared. As shown, state changes within the scope may not be preserved after exiting the scope.++This is a fundamental limitation of state preservation.+When attempting to perform continuational stateful interpretation of an effect,+if there are unelaborated higher-order effects remaining, resets of this continuational state occur for each scope of those higher-order effects.+For higher-order effects that have already been elaborated and removed from the list at that point, there is naturally no impact.++This is simply because @runStateRec@ (generally all @Rec@ functions) recursively applies @runState@ to the scopes of unelaborated higher-order effects.+Interpretation occurs independently for each scope, and the state is not carried over.++From the perspective of @shift/reset@ delimited continuations, this phenomenon can be seen as @reset@s being inserted at the scopes of unelaborated higher-order effects.++Whether this behavior occurs can be determined in advance.+This reset behavior occurs only when using @Rec@ functions and when the program passed to that function performs unelaborated higher-order effects internally.+The reset behavior occurs locally only at the points where those effects are performed.+Whether an unelaborated higher-order effect @e@ is performed internally can generally be determined by looking at the type signature of the effectful program.+Given an effectful program @p@, if its type signature includes @e@ in the list of higher-order effects,+or if the constraint part includes @e t'Data.Effect.OpenUnion.<<|' eh@ or @e t'Control.Effect.<<:' m@, then you know that higher-order effect is being used.+If not, @e@ cannot be performed internally in the function @p@.++If you do not desire this reset behavior, you can avoid it by elaborating all higher-order effects first and emptying them when performing continuational stateful interpretation without using @Rec@ functions:++@+import Prelude hiding (log, span)++prog :: IO ()+prog = 'runEff' do+    runLog . runState \@[Int] [] . runSpan $ do++        v'Data.Effect.State.modify' \@[Int] (++ [1])+        log . show =<< v'Data.Effect.State.get' \@[Int]++        span \"A\" do+            v'Data.Effect.State.modify' \@[Int] (++ [2])+            log . show =<< v'Data.Effect.State.get' \@[Int]++        v'Data.Effect.State.modify' \@[Int] (++ [3])+        log . show =<< v'Data.Effect.State.get' \@[Int]++    'pure' ()++>>> prog+[LOG] [1]+[Start span 'A']+[LOG] [1,2]+[Ene span 'A']+[LOG] [1,2,3]+@++= Interpreting Multiple Effects Simultaneously++For example, consider a situation where you want to use multiple t'Data.Effect.Except.Catch' effects simultaneously.+The following is a case where both @String@ and @Int@ appear as exception types:++@+prog :: 'Eff' '[@t'Data.Effect.Except.Catch'@ String, @t'Data.Effect.Except.Catch'@ Int] '[@t'Data.Effect.Except.Throw'@ String, @t'Data.Effect.Except.Throw'@ Int] ()+@++In this case, you may get stuck trying to use @runCatch@.+This is because @runCatch@ has the following type signature:++@+runCatch :: (@t'Data.Effect.Except.Throw'@ e t'Data.Effect.OpenUnion.<|' ef) => 'Eff' '[@t'Data.Effect.Except.Catch'@ e] ef t'Control.Effect.~>' 'Eff' '[] ef+@++You cannot write @runCatch \@Int . runCatch \@String@. It requires the higher-order effects to be empty after interpretation:+++>runCatch @String . runCatch @Int $ prog+>                   ^^^^^^^^^^^^^+>+>• Couldn't match type: '[]+>                 with: '[Catch String]+>  Expected: Eff '[Catch Int] ef x -> Eff '[Catch String] ef x+>    Actual: Eff '[Catch Int] ef x -> Eff '[] ef x+>• In the second argument of ‘(.)’, namely ‘runCatch @Int’+>  In the first argument of ‘($)’, namely+>    ‘runCatch @String . runCatch @Int’+>  In the expression: runCatch @String . runCatch @Int $ prog++In situations like this, where you want to perform continuational stateful elaboration on multiple higher-order effects simultaneously,+you generally cannot reduce the higher-order effect list step by step or via multi-staging.+Instead, you need to elaborate /all of them at once simultaneously/.++This is possible by pattern matching on the open union of higher-order effects using the '!!+' operator.++@+prog' :: 'Eff' '[] '[@t'Data.Effect.Except.Throw'@ String, @t'Data.Effect.Except.Throw'@ Int] ()+prog' = 'interpretH' (elabCatch \@String '!!+' elabCatch \@Int '!!+' 'nilH') . 'bundleAllH' $ prog+@++'bundleAllH' collects the entire list of higher-order effects into a single higher-order effect using an open union.++Similarly, this can be done for first-order effects using '!+', 'nil', and 'bundleAll'.+-}+module Control.Monad.Hefty (+    -- * Basics+    Eff (Op, Val),+    type (:!!),+    type (!!),+    type (+),+    type (:+:),+    type ($),+    type ($$),+    Interpreter,+    Elaborator,+    type (~~>),+    send,+    sendH,+    send0,+    send0H,+    sendN,+    sendNH,+    sendUnion,+    sendUnionBy,+    sendUnionH,+    sendUnionHBy,++    -- * Interpreting effects++    -- ** Running t`Eff`+    runEff,+    runPure,++    -- ** Standard functions++    -- *** For first-order effects+    interpret,+    interpretWith,+    interpretBy,+    interpretRecWith,++    -- *** For higher-order effects+    interpretH,+    interpretHWith,+    interpretHBy,+    interpretRecHWith,++    -- ** Reinterpretation functions++    -- *** For first-order effects+    reinterpret,+    reinterpretN,+    reinterpretNWith,+    reinterpretBy,+    reinterpretNBy,+    reinterpretRecWith,+    reinterpretRecNWith,++    -- *** For higher-order effects+    reinterpretH,+    reinterpretNH,+    reinterpretHWith,+    reinterpretNHWith,+    reinterpretHBy,+    reinterpretNHBy,+    reinterpretRecHWith,+    reinterpretRecNHWith,++    -- ** Interposition functions++    -- *** For first-order effects+    interpose,+    interposeWith,+    interposeBy,+    interposeRecWith,++    -- *** For higher-order effects+    interposeH,+    interposeRecHWith,++    -- ** Transformation to monads+    iterEffBy,+    iterEffHBy,+    iterEffRecH,+    iterEffRecHWith,+    iterEffRecHFWith,+    iterEffHFBy,+    iterAllEffHFBy,++    -- ** Utilities+    stateless,++    -- ** Ad-hoc stateful interpretation++    -- | Theses entities provides an ad-hoc specialized version to accelerate interpretations that have a+    -- single state type @s@, especially for effects like t'Data.Effect.State.State' or+    --  [@Writer@]("Data.Effect.Writer").+    StateElaborator,+    StateInterpreter,++    -- *** Interpretation functions+    interpretStateBy,+    reinterpretStateBy,+    interpretStateRecWith,+    reinterpretStateRecWith,++    -- *** Interposition functions+    interposeStateBy,++    -- *** Transformation to monads+    iterStateAllEffHFBy,++    -- * Transforming effects++    -- ** Rewriting effectful operations+    transform,+    transformH,+    translate,+    translateH,+    rewrite,+    rewriteH,+    transEff,+    transEffH,+    transEffHF,++    -- ** Manipulating the effect list (without rewriting effectful operations)++    -- *** Insertion functions+    raise,+    raises,+    raiseN,+    raiseUnder,+    raisesUnder,+    raiseNUnder,+    raiseH,+    raisesH,+    raiseNH,+    raiseUnderH,+    raiseNUnderH,++    -- *** Merging functions+    subsume,+    subsumes,+    subsumeN,+    subsumeUnder,+    subsumesUnder,+    subsumeNUnder,+    subsumeH,+    subsumesH,+    subsumeNH,+    subsumeUnderH,+    subsumeNUnderH,++    -- ** Bundling functions+    bundle,+    bundleN,+    unbundle,+    unbundleN,+    bundleUnder,+    unbundleUnder,+    bundleAll,+    unbundleAll,+    bundleH,+    unbundleH,+    bundleUnderH,+    unbundleUnderH,+    bundleAllH,+    unbundleAllH,++    -- *** Manipulating Tags & Keys+    tag,+    untag,+    retag,+    tagH,+    untagH,+    retagH,+    unkey,+    rekey,+    unkeyH,+    rekeyH,++    -- * Misc+    HFunctor,+    ReaderKey,+    WriterKey,+    StateKey,+    ErrorKey,+    Type,+    liftIO,+    module Data.Effect.OpenUnion,+    module Data.Effect,+    module Data.Effect.TH,+    module Control.Effect,+) where++import Control.Monad.Hefty.Interpret (+    interpose,+    interposeBy,+    interposeH,+    interposeRecHWith,+    interposeRecWith,+    interposeWith,+    interpret,+    interpretBy,+    interpretH,+    interpretHBy,+    interpretHWith,+    interpretRecHWith,+    interpretRecWith,+    interpretWith,+    iterAllEffHFBy,+    iterEffBy,+    iterEffHBy,+    iterEffHFBy,+    iterEffRecH,+    iterEffRecHFWith,+    iterEffRecHWith,+    reinterpret,+    reinterpretBy,+    reinterpretH,+    reinterpretHBy,+    reinterpretHWith,+    reinterpretN,+    reinterpretNBy,+    reinterpretNH,+    reinterpretNHBy,+    reinterpretNHWith,+    reinterpretNWith,+    reinterpretRecHWith,+    reinterpretRecNHWith,+    reinterpretRecNWith,+    reinterpretRecWith,+    runEff,+    runPure,+    stateless,+ )++import Control.Monad.Hefty.Interpret.State (+    StateElaborator,+    StateInterpreter,+    interposeStateBy,+    interpretStateBy,+    interpretStateRecWith,+    iterStateAllEffHFBy,+    reinterpretStateBy,+    reinterpretStateRecWith,+ )+import Control.Monad.Hefty.Transform (+    bundle,+    bundleAll,+    bundleAllH,+    bundleH,+    bundleN,+    bundleUnder,+    bundleUnderH,+    raise,+    raiseH,+    raiseN,+    raiseNH,+    raiseNUnder,+    raiseNUnderH,+    raiseUnder,+    raiseUnderH,+    raises,+    raisesH,+    raisesUnder,+    rekey,+    rekeyH,+    retag,+    retagH,+    rewrite,+    rewriteH,+    subsume,+    subsumeH,+    subsumeN,+    subsumeNH,+    subsumeNUnder,+    subsumeNUnderH,+    subsumeUnder,+    subsumeUnderH,+    subsumes,+    subsumesH,+    subsumesUnder,+    tag,+    tagH,+    transEff,+    transEffH,+    transEffHF,+    transform,+    transformH,+    translate,+    translateH,+    unbundle,+    unbundleAll,+    unbundleAllH,+    unbundleH,+    unbundleN,+    unbundleUnder,+    unbundleUnderH,+    unkey,+    unkeyH,+    untag,+    untagH,+ )++import Control.Effect+import Control.Monad.Hefty.Types (+    Eff (..),+    Elaborator,+    ErrorKey,+    Interpreter,+    ReaderKey,+    StateKey,+    WriterKey,+    send,+    send0,+    send0H,+    sendH,+    sendN,+    sendNH,+    sendUnion,+    sendUnionBy,+    sendUnionH,+    sendUnionHBy,+    type (!!),+    type ($),+    type ($$),+    type (:!!),+    type (~~>),+ )+import Control.Monad.IO.Class (liftIO)+import Data.Effect+import Data.Effect.HFunctor (HFunctor)+import Data.Effect.OpenUnion+import Data.Effect.OpenUnion.Sum (type (:+:))+import Data.Effect.TH+import Data.Kind (Type)

@@ -0,0 +1,578 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause++-- 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) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)+Maintainer  :  ymdfield@outlook.jp++This module provides functions for interpretation.+Please refer to the documentation of the [top-level module]("Control.Monad.Hefty").+-}+module Control.Monad.Hefty.Interpret where++import Control.Arrow ((>>>))+import Control.Effect (type (~>))+import Control.Monad.Hefty.Types (+    Eff (Op, Val),+    Elaborator,+    Interpreter,+    sendUnionBy,+    sendUnionHBy,+    type (~~>),+ )+import Data.Effect.HFunctor (HFunctor, hfmap)+import Data.Effect.OpenUnion.Internal (IsSuffixOf, WeakenN)+import Data.Effect.OpenUnion.Internal.FO (+    Member (prj),+    Union,+    extract,+    nil,+    weakenN,+    weakens,+    (!+),+    type (<|),+ )+import Data.Effect.OpenUnion.Internal.HO (+    MemberH (prjH),+    UnionH,+    extractH,+    hfmapUnion,+    nilH,+    weakenNH,+    weakensH,+    (!!+),+    type (<<|),+ )+import Data.FTCQueue (FTCQueue, ViewL (TOne, (:|)), tviewl, (><))++-- * Running t`Eff`++-- | Lowers the computation into a monad @m@ by treating the effect as a monad.+runEff :: (Monad m) => Eff '[] '[m] ~> m+runEff = iterEffBy pure $ stateless id+{-# INLINE runEff #-}++-- | Extracts the value from a computation that contains only pure values without any effect.+runPure :: Eff '[] '[] a -> a+runPure = \case+    Val x -> x+    Op u _ -> case u of+        Left u' -> nilH u'+        Right u' -> nil u'+{-# INLINE runPure #-}++-- * Standard interpretation functions++-- ** For first-order effects++-- | Interprets the first-order effect @e@ at the head of the list using the provided natural transformation style handler.+interpret+    :: forall e ef eh+     . (e ~> Eff eh ef)+    -- ^ Effect handler+    -> Eff eh (e ': ef) ~> Eff eh ef+interpret = reinterpret+{-# INLINE interpret #-}++-- | Interprets the first-order effect @e@ at the head of the list using the provided continuational stateful handler.+interpretWith+    :: forall e ef a+     . Interpreter e (Eff '[] ef) a+    -- ^ Effect handler+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef a+interpretWith = reinterpretWith+{-# INLINE interpretWith #-}++-- | Interprets the first-order effect @e@ at the head of the list using the provided value handler and continuational stateful handler.+interpretBy+    :: forall e ef ans a+     . (a -> Eff '[] ef ans)+    -- ^ Value handler+    -> Interpreter e (Eff '[] ef) ans+    -- ^ Effect handler+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef ans+interpretBy = reinterpretBy+{-# INLINE interpretBy #-}++{- | Interprets the first-order effect @e@ at the head of the list using the provided continuational stateful handler.++Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.+Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.+-}+interpretRecWith+    :: forall e ef eh a+     . (forall ans. Interpreter e (Eff eh ef) ans)+    -- ^ Effect handler+    -> Eff eh (e ': ef) a+    -> Eff eh ef a+interpretRecWith = reinterpretRecWith+{-# INLINE interpretRecWith #-}++-- ** For higher-order effects++-- | Interprets the higher-order effect @e@ at the head of the list using the provided natural transformation style elaborator.+interpretH+    :: forall e eh ef+     . (HFunctor e)+    => e ~~> Eff eh ef+    -- ^ Effect elaborator+    -> Eff (e ': eh) ef ~> Eff eh ef+interpretH = reinterpretH+{-# INLINE interpretH #-}++-- | Interprets the single higher-order effect @e@ using the provided continuational stateful elaborator.+interpretHWith+    :: forall e eh ef a+     . (HFunctor e)+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a+    -- ^ Effect elaborator+    -> Eff '[e] ef a+    -> Eff eh ef a+interpretHWith = reinterpretHWith+{-# INLINE interpretHWith #-}++-- | Interprets the single higher-order effect @e@ using the provided value handler and continuational stateful elaborator.+interpretHBy+    :: forall e eh ef ans a+     . (HFunctor e)+    => (a -> Eff eh ef ans)+    -- ^ Value handler+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans+    -- ^ Effect elaborator+    -> Eff '[e] ef a+    -> Eff eh ef ans+interpretHBy = reinterpretHBy+{-# INLINE interpretHBy #-}++{- | Interprets the higher-order effect @e@ at the head of the list using the provided continuational stateful elaborator.++Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.+Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.+-}+interpretRecHWith+    :: forall e eh ef a+     . (HFunctor e)+    => (forall ans. Elaborator e (Eff eh ef) ans)+    -- ^ Effect elaborator+    -> Eff (e ': eh) ef a+    -> Eff eh ef a+interpretRecHWith = reinterpretRecHWith+{-# INLINE interpretRecHWith #-}++-- * Reinterpretation functions++-- ** For first-order effects++reinterpret+    :: forall e ef' ef eh+     . (ef `IsSuffixOf` ef')+    => (e ~> Eff eh ef')+    -> Eff eh (e ': ef) ~> Eff eh ef'+reinterpret f = reinterpretRecWith (stateless f)+{-# INLINE reinterpret #-}++reinterpretN+    :: forall n e ef' ef eh+     . (WeakenN n ef ef')+    => (e ~> Eff eh ef')+    -> Eff eh (e ': ef) ~> Eff eh ef'+reinterpretN f = reinterpretRecNWith @n (stateless f)+{-# INLINE reinterpretN #-}++reinterpretWith+    :: forall e ef' ef a+     . (ef `IsSuffixOf` ef')+    => Interpreter e (Eff '[] ef') a+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef' a+reinterpretWith = reinterpretBy pure+{-# INLINE reinterpretWith #-}++reinterpretNWith+    :: forall n e ef' ef a+     . (WeakenN n ef ef')+    => Interpreter e (Eff '[] ef') a+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef' a+reinterpretNWith = reinterpretNBy @n pure+{-# INLINE reinterpretNWith #-}++reinterpretBy+    :: forall e ef' ef ans a+     . (ef `IsSuffixOf` ef')+    => (a -> Eff '[] ef' ans)+    -> Interpreter e (Eff '[] ef') ans+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef' ans+reinterpretBy ret hdl = iterAllEffHFBy ret nilH (hdl !+ flip sendUnionBy . weakens)+{-# INLINE reinterpretBy #-}++reinterpretNBy+    :: forall n e ef' ef ans a+     . (WeakenN n ef ef')+    => (a -> Eff '[] ef' ans)+    -> Interpreter e (Eff '[] ef') ans+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef' ans+reinterpretNBy ret hdl = iterAllEffHFBy ret nilH (hdl !+ flip sendUnionBy . weakenN @n)+{-# INLINE reinterpretNBy #-}++reinterpretRecWith+    :: forall e ef' ef eh a+     . (ef `IsSuffixOf` ef')+    => (forall ans. Interpreter e (Eff eh ef') ans)+    -> Eff eh (e ': ef) a+    -> Eff eh ef' a+reinterpretRecWith hdl = loop+  where+    loop :: Eff eh (e ': ef) ~> Eff eh ef'+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmapUnion loop) (hdl !+ flip sendUnionBy . weakens)+{-# INLINE reinterpretRecWith #-}++reinterpretRecNWith+    :: forall n e ef' ef eh a+     . (WeakenN n ef ef')+    => (forall ans. Interpreter e (Eff eh ef') ans)+    -> Eff eh (e ': ef) a+    -> Eff eh ef' a+reinterpretRecNWith hdl = loop+  where+    loop :: Eff eh (e ': ef) ~> Eff eh ef'+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmapUnion loop) (hdl !+ flip sendUnionBy . weakenN @n)+{-# INLINE reinterpretRecNWith #-}++-- ** For higher-order effects++reinterpretH+    :: forall e eh eh' ef+     . (HFunctor e, eh `IsSuffixOf` eh')+    => e ~~> Eff eh' ef+    -> Eff (e ': eh) ef ~> Eff eh' ef+reinterpretH elb = reinterpretRecHWith (stateless elb)+{-# INLINE reinterpretH #-}++reinterpretNH+    :: forall n e eh eh' ef+     . (HFunctor e, WeakenN n eh eh')+    => e ~~> Eff eh' ef+    -> Eff (e ': eh) ef ~> Eff eh' ef+reinterpretNH elb = reinterpretRecNHWith @n (stateless elb)+{-# INLINE reinterpretNH #-}++reinterpretHWith+    :: forall e eh ef a+     . (HFunctor e)+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a+    -> Eff '[e] ef a+    -> Eff eh ef a+reinterpretHWith = reinterpretHBy pure+{-# INLINE reinterpretHWith #-}++reinterpretNHWith+    :: forall n e eh ef a+     . (HFunctor e, WeakenN n '[] eh)+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a+    -> Eff '[e] ef a+    -> Eff eh ef a+reinterpretNHWith = reinterpretHWith+{-# INLINE reinterpretNHWith #-}++reinterpretHBy+    :: forall e eh ef ans a+     . (HFunctor e)+    => (a -> Eff eh ef ans)+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans+    -> Eff '[e] ef a+    -> Eff eh ef ans+reinterpretHBy ret elb = iterAllEffHFBy ret (elb . extractH) (flip sendUnionBy)+{-# INLINE reinterpretHBy #-}++reinterpretNHBy+    :: forall n e eh ef ans a+     . (HFunctor e, WeakenN n '[] eh)+    => (a -> Eff eh ef ans)+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans+    -> Eff '[e] ef a+    -> Eff eh ef ans+reinterpretNHBy = reinterpretHBy+{-# INLINE reinterpretNHBy #-}++reinterpretRecHWith+    :: forall e eh eh' ef a+     . (HFunctor e, eh `IsSuffixOf` eh')+    => (forall ans. Elaborator e (Eff eh' ef) ans)+    -> Eff (e ': eh) ef a+    -> Eff eh' ef a+reinterpretRecHWith elb = loop+  where+    loop :: Eff (e ': eh) ef ~> Eff eh' ef+    loop =+        iterAllEffHFBy+            pure+            (elb . hfmap loop !!+ flip sendUnionHBy . weakensH . hfmapUnion loop)+            (flip sendUnionBy)+{-# INLINE reinterpretRecHWith #-}++reinterpretRecNHWith+    :: forall n e eh eh' ef a+     . (HFunctor e, WeakenN n eh eh')+    => (forall ans. Elaborator e (Eff eh' ef) ans)+    -> Eff (e ': eh) ef a+    -> Eff eh' ef a+reinterpretRecNHWith elb = loop+  where+    loop :: Eff (e ': eh) ef ~> Eff eh' ef+    loop =+        iterAllEffHFBy+            pure+            (elb . hfmap loop !!+ flip sendUnionHBy . weakenNH @n . hfmapUnion loop)+            (flip sendUnionBy)+{-# INLINE reinterpretRecNHWith #-}++-- * Interposition functions++-- ** For first-order effects++{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided natural transformation style handler.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interpose+    :: forall e ef eh+     . (e <| ef)+    => (e ~> Eff eh ef)+    -- ^ Effect handler+    -> Eff eh ef ~> Eff eh ef+interpose f = interposeRecWith (stateless f)+{-# INLINE interpose #-}++{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided continuational stateful handler.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interposeWith+    :: forall e ef a+     . (e <| ef)+    => Interpreter e (Eff '[] ef) a+    -- ^ Effect handler+    -> Eff '[] ef a+    -> Eff '[] ef a+interposeWith = interposeBy pure+{-# INLINE interposeWith #-}++{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided value handler and continuational stateful handler.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interposeBy+    :: forall e ef ans a+     . (e <| ef)+    => (a -> Eff '[] ef ans)+    -- ^ Value handler+    -> Interpreter e (Eff '[] ef) ans+    -- ^ Effect handler+    -> Eff '[] ef a+    -> Eff '[] ef ans+interposeBy ret f = iterAllEffHFBy ret nilH \u -> maybe (`sendUnionBy` u) f (prj @e u)+{-# INLINE interposeBy #-}++{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided continuational stateful handler.++Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.+Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interposeRecWith+    :: forall e ef eh a+     . (e <| ef)+    => (forall ans. Interpreter e (Eff eh ef) ans)+    -- ^ Effect handler+    -> Eff eh ef a+    -> Eff eh ef a+interposeRecWith f = loop+  where+    loop :: Eff eh ef ~> Eff eh ef+    loop = iterAllEffHFBy+        pure+        (flip sendUnionHBy . hfmapUnion loop)+        \u -> maybe (`sendUnionBy` u) f (prj @e u)+{-# INLINE interposeRecWith #-}++-- ** For higher-order effects++{- | Reinterprets (hooks) the higher-order effect @e@ in the list using the provided natural transformation style elaborator.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interposeH+    :: forall e eh ef+     . (e <<| eh, HFunctor e)+    => e ~~> Eff eh ef+    -- ^ Effect elaborator+    -> Eff eh ef ~> Eff eh ef+interposeH f = interposeRecHWith (stateless f)+{-# INLINE interposeH #-}++{- | Reinterprets (hooks) the higher-order effect @e@ in the list using the provided continuational stateful elaborator.++Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.+Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.++If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.+-}+interposeRecHWith+    :: forall e eh ef a+     . (e <<| eh, HFunctor e)+    => (forall ans. Elaborator e (Eff eh ef) ans)+    -- ^ Effect elaborator+    -> Eff eh ef a+    -> Eff eh ef a+interposeRecHWith f = loop+  where+    loop :: Eff eh ef ~> Eff eh ef+    loop =+        iterAllEffHFBy+            pure+            (hfmapUnion loop >>> \u -> maybe (`sendUnionHBy` u) f (prjH @e u))+            (flip sendUnionBy)+{-# INLINE interposeRecHWith #-}++-- * Transformation to monads++-- | Traverses a computation containing only a single first-order effect @e@ using the provided value handler and continuational stateful handler, transforming it into a monad @m@.+iterEffBy+    :: forall e m ans a+     . (Monad m)+    => (a -> m ans)+    -- ^ Value handler+    -> Interpreter e m ans+    -- ^ Effect handler+    -> Eff '[] '[e] a+    -> m ans+iterEffBy ret hdl = iterAllEffHFBy ret nilH (hdl . extract)+{-# INLINE iterEffBy #-}++-- | Traverses a computation containing only a single higher-order effect @e@ using the provided value handler and continuational stateful elaborator, transforming it into a monad @m@.+iterEffHBy+    :: forall e m ans a+     . (Monad m, HFunctor e)+    => (a -> m ans)+    -- ^ Value handler+    -> Interpreter (e (Eff '[e] '[])) m ans+    -- ^ Effect handler+    -> Eff '[e] '[] a+    -> m ans+iterEffHBy ret elb = iterAllEffHFBy ret (elb . extractH) nil+{-# INLINE iterEffHBy #-}++{- | Traverses a computation containing only a single higher-order effect @e@ using the provided natural transformation elaborator, transforming it into a monad @m@.++Traversal is performed recursively with respect to the scope of the higher-order effect @e@.+Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.+-}+iterEffRecH+    :: forall e m+     . (Monad m, HFunctor e)+    => e ~~> m+    -- ^ Effect elaborator+    -> Eff '[e] '[] ~> m+iterEffRecH elb = iterEffRecHWith $ stateless elb+{-# INLINE iterEffRecH #-}++{- | Traverses a computation containing only a single higher-order effect @e@ using the provided continuational stateful elaborator, transforming it into a monad @m@.++Traversal is performed recursively with respect to the scope of the higher-order effect @e@.+Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.+-}+iterEffRecHWith+    :: forall e m+     . (Monad m, HFunctor e)+    => (forall ans. Elaborator e m ans)+    -- ^ Effect elaborator+    -> Eff '[e] '[] ~> m+iterEffRecHWith elb = loop+  where+    loop :: Eff '[e] '[] ~> m+    loop = iterEffHBy pure (elb . hfmap loop)+{-# INLINE iterEffRecHWith #-}++{- | Traverses a computation containing only higher-order effects @eh@ and first-order effects @ef@ using the provided continuational stateful elaborator, transforming it into a monad @m@.++Traversal is performed recursively with respect to the scopes of higher-order effects.+Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.+-}+iterEffRecHFWith+    :: forall eh ef m+     . (Monad m, HFunctor eh)+    => (forall ans. Elaborator eh m ans)+    -- ^ Effect elaborator+    -> (forall ans. Interpreter ef m ans)+    -- ^ Effect handler+    -> Eff '[eh] '[ef] ~> m+iterEffRecHFWith fh ff = loop+  where+    loop :: Eff '[eh] '[ef] ~> m+    loop = iterEffHFBy pure (fh . hfmap loop) ff+{-# INLINE iterEffRecHFWith #-}++{- | Traverses a computation containing only higher-order effects @eh@ and first-order effects @ef@ using the provided value handler,+continuational stateful elaborator, and handler, transforming it into a monad @m@.+-}+iterEffHFBy+    :: forall eh ef m ans a+     . (Monad m, HFunctor eh)+    => (a -> m ans)+    -- ^ Value handler+    -> Interpreter (eh (Eff '[eh] '[ef])) m ans+    -- ^ Effect elaborator+    -> Interpreter ef m ans+    -- ^ Effect handler+    -> Eff '[eh] '[ef] a+    -> m ans+iterEffHFBy ret elb hdl = iterAllEffHFBy ret (elb . extractH) (hdl . extract)+{-# INLINE iterEffHFBy #-}++-- | Traverses all effects using the provided value handler, continuational stateful elaborator, and handler, transforming them into a monad @m@.+iterAllEffHFBy+    :: forall eh ef m ans a+     . (Monad m)+    => (a -> m ans)+    -- ^ Value handler+    -> Interpreter (UnionH eh (Eff eh ef)) m ans+    -- ^ Effect elaborator+    -> Interpreter (Union ef) m ans+    -- ^ Effect handler+    -> Eff eh ef a+    -> m ans+iterAllEffHFBy ret fh ff = loop+  where+    loop = \case+        Val x -> ret x+        Op u q -> either fh ff u k+          where+            k = loop . qApp q+{-# INLINE iterAllEffHFBy #-}++-- * Utilities++-- | Lifts a natural transformation into a continuational stateful interpreter.+stateless :: forall e m ans. (Monad m) => (e ~> m) -> Interpreter e m ans+stateless i e k = i e >>= k+{-# INLINE stateless #-}++-- | Applies a value to a Kleisli arrow in 'FTCQueue' representation.+qApp :: FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b+qApp q' x = case tviewl q' of+    TOne k -> k x+    k :| t -> case k x of+        Val y -> qApp t y+        Op u q -> Op u (q >< t)

@@ -0,0 +1,119 @@+-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause++-- 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) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)+Maintainer  :  ymdfield@outlook.jp++This module provides an ad-hoc specialized version of+ "Control.Monad.Hefty.Interpret" to accelerate interpretations that have a+single state type @s@, especially for effects like t'Data.Effect.State.State' or+ [@Writer@]("Data.Effect.Writer").+-}+module Control.Monad.Hefty.Interpret.State where++import Control.Effect (type (~>))+import Control.Monad.Hefty.Interpret (qApp)+import Control.Monad.Hefty.Types (Eff (Op, Val), sendUnionBy, sendUnionHBy)+import Data.Effect.OpenUnion.Internal (IsSuffixOf)+import Data.Effect.OpenUnion.Internal.FO (Union, prj, weakens, (!+), type (<|))+import Data.Effect.OpenUnion.Internal.HO (UnionH, hfmapUnion, nilH)+import Data.Kind (Type)++-- | An ad-hoc stateful version of t'Control.Monad.Hefty.Types.Interpreter' for performance.+type StateInterpreter s e m (ans :: Type) = forall x. e x -> s -> (s -> x -> m ans) -> m ans++-- | An ad-hoc stateful version of t'Control.Monad.Hefty.Types.Elaborator' for performance.+type StateElaborator s e m ans = StateInterpreter s (e m) m ans++-- * Interpretation functions++interpretStateBy+    :: forall s e ef ans a+     . s+    -> (s -> a -> Eff '[] ef ans)+    -> StateInterpreter s e (Eff '[] ef) ans+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef ans+interpretStateBy = reinterpretStateBy+{-# INLINE interpretStateBy #-}++reinterpretStateBy+    :: forall s e ef' ef ans a+     . (ef `IsSuffixOf` ef')+    => s+    -> (s -> a -> Eff '[] ef' ans)+    -> StateInterpreter s e (Eff '[] ef') ans+    -> Eff '[] (e ': ef) a+    -> Eff '[] ef' ans+reinterpretStateBy s0 ret hdl =+    iterStateAllEffHFBy s0 ret nilH (hdl !+ \u s k -> sendUnionBy (k s) (weakens u))+{-# INLINE reinterpretStateBy #-}++interpretStateRecWith+    :: forall s e ef eh a+     . s+    -> (forall ans. StateInterpreter s e (Eff eh ef) ans)+    -> Eff eh (e ': ef) a+    -> Eff eh ef a+interpretStateRecWith = reinterpretStateRecWith+{-# INLINE interpretStateRecWith #-}++reinterpretStateRecWith+    :: forall s e ef' ef eh a+     . (ef `IsSuffixOf` ef')+    => s+    -> (forall ans. StateInterpreter s e (Eff eh ef') ans)+    -> Eff eh (e ': ef) a+    -> Eff eh ef' a+reinterpretStateRecWith s0 hdl = loop s0+  where+    loop :: s -> Eff eh (e ': ef) ~> Eff eh ef'+    loop s =+        iterStateAllEffHFBy+            s+            (const pure)+            (\u s' k -> sendUnionHBy (k s') $ hfmapUnion (loop s') u)+            (hdl !+ \u s' k -> sendUnionBy (k s') (weakens u))+{-# INLINE reinterpretStateRecWith #-}++-- * Interposition functions++interposeStateBy+    :: forall s e ef ans a+     . (e <| ef)+    => s+    -> (s -> a -> Eff '[] ef ans)+    -> StateInterpreter s e (Eff '[] ef) ans+    -> Eff '[] ef a+    -> Eff '[] ef ans+interposeStateBy s0 ret f =+    iterStateAllEffHFBy s0 ret nilH \u s k ->+        maybe (sendUnionBy (k s) u) (\e -> f e s k) (prj @e u)+{-# INLINE interposeStateBy #-}++-- * Transformation to monads++iterStateAllEffHFBy+    :: forall s eh ef m ans a+     . (Monad m)+    => s+    -> (s -> a -> m ans)+    -> StateInterpreter s (UnionH eh (Eff eh ef)) m ans+    -> StateInterpreter s (Union ef) m ans+    -> Eff eh ef a+    -> m ans+iterStateAllEffHFBy s0 ret fh ff = loop s0+  where+    loop s = \case+        Val x -> ret s x+        Op u q -> either (`fh` s) (`ff` s) u k+          where+            k s' = loop s' . qApp q+{-# INLINE iterStateAllEffHFBy #-}++-- TODO: add other pattern functions.

@@ -0,0 +1,616 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file)+Maintainer  :  ymdfield@outlook.jp++This module provides functions for transforming effects.+Please refer to the documentation of the [top-level module]("Control.Monad.Hefty").+-}+module Control.Monad.Hefty.Transform where++import Control.Effect (type (~>))+import Control.Monad.Hefty.Interpret (iterAllEffHFBy)+import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)+import Data.Effect.HFunctor (HFunctor)+import Data.Effect.Key (Key (Key, unKey), KeyH (KeyH, unKeyH), type (##>), type (#>))+import Data.Effect.OpenUnion.Internal (+    BundleUnder,+    Drop,+    IsSuffixOf,+    Split,+    Strengthen,+    StrengthenN,+    StrengthenNUnder,+    StrengthenUnder,+    Take,+    WeakenN,+    WeakenNUnder,+    WeakenUnder,+ )+import Data.Effect.OpenUnion.Internal.FO (+    Union,+    bundleAllUnion,+    bundleUnion,+    bundleUnionN,+    bundleUnionUnder,+    decomp,+    inj,+    prj,+    strengthen,+    strengthenN,+    strengthenNUnder,+    strengthenUnder,+    strengthens,+    strengthensUnder,+    unbundleAllUnion,+    unbundleUnion,+    unbundleUnionN,+    unbundleUnionUnder,+    weaken,+    weakenN,+    weakenNUnder,+    weakenUnder,+    weakens,+    weakensUnder,+    type (<|),+ )+import Data.Effect.OpenUnion.Internal.HO (+    UnionH,+    bundleAllUnionH,+    bundleUnionH,+    bundleUnionUnderH,+    decompH,+    hfmapUnion,+    injH,+    prjH,+    strengthenH,+    strengthenNH,+    strengthenNUnderH,+    strengthenUnderH,+    strengthensH,+    unbundleAllUnionH,+    unbundleUnionH,+    unbundleUnionUnderH,+    weakenH,+    weakenNH,+    weakenNUnderH,+    weakenUnderH,+    weakensH,+    type (<<|),+ )+import Data.Effect.Tag (Tag (Tag, unTag), TagH (TagH, unTagH), type (#), type (##))+import GHC.TypeNats (KnownNat)++-- * Rewriting effectful operations++{- | Transforms the first-order effect @e@ at the head of the list into another+first-order effect @e'@.+-}+transform+    :: forall e e' ef eh+     . (e ~> e')+    -> Eff eh (e ': ef) ~> Eff eh (e' ': ef)+transform f = transEff (either weaken (inj . f) . decomp)+{-# INLINE transform #-}++{- | Transforms the higher-order effect @e@ at the head of the list into another+higher-order effect @e'@.+-}+transformH+    :: forall e e' eh ef+     . (HFunctor e)+    => (e (Eff (e' ': eh) ef) ~> e' (Eff (e' ': eh) ef))+    -> Eff (e ': eh) ef ~> Eff (e' ': eh) ef+transformH f = transEffH (either weakenH (injH . f) . decompH)+{-# INLINE transformH #-}++{- | Transforms the first-order effect @e@ at the head of the list into another+first-order effect @e'@ and embeds it into the list.++If multiple instances of @e'@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+translate+    :: forall e e' ef eh+     . (e' <| ef)+    => (e ~> e')+    -> Eff eh (e ': ef) ~> Eff eh ef+translate f = transEff (either id (inj . f) . decomp)+{-# INLINE translate #-}++{- | Transforms the higher-order effect @e@ at the head of the list into another+higher-order effect @e'@ and embeds it into the list.++If multiple instances of @e'@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+translateH+    :: forall e e' eh ef+     . (e' <<| eh, HFunctor e)+    => (e (Eff eh ef) ~> e' (Eff eh ef))+    -> Eff (e ': eh) ef ~> Eff eh ef+translateH f = transEffH (either id (injH . f) . decompH)+{-# INLINE translateH #-}++{- | Rewrites the first-order effect @e@ in the list.++If multiple instances of @e@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+rewrite+    :: forall e ef eh+     . (e <| ef)+    => (e ~> e)+    -> Eff eh ef ~> Eff eh ef+rewrite f = transEff \u -> maybe u (inj . f) $ prj @e u+{-# INLINE rewrite #-}++{- | Rewrites the higher-order effect @e@ in the list.++If multiple instances of @e@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+rewriteH+    :: forall e eh ef+     . (e <<| eh, HFunctor e)+    => (e (Eff eh ef) ~> e (Eff eh ef))+    -> Eff eh ef ~> Eff eh ef+rewriteH f = transEffH \u -> maybe u (injH . f) $ prjH @e u+{-# INLINE rewriteH #-}++-- | Transforms all first-order effects in the open union at once.+transEff+    :: forall ef ef' eh+     . (Union ef ~> Union ef')+    -> Eff eh ef ~> Eff eh ef'+transEff = transEffHF id+{-# INLINE transEff #-}++-- | Transforms all higher-order effects in the open union at once.+transEffH+    :: forall eh eh' ef+     . (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))+    -> Eff eh ef ~> Eff eh' ef+transEffH f = transEffHF f id+{-# INLINE transEffH #-}++{- | Transforms all higher-order and first-order effects in the open union at+once.+-}+transEffHF+    :: forall eh eh' ef ef'+     . (UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))+    -> (Union ef ~> Union ef')+    -> Eff eh ef ~> Eff eh' ef'+transEffHF fh ff = loop+  where+    loop :: Eff eh ef ~> Eff eh' ef'+    loop =+        iterAllEffHFBy+            pure+            (flip sendUnionHBy . fh . hfmapUnion loop)+            (flip sendUnionBy . ff)+{-# INLINE transEffHF #-}++-- * Manipulating the effect list (without rewriting effectful operations)++-- ** Insertion functions++-- | Adds an arbitrary first-order effect @e@ to the head of the list.+raise :: forall e ef eh. Eff eh ef ~> Eff eh (e ': ef)+raise = transEff weaken+{-# INLINE raise #-}++-- | Adds multiple arbitrary first-order effects to the head of the list.+raises :: (ef `IsSuffixOf` ef') => Eff eh ef ~> Eff eh ef'+raises = transEff weakens+{-# INLINE raises #-}++{- | Adds a specified number @len@ of arbitrary first-order effects to the head+of the list.+-}+raiseN+    :: forall len ef ef' eh+     . (WeakenN len ef ef')+    => Eff eh ef ~> Eff eh ef'+raiseN = transEff (weakenN @len)+{-# INLINE raiseN #-}++{- | Inserts an arbitrary first-order effect @e2@ just below the head of the+list.+-}+raiseUnder+    :: forall e1 e2 ef eh+     . Eff eh (e1 ': ef) ~> Eff eh (e1 ': e2 ': ef)+raiseUnder = transEff weakenUnder+{-# INLINE raiseUnder #-}++{- | Inserts multiple arbitrary first-order effects at a position @offset@ steps+below the head of the list.+-}+raisesUnder+    :: forall offset ef ef' eh+     . (WeakenUnder offset ef ef')+    => Eff eh ef ~> Eff eh ef'+raisesUnder = transEff (weakensUnder @offset)+{-# INLINE raisesUnder #-}++{- | Inserts @len@ arbitrary first-order effects at a position @offset@ steps+below the head of the list.+-}+raiseNUnder+    :: forall len offset ef ef' eh+     . (WeakenNUnder len offset ef ef')+    => Eff eh ef ~> Eff eh ef'+raiseNUnder = transEff (weakenNUnder @len @offset)+{-# INLINE raiseNUnder #-}++{- | Adds a specified number @len@ of arbitrary higher-order effects to the head+of the list.+-}+raiseH :: forall e eh ef. Eff eh ef ~> Eff (e ': eh) ef+raiseH = transEffH weakenH+{-# INLINE raiseH #-}++{- | Inserts an arbitrary higher-order effect @e2@ just below the head of the+list.+-}+raisesH :: (eh `IsSuffixOf` eh') => Eff eh ef ~> Eff eh' ef+raisesH = transEffH weakensH+{-# INLINE raisesH #-}++{- | Adds a specified number @len@ of arbitrary higher-order effects to the head+of the list.+-}+raiseNH+    :: forall len eh eh' ef+     . (WeakenN len eh eh')+    => Eff eh ef ~> Eff eh' ef+raiseNH = transEffH (weakenNH @len)+{-# INLINE raiseNH #-}++{- | Inserts an arbitrary higher-order effect @e2@ just below the head of the+list.+-}+raiseUnderH+    :: forall e1 e2 eh ef+     . Eff (e1 ': eh) ef ~> Eff (e1 ': e2 ': eh) ef+raiseUnderH = transEffH weakenUnderH+{-# INLINE raiseUnderH #-}++{- | Inserts @len@ arbitrary higher-order effects at a position @offset@ steps+below the head of the list.+-}+raiseNUnderH+    :: forall len offset eh eh' ef+     . (WeakenNUnder len offset eh eh')+    => Eff eh ef ~> Eff eh' ef+raiseNUnderH = transEffH (weakenNUnderH @len @offset)+{-# INLINE raiseNUnderH #-}++-- ** Merging functions++{- | Merges the first first-order effect @e@ at the head of the list into the+same type of effect @e@ that is below it.++If multiple candidates of @e@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+subsume+    :: forall e ef eh+     . (e <| ef)+    => Eff eh (e ': ef) ~> Eff eh ef+subsume = transEff strengthen+{-# INLINE subsume #-}++{- | Merges multiple first-order effects at the head of the list into effects of+the same types that are below them.+-}+subsumes+    :: forall ef ef' eh+     . (Strengthen ef ef')+    => Eff eh ef ~> Eff eh ef'+subsumes = transEff strengthens+{-# INLINE subsumes #-}++{- | Merges a specified number @len@ of first-order effects at the head of the+list into effects of the same types that are below them.+-}+subsumeN+    :: forall len ef ef' eh+     . (StrengthenN len ef ef')+    => Eff eh ef ~> Eff eh ef'+subsumeN = transEff (strengthenN @len)+{-# INLINE subsumeN #-}++{- | Merges the first-order effect @e2@ located just below the head into the+same type of effect @e2@ that is below it.+-}+subsumeUnder+    :: forall e2 e1 ef eh+     . (e2 <| ef)+    => Eff eh (e1 ': e2 ': ef) ~> Eff eh (e1 ': ef)+subsumeUnder = transEff strengthenUnder+{-# INLINE subsumeUnder #-}++{- | Merges multiple first-order effects at an @offset@ below the head into+effects of the same types that are below them.+-}+subsumesUnder+    :: forall offset ef ef' eh+     . (StrengthenUnder offset ef ef')+    => Eff eh ef ~> Eff eh ef'+subsumesUnder = transEff (strengthensUnder @offset)+{-# INLINE subsumesUnder #-}++{- | Merges @len@ first-order effects at an @offset@ below the head into effects+of the same types that are below them.+-}+subsumeNUnder+    :: forall len offset ef ef' eh+     . (StrengthenNUnder len offset ef ef')+    => Eff eh ef ~> Eff eh ef'+subsumeNUnder = transEff (strengthenNUnder @len @offset)+{-# INLINE subsumeNUnder #-}++{- | Merges the first higher-order effect @e@ at the head of the list into the+same type of effect @e@ that is below it.++If multiple candidates of @e@ exist in the list, the one closest to the head+(with the smallest index) will be targeted.+-}+subsumeH+    :: forall e eh ef+     . (e <<| eh)+    => Eff (e ': eh) ef ~> Eff eh ef+subsumeH = transEffH strengthenH+{-# INLINE subsumeH #-}++{- | Merges multiple higher-order effects at the head of the list into effects of+the same types that are below them.+-}+subsumesH+    :: forall eh eh' ef+     . (Strengthen eh eh')+    => Eff eh ef ~> Eff eh' ef+subsumesH = transEffH strengthensH+{-# INLINE subsumesH #-}++{- | Merges a specified number @len@ of higher-order effects at the head of the+list into effects of the same types that are below them.+-}+subsumeNH+    :: forall len eh eh' ef+     . (StrengthenN len eh eh')+    => Eff eh ef ~> Eff eh' ef+subsumeNH = transEffH (strengthenNH @len)+{-# INLINE subsumeNH #-}++{- | Merges the higher-order effect @e2@ located just below the head into the+same type of effect @e2@ that is below it.+-}+subsumeUnderH+    :: forall e2 e1 eh ef+     . (e2 <<| eh)+    => Eff (e1 ': e2 ': eh) ef ~> Eff (e1 ': eh) ef+subsumeUnderH = transEffH strengthenUnderH+{-# INLINE subsumeUnderH #-}++{- | Merges @len@ higher-order effects at an @offset@ below the head into effects+of the same types that are below them.+-}+subsumeNUnderH+    :: forall len offset eh eh' ef+     . (StrengthenNUnder len offset eh eh')+    => Eff eh ef ~> Eff eh' ef+subsumeNUnderH = transEffH (strengthenNUnderH @len @offset)+{-# INLINE subsumeNUnderH #-}++-- ** Bundling functions++{- | Bundles several effects at the head of the list into a single element using+an open union.+-}+bundle+    :: forall ef bundle rest eh+     . (Split ef bundle rest)+    => Eff eh ef ~> Eff eh (Union bundle ': rest)+bundle = transEff bundleUnion+{-# INLINE bundle #-}++{- | Bundles the first @len@ effects at the head of the list into a single+element using an open union.+-}+bundleN+    :: forall len ef eh+     . (KnownNat len)+    => Eff eh ef ~> Eff eh (Union (Take len ef) ': Drop len ef)+bundleN = transEff (bundleUnionN @len)+{-# INLINE bundleN #-}++-- | Expands effects that have been bundled into an open union.+unbundle+    :: forall ef bundle rest eh+     . (Split ef bundle rest)+    => Eff eh (Union bundle ': rest) ~> Eff eh ef+unbundle = transEff unbundleUnion+{-# INLINE unbundle #-}++-- | Expands the first @len@ effects that have been bundled into an open union.+unbundleN+    :: forall len ef eh+     . (KnownNat len)+    => Eff eh (Union (Take len ef) ': Drop len ef) ~> Eff eh ef+unbundleN = transEff (unbundleUnionN @len)+{-# INLINE unbundleN #-}++{- | Expands effects at an @offset@ below the head of the list into a single+element using an open union.+-}+bundleUnder+    :: forall offset bundle ef ef' eh+     . (BundleUnder Union offset ef ef' bundle)+    => Eff eh ef ~> Eff eh ef'+bundleUnder = transEff (bundleUnionUnder @offset)+{-# INLINE bundleUnder #-}++-- TODO: add *bundle*N(H) functions++{- | Expands effects that have been bundled into an open union at an @offset@+below the head of the list.+-}+unbundleUnder+    :: forall offset bundle ef ef' eh+     . (BundleUnder Union offset ef ef' bundle)+    => Eff eh ef' ~> Eff eh ef+unbundleUnder = transEff (unbundleUnionUnder @offset)+{-# INLINE unbundleUnder #-}++-- | Bundles all first-order effects into a single open union.+bundleAll :: Eff eh ef ~> Eff eh '[Union ef]+bundleAll = transEff bundleAllUnion+{-# INLINE bundleAll #-}++-- | Expands all first-order effects from a single open union.+unbundleAll :: Eff eh '[Union ef] ~> Eff eh ef+unbundleAll = transEff unbundleAllUnion+{-# INLINE unbundleAll #-}++{- | Bundles several effects at the head of the list into a single element using+an open union.+-}+bundleH+    :: forall eh bundle rest ef+     . (Split eh bundle rest)+    => Eff eh ef ~> Eff (UnionH bundle ': rest) ef+bundleH = transEffH bundleUnionH+{-# INLINE bundleH #-}++-- | Expands effects that have been bundled into an open union.+unbundleH+    :: forall eh bundle rest ef+     . (Split eh bundle rest)+    => Eff (UnionH bundle ': rest) ef ~> Eff eh ef+unbundleH = transEffH unbundleUnionH+{-# INLINE unbundleH #-}++{- | Expands effects at an @offset@ below the head of the list into a single+element using an open union.+-}+bundleUnderH+    :: forall offset bundle eh eh' ef+     . (BundleUnder UnionH offset eh eh' bundle)+    => Eff eh ef ~> Eff eh' ef+bundleUnderH = transEffH (bundleUnionUnderH @offset)+{-# INLINE bundleUnderH #-}++{- | Expands effects that have been bundled into an open union at an @offset@+below the head of the list.+-}+unbundleUnderH+    :: forall offset bundle eh eh' ef+     . (BundleUnder UnionH offset eh eh' bundle)+    => Eff eh' ef ~> Eff eh ef+unbundleUnderH = transEffH (unbundleUnionUnderH @offset)+{-# INLINE unbundleUnderH #-}++-- | Bundles all higher-order effects into a single open union.+bundleAllH :: Eff eh ef ~> Eff '[UnionH eh] ef+bundleAllH = transEffH bundleAllUnionH+{-# INLINE bundleAllH #-}++-- | Expands all higher-order effects from a single open union.+unbundleAllH :: Eff '[UnionH eh] ef ~> Eff eh ef+unbundleAllH = transEffH unbundleAllUnionH+{-# INLINE unbundleAllH #-}++-- ** Manipulating Tags & Keys++-- | Attaches the @tag@ to the first-order effect at the head of the list.+tag+    :: forall tag e ef eh+     . Eff eh (e ': ef) ~> Eff eh (e # tag ': ef)+tag = transform Tag+{-# INLINE tag #-}++-- | Removes the @tag@ from the tagged first-order effect at the head of the list.+untag+    :: forall tag e ef eh+     . Eff eh (e # tag ': ef) ~> Eff eh (e ': ef)+untag = transform unTag+{-# INLINE untag #-}++{- | Changes the @tag@ of the tagged first-order effect at the head of the list+to another tag @tag'@.+-}+retag+    :: forall tag' tag e ef eh+     . Eff eh (e # tag ': ef) ~> Eff eh (e # tag' ': ef)+retag = transform $ Tag . unTag+{-# INLINE retag #-}++-- | Attaches the @tag@ to the higher-order effect at the head of the list.+tagH+    :: forall tag e ef eh+     . (HFunctor e)+    => Eff (e ': eh) ef ~> Eff (e ## tag ': eh) ef+tagH = transformH TagH+{-# INLINE tagH #-}++{- | Removes the @tag@ from the tagged higher-order effect at the head of the+ list.+-}+untagH+    :: forall tag e eh ef+     . (HFunctor e)+    => Eff (e ## tag ': eh) ef ~> Eff (e ': eh) ef+untagH = transformH unTagH+{-# INLINE untagH #-}++{- | Changes the @tag@ of the tagged higher-order effect at the head of the list+to another tag @tag'@.+-}+retagH+    :: forall tag' tag e eh ef+     . (HFunctor e)+    => Eff (e ## tag ': eh) ef ~> Eff (e ## tag' ': eh) ef+retagH = transformH $ TagH . unTagH+{-# INLINE retagH #-}++-- | Removes the @key@ from the keyed first-order effect at the head of the list.+unkey+    :: forall key e ef eh+     . Eff eh (key #> e ': ef) ~> Eff eh (e ': ef)+unkey = transform unKey+{-# INLINE unkey #-}++{- | Changes the @key@ of the keyed first-order effect at the head of the list+to another key @key'@.+-}+rekey+    :: forall key' key e ef eh+     . Eff eh (key #> e ': ef) ~> Eff eh (key' #> e ': ef)+rekey = transform $ Key . unKey+{-# INLINE rekey #-}++-- | Removes the @key@ from the keyed higher-order effect at the head of the list.+unkeyH+    :: forall key e eh ef+     . (HFunctor e)+    => Eff (key ##> e ': eh) ef ~> Eff (e ': eh) ef+unkeyH = transformH unKeyH+{-# INLINE unkeyH #-}++{- | Changes the @key@ of the keyed higher-order effect at the head of the list+to another key @key'@.+-}+rekeyH+    :: forall key' key e eh ef+     . (HFunctor e)+    => Eff (key ##> e ': eh) ef ~> Eff (key' ##> e ': eh) ef+rekeyH = transformH $ KeyH . unKeyH+{-# INLINE rekeyH #-}

@@ -0,0 +1,292 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file)+Maintainer  :  ymdfield@outlook.jp++This module defines the t'Eff' monad and related fundamental types and functions.+Please refer to the documentation of the [top-level module]("Control.Monad.Hefty").+-}+module Control.Monad.Hefty.Types where++import Control.Applicative (Alternative, empty, (<|>))+import Control.Effect (SendFOE, SendHOE, sendFOE, sendHOE, type (~>))+import Control.Effect.Key (ByKey (ByKey), SendFOEBy, SendHOEBy, key, sendFOEBy, sendHOEBy)+import Control.Monad (MonadPlus)+import Control.Monad.Error.Class (MonadError, catchError, throwError)+import Control.Monad.Fix (MonadFix, mfix)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.RWS (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.Except (Catch, Throw, catch'', throw'')+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.Key (Key (Key), KeyH (KeyH))+import Data.Effect.NonDet (ChooseH, Empty, chooseH)+import Data.Effect.NonDet qualified as E+import Data.Effect.OpenUnion.Internal (ElemAt)+import Data.Effect.OpenUnion.Internal.FO (MemberBy, Union, inj, inj0, injN, type (<|))+import Data.Effect.OpenUnion.Internal.HO (MemberHBy, UnionH, inj0H, injH, injNH, type (<<|))+import Data.Effect.OpenUnion.Sum (SumToRecUnionList)+import Data.Effect.Reader (Ask, Local, ask'', local'')+import Data.Effect.State (State, get'', put'')+import Data.Effect.Unlift (UnliftIO)+import Data.Effect.Unlift qualified as E+import Data.Effect.Writer (Tell, WriterH, listen'', tell'')+import Data.FTCQueue (FTCQueue, tsingleton, (|>))+import Data.Function ((&))+import Data.Kind (Type)+import Data.Tuple (swap)+import GHC.TypeNats (KnownNat)+import UnliftIO (MonadUnliftIO, withRunInIO)++{- | The 'Eff' monad represents computations with effects.+It supports higher-order effects @eh@ and first-order effects @ef@.+-}+data Eff eh ef a+    = -- | A pure value.+      Val a+    | -- | An effectful operation, which can be either a higher-order effect or a first-order effect.+      forall x. Op+        (Either (UnionH eh (Eff eh ef) x) (Union ef x))+        (FTCQueue (Eff eh ef) x a)+        -- ^ the continuation of the operation.++infixr 4 :!!++{- | Type-level infix operator for 'Eff'.+Allows writing @eh :!! ef@ instead of @Eff eh ef@.+-}+type (:!!) = Eff++infixr 5 !!++{- | An infix operator version of t`Eff` for sum notation.++Example:++@Span t'Control.Monad.Hefty.Types.!!' FileSystem t'Data.Effect.OpenUnion.Sum.+' Time t'Data.Effect.OpenUnion.Sum.+' Log t'Data.Effect.OpenUnion.Sum.+' t'IO' t'Control.Effect.~>' t'IO'@+-}+type eh !! ef = SumToRecUnionList UnionH eh :!! SumToRecUnionList Union ef++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 alias for an interpreter function.++@Interpreter e m ans@ transforms an effect @e@ into a computation in @m@ where the result type (answer type) is @ans@.+-}+type Interpreter e m (ans :: Type) = forall x. e x -> (x -> m ans) -> m ans++{- | Type alias for an elaborator function.++An 'Elaborator' is an interpreter for higher-order effects.+-}+type Elaborator e m ans = Interpreter (e m) m ans++infix 2 ~~>++-- | Type alias for a natural transformation style elaborator.+type e ~~> f = e f ~> f++-- | Send a first-order effect @e@ to the t`Eff` carrier.+send :: (e <| ef) => e ~> Eff eh ef+send = sendUnion . inj+{-# INLINE send #-}++-- | Send a higher-order effect @e@ to the t`Eff` carrier.+sendH :: (e <<| eh) => e (Eff eh ef) ~> Eff eh ef+sendH = sendUnionH . injH+{-# INLINE sendH #-}++-- | Send the first-order effect @e@ at the head of the list to the t`Eff` carrier.+send0 :: e ~> Eff eh (e ': ef)+send0 = sendUnion . inj0+{-# INLINE send0 #-}++-- | Send the higher-order effect @e@ at the head of the list to the t`Eff` carrier.+send0H :: e (Eff (e ': eh) ef) ~> Eff (e ': eh) ef+send0H = sendUnionH . inj0H+{-# INLINE send0H #-}++-- | Send the @i@-th first-order effect in the list to the t`Eff` carrier.+sendN :: forall i ef eh. (KnownNat i) => ElemAt i ef ~> Eff eh ef+sendN = sendUnion . injN @i+{-# INLINE sendN #-}++-- | Send the @i@-th higher-order effect in the list to the t`Eff` carrier.+sendNH :: forall i eh ef. (KnownNat i) => ElemAt i eh (Eff eh ef) ~> Eff eh ef+sendNH = sendUnionH . injNH @i+{-# INLINE sendNH #-}++-- | Send an open union of all first-order effects to the t`Eff` carrier.+sendUnion :: Union ef a -> Eff eh ef a+sendUnion = sendUnionBy pure+{-# INLINE sendUnion #-}++-- | Send an open union of all first-order effects, along with its continuation, to the t`Eff` carrier.+sendUnionBy :: (a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans+sendUnionBy k u = Op (Right u) (tsingleton k)+{-# INLINE sendUnionBy #-}++-- | Send an open union of all higher-order effects to the t`Eff` carrier.+sendUnionH :: UnionH eh (Eff eh ef) a -> Eff eh ef a+sendUnionH = sendUnionHBy pure+{-# INLINE sendUnionH #-}++-- | Send an open union of all higher-order effects, along with its continuation, to the t`Eff` carrier.+sendUnionHBy :: (a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans+sendUnionHBy k u = Op (Left u) (tsingleton k)+{-# INLINE sendUnionHBy #-}++instance Functor (Eff eh ef) where+    fmap f = \case+        Val x -> Val (f x)+        Op u q -> Op u (q |> (Val . f))+    {-# INLINE fmap #-}++instance Applicative (Eff eh ef) where+    pure = Val+    {-# INLINE pure #-}++    Val f <*> Val x = Val $ f x+    Val f <*> Op u q = Op u (q |> (Val . f))+    Op u q <*> m = Op u (q |> (<$> m))+    {-# INLINE (<*>) #-}++instance Monad (Eff eh ef) where+    m >>= k = case m of+        Val x -> k x+        Op e q -> Op e (q |> k)+    {-# INLINE (>>=) #-}++instance (e <| ef) => SendFOE e (Eff eh ef) where+    sendFOE = send+    {-# INLINE sendFOE #-}++instance (e <<| eh) => SendHOE e (Eff eh ef) where+    sendHOE = sendH+    {-# INLINE sendHOE #-}++instance (MemberBy key e ef) => SendFOEBy key e (Eff eh ef) where+    sendFOEBy = send . Key @key+    {-# INLINE sendFOEBy #-}++instance (MemberHBy key e eh) => SendHOEBy key e (Eff eh ef) where+    sendHOEBy = sendH . KeyH @key+    {-# INLINE sendHOEBy #-}++instance+    ( SendFOEBy ReaderKey (Ask r) (Eff eh ef)+    , SendHOEBy ReaderKey (Local r) (Eff eh ef)+    )+    => MonadReader r (Eff eh ef)+    where+    ask = ask'' @ReaderKey+    local = local'' @ReaderKey+    {-# INLINE ask #-}+    {-# INLINE local #-}++{- | A key to be attached to the effect targeted by the t`MonadReader` instance.++Since t`MonadReader` has a functional dependency on @r@, this is needed to uniquely specify @r@.+-}+data ReaderKey++instance+    ( SendFOEBy WriterKey (Tell w) (Eff eh ef)+    , SendHOEBy WriterKey (WriterH w) (Eff eh ef)+    , Monoid w+    )+    => MonadWriter w (Eff eh ef)+    where+    tell = tell'' @WriterKey+    listen = fmap swap . listen'' @WriterKey+    pass m = pass (ByKey m) & key @WriterKey+    {-# INLINE tell #-}+    {-# INLINE listen #-}++{- | A key to be attached to the effect targeted by the t'Control.Monad.Writer.Class.MonadWriter' instance.++Since t'Control.Monad.Writer.Class.MonadWriter' has a functional dependency on @w@, this is needed to uniquely specify @w@.+-}+data WriterKey++instance+    (SendFOEBy StateKey (State s) (Eff eh ef))+    => MonadState s (Eff eh ef)+    where+    get = get'' @StateKey+    put = put'' @StateKey+    {-# INLINE get #-}+    {-# INLINE put #-}++{- | A key to be attached to the effect targeted by the t`MonadState` instance.++Since t`MonadState` has a functional dependency on @s@, this is needed to uniquely specify @s@.+-}+data StateKey++instance+    ( SendFOEBy ErrorKey (Throw e) (Eff eh ef)+    , SendHOEBy ErrorKey (Catch e) (Eff eh ef)+    )+    => MonadError e (Eff eh ef)+    where+    throwError = throw'' @ErrorKey+    catchError = catch'' @ErrorKey+    {-# INLINE throwError #-}+    {-# INLINE catchError #-}++{- | A key to be attached to the effect targeted by the t`Control.Monad.Error.Class.MonadError` instance.++Since t`Control.Monad.Error.Class.MonadError` has a functional dependency on @e@, this is needed to uniquely specify @e@.+-}+data ErrorKey++instance+    ( SendFOEBy ReaderKey (Ask r) (Eff eh ef)+    , SendHOEBy ReaderKey (Local r) (Eff eh ef)+    , SendFOEBy WriterKey (Tell w) (Eff eh ef)+    , SendHOEBy WriterKey (WriterH w) (Eff eh ef)+    , SendFOEBy StateKey (State s) (Eff eh ef)+    , Monoid w+    )+    => MonadRWS r w s (Eff eh ef)++instance (Empty <| ef, ChooseH <<| eh) => Alternative (Eff eh ef) where+    empty = E.empty+    a <|> b = chooseH a b+    {-# INLINE empty #-}+    {-# INLINE (<|>) #-}++instance (Empty <| ef, ChooseH <<| eh) => MonadPlus (Eff eh ef)++instance (IO <| ef) => MonadIO (Eff eh ef) where+    liftIO = send+    {-# INLINE liftIO #-}++instance (Fail <| ef) => MonadFail (Eff eh ef) where+    fail = E.fail+    {-# INLINE fail #-}++instance (Fix <<| eh) => MonadFix (Eff eh ef) where+    mfix = E.mfix++instance (UnliftIO <<| eh, IO <| ef) => MonadUnliftIO (Eff eh ef) where+    withRunInIO = E.withRunInIO+    {-# INLINE withRunInIO #-}

@@ -0,0 +1,121 @@+-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file)+Maintainer  :  ymdfield@outlook.jp+-}+module Data.Effect.OpenUnion (+    module Data.Effect.OpenUnion.Internal,+    module Data.Effect.OpenUnion.Internal.HO,+    module Data.Effect.OpenUnion.Internal.FO,+    module Data.Effect.OpenUnion.Sum,+) where++import Data.Effect.OpenUnion.Internal (+    BundleUnder,+    Drop,+    ElemAt,+    IsSuffixOf,+    KnownLength,+    Length,+    Reverse,+    Split,+    Strengthen,+    StrengthenN,+    StrengthenNUnder,+    StrengthenUnder,+    Take,+    WeakenN,+    WeakenNUnder,+    WeakenUnder,+    type (++),+ )+import Data.Effect.OpenUnion.Internal.FO (+    Lookup,+    Member,+    MemberBy,+    Union,+    bundleAllUnion,+    bundleUnion,+    bundleUnionUnder,+    decomp,+    decomp0,+    extract,+    flipAllUnion,+    flipUnion,+    flipUnionUnder,+    inj,+    inj0,+    injN,+    nil,+    prefixUnion,+    prefixUnionUnder,+    prj,+    prjN,+    strengthen,+    strengthenN,+    strengthenNUnder,+    strengthenUnder,+    suffixUnion,+    suffixUnionOverN,+    unbundleAllUnion,+    unbundleUnion,+    unbundleUnionUnder,+    weaken,+    weakenN,+    weakenNUnder,+    weakenUnder,+    weakens,+    weakensUnder,+    (!+),+    type (<|),+ )+import Data.Effect.OpenUnion.Internal.HO (+    LookupH,+    MemberH,+    MemberHBy,+    UnionH,+    bundleAllUnionH,+    bundleUnionH,+    bundleUnionUnderH,+    decomp0H,+    decompH,+    extractH,+    flipAllUnionH,+    flipUnionH,+    flipUnionUnderH,+    hfmapUnion,+    inj0H,+    injH,+    injNH,+    nilH,+    prefixUnionH,+    prefixUnionUnderH,+    prjH,+    prjNH,+    strengthenNH,+    strengthenNUnderH,+    suffixUnionH,+    suffixUnionOverNH,+    unbundleAllUnionH,+    unbundleUnionH,+    unbundleUnionUnderH,+    weakenH,+    weakenNH,+    weakenNUnderH,+    weakenUnderH,+    weakensH,+    weakensUnderH,+    (!!+),+    type (<<|),+ )+import Data.Effect.OpenUnion.Sum (+    SumToRecUnion,+    SumToRecUnionList,+    U,+    UL,+    type (+),+ )++-- TODO: add move/swap/insert/rotate functions.

@@ -0,0 +1,187 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}++-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause++-- 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) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)+Maintainer  :  ymdfield@outlook.jp+Description :  Open unions (type-indexed co-products) for extensible effects.+-}+module Data.Effect.OpenUnion.Internal where++import Data.Proxy (Proxy (Proxy))+import Data.Type.Equality (type (==))+import GHC.TypeError (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), TypeError)+import GHC.TypeNats (KnownNat, natVal, type (+), type (-))++{- |+Represents position of element @e :: k@ in a type list @es :: [k]@.+-}+newtype P (e :: k) (es :: [k]) = P {unP :: Word}++type FindElem e es = KnownNat (ElemIndex e es)++elemNo :: forall e es. (FindElem e es) => P e es+elemNo = P $ wordVal @(ElemIndex e es)+{-# INLINE elemNo #-}++type family ElemIndex e es where+    ElemIndex e (e ': es) = 0+    ElemIndex e (_ ': es) = 1 + ElemIndex e es++type family ElemAt i es where+    ElemAt 0 (e ': _) = e+    ElemAt n (_ ': es) = ElemAt (n - 1) es++{- | Instance resolution for this class fails with a custom type error+if @e :: k@ is not in the list @w :: [k]@.+-}+class IfNotFound (e :: k) (r :: [k]) (w :: [k])++{- | If we reach an empty list, that’s a failure, since it means the type isn’t+in the list.+-}+instance+    ( TypeError+        ( 'Text "‘"+            ':<>: 'ShowType e+            ':<>: 'Text "’ is not a member of the type-level list"+            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"+        )+    )+    => IfNotFound e '[] w++instance IfNotFound e (e ': r) w+instance {-# OVERLAPPABLE #-} (IfNotFound e r w) => IfNotFound e (e' ': r) w++{- |+Pass if @r@ is uninstantiated. The incoherence here is safe, since picking+this instance doesn’t cause any variation in behavior, except possibly the+production of an inferior error message. For more information, see+lexi-lambda/freer-simple#3, which describes the motivation in more detail.+-}+instance {-# INCOHERENT #-} IfNotFound e r w++type LookupError (key :: kk) (w :: [ke]) =+    TypeError+        ( 'Text "The key ‘"+            ':<>: 'ShowType key+            ':<>: 'Text "’ does not exist in the type-level list"+            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"+        )++infixr 5 +++type family xs ++ ys where+    '[] ++ ys = ys+    (x ': xs) ++ ys = x ': (xs ++ ys)++wordVal :: forall n. (KnownNat n) => Word+wordVal = fromIntegral $ natVal @n Proxy+{-# INLINE wordVal #-}++class IsSuffixOf es es' where+    prefixLen :: Word++instance IsSuffixOf es es where+    prefixLen = 0++instance {-# INCOHERENT #-} (IsSuffixOf es es') => IsSuffixOf es (e ': es') where+    prefixLen = prefixLen @es @es' + 1++type family Length es where+    Length '[] = 0+    Length (e ': es) = 1 + Length es++class (KnownNat (Length es)) => KnownLength es+instance (KnownNat (Length es)) => KnownLength es++reifyLength :: forall es. (KnownLength es) => Word+reifyLength = wordVal @(Length es)+{-# INLINE reifyLength #-}++type family PrefixLength es es' where+    PrefixLength es es = 0+    PrefixLength es (e ': es') = 1 + PrefixLength es es'++-- fixme: Use type class with functional dependencies instaed of type family for readable compile error and compile speed.++type WeakenN len es es' = (es ~ Drop len es', KnownNat len)++type WeakenUnder offset es es' =+    (WeakenNUnder (PrefixLength es es') offset es es', KnownNat (PrefixLength es es'))++type WeakenNUnder len offset es es' =+    (WeakenN len (Drop offset es) (Drop offset es'), KnownNat offset)++type Strengthen es es' =+    (StrengthenMap (PrefixLength es' es) es es', KnownNat (PrefixLength es' es))++type StrengthenN len es es' = (StrengthenMap len es es', KnownNat len)++type StrengthenUnder offset es es' =+    (StrengthenNUnder (PrefixLength es' es) offset es es')++type StrengthenNUnder len offset es es' =+    (StrengthenMap len (Drop offset es) (Drop offset es'), KnownNat len, KnownNat offset)++type StrengthenMap len es es' = (StrengthenMap_ (len == 0) len es es')++class+    (isLenZero ~ (len == 0)) =>+    StrengthenMap_ isLenZero len (es :: [k]) (es' :: [k])+    where+    strengthenMap :: Word -> Word++instance StrengthenMap_ 'True 0 es es where+    strengthenMap = id+    {-# INLINE strengthenMap #-}++instance+    (StrengthenMap (len - 1) es es', FindElem e es, (len == 0) ~ 'False)+    => StrengthenMap_ 'False len (e ': es) es'+    where+    strengthenMap = \case+        0 -> wordVal @(ElemIndex e es)+        n -> strengthenMap @_ @_ @(len - 1) @es @es' $ n - 1+    {-# INLINE strengthenMap #-}++strengthenMapUnder :: forall len offset es es'. (StrengthenNUnder len offset es es') => Word -> Word+strengthenMapUnder = strengthenMap @_ @_ @len @(Drop offset es) @(Drop offset es')+{-# INLINE strengthenMapUnder #-}++type BundleUnder u offset es es' bundle =+    ( es' ~ Take offset es ++ (u bundle ': Drop (Length bundle) (Drop offset es))+    , es ~ Take offset es' ++ bundle ++ Drop 1 (Drop offset es')+    , bundle ~ Take (PrefixLength (Drop 1 (Drop offset es')) (Drop offset es)) (Drop offset es)+    , KnownLength bundle+    , KnownNat offset+    , Length bundle ~ PrefixLength (Drop 1 (Drop offset es')) (Drop offset es)+    )++type Split es init tail =+    ( es ~ init ++ tail+    , init ~ Take (PrefixLength tail es) es+    , tail ~ Drop (Length init) es+    , KnownLength init+    , Length init ~ PrefixLength tail es+    )++type family Take n es where+    Take 0 es = '[]+    Take n (e ': es) = e ': Take (n - 1) es++type family Drop n es where+    Drop 0 es = es+    Drop n (e ': es) = Drop (n - 1) es++type Reverse es = Reverse_ '[] es++type family Reverse_ acc es where+    Reverse_ acc '[] = acc+    Reverse_ acc (e ': es) = Reverse_ (e ': acc) es

@@ -0,0 +1,445 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}++-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause++-- 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) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)+Maintainer  :  ymdfield@outlook.jp+Description :  Open unions (type-indexed co-products) for extensible first-order effects.++Implementation of an open union for first-order effects.++Importing this module allows unsafe access to the data structure of the open+union, so it should not usually be imported directly.++Based on [the open union in freer-simple](https://hackage.haskell.org/package/freer-simple-1.2.1.2/docs/Data-OpenUnion-Internal.html).+-}+module Data.Effect.OpenUnion.Internal.FO where++import Data.Coerce (coerce)+import Data.Effect (EffectF)+import Data.Effect.Key (type (#>))+import Data.Effect.OpenUnion.Internal (+    BundleUnder,+    Drop,+    ElemAt,+    ElemIndex,+    FindElem,+    IfNotFound,+    IsSuffixOf,+    KnownLength,+    Length,+    LookupError,+    P (unP),+    PrefixLength,+    Reverse,+    Split,+    Strengthen,+    StrengthenN,+    StrengthenNUnder,+    StrengthenUnder,+    Take,+    WeakenN,+    WeakenNUnder,+    WeakenUnder,+    elemNo,+    prefixLen,+    reifyLength,+    strengthenMap,+    strengthenMapUnder,+    wordVal,+    type (++),+ )+import Data.Kind (Type)+import GHC.TypeNats (KnownNat, type (-))+import Unsafe.Coerce (unsafeCoerce)++-- | Open union for first-order effects.+data Union (es :: [EffectF]) (a :: Type) where+    Union+        :: {-# UNPACK #-} !Word+        -- ^ A natural number tag to identify the element of the union.+        -> e a+        -- ^ The data of the higher-order effect that is an element of the union.+        -> Union es a++{- | Takes a request of type @e :: 'EffectF'@, and injects it into the 'Union'.++Summand is assigning a specified 'Word' value, which is a position in the+type-list @(e ': es) :: 'EffectF'@.++__This function is unsafe.__++/O(1)/+-}+unsafeInj :: Word -> e a -> Union es a+unsafeInj = Union+{-# INLINE unsafeInj #-}++{- | Project a value of type @'Union' (e ': es) :: 'EffectF'@ into a possible+summand of the type @e :: 'EffectF'@. 'Nothing' means that @e :: 'EffectF'@ is not+the value stored in the @'Union' (e ': es) :: 'EffectF'@.++It is assumed that summand is stored in the 'Union' when the 'Word' value is+the same value as is stored in the 'Union'.++__This function is unsafe.__++/O(1)/+-}+unsafePrj :: Word -> Union es a -> Maybe (e a)+unsafePrj n (Union n' e)+    | n == n' = Just (unsafeCoerce e)+    | otherwise = Nothing+{-# INLINE unsafePrj #-}++{- | A constraint that requires that a particular effect, @e@, is a member of+the type-level list @es@. This is used to parameterize an+'Control.Monad.Hefty.Eff' computation over an arbitrary list of first-order effects, so+long as @e@ is /somewhere/ in the list.++For example, a computation that only needs access to a cell of mutable state+containing an 'Integer' would likely use the following type:++@+'Data.Effect.State.State' 'Integer' t'Data.Effect.OpenUnion.<|' ef => 'Control.Monad.Hefty.Eff' eh ef ()+@+-}+class (FindElem e es) => Member (e :: EffectF) es where+    -- This type class is used for two following purposes:+    --++    -- * As a @Constraint@ it guarantees that @e :: 'EffectF'@ is a member of a++    --   type-list @es :: ['EffectF']@.+    --++    -- * Provides a way how to inject\/project @e :: 'EffectF'@ into\/from a 'Union',++    --   respectively.+    --+    -- Following law has to hold:+    --+    -- @+    -- 'prj' . 'inj' === 'Just'+    -- @++    -- | Takes a request of type @e :: 'EffectF'@, and injects it into the+    -- 'Union'.+    --+    -- /O(1)/+    inj :: e a -> Union es a++    -- | Project a value of type @'Union' (e ': es) :: 'EffectF'@ into a possible+    -- summand of the type @e :: 'EffectF'@. 'Nothing' means that @e :: 'EffectF'@ is+    -- not the value stored in the @'Union' (e ': es) :: 'EffectF'@.+    --+    -- /O(1)/+    prj :: Union es a -> Maybe (e a)++instance (FindElem e es, IfNotFound e es es) => Member e es where+    inj = unsafeInj $ unP (elemNo :: P e es)+    {-# INLINE inj #-}++    prj = unsafePrj $ unP (elemNo :: P e es)+    {-# INLINE prj #-}++infix 3 <|+type (<|) = Member++type MemberBy key e es = (key #> e <| es, Lookup key es ~ key #> e)++type Lookup key es = Lookup_ key es es++type family Lookup_ (key :: k) r w :: EffectF where+    Lookup_ key (key #> e ': _) w = key #> e+    Lookup_ key (_ ': r) w = Lookup_ key r w+    Lookup_ key '[] w = LookupError key w++{- | Orthogonal decomposition of a @'Union' (e ': es) :: 'EffectF'@. 'Right' value+is returned if the @'Union' (e ': es) :: 'EffectF'@ contains @e :: 'EffectF'@, and+'Left' when it doesn't. Notice that 'Left' value contains+@'Union' es :: 'EffectF'@, i.e. it can not contain @e :: 'EffectF'@.++/O(1)/+-}+decomp :: Union (e ': es) a -> Either (Union es a) (e a)+decomp (Union 0 a) = Right $ unsafeCoerce a+decomp (Union n a) = Left $ Union (n - 1) a+{-# INLINE [2] decomp #-}++{- | Specialized version of 'decomp' for efficiency.++/O(1)/+-}++-- TODO: Check that it actually adds on efficiency.+decomp0 :: Union '[e] a -> Either (Union '[] a) (e a)+decomp0 (Union _ a) = Right $ unsafeCoerce a+{-# INLINE decomp0 #-}++{-# RULES "decomp/singleton" decomp = decomp0 #-}++infixr 5 !++(!+) :: (e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r+(f !+ g) u = case decomp u of+    Left x -> g x+    Right x -> f x+{-# INLINE (!+) #-}++{- | Specialised version of 'prj'\/'decomp' that works on an+@'Union' '[e] :: 'EffectF'@ which contains only one specific summand. Hence the+absence of 'Maybe', and 'Either'.++/O(1)/+-}+extract :: Union '[e] a -> e a+extract (Union _ a) = unsafeCoerce a+{-# INLINE extract #-}++inj0 :: forall e es a. e a -> Union (e ': es) a+inj0 = Union 0+{-# INLINE inj0 #-}++injN :: forall i es a. (KnownNat i) => ElemAt i es a -> Union es a+injN = Union (wordVal @i)+{-# INLINE injN #-}++prjN :: forall i es a. (KnownNat i) => Union es a -> Maybe (ElemAt i es a)+prjN (Union n a)+    | n == wordVal @i = Just $ unsafeCoerce a+    | otherwise = Nothing+{-# INLINE prjN #-}++{- | Inject whole @'Union' es@ into a weaker @'Union' (any ': es)@ that has one+more summand.++/O(1)/+-}+weaken :: forall any es a. Union es a -> Union (any ': es) a+weaken (Union n a) = Union (n + 1) a+{-# INLINE weaken #-}++weakens :: forall es es' a. (es `IsSuffixOf` es') => Union es a -> Union es' a+weakens (Union n a) = Union (n + prefixLen @es @es') a+{-# INLINE weakens #-}++weakenN :: forall len es es' a. (WeakenN len es es') => Union es a -> Union es' a+weakenN (Union n a) = Union (n + wordVal @len) a+{-# INLINE weakenN #-}++weakenUnder :: forall any e es a. Union (e ': es) a -> Union (e ': any ': es) a+weakenUnder u@(Union n a)+    | n == 0 = coerce u+    | otherwise = Union (n + 1) a+{-# INLINE weakenUnder #-}++weakensUnder :: forall offset es es' a. (WeakenUnder offset es es') => Union es a -> Union es' a+weakensUnder = weakenNUnder @(PrefixLength es es') @offset+{-# INLINE weakensUnder #-}++weakenNUnder+    :: forall len offset es es' a+     . (WeakenNUnder len offset es es')+    => Union es a+    -> Union es' a+weakenNUnder u@(Union n a)+    | n < wordVal @offset = coerce u+    | otherwise = Union (n + wordVal @len) a+{-# INLINE weakenNUnder #-}++strengthen :: forall e es a. (e <| es) => Union (e ': es) a -> Union es a+strengthen (Union n a)+    | n == 0 = Union (wordVal @(ElemIndex e es)) a+    | otherwise = Union (n - 1) a+{-# INLINE strengthen #-}++strengthens :: forall es es' a. (Strengthen es es') => Union es a -> Union es' a+strengthens = strengthenN @(PrefixLength es' es)+{-# INLINE strengthens #-}++strengthenN :: forall len es es' a. (StrengthenN len es es') => Union es a -> Union es' a+strengthenN (Union n a) = Union (strengthenMap @_ @_ @len @es @es' n) a+{-# INLINE strengthenN #-}++strengthenUnder :: forall e2 e1 es a. (e2 <| es) => Union (e1 ': e2 ': es) a -> Union (e1 ': es) a+strengthenUnder u@(Union n a)+    | n == 0 = coerce u+    | n == 1 = Union (1 + wordVal @(ElemIndex e2 es)) a+    | otherwise = Union (n - 1) a+{-# INLINE strengthenUnder #-}++strengthensUnder :: forall offset es es' a. (StrengthenUnder offset es es') => Union es a -> Union es' a+strengthensUnder = strengthenNUnder @(PrefixLength es' es) @offset+{-# INLINE strengthensUnder #-}++strengthenNUnder+    :: forall len offset es es' a+     . (StrengthenNUnder len offset es es')+    => Union es a+    -> Union es' a+strengthenNUnder u@(Union n a)+    | n < off = coerce u+    | otherwise = Union (off + strengthenMapUnder @len @offset @es @es' (n - off)) a+  where+    off = wordVal @offset+{-# INLINE strengthenNUnder #-}++bundleUnion+    :: forall es bundle rest a+     . (Split es bundle rest)+    => Union es a+    -> Union (Union bundle ': rest) a+bundleUnion = bundleUnionN @(Length bundle)++bundleUnionN+    :: forall len es a+     . (KnownNat len)+    => Union es a+    -> Union (Union (Take len es) ': Drop len es) a+bundleUnionN (Union n a)+    | n < len = Union 0 $ Union n a+    | otherwise = Union (n - len + 1) a+  where+    len = wordVal @len+{-# INLINE bundleUnionN #-}++unbundleUnion+    :: forall es bundle rest a+     . (Split es bundle rest)+    => Union (Union bundle ': rest) a+    -> Union es a+unbundleUnion = unbundleUnionN @(Length bundle)+{-# INLINE unbundleUnion #-}++unbundleUnionN+    :: forall len es a+     . (KnownNat len)+    => Union (Union (Take len es) ': Drop len es) a+    -> Union es a+unbundleUnionN (Union n a)+    | n == 0 = unsafeCoerce a+    | otherwise = Union (n - 1 + wordVal @len) a+{-# INLINE unbundleUnionN #-}++bundleUnionUnder+    :: forall offset bundle es es' a+     . (BundleUnder Union offset es es' bundle)+    => Union es a+    -> Union es' a+bundleUnionUnder = bundleUnionNUnder @(Length bundle) @offset+{-# INLINE bundleUnionUnder #-}++bundleUnionNUnder+    :: forall len offset es a+     . (KnownNat len, KnownNat offset)+    => Union es a+    -> Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a+bundleUnionNUnder u@(Union n a)+    | n < off = coerce u+    | n' < len = Union 0 $ Union n' a+    | otherwise = Union (n - len + 1) a+  where+    off = wordVal @offset+    len = wordVal @len+    n' = n - off+{-# INLINE bundleUnionNUnder #-}++unbundleUnionUnder+    :: forall offset bundle es es' a+     . (BundleUnder Union offset es es' bundle)+    => Union es' a+    -> Union es a+unbundleUnionUnder = unbundleUnionNUnder @(Length bundle) @offset+{-# INLINE unbundleUnionUnder #-}++unbundleUnionNUnder+    :: forall len offset es a+     . (KnownNat len, KnownNat offset)+    => Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a+    -> Union es a+unbundleUnionNUnder u@(Union n a)+    | n < off = coerce u+    | n == off =+        case unsafeCoerce a of+            Union n' a' -> Union (off + n') a'+    | otherwise = Union (n - 1 + len) a+  where+    off = wordVal @offset+    len = wordVal @len+{-# INLINE unbundleUnionNUnder #-}++bundleAllUnion :: Union es a -> Union '[Union es] a+bundleAllUnion = Union 0+{-# INLINE bundleAllUnion #-}++unbundleAllUnion :: Union '[Union es] a -> Union es a+unbundleAllUnion = extract+{-# INLINE unbundleAllUnion #-}++prefixUnion :: forall any es a. (KnownLength any) => Union es a -> Union (any ++ es) a+prefixUnion (Union n a) = Union (n + reifyLength @any) a+{-# INLINE prefixUnion #-}++prefixUnionUnder+    :: forall any offset es a+     . (KnownLength any, KnownNat offset)+    => Union es a+    -> Union (Take offset es ++ any ++ Drop offset es) a+prefixUnionUnder u@(Union n a)+    | n < wordVal @offset = coerce u+    | otherwise = Union (n + reifyLength @any) a+{-# INLINE prefixUnionUnder #-}++suffixUnion :: forall any es a. Union es a -> Union (es ++ any) a+suffixUnion = coerce+{-# INLINE suffixUnion #-}++suffixUnionOverN+    :: forall any offset es a+     . (KnownLength any, KnownNat offset, KnownLength es)+    => Union es a+    -> Union (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) a+suffixUnionOverN u@(Union n a)+    | n < reifyLength @es - wordVal @offset = coerce u+    | otherwise = Union (n + reifyLength @any) a+{-# INLINE suffixUnionOverN #-}++flipAllUnion :: forall es a. (KnownLength es) => Union es a -> Union (Reverse es) a+flipAllUnion (Union n a) = Union (reifyLength @es - n) a+{-# INLINE flipAllUnion #-}++flipUnion+    :: forall len es a+     . (KnownNat len)+    => Union es a+    -> Union (Reverse (Take len es) ++ Drop len es) a+flipUnion u@(Union n a)+    | n < len = Union (len - n) a+    | otherwise = coerce u+  where+    len = wordVal @len+{-# INLINE flipUnion #-}++flipUnionUnder+    :: forall len offset es a+     . (KnownNat len, KnownNat offset)+    => Union es a+    -> Union (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) a+flipUnionUnder u@(Union n a)+    | n >= off && n' < len = Union (off + len - n') a+    | otherwise = coerce u+  where+    off = wordVal @offset+    len = wordVal @len+    n' = n - off+{-# INLINE flipUnionUnder #-}++nil :: Union '[] a -> r+nil _ = error "Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."

@@ -0,0 +1,387 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Eta reduce" #-}++-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause++-- 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) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda+License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)+Maintainer  :  ymdfield@outlook.jp+Description :  Open unions (type-indexed co-products) for extensible higher-order effects.++Implementation of an open union for higher-order effects.++Importing this module allows unsafe access to the data structure of the open+union, so it should not usually be imported directly.++Based on [the open union in freer-simple](https://hackage.haskell.org/package/freer-simple-1.2.1.2/docs/Data-OpenUnion-Internal.html).+-}+module Data.Effect.OpenUnion.Internal.HO where++import Control.Effect (type (~>))+import Data.Coerce (coerce)+import Data.Effect (EffectH)+import Data.Effect.HFunctor (HFunctor, hfmap)+import Data.Effect.Key (type (##>))+import Data.Effect.OpenUnion.Internal (+    BundleUnder,+    Drop,+    ElemAt,+    ElemIndex,+    FindElem,+    IfNotFound,+    IsSuffixOf,+    KnownLength,+    Length,+    LookupError,+    P (unP),+    PrefixLength,+    Reverse,+    Split,+    Strengthen,+    StrengthenN,+    StrengthenNUnder,+    StrengthenUnder,+    Take,+    WeakenN,+    WeakenNUnder,+    WeakenUnder,+    elemNo,+    prefixLen,+    reifyLength,+    strengthenMap,+    strengthenMapUnder,+    wordVal,+    type (++),+ )+import Data.Kind (Type)+import GHC.TypeNats (KnownNat, type (-))+import Unsafe.Coerce (unsafeCoerce)++-- | Open union for higher-order effects.+data UnionH (es :: [EffectH]) (f :: Type -> Type) (a :: Type) where+    UnionH+        :: {-# UNPACK #-} !Word+        -- ^ A natural number tag to identify the element of the union.+        -> e g a+        -- ^ The data of the higher-order effect that is an element of the union.+        -> (g ~> f)+        -- ^ Continuation of interpretation.+        -- Due to this component, v'hfmap' for t'UnionH' becomes faster (because+        -- it no longer requires the t'HFunctor' dictionary), thus improving overall performance.+        -> UnionH es f a++hfmapUnion :: (f ~> g) -> UnionH es f a -> UnionH es g a+hfmapUnion phi (UnionH n e koi) = UnionH n e (phi . koi)+{-# INLINE hfmapUnion #-}++instance HFunctor (UnionH es) where+    hfmap f = hfmapUnion f+    {-# INLINE hfmap #-}++unsafeInjH :: Word -> e f a -> UnionH es f a+unsafeInjH n e = UnionH n e id+{-# INLINE unsafeInjH #-}++unsafePrjH :: (HFunctor e) => Word -> UnionH es f a -> Maybe (e f a)+unsafePrjH n (UnionH n' e koi)+    | n == n' = Just (hfmap koi $ unsafeCoerce e)+    | otherwise = Nothing+{-# INLINE unsafePrjH #-}++class (FindElem e es) => MemberH (e :: EffectH) es where+    injH :: e f a -> UnionH es f a+    prjH :: (HFunctor e) => UnionH es f a -> Maybe (e f a)++instance (FindElem e es, IfNotFound e es es) => MemberH e es where+    injH = unsafeInjH $ unP (elemNo :: P e es)+    {-# INLINE injH #-}++    prjH = unsafePrjH $ unP (elemNo :: P e es)+    {-# INLINE prjH #-}++infix 3 <<|+type (<<|) = MemberH++type MemberHBy key e es = (key ##> e <<| es, LookupH key es ~ key ##> e)++type LookupH key es = LookupH_ key es es++type family LookupH_ (key :: k) r w :: EffectH where+    LookupH_ key (key ##> e ': _) w = key ##> e+    LookupH_ key (_ ': r) w = LookupH_ key r w+    LookupH_ key '[] w = LookupError key w++decompH :: (HFunctor e) => UnionH (e ': es) f a -> Either (UnionH es f a) (e f a)+decompH (UnionH 0 a koi) = Right $ hfmap koi $ unsafeCoerce a+decompH (UnionH n a koi) = Left $ UnionH (n - 1) a koi+{-# INLINE [2] decompH #-}++decomp0H :: (HFunctor e) => UnionH '[e] f a -> Either (UnionH '[] f a) (e f a)+decomp0H (UnionH _ a koi) = Right $ hfmap koi $ unsafeCoerce a+{-# INLINE decomp0H #-}+{-# RULES "decomp/singleton" decompH = decomp0H #-}++infixr 5 !!++(!!+) :: (HFunctor e) => (e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r+(f !!+ g) u = case decompH u of+    Left x -> g x+    Right x -> f x+{-# INLINE (!!+) #-}++extractH :: (HFunctor e) => UnionH '[e] f a -> e f a+extractH (UnionH _ a koi) = hfmap koi $ unsafeCoerce a+{-# INLINE extractH #-}++inj0H :: forall e es f a. e f a -> UnionH (e ': es) f a+inj0H a = UnionH 0 a id+{-# INLINE inj0H #-}++injNH :: forall i es f a. (KnownNat i) => ElemAt i es f a -> UnionH es f a+injNH a = UnionH (wordVal @i) a id+{-# INLINE injNH #-}++prjNH+    :: forall i es f a+     . (KnownNat i, HFunctor (ElemAt i es))+    => UnionH es f a+    -> Maybe (ElemAt i es f a)+prjNH (UnionH n a koi)+    | n == wordVal @i = Just $ hfmap koi $ unsafeCoerce a+    | otherwise = Nothing+{-# INLINE prjNH #-}++weakenH :: forall any es f a. UnionH es f a -> UnionH (any ': es) f a+weakenH (UnionH n a koi) = UnionH (n + 1) a koi+{-# INLINE weakenH #-}++weakensH :: forall es es' f a. (es `IsSuffixOf` es') => UnionH es f a -> UnionH es' f a+weakensH (UnionH n a koi) = UnionH (n + prefixLen @es @es') a koi+{-# INLINE weakensH #-}++weakenNH :: forall len es es' f a. (WeakenN len es es') => UnionH es f a -> UnionH es' f a+weakenNH (UnionH n a koi) = UnionH (n + wordVal @len) a koi+{-# INLINE weakenNH #-}++weakenUnderH :: forall any e es f a. UnionH (e ': es) f a -> UnionH (e ': any ': es) f a+weakenUnderH u@(UnionH n a koi)+    | n == 0 = coerce u+    | otherwise = UnionH (n + 1) a koi+{-# INLINE weakenUnderH #-}++weakensUnderH :: forall offset es es' f a. (WeakenUnder offset es es') => UnionH es f a -> UnionH es' f a+weakensUnderH = weakenNUnderH @(PrefixLength es es') @offset+{-# INLINE weakensUnderH #-}++weakenNUnderH+    :: forall len offset es es' f a+     . (WeakenNUnder len offset es es')+    => UnionH es f a+    -> UnionH es' f a+weakenNUnderH u@(UnionH n a koi)+    | n < wordVal @offset = coerce u+    | otherwise = UnionH (n + wordVal @len) a koi+{-# INLINE weakenNUnderH #-}++strengthenH :: forall e es f a. (e <<| es) => UnionH (e ': es) f a -> UnionH es f a+strengthenH (UnionH n a koi)+    | n == 0 = UnionH (wordVal @(ElemIndex e es)) a koi+    | otherwise = UnionH (n - 1) a koi+{-# INLINE strengthenH #-}++strengthensH :: forall es es' f a. (Strengthen es es') => UnionH es f a -> UnionH es' f a+strengthensH = strengthenNH @(PrefixLength es' es)+{-# INLINE strengthensH #-}++strengthenNH :: forall len es es' f a. (StrengthenN len es es') => UnionH es f a -> UnionH es' f a+strengthenNH (UnionH n a koi) = UnionH (strengthenMap @_ @_ @len @es @es' n) a koi+{-# INLINE strengthenNH #-}++strengthenUnderH :: forall e2 e1 es f a. (e2 <<| es) => UnionH (e1 ': e2 ': es) f a -> UnionH (e1 ': es) f a+strengthenUnderH u@(UnionH n a koi)+    | n == 0 = coerce u+    | n == 1 = UnionH (1 + wordVal @(ElemIndex e2 es)) a koi+    | otherwise = UnionH (n - 1) a koi+{-# INLINE strengthenUnderH #-}++strengthensUnderH+    :: forall offset es es' f a+     . (StrengthenUnder offset es es')+    => UnionH es f a+    -> UnionH es' f a+strengthensUnderH = strengthenNUnderH @(PrefixLength es' es) @offset+{-# INLINE strengthensUnderH #-}++strengthenNUnderH+    :: forall len offset es es' f a+     . (StrengthenNUnder len offset es es')+    => UnionH es f a+    -> UnionH es' f a+strengthenNUnderH u@(UnionH n a koi)+    | n < off = coerce u+    | otherwise = UnionH (off + strengthenMapUnder @len @offset @es @es' (n - off)) a koi+  where+    off = wordVal @offset+{-# INLINE strengthenNUnderH #-}++bundleUnionH+    :: forall bundle es rest f a+     . (Split es bundle rest)+    => UnionH es f a+    -> UnionH (UnionH bundle ': rest) f a+bundleUnionH = bundleUnionNH @(Length bundle)+{-# INLINE bundleUnionH #-}++bundleUnionNH+    :: forall len es f a+     . (KnownNat len)+    => UnionH es f a+    -> UnionH (UnionH (Take len es) ': Drop len es) f a+bundleUnionNH (UnionH n a koi)+    | n < len = UnionH 0 (UnionH n a koi) id+    | otherwise = UnionH (n - len + 1) a koi+  where+    len = wordVal @len+{-# INLINE bundleUnionNH #-}++unbundleUnionH+    :: forall bundle es rest f a+     . (Split es bundle rest)+    => UnionH (UnionH bundle ': rest) f a+    -> UnionH es f a+unbundleUnionH = unbundleUnionNH @(Length bundle)+{-# INLINE unbundleUnionH #-}++unbundleUnionNH+    :: forall len es f a+     . (KnownNat len)+    => UnionH (UnionH (Take len es) ': Drop len es) f a+    -> UnionH es f a+unbundleUnionNH (UnionH n a koi)+    | n == 0 = case unsafeCoerce a of+        UnionH n' a' koi' -> UnionH n' a' (koi . koi')+    | otherwise = UnionH (n - 1 + wordVal @len) a koi+{-# INLINE unbundleUnionNH #-}++bundleUnionUnderH+    :: forall offset bundle es es' f a+     . (BundleUnder UnionH offset es es' bundle)+    => UnionH es f a+    -> UnionH es' f a+bundleUnionUnderH = bundleUnionNUnderH @(Length bundle) @offset+{-# INLINE bundleUnionUnderH #-}++bundleUnionNUnderH+    :: forall len offset es f a+     . (KnownNat len, KnownNat offset)+    => UnionH es f a+    -> UnionH (Take offset es ++ (UnionH (Take len (Drop offset es)) ': Drop len (Drop offset es))) f a+bundleUnionNUnderH u@(UnionH n a koi)+    | n < off = coerce u+    | n' < len = UnionH 0 (UnionH n' a koi) id+    | otherwise = UnionH (n - len + 1) a koi+  where+    off = wordVal @offset+    len = wordVal @len+    n' = n - off+{-# INLINE bundleUnionNUnderH #-}++unbundleUnionUnderH+    :: forall offset bundle es es' f a+     . (BundleUnder UnionH offset es es' bundle)+    => UnionH es' f a+    -> UnionH es f a+unbundleUnionUnderH = unbundleUnionNUnderH @(Length bundle) @offset+{-# INLINE unbundleUnionUnderH #-}++unbundleUnionNUnderH+    :: forall len offset es f a+     . (KnownNat len, KnownNat offset)+    => UnionH (Take offset es ++ (UnionH (Take len (Drop offset es)) ': Drop len (Drop offset es))) f a+    -> UnionH es f a+unbundleUnionNUnderH u@(UnionH n a koi)+    | n < off = coerce u+    | n == off =+        case unsafeCoerce a of+            UnionH n' a' koi' -> UnionH (off + n') a' (koi . koi')+    | otherwise = UnionH (n - 1 + len) a koi+  where+    off = wordVal @offset+    len = wordVal @len+{-# INLINE unbundleUnionNUnderH #-}++bundleAllUnionH :: UnionH es f a -> UnionH '[UnionH es] f a+bundleAllUnionH u = UnionH 0 u id+{-# INLINE bundleAllUnionH #-}++unbundleAllUnionH :: UnionH '[UnionH es] f a -> UnionH es f a+unbundleAllUnionH = extractH+{-# INLINE unbundleAllUnionH #-}++prefixUnionH :: forall any es f a. (KnownLength any) => UnionH es f a -> UnionH (any ++ es) f a+prefixUnionH (UnionH n a koi) = UnionH (n + reifyLength @any) a koi+{-# INLINE prefixUnionH #-}++prefixUnionUnderH+    :: forall any offset es f a+     . (KnownLength any, KnownNat offset)+    => UnionH es f a+    -> UnionH (Take offset es ++ any ++ Drop offset es) f a+prefixUnionUnderH u@(UnionH n a koi)+    | n < wordVal @offset = coerce u+    | otherwise = UnionH (n + reifyLength @any) a koi+{-# INLINE prefixUnionUnderH #-}++suffixUnionH :: forall any es f a. UnionH es f a -> UnionH (es ++ any) f a+suffixUnionH = coerce+{-# INLINE suffixUnionH #-}++suffixUnionOverNH+    :: forall any offset es f a+     . (KnownLength any, KnownNat offset, KnownLength es)+    => UnionH es f a+    -> UnionH (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) f a+suffixUnionOverNH u@(UnionH n a koi)+    | n < reifyLength @es - wordVal @offset = coerce u+    | otherwise = UnionH (n + reifyLength @any) a koi+{-# INLINE suffixUnionOverNH #-}++flipAllUnionH :: forall es f a. (KnownLength es) => UnionH es f a -> UnionH (Reverse es) f a+flipAllUnionH (UnionH n a koi) = UnionH (reifyLength @es - n) a koi+{-# INLINE flipAllUnionH #-}++flipUnionH+    :: forall len es f a+     . (KnownNat len)+    => UnionH es f a+    -> UnionH (Reverse (Take len es) ++ Drop len es) f a+flipUnionH u@(UnionH n a koi)+    | n < len = UnionH (len - n) a koi+    | otherwise = coerce u+  where+    len = wordVal @len+{-# INLINE flipUnionH #-}++flipUnionUnderH+    :: forall len offset es f a+     . (KnownNat len, KnownNat offset)+    => UnionH es f a+    -> UnionH (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) f a+flipUnionUnderH u@(UnionH n a koi)+    | n >= off && n' < len = UnionH (off + len - n') a koi+    | otherwise = coerce u+  where+    off = wordVal @offset+    len = wordVal @len+    n' = n - off+{-# INLINE flipUnionUnderH #-}++nilH :: UnionH '[] f a -> r+nilH _ = error "Effect system internal error: nilH - An empty effect union, which should not be possible to create, has been created."

@@ -0,0 +1,31 @@+-- SPDX-License-Identifier: MPL-2.0++module Data.Effect.OpenUnion.Sum where++import Data.Effect (EffectF, EffectH, LNop, Nop)+import Data.Effect.HFunctor qualified as H+import Data.Effect.OpenUnion.Internal.FO (Union)+import Data.Effect.OpenUnion.Internal.HO (UnionH)+import GHC.Generics qualified as G++infixr 5 +++-- | Sum for first-order effects.+type (+) = (G.:+:) :: EffectF -> EffectF -> EffectF++-- | Sum for higher-order effects.+type (:+:) = (H.:+:) :: EffectH -> EffectH -> EffectH++type U u e = SumToRecUnion u e+type UL u e = SumToRecUnionList u e++type SumToRecUnion u e = u (SumToRecUnionList u e)++type SumToRecUnionList :: forall k. ([k] -> k) -> k -> [k]+type family SumToRecUnionList u e where+    SumToRecUnionList Union Nop = '[]+    SumToRecUnionList Union (e + r) = e ': SumToRecUnionList Union r+    SumToRecUnionList Union e = '[e]+    SumToRecUnionList UnionH LNop = '[]+    SumToRecUnionList UnionH (e :+: r) = e ': SumToRecUnionList UnionH r+    SumToRecUnionList UnionH e = '[e]

@@ -1,39 +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-2024 Yamada Ryo-License     :  MPL-2.0 (see the file LICENSE)-Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--Binary sums for first-order effects.--}-module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1) where--import Control.Effect (type (~>))-import Data.Effect (Nop)-import GHC.Generics (type (:+:) (L1, R1))--type (+) = (:+:)-infixr 5 +--caseF :: (f a -> r) -> (g a -> r) -> (f + g) a -> r-caseF f g = \case-    L1 x -> f x-    R1 x -> g x-{-# INLINE caseF #-}--absurdL :: Nop + f ~> f-absurdL = caseF \case {} id-{-# INLINE absurdL #-}--absurdR :: f + Nop ~> f-absurdR = caseF id \case {}-{-# INLINE absurdR #-}--swapSum :: (f + g) a -> (g + f) a-swapSum = caseF R1 L1-{-# INLINE swapSum #-}

@@ -1,132 +0,0 @@-{-# LANGUAGE ImpredicativeTypes #-}-{-# 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 higher-order effects using-the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.--}-module Data.Hefty.Extensible (-    module Data.Hefty.Extensible,-    Forall,-) where--import Control.Effect.Free qualified as E-import Control.Effect.Hefty qualified as E-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 (-    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.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 ExtensibleUnion es f a = ExtensibleUnion {unExtensibleUnion :: es :/ FieldApp f a}--newtype FieldApp f a (e :: SigClass) = FieldApp {unFieldApp :: e f a}--instance Forall HFunctor es => HFunctor (ExtensibleUnion es) where-    hfmap f =-        ExtensibleUnion-            . match-                ( htabulateFor @HFunctor Proxy \w ->-                    Match $ EmbedAt w . FieldApp . hfmap f . unFieldApp-                )-            . unExtensibleUnion-    {-# INLINE hfmap #-}---- todo: Functor, Foldable, Traversable instances--instance Union ExtensibleUnion where-    type HasMembership _ e es = KnownNat (ClassIndex es e)--    inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp-    {-# INLINE inject #-}--    project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u-    {-# INLINE project #-}--    exhaust = E.exhaust . unExtensibleUnion-    {-# INLINE exhaust #-}--    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 (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--type Eff fr eh ef = E.Eff ExtensibleUnion fr eh ef-type EffF fr es = E.EffF ExtensibleUnion fr es

@@ -1,531 +0,0 @@-{-# 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-2024 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 higher-order effects, independent of the internal-implementation.--}-module Data.Hefty.Union where--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 Union (u :: [SigClass] -> SigClass) where-    {-# MINIMAL inject, project, exhaust, (comp | (inject0, weaken), decomp | (|+:)) #-}--    type HasMembership u (e :: SigClass) (es :: [SigClass]) :: Constraint--    inject :: HasMembership u e es => e f ~> u es f-    project :: HasMembership u e es => u es f a -> Maybe (e f a)--    exhaust :: u '[] f a -> x--    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 #-}--    decomp :: u (e ': es) f a -> (e :+: u es) f a-    decomp = Inl |+: Inr-    {-# INLINE decomp #-}--    infixr 5 |+:-    (|+:) :: (e f a -> r) -> (u es f a -> r) -> u (e ': es) f a -> r-    f |+: g = caseH f g . decomp-    {-# INLINE (|+:) #-}--    inject0 :: e f ~> u (e ': es) f-    inject0 = comp . Left-    {-# INLINE inject0 #-}--    injectUnder :: h2 f ~> u (h1 ': h2 ': es) f-    injectUnder = weaken . inject0-    {-# INLINE injectUnder #-}--    injectUnder2 :: h3 f ~> u (h1 ': h2 ': h3 ': es) f-    injectUnder2 = weaken2 . inject0-    {-# INLINE injectUnder2 #-}--    injectUnder3 :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': es) f-    injectUnder3 = weaken3 . inject0-    {-# INLINE injectUnder3 #-}--    weaken :: u es f ~> u (e ': es) f-    weaken = comp . Right-    {-# INLINE weaken #-}--    weaken2 :: u es f ~> u (e1 ': e2 ': es) f-    weaken2 = weaken . weaken-    {-# INLINE weaken2 #-}--    weaken3 :: u es f ~> u (e1 ': e2 ': e3 ': es) f-    weaken3 = weaken2 . weaken-    {-# INLINE weaken3 #-}--    weaken4 :: u es f ~> u (e1 ': e2 ': e3 ': e4 ': es) f-    weaken4 = weaken3 . weaken-    {-# INLINE weaken4 #-}--    weakenUnder :: u (e1 ': es) f ~> u (e1 ': e2 ': es) f-    weakenUnder = inject0 |+: weaken2--    weakenUnder2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': es) f-    weakenUnder2 = inject0 |+: injectUnder |+: weaken3--    weakenUnder3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f-    weakenUnder3 = inject0 |+: injectUnder |+: injectUnder2 |+: weaken4--    weaken2Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': es) f-    weaken2Under = inject0 |+: weaken3--    weaken2Under2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f-    weaken2Under2 = inject0 |+: injectUnder |+: weaken4--    weaken3Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f-    weaken3Under = inject0 |+: weaken4--    flipUnion :: u (e1 ': e2 ': es) f ~> u (e2 ': e1 ': es) f-    flipUnion = injectUnder |+: inject0 |+: weaken2--    flipUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e2 ': e1 ': es) f-    flipUnion3 = injectUnder2 |+: injectUnder |+: inject0 |+: weaken3--    flipUnionUnder :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e3 ': e2 ': es) f-    flipUnionUnder = inject0 |+: injectUnder2 |+: injectUnder |+: weaken3--    rot3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e2 ': e3 ': e1 ': es) f-    rot3 = injectUnder2 |+: inject0 |+: injectUnder |+: weaken3--    rot3' :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e1 ': e2 ': es) f-    rot3' = injectUnder |+: injectUnder2 |+: inject0 |+: weaken3--    bundleUnion2 :: u (e1 ': e2 ': es) f ~> u (u '[e1, e2] ': es) f-    bundleUnion2 = inject0 . inject0 |+: inject0 . injectUnder |+: weaken--    bundleUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (u '[e1, e2, e3] ': es) f-    bundleUnion3 =-        (inject0 . inject0)-            |+: (inject0 . injectUnder)-            |+: (inject0 . injectUnder2)-            |+: weaken--    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--    unbundleUnion2 :: u (u '[e1, e2] ': es) f ~> u (e1 ': e2 ': es) f-    unbundleUnion2 = (inject0 |+: injectUnder |+: exhaust) |+: weaken2--    unbundleUnion3 :: u (u '[e1, e2, e3] ': es) f ~> u (e1 ': e2 ': e3 ': es) f-    unbundleUnion3 = (inject0 |+: injectUnder |+: injectUnder2 |+: exhaust) |+: weaken3--    unbundleUnion4 ::-        u (u '[e1, e2, e3, e4] ': es) f-            ~> u (e1 ': e2 ': e3 ': e4 ': es) f-    unbundleUnion4 =-        (inject0 |+: injectUnder |+: injectUnder2 |+: injectUnder3 |+: exhaust)-            |+: weaken4--type HFunctorUnion u = HFunctorUnion_ (ForallHFunctor u) u---- 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