heftia 0.2.0.0 → 0.3.0.0

raw patch · 8 files changed

+408/−55 lines, 8 filesdep ~data-effectsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: data-effects

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−0
• README.md +73/−38
• heftia.cabal +4/−2
• src/Control/Effect/Free.hs +1/−1
• src/Control/Effect/Hefty.hs +206/−14
• src/Data/Hefty/Extensible.hs +5/−0
• src/Data/Hefty/Union/Strengthen.hs +56/−0
• src/Data/Hefty/Union/Weaken.hs +56/−0

@@ -8,3 +8,10 @@  * Redesign from scratch. * Released as a beta version.++## 0.3.0.0 -- 2024-09-01++* Fixed #7: bug on `interposeRecH`. https://github.com/sayo-hs/heftia/issues/7+* 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.

@@ -27,8 +27,57 @@  **We are looking forward to your feedback!** +## Installation+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:++    * `LambdaCase`+    * `DerivingStrategies`+    * `DataKinds`+    * `TypeFamilies`+    * `BlockArguments`+    * `FunctionalDependencies`+    * `RecordWildCards`+    * `DefaultSignatures`+    * `PatternSynonyms`++Example .cabal:++```+...+    build-depends:+        ...+        heftia-effects ^>= 0.2,+        ghc-typelits-knownnat ^>= 0.7,++    default-language: GHC2021++    default-extensions:+        ...+        LambdaCase,+        DerivingStrategies,+        DataKinds,+        TypeFamilies,+        BlockArguments,+        FunctionalDependencies,+        RecordWildCards,+        DefaultSignatures,+        PatternSynonyms,+        TemplateHaskell,+        PartialTypeSignatures,+        AllowAmbiguousTypes++    ghc-options: ... -fplugin GHC.TypeLits.KnownNat.Solver+...+```++This library has been tested to work with GHC 9.2.8.+ ## Getting Started-To run the [SemanticsZoo example](heftia-effects/Example/SemanticsZoo/Main.hs):+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@@ -63,7 +112,7 @@ In handling higher-order effects, it's easy to work with **multi-shot delimited continuations**. This enables an almost complete emulation of "Algebraic Effects and Handlers". For more details, please refer to-the [example code](heftia-effects/Example/Continuation/Main.hs).+the [example code](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/Continuation/Main.hs).  ### Two interpretations of the `censor` effect for Writer @@ -116,7 +165,7 @@ Post-applying: Hello world!! ``` -For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).+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).  Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being eliminated.@@ -127,47 +176,34 @@ Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs).  ## Documentation-The example codes are located in the [heftia-effects/Example/](heftia-effects/Example/) directory.+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 -~~Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.~~ Documents have become outdated.-Please wait for the documentation for the new version to be written.--## Limitation and how to avoid it-### The *reset* behavior of the scopes held by unhandled higher-order effects-When attempting to interpret an effect while there are unhandled higher-order effects present, you cannot obtain delimited continuations beyond the action scope held by these unhandled higher-order effects.-It appears as if a *reset* (in the sense of *shift/reset*) is applied to each of the scopes still held by the remaining unhandled higher-order effects.--In other words, to obtain delimited continuations beyond their scope, it is necessary to first handle and eliminate all higher-order effects that hold those scopes,-and then handle the effect targeted for stateful interpretation in that order.-For this purpose, it might sometimes be possible to use *multi-layering*. For an example of multi-layering,-see `handleReaderThenShift` defined in [Example/Continuation2](https://github.com/sayo-hs/heftia/blob/8f71a2d4e6125018b64cbbacd32151565a29046d/heftia-effects/Example/Continuation2/Main.hs)-(particularly, the type signature of `prog` within it).-For more details, please refer to the documentation of the `interpretRec` family of functions.+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.  ## Comparison  * Higher-Order Effects: Does it support higher-order effects? * Delimited Continuation: The ability to manipulate delimited continuations.-* Statically Typed Set of Effects: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce?+* Effect System: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce? * Purely Monadic: Is an effectful program represented as a transparent data structure that is a monad, and can it be interpreted into other data types using only pure operations without side effects or `unsafePerformIO`? * Dynamic Effect Rewriting: Can an effectful program have its internal effects altered afterwards (by functions typically referred to as `handle with`, `intercept`, `interpose`, `transform`, `translate`, or `rewrite`) ? * Performance: Time complexity or space complexity. -| Library or Language | Higher-Order Effects | Delimited Continuation | Statically Typed Set of Effects                 | Purely Monadic                    | Dynamic Effect Rewriting | Performance (TODO) |-| ------------------- | -------------------- | ---------------------- | ----------------------------------------------- | --------------------------------- | ------------------------ | ------------------ |-| Heftia              | Yes [^1]             | Multi-shot             | Yes                                             | Yes (also Applicative and others) | Yes                      | ?                  |-| freer-simple        | No                   | Multi-shot             | Yes                                             | Yes                               | Yes                      | ?                  |-| Polysemy            | Yes                  | No                     | Yes                                             | Yes                               | Yes                      | ?                  |-| Effectful           | Yes                  | No                     | Yes                                             | No (based on the `IO` monad)      | Yes                      | ?                  |-| eff                 | Yes                  | Multi-shot?            | Yes                                             | No (based on the `IO` monad)      | Yes                      | Fast               |-| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes                                             | Yes                               | No                       | ?                  |-| fused-effects       | Yes                  | No?                    | Yes                                             | Yes                               | No                       | ?                  |-| koka-lang           | No?                  | Multi-shot             | Yes                                             | No (language built-in)            | ?                        | ?                  |-| OCaml-lang 5        | Yes                  | One-shot               | No [^2]                                         | No (language built-in)            | ?                        | ?                  |+| Library or Language | Higher-Order Effects | Delimited Continuation | Effect System | Purely Monadic                    | Dynamic Effect Rewriting | Performance (TODO) |+| ------------------- | -------------------- | ---------------------- | --------------| --------------------------------- | ------------------------ | ------------------ |+| Heftia              | Yes                  | Multi-shot             | Yes           | Yes (also Applicative and others) | Yes                      | ?                  |+| freer-simple        | No                   | Multi-shot             | Yes           | Yes                               | Yes                      | ?                  |+| Polysemy            | Yes                  | No                     | Yes           | Yes                               | Yes                      | ?                  |+| Effectful           | Yes                  | No                     | Yes           | No (based on the `IO` monad)      | Yes                      | ?                  |+| eff                 | Yes                  | Multi-shot?            | Yes           | No (based on the `IO` monad)      | Yes                      | Fast               |+| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes           | Yes                               | No                       | ?                  |+| fused-effects       | Yes                  | No?                    | Yes           | Yes                               | No                       | ?                  |+| koka-lang           | No [^2]              | Multi-shot             | Yes           | No (language built-in)            | Yes                      | ?                  |+| OCaml-lang 5        | ?                    | One-shot               | No [^3]       | No (language built-in)            | ?                        | ?                  | -[^1]: limitation: https://github.com/sayo-hs/heftia?tab=readme-ov-file#the-reset-behavior-of-the-scopes-held-by-unhandled-higher-order-effects-[^2]: potential for 'unhandled' runtime errors+[^2]: https://gist.github.com/ymdryo/6fb2f7f4020c6fcda98ccc67c090dc75+[^3]: Effects do not appear in the type signature and can potentially cause unhandled errors at runtime  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.@@ -185,7 +221,7 @@  * GADTs for higher-order effects need to be instances of the [HFunctor](https://hackage.haskell.org/package/compdata-0.13.1/docs/Data-Comp-Multi-HFunctor.html#t:HFunctor) type class for convenient usage.     While it is still possible to use them without being instances of `HFunctor`,-    the `interpretRec` family of functions cannot be used when higher-order effects that are not `HFunctor` are unhandled.+    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. @@ -198,20 +234,19 @@ ## Future Plans * Enriching the documentation and tests * Completing missing definitions such as-    * `raise`, `raiseUnder`, and `subsume` for arbitrary numbers of effects by type classes.     * more patterns of interpret & transform function-families.-    * handlers for the `Accum` and others effect classes+    * interpreters for the `Accum` and others effect classes      and others. * Benchmarking  ## License-The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/develop/NOTICE).-Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed+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.  ## Your contributions are welcome!-Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md).+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/v0.3.0/CONTRIBUTING.md).  ## Credits Parts of this project have been inspired by the following resources:

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               heftia-version:            0.2.0.0+version:            0.3.0.0  -- A short (one-line) description of the package. synopsis: higher-order effects done right@@ -73,6 +73,8 @@         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 @@ -96,7 +98,7 @@     -- other-extensions:     build-depends:         base                          ^>= 4.16.4.0,-        data-effects                ^>= 0.1,+        data-effects                ^>= 0.1.1,         mtl ^>= 2.2.2,         free ^>= 5.2,         kan-extensions ^>= 5.2.5,

@@ -12,7 +12,7 @@ Portability :  portable  A Freer carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+on [@data-effects@](https://hackage.haskell.org/package/data-effects). -} module Control.Effect.Free where 

@@ -12,11 +12,12 @@ Stability   :  experimental Portability :  portable -A Heftia carrier that can be used as a handler for effect systems based-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+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)@@ -27,13 +28,14 @@ import Control.Monad.Trans (MonadTrans) import Data.Coerce (coerce) import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)-import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:))+import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr)) import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>))-import Data.Effect.Tag (Tag (unTag), TagH (unTagH), 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,@@ -49,17 +51,20 @@     flipUnion,     flipUnion3,     flipUnionUnder,-    inject,     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) @@ -421,7 +426,7 @@     e (Eff u fr ehs efs) ~> Eff u fr ehs efs ->     Eff u fr ehs efs ~> Eff u fr ehs efs interposeRecH f =-    interpretAllH+    interpretAllRecH         \u -> case projectRec u of             Just e -> f e             Nothing -> injectH u@@ -808,6 +813,54 @@                     (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)) =>@@ -815,6 +868,27 @@ 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)) =>@@ -829,6 +903,20 @@ 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)) =>@@ -971,18 +1059,100 @@  subsume ::     forall e r ehs fr u c.-    (Freer c fr, Union u, HFunctor (u ehs), HasMembership u e r) =>+    (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 $ inject |+: id+subsume = transformAll $ injectRec |+: id {-# INLINE subsume #-}  subsumeH ::     forall e r efs fr u c.-    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembership u e r) =>+    (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 $ inject |+: id+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) =>@@ -1028,21 +1198,29 @@         . unHefty  send0 :: (Freer c fr, Union u, HeadIns e) => UnliftIfSingle e ~> Eff u fr eh (e ': r)-send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle+send0 = liftEff . inject0 . liftInsIfSingle {-# INLINE send0 #-}  send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r)-send1 = Hefty . liftIns . EffUnion . R1 . weaken . inject0 . liftInsIfSingle+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 = Hefty . liftIns . EffUnion . L1 . inject0+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 = Hefty . liftIns . EffUnion . L1 . weaken . inject0+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 #-}@@ -1050,6 +1228,20 @@ 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.

@@ -20,6 +20,8 @@     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)@@ -125,3 +127,6 @@  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

@@ -0,0 +1,56 @@+{-# 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) 2024 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable+-}+module Data.Hefty.Union.Strengthen where++import Control.Effect (type (~>))+import Data.Hefty.Union (MemberRec, Union (inject0, (|+:)), injectRec, weaken)+import Data.Type.Equality (type (==))+import GHC.TypeNats (Natural, type (-))++class+    (Union u, isMZero ~ (m == 0), isNZero ~ (n == 0)) =>+    StrengthenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) u es es'+        | m n es -> es'+    where+    strengthenNUnderM_ :: u es f ~> u es' f++type StrengthenUnder n m = StrengthenUnder_ (m == 0) m (n == 0) n+type Strengthen n = StrengthenUnder_ 'True 0 (n == 0) n++strengthenNUnderM :: forall n m u es' f es. StrengthenUnder n m u es es' => u es f ~> u es' f+strengthenNUnderM = strengthenNUnderM_ @(m == 0) @m @(n == 0) @n+{-# INLINE strengthenNUnderM #-}++strengthenN :: forall n u es' f es. Strengthen n u es es' => u es f ~> u es' f+strengthenN = strengthenNUnderM_ @( 'True) @0 @(n == 0) @n+{-# INLINE strengthenN #-}++instance+    (Union u, StrengthenUnder n (m - 1) u es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>+    StrengthenUnder_ 'False m isNZero n u (e ': es) (e ': es')+    where+    strengthenNUnderM_ = inject0 |+: weaken . strengthenNUnderM @n @(m - 1)+    {-# INLINE strengthenNUnderM_ #-}++instance+    (Union u, Strengthen (n - 1) u es es', MemberRec u e es, (n == 0) ~ 'False) =>+    StrengthenUnder_ 'True 0 'False n u (e ': es) es'+    where+    strengthenNUnderM_ = strengthenN @(n - 1) . (injectRec |+: id)+    {-# INLINE strengthenNUnderM_ #-}++instance Union u => StrengthenUnder_ 'True 0 'True 0 u es es where+    strengthenNUnderM_ = id+    {-# INLINE strengthenNUnderM_ #-}

@@ -0,0 +1,56 @@+{-# 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) 2024 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable+-}+module Data.Hefty.Union.Weaken where++import Control.Effect (type (~>))+import Data.Hefty.Union (Union (inject0, weaken, (|+:)))+import Data.Type.Equality (type (==))+import GHC.TypeNats (Natural, type (-))++class+    (isMZero ~ (m == 0), isNZero ~ (n == 0)) =>+    WeakenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) es es'+        | m n es' -> es+    where+    weakenNUnderM_ :: Union u => u es f ~> u es' f++type WeakenUnder n m = WeakenUnder_ (m == 0) m (n == 0) n+type Weaken n = WeakenUnder_ 'True 0 (n == 0) n++weakenNUnderM :: forall n m u es' f es. (Union u, WeakenUnder n m es es') => u es f ~> u es' f+weakenNUnderM = weakenNUnderM_ @(m == 0) @m @(n == 0) @n+{-# INLINE weakenNUnderM #-}++weakenN :: forall n u es' f es. (Union u, Weaken n es es') => u es f ~> u es' f+weakenN = weakenNUnderM_ @( 'True) @0 @(n == 0) @n+{-# INLINE weakenN #-}++instance+    (WeakenUnder n (m - 1) es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>+    WeakenUnder_ 'False m isNZero n (e ': es) (e ': es')+    where+    weakenNUnderM_ = inject0 |+: weaken . weakenNUnderM @n @(m - 1)+    {-# INLINE weakenNUnderM_ #-}++instance+    (Weaken (n - 1) es es', (n == 0) ~ 'False) =>+    WeakenUnder_ 'True 0 'False n es (e ': es')+    where+    weakenNUnderM_ = weaken . weakenN @(n - 1)+    {-# INLINE weakenNUnderM_ #-}++instance WeakenUnder_ 'True 0 'True 0 es es where+    weakenNUnderM_ = id+    {-# INLINE weakenNUnderM_ #-}