packages feed

heftia (empty) → 0.1.0.0

raw patch · 25 files changed

+3459/−0 lines, 25 filesdep +basedep +classy-effects-basedep +constraints

Dependencies added: base, classy-effects-base, constraints, extensible, free, heftia, kan-extensions, membership, mtl, tasty, tasty-hunit, transformers, transformers-base

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for heftia++## 0.1.0.0 -- 2023-09-18++* Initial public release.
+ LICENSE view
@@ -0,0 +1,373 @@+Mozilla Public License Version 2.0+==================================++1. Definitions+--------------++1.1. "Contributor"+    means each individual or legal entity that creates, contributes to+    the creation of, or owns Covered Software.++1.2. "Contributor Version"+    means the combination of the Contributions of others (if any) used+    by a Contributor and that particular Contributor's Contribution.++1.3. "Contribution"+    means Covered Software of a particular Contributor.++1.4. "Covered Software"+    means Source Code Form to which the initial Contributor has attached+    the notice in Exhibit A, the Executable Form of such Source Code+    Form, and Modifications of such Source Code Form, in each case+    including portions thereof.++1.5. "Incompatible With Secondary Licenses"+    means++    (a) that the initial Contributor has attached the notice described+        in Exhibit B to the Covered Software; or++    (b) that the Covered Software was made available under the terms of+        version 1.1 or earlier of the License, but not also under the+        terms of a Secondary License.++1.6. "Executable Form"+    means any form of the work other than Source Code Form.++1.7. "Larger Work"+    means a work that combines Covered Software with other material, in+    a separate file or files, that is not Covered Software.++1.8. "License"+    means this document.++1.9. "Licensable"+    means having the right to grant, to the maximum extent possible,+    whether at the time of the initial grant or subsequently, any and+    all of the rights conveyed by this License.++1.10. "Modifications"+    means any of the following:++    (a) any file in Source Code Form that results from an addition to,+        deletion from, or modification of the contents of Covered+        Software; or++    (b) any new file in Source Code Form that contains any Covered+        Software.++1.11. "Patent Claims" of a Contributor+    means any patent claim(s), including without limitation, method,+    process, and apparatus claims, in any patent Licensable by such+    Contributor that would be infringed, but for the grant of the+    License, by the making, using, selling, offering for sale, having+    made, import, or transfer of either its Contributions or its+    Contributor Version.++1.12. "Secondary License"+    means either the GNU General Public License, Version 2.0, the GNU+    Lesser General Public License, Version 2.1, the GNU Affero General+    Public License, Version 3.0, or any later versions of those+    licenses.++1.13. "Source Code Form"+    means the form of the work preferred for making modifications.++1.14. "You" (or "Your")+    means an individual or a legal entity exercising rights under this+    License. For legal entities, "You" includes any entity that+    controls, is controlled by, or is under common control with You. For+    purposes of this definition, "control" means (a) the power, direct+    or indirect, to cause the direction or management of such entity,+    whether by contract or otherwise, or (b) ownership of more than+    fifty percent (50%) of the outstanding shares or beneficial+    ownership of such entity.++2. License Grants and Conditions+--------------------------------++2.1. Grants++Each Contributor hereby grants You a world-wide, royalty-free,+non-exclusive license:++(a) under intellectual property rights (other than patent or trademark)+    Licensable by such Contributor to use, reproduce, make available,+    modify, display, perform, distribute, and otherwise exploit its+    Contributions, either on an unmodified basis, with Modifications, or+    as part of a Larger Work; and++(b) under Patent Claims of such Contributor to make, use, sell, offer+    for sale, have made, import, and otherwise transfer either its+    Contributions or its Contributor Version.++2.2. Effective Date++The licenses granted in Section 2.1 with respect to any Contribution+become effective for each Contribution on the date the Contributor first+distributes such Contribution.++2.3. Limitations on Grant Scope++The licenses granted in this Section 2 are the only rights granted under+this License. No additional rights or licenses will be implied from the+distribution or licensing of Covered Software under this License.+Notwithstanding Section 2.1(b) above, no patent license is granted by a+Contributor:++(a) for any code that a Contributor has removed from Covered Software;+    or++(b) for infringements caused by: (i) Your and any other third party's+    modifications of Covered Software, or (ii) the combination of its+    Contributions with other software (except as part of its Contributor+    Version); or++(c) under Patent Claims infringed by Covered Software in the absence of+    its Contributions.++This License does not grant any rights in the trademarks, service marks,+or logos of any Contributor (except as may be necessary to comply with+the notice requirements in Section 3.4).++2.4. Subsequent Licenses++No Contributor makes additional grants as a result of Your choice to+distribute the Covered Software under a subsequent version of this+License (see Section 10.2) or under the terms of a Secondary License (if+permitted under the terms of Section 3.3).++2.5. Representation++Each Contributor represents that the Contributor believes its+Contributions are its original creation(s) or it has sufficient rights+to grant the rights to its Contributions conveyed by this License.++2.6. Fair Use++This License is not intended to limit any rights You have under+applicable copyright doctrines of fair use, fair dealing, or other+equivalents.++2.7. Conditions++Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted+in Section 2.1.++3. Responsibilities+-------------------++3.1. Distribution of Source Form++All distribution of Covered Software in Source Code Form, including any+Modifications that You create or to which You contribute, must be under+the terms of this License. You must inform recipients that the Source+Code Form of the Covered Software is governed by the terms of this+License, and how they can obtain a copy of this License. You may not+attempt to alter or restrict the recipients' rights in the Source Code+Form.++3.2. Distribution of Executable Form++If You distribute Covered Software in Executable Form then:++(a) such Covered Software must also be made available in Source Code+    Form, as described in Section 3.1, and You must inform recipients of+    the Executable Form how they can obtain a copy of such Source Code+    Form by reasonable means in a timely manner, at a charge no more+    than the cost of distribution to the recipient; and++(b) You may distribute such Executable Form under the terms of this+    License, or sublicense it under different terms, provided that the+    license for the Executable Form does not attempt to limit or alter+    the recipients' rights in the Source Code Form under this License.++3.3. Distribution of a Larger Work++You may create and distribute a Larger Work under terms of Your choice,+provided that You also comply with the requirements of this License for+the Covered Software. If the Larger Work is a combination of Covered+Software with a work governed by one or more Secondary Licenses, and the+Covered Software is not Incompatible With Secondary Licenses, this+License permits You to additionally distribute such Covered Software+under the terms of such Secondary License(s), so that the recipient of+the Larger Work may, at their option, further distribute the Covered+Software under the terms of either this License or such Secondary+License(s).++3.4. Notices++You may not remove or alter the substance of any license notices+(including copyright notices, patent notices, disclaimers of warranty,+or limitations of liability) contained within the Source Code Form of+the Covered Software, except that You may alter any license notices to+the extent required to remedy known factual inaccuracies.++3.5. Application of Additional Terms++You may choose to offer, and to charge a fee for, warranty, support,+indemnity or liability obligations to one or more recipients of Covered+Software. However, You may do so only on Your own behalf, and not on+behalf of any Contributor. You must make it absolutely clear that any+such warranty, support, indemnity, or liability obligation is offered by+You alone, and You hereby agree to indemnify every Contributor for any+liability incurred by such Contributor as a result of warranty, support,+indemnity or liability terms You offer. You may include additional+disclaimers of warranty and limitations of liability specific to any+jurisdiction.++4. Inability to Comply Due to Statute or Regulation+---------------------------------------------------++If it is impossible for You to comply with any of the terms of this+License with respect to some or all of the Covered Software due to+statute, judicial order, or regulation then You must: (a) comply with+the terms of this License to the maximum extent possible; and (b)+describe the limitations and the code they affect. Such description must+be placed in a text file included with all distributions of the Covered+Software under this License. Except to the extent prohibited by statute+or regulation, such description must be sufficiently detailed for a+recipient of ordinary skill to be able to understand it.++5. Termination+--------------++5.1. The rights granted under this License will terminate automatically+if You fail to comply with any of its terms. However, if You become+compliant, then the rights granted under this License from a particular+Contributor are reinstated (a) provisionally, unless and until such+Contributor explicitly and finally terminates Your grants, and (b) on an+ongoing basis, if such Contributor fails to notify You of the+non-compliance by some reasonable means prior to 60 days after You have+come back into compliance. Moreover, Your grants from a particular+Contributor are reinstated on an ongoing basis if such Contributor+notifies You of the non-compliance by some reasonable means, this is the+first time You have received notice of non-compliance with this License+from such Contributor, and You become compliant prior to 30 days after+Your receipt of the notice.++5.2. If You initiate litigation against any entity by asserting a patent+infringement claim (excluding declaratory judgment actions,+counter-claims, and cross-claims) alleging that a Contributor Version+directly or indirectly infringes any patent, then the rights granted to+You by any and all Contributors for the Covered Software under Section+2.1 of this License shall terminate.++5.3. In the event of termination under Sections 5.1 or 5.2 above, all+end user license agreements (excluding distributors and resellers) which+have been validly granted by You or Your distributors under this License+prior to termination shall survive termination.++************************************************************************+*                                                                      *+*  6. Disclaimer of Warranty                                           *+*  -------------------------                                           *+*                                                                      *+*  Covered Software is provided under this License on an "as is"       *+*  basis, without warranty of any kind, either expressed, implied, or  *+*  statutory, including, without limitation, warranties that the       *+*  Covered Software is free of defects, merchantable, fit for a        *+*  particular purpose or non-infringing. The entire risk as to the     *+*  quality and performance of the Covered Software is with You.        *+*  Should any Covered Software prove defective in any respect, You     *+*  (not any Contributor) assume the cost of any necessary servicing,   *+*  repair, or correction. This disclaimer of warranty constitutes an   *+*  essential part of this License. No use of any Covered Software is   *+*  authorized under this License except under this disclaimer.         *+*                                                                      *+************************************************************************++************************************************************************+*                                                                      *+*  7. Limitation of Liability                                          *+*  --------------------------                                          *+*                                                                      *+*  Under no circumstances and under no legal theory, whether tort      *+*  (including negligence), contract, or otherwise, shall any           *+*  Contributor, or anyone who distributes Covered Software as          *+*  permitted above, be liable to You for any direct, indirect,         *+*  special, incidental, or consequential damages of any character      *+*  including, without limitation, damages for lost profits, loss of    *+*  goodwill, work stoppage, computer failure or malfunction, or any    *+*  and all other commercial damages or losses, even if such party      *+*  shall have been informed of the possibility of such damages. This   *+*  limitation of liability shall not apply to liability for death or   *+*  personal injury resulting from such party's negligence to the       *+*  extent applicable law prohibits such limitation. Some               *+*  jurisdictions do not allow the exclusion or limitation of           *+*  incidental or consequential damages, so this exclusion and          *+*  limitation may not apply to You.                                    *+*                                                                      *+************************************************************************++8. Litigation+-------------++Any litigation relating to this License may be brought only in the+courts of a jurisdiction where the defendant maintains its principal+place of business and such litigation shall be governed by laws of that+jurisdiction, without reference to its conflict-of-law provisions.+Nothing in this Section shall prevent a party's ability to bring+cross-claims or counter-claims.++9. Miscellaneous+----------------++This License represents the complete agreement concerning the subject+matter hereof. If any provision of this License is held to be+unenforceable, such provision shall be reformed only to the extent+necessary to make it enforceable. Any law or regulation which provides+that the language of a contract shall be construed against the drafter+shall not be used to construe this License against a Contributor.++10. Versions of the License+---------------------------++10.1. New Versions++Mozilla Foundation is the license steward. Except as provided in Section+10.3, no one other than the license steward has the right to modify or+publish new versions of this License. Each version will be given a+distinguishing version number.++10.2. Effect of New Versions++You may distribute the Covered Software under the terms of the version+of the License under which You originally received the Covered Software,+or under the terms of any subsequent version published by the license+steward.++10.3. Modified Versions++If you create software not governed by this License, and you want to+create a new license for such software, you may create and use a+modified version of this License if you rename the license and remove+any references to the name of the license steward (except to note that+such modified license differs from this License).++10.4. Distributing Source Code Form that is Incompatible With Secondary+Licenses++If You choose to distribute Source Code Form that is Incompatible With+Secondary Licenses under the terms of this version of the License, the+notice described in Exhibit B of this License must be attached.++Exhibit A - Source Code Form License Notice+-------------------------------------------++  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/.++If it is not possible or desirable to put the notice in a particular+file, then You may include the notice in a location (such as a LICENSE+file in a relevant directory) where a recipient would be likely to look+for such a notice.++You may add additional accurate notices of copyright ownership.++Exhibit B - "Incompatible With Secondary Licenses" Notice+---------------------------------------------------------++  This Source Code Form is "Incompatible With Secondary Licenses", as+  defined by the Mozilla Public License, v. 2.0.
+ NOTICE view
@@ -0,0 +1,7 @@+NOTICE+======++Unless explicitly stated otherwise, all Source Code Forms+(recursively, including under subdirectories) contained in the directory+where this NOTICE file is located are subject to the terms of the+Mozilla Public License, v. 2.0.
+ README.md view
@@ -0,0 +1,95 @@+# Heftia+Heftia, a composition of hefty trees and co-Yoneda, is a higher-order effects+version of Freer.++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.++This library offers Heftia monads and Freer monads, encoded into data+types in several ways to enable tuning in pursuit of high performance.++Additionally, it's designed to operate as a handler system based+on [`classy-effects`](https://github.com/sayo-hs/classy-effects), which aims to+standardize and unify the definitions of effects in Haskell.++Compared to existing Effect System libraries in Haskell that handle higher-order effects, this+library's approach allows for a more effortless and flexible handling of higher-order effects. Here+are some examples:++* Two interpretations of the `censor` effect for Writer++    Let's consider the following Writer effectful program:++    ```hs+    hello :: (Writer String m, Monad m) => m ()+    hello = do+        tell "Hello"+        tell " world!"++    censorHello :: (Writer String m, Monad m) => m ()+    censorHello =+        censor+            (\s -> if s == "Hello" then "Goodbye" else s)+            hello+    ```++    For `censorHello`, should the final written string be `"Goodbye world!"`? Or should it be `"Hello world!"`?+    With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use.++    ```hs+    main :: IO ()+    main = runFreerEffects do+        (s :: String, _) <-+            interpretTell+                . runElaborate' (elaborateWriterT @String)+                $ censorHello++        (sTransactional :: String, _) <-+            interpretTell+                . runElaborate' (elaborateWriterTransactionalT @String)+                $ censorHello++        sendIns $ putStrLn $ "Normal: " <> s+        sendIns $ putStrLn $ "Transactional: " <> sTransactional+    ```++    Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!".+    For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).++* 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+    [Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/master/docs/examples/03%20Delimited%20Continuation.md>) .++Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being+eliminated.++Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).++## Documentation+Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.++## Future Plans+* Benchmarking+* Enriching the documentation+* Completing missing definitions such as+    * the Heftia monad transformer encoded in tree structure+    * handlers for the `Accum`, `Coroutine`, `Fresh`, `Input`, `Output` effect classes++    and others.++## License+The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/master/NOTICE).+Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed+under CC BY-SA 4.0.++## Your contributions are welcome!+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/master/CONTRIBUTING.md).
+ heftia.cabal view
@@ -0,0 +1,136 @@+cabal-version:      2.4+name:               heftia+version:            0.1.0.0++-- A short (one-line) description of the package.+synopsis: Higher-order version of Freer.++-- A longer description of the package.+description:+    Heftia, a composition of hefty trees and co-Yoneda, is a higher-order+    effects version of Freer.+    .+    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.+    .+    This library provides Heftia monads and Freer monads, encoded into data+    types in several ways to enable tuning in pursuit of high performance.+    .++-- 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>++-- A copyright notice.+copyright:+    2023 Yamada Ryo,+    2023 Casper Bach Poulsen and Cas van der Rest+category: Control, Monads++extra-source-files:+    ChangeLog.md+    NOTICE+    README.md++tested-with:+    GHC == 9.2.8++source-repository head+    type: git+    location: https://github.com/sayo-hs/heftia+    tag: v0.1.0+    subdir: heftia++library+    exposed-modules:+        Control.Freer+        Control.Freer.Trans+        Control.Heftia+        Control.Heftia.Trans+        Control.Monad.Trans.Freer+        Control.Monad.Trans.Freer.Tree+        Control.Monad.Trans.Freer.Church+        Control.Monad.Trans.Heftia+        Control.Monad.Trans.Heftia.Tree+        Control.Monad.Trans.Heftia.Church+        Control.Monad.Trans.Hefty+        Control.Effect.Freer+        Control.Effect.Heftia+        Data.Free.Union+        Data.Free.Extensible+        Data.Free.Sum+        Data.Hefty.Union+        Data.Hefty.Extensible+        Data.Hefty.Sum++    -- Modules included in this executable, other than Main.+    -- other-modules:++    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:+    build-depends:+        base                          ^>= 4.16.4.0,+        classy-effects-base           ^>= 0.1,+        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,++    hs-source-dirs:   src+    ghc-options:      -Wall+    default-language: GHC2021++    default-extensions:+        LambdaCase,+        DerivingStrategies,+        DataKinds,+        TypeFamilies,+        BlockArguments,+        FunctionalDependencies,+        RecordWildCards,+        DefaultSignatures,+        PatternSynonyms+++test-suite test+    main-is: Driver.hs+    hs-source-dirs: test+    build-depends:+        heftia,+        base,+        tasty                         ^>= 1.4,+        tasty-hunit                   ^>= 0.10,++    type: exitcode-stdio-1.0++    build-tool-depends:+        tasty-discover:tasty-discover++    default-language: GHC2021++    default-extensions:+        LambdaCase,+        DerivingStrategies,+        DataKinds,+        TypeFamilies,+        BlockArguments,+        FunctionalDependencies,+        RecordWildCards,+        DefaultSignatures,+        PatternSynonyms
+ src/Control/Effect/Freer.hs view
@@ -0,0 +1,632 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A Freer carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+module Control.Effect.Freer where++import Control.Applicative (Alternative)+import Control.Effect.Class (+    EffectDataHandler,+    EffectsVia (EffectsVia),+    Instruction,+    SendIns,+    Tag,+    getTag,+    runEffectsVia,+    sendIns,+    type (~>),+ )+import Control.Freer.Trans (+    TransFreer,+    hoistFreer,+    interposeLowerT,+    interpretFT,+    liftInsT,+    liftLowerFT,+    reinterpretFT,+    runInterpretF,+    transformT,+ )+import Control.Monad (MonadPlus)+import Control.Monad.Cont (ContT (ContT), runContT)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.Trans (MonadTrans, lift)+import Control.Monad.Trans.Freer (MonadTransFreer, interpretMK, interpretMT, reinterpretMK, reinterpretMT)+import Control.Monad.Trans.Freer.Church (FreerChurchT)+import Data.Coerce (Coercible, coerce)+import Data.Free.Extensible (ExtensibleUnion)+import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))+import Data.Free.Union (+    IsMember,+    Member,+    Union (+        absurdUnion,+        bundleUnion2,+        bundleUnion3,+        bundleUnion4,+        decomp,+        flipUnion,+        flipUnion3,+        flipUnionUnder,+        inject,+        inject0,+        project,+        rot3,+        rot3',+        unbundleUnion2,+        unbundleUnion3,+        unbundleUnion4,+        weaken,+        weaken2,+        weaken2Under,+        weaken2Under2,+        weaken3,+        weaken3Under,+        weaken4,+        weakenUnder,+        weakenUnder2,+        weakenUnder3+    ),+    (|+|:),+ )+import Data.Function ((&))+import Data.Kind (Type)++{- |+A data type that wraps Freer with any encoding to become an instance of 'SendIns' based on the+`liftInsT` from the `TransFreer` type class.+-}+newtype+    FreerUnion+        (fr :: Instruction -> (Type -> Type) -> Type -> Type)+        u+        (es :: [Instruction])+        f+        a = FreerUnion {runFreerUnion :: fr (u es) f a}+    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)+    deriving stock (Foldable, Traversable)++{- |+A Freer carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+type FreerEffects fr u es f = EffectsVia EffectDataHandler (FreerUnion fr u es f)++-- | Unwrap the `FreerEffects` wrapper.+unFreerEffects :: FreerEffects fr u es f ~> fr (u es) f+unFreerEffects = runFreerUnion . runEffectsVia+{-# INLINE unFreerEffects #-}++-- | Wrap with `FreerEffects`.+freerEffects :: fr (u es) f ~> FreerEffects fr u es f+freerEffects = EffectsVia . FreerUnion+{-# INLINE freerEffects #-}++{- |+A wrapper data type designed to induce instance resolution to delegate the search for effect classes+to a lower carrier @f@ even when there are no target effect classes in the effect class list @es@.++When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it+doesn't exist, it's induced to be @'False@.+-}+newtype FreerUnionForSend handleHere fr u es f a = FreerUnionForSend+    {runFreerUnionForSend :: FreerUnion fr u es f a}+    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)+    deriving stock (Foldable, Traversable)++instance+    SendIns e (FreerUnionForSend (e `IsMember` es) fr u es f) =>+    SendIns e (FreerUnion fr u es f)+    where+    sendIns = runFreerUnionForSend @(e `IsMember` es) . sendIns+    {-# INLINE sendIns #-}++instance+    (TransFreer c fr, Union u, Member u e es) =>+    SendIns e (FreerUnionForSend 'True fr u es f)+    where+    sendIns = FreerUnionForSend . FreerUnion . liftInsT . inject+    {-# INLINE sendIns #-}++instance (TransFreer c fr, SendIns e f, c f) => SendIns e (FreerUnionForSend 'False fr u es f) where+    sendIns = FreerUnionForSend . FreerUnion . liftLowerFT . sendIns+    {-# INLINE sendIns #-}++-- | Interpret the leading effect class in the effect class list.+interpret ::+    (TransFreer c fr, Union u, c f) =>+    (e ~> FreerEffects fr u es f) ->+    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f+interpret i =+    overFreerEffects $ interpretFT liftLowerFT \u ->+        case decomp u of+            Left e -> unFreerEffects $ i e+            Right e -> liftInsT e++-- | Interpret the leading effect class in the effect class list using a monad transformer.+interpretT ::+    forall t fr u e es f.+    (MonadTransFreer fr, Union u, MonadTrans t, Monad f, Monad (t (FreerEffects fr u es f))) =>+    (e ~> t (FreerEffects fr u es f)) ->+    FreerEffects fr u (e ': es) f ~> t (FreerEffects fr u es f)+interpretT i = interpretMT i . splitFreerEffects @_ @fr+{-# INLINE interpretT #-}++-- | Interpret the leading effect class in the effect class list using a delimited continuation.+interpretK ::+    (MonadTransFreer fr, Union u, Monad f) =>+    (a -> FreerEffects fr u es f r) ->+    (forall x. (x -> FreerEffects fr u es f r) -> e x -> FreerEffects fr u es f r) ->+    FreerEffects fr u (e ': es) f a ->+    FreerEffects fr u es f r+interpretK k i = (`runContT` k) . interpretContT \e -> ContT (`i` e)+{-# INLINE interpretK #-}++{- |+Interpret the leading effect class in the effect class list using a continuation monad transformer.+-}+interpretContT ::+    forall r fr u e es f.+    (MonadTransFreer fr, Union u, Monad f) =>+    (e ~> ContT r (FreerEffects fr u es f)) ->+    FreerEffects fr u (e ': es) f ~> ContT r (FreerEffects fr u es f)+interpretContT i = interpretMK i . splitFreerEffects @_ @fr+{-# INLINE interpretContT #-}++{- |+Interpret not only the leading effect class but also all the remaining effect classes and the+underlying carrier simultaneously, transforming them into any carrier @g@.+-}+interpretAll ::+    (TransFreer c fr, Union u, c f, c g) =>+    (f ~> g) ->+    (u es ~> g) ->+    (e ~> g) ->+    FreerEffects fr u (e ': es) f ~> g+interpretAll iLower iOther iTarget a =+    unFreerEffects a & interpretFT iLower \u ->+        case decomp u of+            Left e -> iTarget e+            Right e -> iOther e++-- | Reinterpret the leading effect class in the effect class list.+reinterpret ::+    (TransFreer c fr, Union u, c f) =>+    (e ~> FreerEffects fr u (e ': es) f) ->+    FreerEffects fr u (e ': es) f ~> FreerEffects fr u (e ': es) f+reinterpret i =+    overFreerEffects $ reinterpretFT \u ->+        case decomp u of+            Left e -> unFreerEffects $ i e+            Right e -> liftInsT $ weaken e++-- | Transform all effect classes in the effect class list into another union of effect classes.+transformAll ::+    (TransFreer c fr, Union u, Union u', c f) =>+    (u es ~> u' es') ->+    FreerEffects fr u es f ~> FreerEffects fr u' es' f+transformAll f = overFreerEffects $ transformT f+{-# INLINE transformAll #-}++-- | Transform the leading effect class in the effect class list into another effect class.+transform ::+    forall e' e fr u r f c.+    (TransFreer c fr, Union u, c f) =>+    (e ~> e') ->+    FreerEffects fr u (e ': r) f ~> FreerEffects fr u (e' ': r) f+transform f =+    overFreerEffects $ transformT \u ->+        case decomp u of+            Left e -> inject0 $ f e+            Right e -> weaken e++-- | Remove the tag attached to the effect class.+untag ::+    forall tag e fr u r f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (Tag e tag ': r) f ~> FreerEffects fr u (e ': r) f+untag = transform getTag++-- | Interpose the effect class that exists within the effect class list.+interpose ::+    forall e fr u es f c.+    (TransFreer c fr, Union u, Member u e es, c f) =>+    (e ~> FreerEffects fr u es f) ->+    FreerEffects fr u es f ~> FreerEffects fr u es f+interpose f =+    overFreerEffects $ reinterpretFT \u ->+        case project @_ @e u of+            Just e -> unFreerEffects $ f e+            Nothing -> liftInsT u++-- | Interpose the effect class that exists within the effect class list using a monad transformer.+interposeT ::+    forall e t fr u es m.+    ( MonadTransFreer fr+    , Union u+    , Member u e es+    , Monad m+    , MonadTrans t+    , forall m1 m2 x. Coercible m1 m2 => Coercible (t m1 x) (t m2 x)+    , Monad (t (fr (u es) m))+    ) =>+    (e ~> t (FreerEffects fr u es m)) ->+    FreerEffects fr u es m ~> t (FreerEffects fr u es m)+interposeT f a =+    hoistT @(fr (u es) m) $+        unFreerEffects a & reinterpretMT \u ->+            case project @_ @e u of+                Just e -> hoistT $ f e+                Nothing -> lift $ liftInsT u+  where+    hoistT :: Coercible (t m1 a) (t m2 a) => t m1 a -> t m2 a+    hoistT = coerce+    {-# INLINE hoistT #-}++{- |+Transform all other effect classes in the effect class list and the underlying carrier, along+with the effect class that exists within the effect class list, into any carrier @g@.+-}+interposeAll ::+    forall e g fr u es f c.+    ( TransFreer c fr+    , Union u+    , Member u e es+    , c f+    , c g+    ) =>+    (f ~> g) ->+    (u es ~> g) ->+    (e ~> g) ->+    FreerEffects fr u es f ~> g+interposeAll iLower iOther iTarget a =+    unFreerEffects a & interpretFT iLower \u ->+        case project @_ @e u of+            Just e -> iTarget e+            Nothing -> iOther u++{- |+Interpose the effect class that exists within the effect class list using a delimited continuation.+-}+interposeK ::+    (MonadTransFreer fr, Union u, Member u e es, Monad m) =>+    (a -> FreerEffects fr u es m r) ->+    (forall x. (x -> FreerEffects fr u es m r) -> e x -> FreerEffects fr u es m r) ->+    FreerEffects fr u es m a ->+    FreerEffects fr u es m r+interposeK k i = (`runContT` k) . interposeContT \e -> ContT (`i` e)+{-# INLINE interposeK #-}++{- |+Interpose the effect class that exists within the effect class list using a continuation monad+transformer.+-}+interposeContT ::+    forall e r fr u es m.+    (MonadTransFreer fr, Union u, Member u e es, Monad m) =>+    (e ~> ContT r (FreerEffects fr u es m)) ->+    FreerEffects fr u es m ~> ContT r (FreerEffects fr u es m)+interposeContT f a =+    hoistContT $+        unFreerEffects a & reinterpretMK \u ->+            case project @_ @e u of+                Just e -> hoistContT $ f e+                Nothing -> lift $ liftInsT u+  where+    hoistContT :: Coercible m1 m2 => ContT r m1 a -> ContT r m2 a+    hoistContT = coerce+    {-# INLINE hoistContT #-}++-- | Transform the effect of the effect class that exists within the effect class list.+intercept ::+    forall e fr u es f c.+    (TransFreer c fr, Union u, Member u e es, c f) =>+    (e ~> e) ->+    FreerEffects fr u es f ~> FreerEffects fr u es f+intercept f =+    overFreerEffects $ transformT \u ->+        case project @_ @e u of+            Just e -> inject $ f e+            Nothing -> u++-- | Insert an arbitrary effect class at the beginning of the effect class list.+raise ::+    forall e es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u es f ~> FreerEffects fr u (e ': es) f+raise = transformAll weaken+{-# INLINE raise #-}++-- | Insert two arbitrary effect classes at the beginning of the effect class list.+raise2 ::+    forall e1 e2 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': es) f+raise2 = transformAll weaken2+{-# INLINE raise2 #-}++-- | Insert three arbitrary effect classes at the beginning of the effect class list.+raise3 ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f+raise3 = transformAll weaken3+{-# INLINE raise3 #-}++-- | Insert four arbitrary effect classes at the beginning of the effect class list.+raise4 ::+    forall e1 e2 e3 e4 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f+raise4 = transformAll weaken4+{-# INLINE raise4 #-}++-- | Insert an arbitrary effect class below the leading effect class in the effect class list.+raiseUnder ::+    forall e1 e2 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f+raiseUnder = transformAll weakenUnder+{-# INLINE raiseUnder #-}++{- |+Insert an arbitrary effect class below the first two leading effect classes in the effect class+list.+-}+raiseUnder2 ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f+raiseUnder2 = transformAll weakenUnder2+{-# INLINE raiseUnder2 #-}++{- |+Insert an arbitrary effect class below the first three leading effect classes in the effect class list.+-}+raiseUnder3 ::+    forall e1 e2 e3 e4 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f+raiseUnder3 = transformAll weakenUnder3+{-# INLINE raiseUnder3 #-}++-- | Insert two arbitrary effect classes below the leading effect class in the effect class list.+raise2Under ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f+raise2Under = transformAll weaken2Under+{-# INLINE raise2Under #-}++{- |+Insert two arbitrary effect classes below the first two leading effect classes in the effect class list.+-}+raise2Under2 ::+    forall e1 e2 e3 e4 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f+raise2Under2 = transformAll weaken2Under2+{-# INLINE raise2Under2 #-}++-- | Inserts three arbitrary effect classes under the top effect class in the effect class list.+raise3Under ::+    forall e1 e2 e3 e4 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f+raise3Under = transformAll weaken3Under+{-# INLINE raise3Under #-}++-- | Swaps the top two effect classes in the effect class list.+flipFreer ::+    forall e1 e2 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e2 ': e1 ': es) f+flipFreer = transformAll flipUnion+{-# INLINE flipFreer #-}++-- | Reverses the order of the top three effect classes in the effect class list.+flipFreer3 ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e2 ': e1 ': es) f+flipFreer3 = transformAll flipUnion3+{-# INLINE flipFreer3 #-}++-- | Swaps the second and third effect classes from the top in the effect class list.+flipFreerUnder ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e3 ': e2 ': es) f+flipFreerUnder = transformAll flipUnionUnder+{-# INLINE flipFreerUnder #-}++-- | Rotates the top three effect classes in the effect class list to the left.+rotate3 ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e2 ': e3 ': e1 ': es) f+rotate3 = transformAll rot3+{-# INLINE rotate3 #-}++-- | Rotates the top three effect classes in the effect class list to the left twice.+rotate3' ::+    forall e1 e2 e3 es fr u f c.+    (TransFreer c fr, Union u, c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e1 ': e2 ': es) f+rotate3' = transformAll rot3'+{-# INLINE rotate3' #-}++-- | Bundles the top two effect classes in the effect class list into any open union.+bundle2 ::+    forall e1 e2 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (u' '[e1, e2] ': es) f+bundle2 = transformAll bundleUnion2+{-# INLINE bundle2 #-}++-- | Bundles the top three effect classes in the effect class list into any open union.+bundle3 ::+    forall e1 e2 e3 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3] ': es) f+bundle3 = transformAll bundleUnion3+{-# INLINE bundle3 #-}++-- | Bundles the top four effect classes in the effect class list into any open union.+bundle4 ::+    forall e1 e2 e3 e4 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f+bundle4 = transformAll bundleUnion4+{-# INLINE bundle4 #-}++-- | Expands the open union at the top of the effect class list.+unbundle2 ::+    forall e1 e2 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (u' '[e1, e2] ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f+unbundle2 = transformAll unbundleUnion2+{-# INLINE unbundle2 #-}++-- | Expands the open union at the top of the effect class list.+unbundle3 ::+    forall e1 e2 e3 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (u' '[e1, e2, e3] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f+unbundle3 = transformAll unbundleUnion3+{-# INLINE unbundle3 #-}++-- | Expands the open union at the top of the effect class list.+unbundle4 ::+    forall e1 e2 e3 e4 es fr u f c u'.+    (TransFreer c fr, Union u, Union u', c f) =>+    FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f+unbundle4 = transformAll unbundleUnion4+{-# INLINE unbundle4 #-}++{- |+Transforms the lower carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+hoistFreerEffects ::+    (TransFreer c fr, c f, c g) => (f ~> g) -> FreerEffects fr u es f ~> FreerEffects fr u es g+hoistFreerEffects f = overFreerEffects $ hoistFreer f+{-# INLINE hoistFreerEffects #-}++-- | Converts the lower carrier to an instruction.+lowerToIns ::+    (TransFreer c fr, c g, c (f + g), Union u) =>+    FreerEffects fr u es (f + g) ~> FreerEffects fr u (f ': es) g+lowerToIns =+    overFreerEffects $+        interpretFT+            (caseF (liftInsT . inject0) liftLowerFT)+            (liftInsT . weaken)+{-# INLINE lowerToIns #-}++-- | Converts the instruction to the lower carrier.+insToLower ::+    (TransFreer c fr, c (f + g), c g, Union u) =>+    FreerEffects fr u (f ': es) g ~> FreerEffects fr u es (f + g)+insToLower = overFreerEffects $ interpretFT (liftLowerFT . R1) (liftLowerFT . L1 |+|: liftInsT)+{-# INLINE insToLower #-}++{- |+Interprets the lower carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+interpretLower ::+    (TransFreer c fr, c f, c g) =>+    (f ~> FreerEffects fr u es g) ->+    FreerEffects fr u es f ~> FreerEffects fr u es g+interpretLower f = overFreerEffects $ interposeLowerT (unFreerEffects . f)+{-# INLINE interpretLower #-}++-- | Accesses the inside of the 'FreerEffects' wrapper.+overFreerEffects ::+    (fr (u es) f a -> fr' (u' es') g b) ->+    FreerEffects fr u es f a ->+    FreerEffects fr' u' es' g b+overFreerEffects f = freerEffects . f . unFreerEffects+{-# INLINE overFreerEffects #-}++-- | Drops a Freer with no effect classes to interpret to the lower carrier.+interpreted :: (TransFreer c fr, c f, Union u) => FreerEffects fr u '[] f ~> f+interpreted = runInterpretF absurdUnion . unFreerEffects+{-# INLINE interpreted #-}++-- | Splits the Freer into the lower carrier.+splitFreerEffects ::+    (TransFreer c fr', TransFreer c fr, c f, c (FreerEffects fr u es f), Union u) =>+    FreerEffects fr u (e ': es) f ~> fr' e (FreerEffects fr u es f)+splitFreerEffects a =+    unFreerEffects a & interpretFT (liftLowerFT . freerEffects . liftLowerFT) \u ->+        case decomp u of+            Left e -> liftInsT e+            Right e -> liftLowerFT $ freerEffects $ liftInsT e++-- | Transfer the effect to the underlying level.+subsume ::+    (TransFreer c fr, SendIns e (FreerEffects fr u es f), Union u, c f) =>+    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f+subsume = interpret sendIns+{-# INLINE subsume #-}++-- | Transfer the effect to the lower carrier.+subsumeLower ::+    (TransFreer c fr, SendIns e f, Union u, c f) =>+    FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f+subsumeLower = interpret $ liftLower . sendIns+{-# INLINE subsumeLower #-}++-- | Lifts the lower carrier.+liftLower :: (TransFreer c fr, c f) => f ~> FreerEffects fr u es f+liftLower = freerEffects . liftLowerFT+{-# INLINE liftLower #-}++-- | Embeds an IO action into a lower carrier that is a `MonadIO`.+runIO :: MonadIO m => Fre (IO ': es) m ~> Fre es m+runIO = interpret $ liftLower . liftIO+{-# INLINE runIO #-}++-- | Interprets all effects in the effect class list at once.+runInterpret :: (TransFreer c fr, c f) => (u es ~> f) -> FreerEffects fr u es f ~> f+runInterpret f = runInterpretF f . unFreerEffects+{-# INLINE runInterpret #-}++-- | Drops the Freer to the lower carrier.+runFreerEffects ::+    (TransFreer c fr, c f, Union u) =>+    FreerEffects fr u '[f] f ~> f+runFreerEffects = runInterpret $ id |+|: absurdUnion+{-# INLINE runFreerEffects #-}++-- | A type synonym for commonly used Monad Freer.+type Fre es f = FreerEffects FreerChurchT ExtensibleUnion es f++-- -- | Type synonym for commonly used Applicative Freer.+-- type FreA es f = FreerEffects (FreerFinalT Applicative) SumUnion es f++-- | An operator representing the membership relationship of the effect class list.+type e <| es = Member ExtensibleUnion e es
+ src/Control/Effect/Heftia.hs view
@@ -0,0 +1,760 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A Heftia carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+module Control.Effect.Heftia where++import Control.Applicative (Alternative)+import Control.Arrow ((>>>))+import Control.Effect.Class (+    EffectDataHandler,+    EffectsVia (EffectsVia),+    LiftIns (LiftIns),+    SendIns,+    SendSig,+    Signature,+    TagH,+    getTagH,+    runEffectsVia,+    sendIns,+    sendSig,+    unliftIns,+    type (~>),+ )+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)+import Control.Effect.Freer (FreerEffects, freerEffects, interpose, unFreerEffects)+import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)+import Control.Heftia.Trans (+    TransHeftia,+    elaborateHT,+    hoistHeftia,+    interpretLowerHT,+    liftLowerHT,+    liftSigT,+    reelaborateHT,+    runElaborateH,+    transformHT,+    translateT,+ )+import Control.Monad (MonadPlus)+import Control.Monad.Cont (ContT (ContT), MonadTrans, runContT)+import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, elaborateMT)+import Control.Monad.Trans.Heftia.Church (HeftiaChurchT)+import Data.Extensible.Class (Forall)+import Data.Free.Union (Member, Union, project)+import Data.Hefty.Extensible (ExtensibleUnionH)+import Data.Hefty.Union (+    IsMemberH,+    MemberH,+    UnionH (+        absurdUnionH,+        bundleUnion2H,+        bundleUnion3H,+        bundleUnion4H,+        decompH,+        flipUnion3H,+        flipUnionH,+        flipUnionUnderH,+        inject0H,+        injectH,+        projectH,+        rot3H,+        rot3H',+        unbundleUnion2H,+        unbundleUnion3H,+        unbundleUnion4H,+        weaken2H,+        weaken2Under2H,+        weaken2UnderH,+        weaken3H,+        weaken3UnderH,+        weaken4H,+        weakenH,+        weakenUnder2H,+        weakenUnder3H,+        weakenUnderH+    ),+    (|+:),+ )+import Data.Kind (Type)++{- |+A data type that wraps Heftia with any encoding to become an instance of 'SendIns'/'SendSig' based+on the `liftInsT` or `liftSigT` from the `TransFreer` or `TransHeftia` type class.+-}+newtype+    HeftiaUnion+        (h :: Signature -> (Type -> Type) -> Type -> Type)+        u+        (es :: [Signature])+        f+        a = HeftiaUnion {runHeftiaUnion :: h (u es) f a}+    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)+    deriving stock (Foldable, Traversable)++{- |+A Heftia carrier that can be used as a handler for effect systems based+on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).+-}+type HeftiaEffects h u es f = EffectsVia EffectDataHandler (HeftiaUnion h u es f)++-- | Unwrap the `HeftiaEffects` wrapper.+unHeftiaEffects :: HeftiaEffects h u es f ~> h (u es) f+unHeftiaEffects = runHeftiaUnion . runEffectsVia+{-# INLINE unHeftiaEffects #-}++-- | Wrap with `HeftiaEffects`.+heftiaEffects :: h (u es) f ~> HeftiaEffects h u es f+heftiaEffects = EffectsVia . HeftiaUnion+{-# INLINE heftiaEffects #-}++{- |+A wrapper data type designed to induce instance resolution to delegate the search for first-order+effect classes to a lower carrier @f@ even when there are no target effect classes in the effect+class list @es@.++When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it+doesn't exist, it's induced to be @'False@.+-}+newtype HeftiaUnionForSendIns handleHere h u es f a = HeftiaUnionForSendIns+    {runHeftiaUnionForSendIns :: HeftiaUnion h u es f a}+    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)+    deriving stock (Foldable, Traversable)++instance+    SendIns e (HeftiaUnionForSendIns (LiftIns e `IsMemberH` es) h u es f) =>+    SendIns e (HeftiaUnion h u es f)+    where+    sendIns = runHeftiaUnionForSendIns @(LiftIns e `IsMemberH` es) . sendIns+    {-# INLINE sendIns #-}++instance+    (TransHeftia c h, UnionH u, MemberH u (LiftIns e) es, HFunctor (u es)) =>+    SendIns e (HeftiaUnionForSendIns 'True h u es f)+    where+    sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftSigT . injectH . LiftIns+    {-# INLINE sendIns #-}++instance+    (TransHeftia c h, SendIns e f, c f, HFunctor (u es)) =>+    SendIns e (HeftiaUnionForSendIns 'False h u es f)+    where+    sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftLowerHT . sendIns+    {-# INLINE sendIns #-}++instance+    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es)) =>+    SendSig e (HeftiaUnion h u es f)+    where+    sendSig = HeftiaUnion . liftSigT . hfmap runHeftiaUnion . injectH+    {-# INLINE sendSig #-}++-- | Elaborate all effects in the effect class list at once.+runElaborate ::+    (TransHeftia c h, HFunctor (u es), c f, UnionH u) =>+    (u es f ~> f) ->+    HeftiaEffects h u es f ~> f+runElaborate f = runElaborateH f . unHeftiaEffects+{-# INLINE runElaborate #-}++-- | Elaborate all effects in the effect class list using a delimited continuation.+runElaborateK ::+    (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) =>+    (a -> m r) ->+    (forall x. (x -> m r) -> u es (ContT r m) x -> m r) ->+    HeftiaEffects h u es m a ->+    m r+runElaborateK k f = (`runContT` k) . runElaborateContT \e -> ContT (`f` e)+{-# INLINE runElaborateK #-}++{- |+Elaborate all effects in the effect class list using a continuation monad transformer.+-}+runElaborateContT ::+    (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) =>+    (u es (ContT r m) ~> ContT r m) ->+    HeftiaEffects h u es m ~> ContT r m+runElaborateContT f = elaborateMK f . unHeftiaEffects+{-# INLINE runElaborateContT #-}++{- |+Elaborate all effects in the effect class list using a monad transformer.+-}+runElaborateT ::+    (MonadTransHeftia h, HFunctor (u es), UnionH u, MonadTrans t, Monad m, Monad (t m)) =>+    (u es (t m) ~> t m) ->+    HeftiaEffects h u es m ~> t m+runElaborateT f = elaborateMT f . unHeftiaEffects+{-# INLINE runElaborateT #-}++{- |+Elaborate all effects in the effect class list and the underlying carrier simultaneously,+transforming them into any carrier @g@.+-}+elaborate ::+    (TransHeftia c h, HFunctor (u es), c f, UnionH u, c g) =>+    (f ~> g) ->+    (u es g ~> g) ->+    HeftiaEffects h u es f ~> g+elaborate f g = elaborateHT f g . unHeftiaEffects+{-# INLINE elaborate #-}++-- | Elaborate the leading effect class in the effect class list.+interpretH ::+    (TransHeftia c h, UnionH u, HFunctor (u es), HFunctor (u (e : es)), HFunctor e, c f) =>+    (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) ->+    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u es f+interpretH i =+    overHeftiaEffects $ elaborateHT liftLowerHT \u ->+        case decompH u of+            Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e+            Right e -> liftSigT e++-- | Re-elaborate the leading effect class in the effect class list.+reinterpretH ::+    (TransHeftia c h, UnionH u, HFunctor (u (e : es)), HFunctor e, c f) =>+    (e (HeftiaEffects h u (e ': es) f) ~> HeftiaEffects h u (e ': es) f) ->+    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u (e ': es) f+reinterpretH i =+    overHeftiaEffects $ reelaborateHT \u ->+        case decompH u of+            Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e+            Right e -> liftSigT $ weakenH e++-- | Transform all effect classes in the effect class list into another union of effect classes.+transformAllH ::+    ( TransHeftia c h+    , UnionH u+    , UnionH u'+    , HFunctor (u es)+    , HFunctor (u' es')+    , c f+    ) =>+    (forall g. u es g ~> u' es' g) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f+transformAllH f = overHeftiaEffects $ transformHT f+{-# INLINE transformAllH #-}++-- | Transform the leading effect class in the effect class list into another effect class.+transformH ::+    forall e' e h u r f c.+    ( TransHeftia c h+    , UnionH u+    , c f+    , HFunctor (u (e : r))+    , HFunctor (u (e' : r))+    ) =>+    (forall g. e g ~> e' g) ->+    HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f+transformH f = overHeftiaEffects $ translateT \u ->+    case decompH u of+        Left e -> inject0H $ f e+        Right e -> weakenH e++-- | Remove the tag attached to the effect class.+untagH ::+    forall tag e h u r f c.+    ( TransHeftia c h+    , UnionH u+    , c f+    , HFunctor (u (e : r))+    , HFunctor (u (TagH e tag : r))+    ) =>+    HeftiaEffects h u (TagH e tag ': r) f ~> HeftiaEffects h u (e ': r) f+untagH = transformH getTagH++-- | Transform the leading effect class in the effect class list into another effect class.+translate ::+    forall e' e h u r f c.+    ( TransHeftia c h+    , UnionH u+    , HFunctor (u (e : r))+    , HFunctor (u (e' : r))+    , HFunctor e+    , HFunctor e'+    , c f+    ) =>+    (e (HeftiaEffects h u (e' ': r) f) ~> e' (HeftiaEffects h u (e' ': r) f)) ->+    HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f+translate f =+    overHeftiaEffects $ translateT \u ->+        case decompH u of+            Left e -> inject0H $ hfmap unHeftiaEffects $ f $ hfmap heftiaEffects e+            Right e -> weakenH e++-- | Transform all effect classes in the effect class list into another union of effect classes.+translateAll ::+    ( TransHeftia c h+    , UnionH u+    , UnionH u'+    , HFunctor (u es)+    , HFunctor (u' es')+    , c f+    ) =>+    (u es (HeftiaEffects h u' es' f) ~> u' es' (HeftiaEffects h u' es' f)) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f+translateAll f =+    overHeftiaEffects $ translateT (hfmap unHeftiaEffects . f . hfmap heftiaEffects)+{-# INLINE translateAll #-}++-- | Interpose the effect class that exists within the effect class list using a monad transformer.+interposeH ::+    forall e h u es f c.+    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), c f) =>+    (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u es f+interposeH f =+    overHeftiaEffects $ reelaborateHT \u ->+        let u' = hfmap (interposeH f . heftiaEffects) u+         in case projectH @_ @e u' of+                Just e -> unHeftiaEffects $ f e+                Nothing -> liftSigT $ hfmap unHeftiaEffects u'++-- | Transform the effect of the effect class that exists within the effect class list.+interceptH ::+    forall e h u es f c.+    (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), HFunctor e, c f) =>+    (e (HeftiaEffects h u es f) ~> e (HeftiaEffects h u es f)) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u es f+interceptH f =+    overHeftiaEffects $ translateT \u ->+        let u' = hfmap (interceptH f . heftiaEffects) u+         in case projectH @_ @e u' of+                Just e -> injectH $ hfmap unHeftiaEffects $ f e+                Nothing -> hfmap unHeftiaEffects u'++-- | Insert an arbitrary effect class at the beginning of the effect class list.+raiseH ::+    forall e hs h u f c.+    ( TransHeftia c h+    , HFunctor (u hs)+    , HFunctor (u (e ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e ': hs) f+raiseH = transformAllH weakenH+{-# INLINE raiseH #-}++-- | Insert two arbitrary effect classes at the beginning of the effect class list.+raise2H ::+    forall e1 e2 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u hs)+    , HFunctor (u (e1 ': e2 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': hs) f+raise2H = transformAllH weaken2H+{-# INLINE raise2H #-}++-- | Insert three arbitrary effect classes at the beginning of the effect class list.+raise3H ::+    forall e1 e2 e3 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u hs)+    , HFunctor (u (e1 ': e2 ': e3 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f+raise3H = transformAllH weaken3H+{-# INLINE raise3H #-}++-- | Insert four arbitrary effect classes at the beginning of the effect class list.+raise4H ::+    forall e1 e2 e3 e4 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u hs)+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f+raise4H = transformAllH weaken4H+{-# INLINE raise4H #-}++-- | Insert an arbitrary effect class below the leading effect class in the effect class list.+raiseUnderH ::+    forall e1 e2 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': hs))+    , HFunctor (u (e1 ': e2 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': hs) f+raiseUnderH = transformAllH weakenUnderH+{-# INLINE raiseUnderH #-}++{- |+Insert an arbitrary effect class below the first two leading effect classes in the effect class+list.+-}+raiseUnder2H ::+    forall e1 e2 e3 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': hs))+    , HFunctor (u (e1 ': e2 ': e3 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f+raiseUnder2H = transformAllH weakenUnder2H+{-# INLINE raiseUnder2H #-}++{- |+Insert an arbitrary effect class below the first three leading effect classes in the effect class list.+-}+raiseUnder3H ::+    forall e1 e2 e3 e4 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': hs))+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f+raiseUnder3H = transformAllH weakenUnder3H+{-# INLINE raiseUnder3H #-}++-- | Insert two arbitrary effect classes below the leading effect class in the effect class list.+raise2UnderH ::+    forall e1 e2 e3 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': hs))+    , HFunctor (u (e1 ': e2 ': e3 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f+raise2UnderH = transformAllH weaken2UnderH+{-# INLINE raise2UnderH #-}++{- |+Insert two arbitrary effect classes below the first two leading effect classes in the effect class list.+-}+raise2Under2H ::+    forall e1 e2 e3 e4 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': hs))+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f+raise2Under2H = transformAllH weaken2Under2H+{-# INLINE raise2Under2H #-}++-- | Inserts three arbitrary effect classes under the top effect class in the effect class list.+raise3UnderH ::+    forall e1 e2 e3 e4 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': hs))+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f+raise3UnderH = transformAllH weaken3UnderH+{-# INLINE raise3UnderH #-}++-- | Swaps the top two effect classes in the effect class list.+flipHeftia ::+    forall e1 e2 hs h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': hs))+    , HFunctor (u (e2 ': e1 ': hs))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e2 ': e1 ': hs) f+flipHeftia = transformAllH flipUnionH+{-# INLINE flipHeftia #-}++-- | Reverses the order of the top three effect classes in the effect class list.+flipHeftia3 ::+    forall e1 e2 e3 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (e3 : e2 : e1 : es))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e2 ': e1 ': es) f+flipHeftia3 = transformAllH flipUnion3H+{-# INLINE flipHeftia3 #-}++-- | Swaps the second and third effect classes from the top in the effect class list.+flipHeftiaUnder ::+    forall e1 e2 e3 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (e1 : e3 : e2 : es))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e1 ': e3 ': e2 ': es) f+flipHeftiaUnder = transformAllH flipUnionUnderH+{-# INLINE flipHeftiaUnder #-}++-- | Rotates the top three effect classes in the effect class list to the left.+rotate3H ::+    forall e1 e2 e3 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (e2 : e3 : e1 : es))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e2 ': e3 ': e1 ': es) f+rotate3H = transformAllH rot3H+{-# INLINE rotate3H #-}++-- | Rotates the top three effect classes in the effect class list to the left twice.+rotate3H' ::+    forall e1 e2 e3 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (e3 : e1 : e2 : es))+    , c f+    , UnionH u+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e1 ': e2 ': es) f+rotate3H' = transformAllH rot3H'+{-# INLINE rotate3H' #-}++-- | Bundles the top two effect classes in the effect class list into any open union.+bundle2H ::+    forall u' e1 e2 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': es))+    , HFunctor (u (u' '[e1, e2] ': es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (e1 ': e2 ': es) f ~> HeftiaEffects h u (u' '[e1, e2] ': es) f+bundle2H = transformAllH bundleUnion2H+{-# INLINE bundle2H #-}++-- | Bundles the top three effect classes in the effect class list into any open union.+bundle3H ::+    forall u' e1 e2 e3 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (u' '[e1, e2, e3] : es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (u' '[e1, e2, e3] ': es) f+bundle3H = transformAllH bundleUnion3H+{-# INLINE bundle3H #-}++-- | Bundles the top four effect classes in the effect class list into any open union.+bundle4H ::+    forall u' e1 e2 e3 e4 es h u f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))+    , HFunctor (u (u' '[e1, e2, e3, e4] : es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f+        ~> HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f+bundle4H = transformAllH bundleUnion4H+{-# INLINE bundle4H #-}++-- | Expands the open union at the top of the effect class list.+unbundle2H ::+    forall e1 e2 es h u u' f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': es))+    , HFunctor (u (u' '[e1, e2] ': es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (u' '[e1, e2] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': es) f+unbundle2H = transformAllH unbundleUnion2H+{-# INLINE unbundle2H #-}++-- | Expands the open union at the top of the effect class list.+unbundle3H ::+    forall e1 e2 e3 es h u u' f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': es))+    , HFunctor (u (u' '[e1, e2, e3] ': es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (u' '[e1, e2, e3] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': es) f+unbundle3H = transformAllH unbundleUnion3H+{-# INLINE unbundle3H #-}++-- | Expands the open union at the top of the effect class list.+unbundle4H ::+    forall e1 e2 e3 e4 es h u u' f c.+    ( TransHeftia c h+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))+    , HFunctor (u (u' '[e1, e2, e3, e4] ': es))+    , c f+    , UnionH u+    , UnionH u'+    ) =>+    HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f+        ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f+unbundle4H = transformAllH unbundleUnion4H+{-# INLINE unbundle4H #-}++{- |+Transforms the lower carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+hoistHeftiaEffects ::+    (TransHeftia c h, HFunctor (u es), c f, c g) =>+    (f ~> g) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u es g+hoistHeftiaEffects f = overHeftiaEffects $ hoistHeftia f+{-# INLINE hoistHeftiaEffects #-}++-- | Accesses the inside of the 'HeftiaEffects' wrapper.+overHeftiaEffects ::+    (h (u es) f a -> h' (u' es') g b) ->+    HeftiaEffects h u es f a ->+    HeftiaEffects h' u' es' g b+overHeftiaEffects f = heftiaEffects . f . unHeftiaEffects+{-# INLINE overHeftiaEffects #-}++{- |+Interpose the lower Freer carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+hoistInterpose ::+    forall e h u es fr u' es' f c c'.+    ( TransHeftia c h+    , HFunctor (u es)+    , TransFreer c' fr+    , Union u'+    , Member u' e es'+    , c (FreerEffects fr u' es' f)+    , c' f+    ) =>+    (e ~> FreerEffects fr u' es' f) ->+    HeftiaEffects h u es (FreerEffects fr u' es' f)+        ~> HeftiaEffects h u es (FreerEffects fr u' es' f)+hoistInterpose f = hoistHeftiaEffects $ interpose f+{-# INLINE hoistInterpose #-}++{- |+Interpose the lower Freer carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+interposeLower ::+    forall e h u es fr u' es' f c c'.+    ( TransHeftia c h+    , HFunctor (u es)+    , TransFreer c' fr+    , Union u'+    , Member u' e es'+    , c (FreerEffects fr u' es' f)+    , c' f+    , c' (HeftiaEffects h u es (FreerEffects fr u' es' f))+    ) =>+    (e ~> HeftiaEffects h u es (FreerEffects fr u' es' f)) ->+    HeftiaEffects h u es (FreerEffects fr u' es' f)+        ~> HeftiaEffects h u es (FreerEffects fr u' es' f)+interposeLower f =+    interpretLowerH $+        unFreerEffects+            >>> interpretFT+                (liftLowerH . freerEffects . liftLowerFT)+                \u -> case project @_ @e u of+                    Just e -> f e+                    Nothing -> liftLowerH $ freerEffects $ liftInsT u++{- |+Interprets the lower carrier.++__Warning__: The given natural transformation must be a monad morphism+(see <https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html>).+If not, the result will be ill-behaved.+-}+interpretLowerH ::+    (c f, c g, TransHeftia c h, HFunctor (u es)) =>+    (f ~> HeftiaEffects h u es g) ->+    HeftiaEffects h u es f ~> HeftiaEffects h u es g+interpretLowerH f = overHeftiaEffects $ interpretLowerHT (unHeftiaEffects . f)+{-# INLINE interpretLowerH #-}++-- | Transfer the higher-order effect to the underlying level.+subsume ::+    ( TransHeftia c h+    , MemberH u e es+    , UnionH u+    , HFunctor e+    , HFunctor (u es)+    , HFunctor (u (e : es))+    , c f+    ) =>+    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u es f+subsume = interpretH $ heftiaEffects . liftSigT . hfmap unHeftiaEffects . injectH+{-# INLINE subsume #-}++-- | Lifts the lower carrier.+liftLowerH :: (TransHeftia c h, c f, HFunctor (u es)) => f ~> HeftiaEffects h u es f+liftLowerH = heftiaEffects . liftLowerHT+{-# INLINE liftLowerH #-}++-- | Drops a Heftia with no effect classes to elaborate to the lower carrier.+elaborated :: (TransHeftia c h, UnionH u, HFunctor (u '[]), c f) => HeftiaEffects h u '[] f ~> f+elaborated = runElaborateH absurdUnionH . unHeftiaEffects+{-# INLINE elaborated #-}++-- | Drops the Heftia to the lower carrier.+runHeftiaEffects ::+    (TransHeftia c h, HFunctor (u '[LiftIns f]), UnionH u, c f) =>+    HeftiaEffects h u '[LiftIns f] f ~> f+runHeftiaEffects = runElaborate $ unliftIns |+: absurdUnionH+{-# INLINE runHeftiaEffects #-}++-- | A type synonym for commonly used Monad Heftia.+type Hef es f = HeftiaEffects HeftiaChurchT ExtensibleUnionH es f++-- -- | Type synonym for commonly used Applicative Heftia.+-- type HefA es f = HeftiaEffects (HeftiaFinalT Applicative) SumUnionH es f++-- | An operator representing the membership relationship of the higher-order effect class list.+type e <<| es = MemberH ExtensibleUnionH e es++-- | A type synonym for functions that perform the elaboration of higher-order effects.+type Elaborator e f = e f ~> f++-- | A type synonym for frequently occurring constraints on a list of effect classes.+type ForallHFunctor = Forall HFunctor
+ src/Control/Freer.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE QuantifiedConstraints #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Freer carriers.+-}+module Control.Freer where++import Control.Applicative.Free (Ap, liftAp, runAp)+import Control.Effect.Class (type (~>))+import Data.Functor.Coyoneda (Coyoneda, hoistCoyoneda, liftCoyoneda, lowerCoyoneda)++-- | A type class to abstract away the encoding details of the Freer carrier.+class (forall ins. c (f ins)) => Freer c f | f -> c where+    {-# MINIMAL liftIns, (interpretF | retract, transformF) #-}++    -- | Lift a /instruction/ into a Freer carrier.+    liftIns :: ins a -> f ins a++    interpretF :: c m => (ins ~> m) -> f ins a -> m a+    interpretF i = retract . transformF i+    {-# INLINE interpretF #-}++    retract :: c m => f m a -> m a+    retract = interpretF id+    {-# INLINE retract #-}++    -- | Translate /instruction/s embedded in a Freer carrier.+    transformF ::+        (ins ~> ins') ->+        f ins a ->+        f ins' a+    transformF phi = interpretF $ liftIns . phi+    {-# INLINE transformF #-}++    reinterpretF :: (ins ~> f ins) -> f ins a -> f ins a+    reinterpretF = interpretF+    {-# INLINE reinterpretF #-}++instance Freer Functor Coyoneda where+    liftIns = liftCoyoneda+    interpretF i = lowerCoyoneda . hoistCoyoneda i+    {-# INLINE liftIns #-}+    {-# INLINE interpretF #-}++instance Freer Applicative Ap where+    liftIns = liftAp+    interpretF = runAp+    {-# INLINE liftIns #-}+    {-# INLINE interpretF #-}
+ src/Control/Freer/Trans.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE QuantifiedConstraints #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Freer carrier transformers.+-}+module Control.Freer.Trans where++import Control.Effect.Class (type (~>))+import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)+import Data.Free.Sum (pattern L1, pattern R1, type (+))++-- | A type class to abstract away the encoding details of the Freer carrier transformers.+class (forall ins f. c f => c (fr ins f)) => TransFreer c fr | fr -> c where+    {-# MINIMAL liftInsT, liftLowerFT, (hoistFreer, runInterpretF | interpretFT) #-}++    -- | Lift a /instruction/ into a Freer carrier transformer.+    liftInsT :: ins ~> fr ins f++    liftLowerFT :: forall ins f. c f => f ~> fr ins f++    -- | Translate /instruction/s embedded in a Freer carrier transformer.+    transformT :: c f => (ins ~> ins') -> fr ins f ~> fr ins' f+    transformT f = interpretFT liftLowerFT (liftInsT . f)+    {-# INLINE transformT #-}++    -- | Translate an underlying carrier.+    hoistFreer :: (c f, c g) => (f ~> g) -> fr ins f ~> fr ins g+    hoistFreer f = interpretFT (liftLowerFT . f) liftInsT+    {-# INLINE hoistFreer #-}++    interposeLowerT :: (c f, c g) => (f ~> fr ins g) -> fr ins f ~> fr ins g+    interposeLowerT f = interpretFT f liftInsT+    {-# INLINE interposeLowerT #-}++    runInterpretF :: c f => (ins ~> f) -> fr ins f a -> f a+    default runInterpretF :: (c f, c (IdentityT f)) => (ins ~> f) -> fr ins f a -> f a+    runInterpretF f = runIdentityT . interpretFT IdentityT (IdentityT . f)+    {-# INLINE runInterpretF #-}++    interpretFT :: (c f, c g) => (f ~> g) -> (ins ~> g) -> fr ins f ~> g+    interpretFT f i = runInterpretF i . hoistFreer f+    {-# INLINE interpretFT #-}++    reinterpretFT :: c f => (ins ~> fr ins f) -> fr ins f ~> fr ins f+    reinterpretFT = interpretFT liftLowerFT+    {-# INLINE reinterpretFT #-}++mergeFreer ::+    forall fr m ins ins' c.+    (TransFreer c fr, c m) =>+    fr ins (fr ins' m) ~> fr (ins + ins') m+mergeFreer = interpretFT (transformT @c R1) (liftInsT @c . L1)++splitFreer ::+    forall fr m ins ins' c.+    (TransFreer c fr, c m) =>+    fr (ins + ins') m ~> fr ins (fr ins' m)+splitFreer = interpretFT (liftLowerFT . liftLowerFT) \case+    L1 e -> liftInsT e+    R1 e -> liftLowerFT $ liftInsT e
+ src/Control/Heftia.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE QuantifiedConstraints #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Heftia carriers.+-}+module Control.Heftia where++import Control.Effect.Class (LiftIns, unliftIns, type (~>))+import Control.Effect.Class.Machinery.HFunctor (HFunctor)++-- | A type class to abstract away the encoding details of the Heftia carrier.+class (forall sig. HFunctor sig => c (h sig)) => Heftia c h | h -> c where+    {-# MINIMAL liftSig, interpretHH #-}++    -- | Lift a /signature/ into a Heftia carrier.+    liftSig :: HFunctor sig => sig (h sig) a -> h sig a++    interpretHH :: (c m, HFunctor sig) => (sig m ~> m) -> h sig a -> m a++    -- | Translate /signature/s embedded in a Heftia carrier.+    translateHH ::+        (HFunctor sig, HFunctor sig') =>+        (sig (h sig') ~> sig' (h sig')) ->+        h sig a ->+        h sig' a+    translateHH phi = interpretHH $ liftSig . phi+    {-# INLINE translateHH #-}++    reinterpretHH :: HFunctor sig => (sig (h sig) ~> h sig) -> h sig a -> h sig a+    reinterpretHH = interpretHH+    {-# INLINE reinterpretHH #-}++retractH :: (Heftia c h, c m) => h (LiftIns m) a -> m a+retractH = interpretHH unliftIns+{-# INLINE retractH #-}
+ src/Control/Heftia/Trans.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Eta reduce" #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Heftia carrier transformers.+-}+module Control.Heftia.Trans where++import Control.Effect.Class (LiftIns (LiftIns), unliftIns, type (~>))+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))+import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)+import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)++-- | A type class to abstract away the encoding details of the Heftia carrier transformers.+class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where+    {-# MINIMAL liftSigT, liftLowerHT, (hoistHeftia, runElaborateH | elaborateHT) #-}++    -- | Lift a /signature/ into a Heftia carrier transformer.+    liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a++    transformHT ::+        (c f, HFunctor sig, HFunctor sig') =>+        (forall g. sig g ~> sig' g) ->+        h sig f ~> h sig' f+    transformHT f = translateT f+    {-# INLINE transformHT #-}++    -- | Translate /signature/s embedded in a Heftia carrier transformer.+    translateT ::+        (c f, HFunctor sig, HFunctor sig') =>+        (sig (h sig' f) ~> sig' (h sig' f)) ->+        h sig f ~> h sig' f+    translateT f = elaborateHT liftLowerHT (liftSigT . f)+    {-# INLINE translateT #-}++    liftLowerHT :: forall sig f. (c f, HFunctor sig) => f ~> h sig f++    -- | Translate an underlying monad.+    hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f ~> h sig g+    hoistHeftia phi = elaborateHT (liftLowerHT . phi) liftSigT+    {-# INLINE hoistHeftia #-}++    interpretLowerHT :: (HFunctor sig, c f, c g) => (f ~> h sig g) -> h sig f ~> h sig g+    interpretLowerHT f = elaborateHT f liftSigT+    {-# INLINE interpretLowerHT #-}++    runElaborateH :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f ~> f+    default runElaborateH :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f ~> f+    runElaborateH f = runIdentityT . elaborateHT IdentityT (IdentityT . f . hfmap runIdentityT)+    {-# INLINE runElaborateH #-}++    elaborateHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f ~> g+    elaborateHT f i = runElaborateH i . hoistHeftia f+    {-# INLINE elaborateHT #-}++    reelaborateHT :: (c f, HFunctor sig) => (sig (h sig f) ~> h sig f) -> h sig f ~> h sig f+    reelaborateHT = elaborateHT liftLowerHT+    {-# INLINE reelaborateHT #-}++heftiaToFreer ::+    (TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>+    h (LiftIns ins) f ~> fr ins f+heftiaToFreer = elaborateHT liftLowerFT (liftInsT . unliftIns)+{-# INLINE heftiaToFreer #-}++freerToHeftia ::+    (TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f), c' (h (LiftIns ins) f), c f) =>+    fr ins f ~> h (LiftIns ins) f+freerToHeftia = interpretFT liftLowerHT (liftSigT . LiftIns)+{-# INLINE freerToHeftia #-}++mergeHeftia ::+    forall h m sig sig' a c.+    (HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>+    h sig (h sig' m) a ->+    h (sig :+: sig') m a+mergeHeftia = elaborateHT (translateT @c Inr) (liftSigT @c . Inl)
+ src/Control/Monad/Trans/Freer.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE QuantifiedConstraints #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Freer monad transformers.+-}+module Control.Monad.Trans.Freer where++import Control.Effect.Class (Instruction, type (~>))+import Control.Freer.Trans (TransFreer, hoistFreer, interpretFT, liftLowerFT)+import Control.Monad.Cont (ContT)+import Control.Monad.Trans (MonadTrans, lift)+import Data.Coerce (Coercible, coerce)+import Data.Kind (Type)++-- | A type class to abstract away the encoding details of the Freer monad transformers.+class+    (TransFreer Monad fr, forall ins. MonadTrans (fr ins)) =>+    MonadTransFreer fr+    where+    interpretMK :: Monad m => (ins ~> ContT r m) -> fr ins m ~> ContT r m+    interpretMK = interpretMT+    {-# INLINE interpretMK #-}++    reinterpretMK :: Monad m => (ins ~> ContT r (fr ins m)) -> fr ins m ~> ContT r (fr ins m)+    reinterpretMK = reinterpretMT+    {-# INLINE reinterpretMK #-}++    interpretMT :: (Monad m, MonadTrans t, Monad (t m)) => (ins ~> t m) -> fr ins m ~> t m+    interpretMT = interpretFT lift+    {-# INLINE interpretMT #-}++    reinterpretMT ::+        forall m t n ins.+        (Monad m, MonadTrans t, Coercible n (fr ins m), Monad (t n), Monad n) =>+        (ins ~> t n) ->+        fr ins m ~> t n+    reinterpretMT f = interpretMT f . hoistFreer (coerce . liftLowerFT @Monad @fr @ins)+    {-# INLINE reinterpretMT #-}++reinterpretTTViaFinal ::+    forall fr m t n ins.+    ( MonadTransFreer fr+    , Monad m+    , MonadTrans t+    , Coercible n (fr ins m)+    , Monad (t n)+    , Monad n+    ) =>+    (ins ~> t n) ->+    fr ins m ~> t n+reinterpretTTViaFinal = interpretFT $ lift . coerce . liftLowerFT @Monad @fr @ins+{-# INLINE reinterpretTTViaFinal #-}++newtype ViaLiftLower (fr :: Instruction -> (Type -> Type) -> Type -> Type) ins m a = ViaLiftLower+    {runViaLiftLower :: fr ins m a}+    deriving newtype (Functor, Applicative, Monad)+    deriving stock (Foldable, Traversable)++instance TransFreer Monad h => MonadTrans (ViaLiftLower h ins) where+    lift = ViaLiftLower . liftLowerFT+    {-# INLINE lift #-}
+ src/Control/Monad/Trans/Freer/Church.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE DerivingVia #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A Church-encoded Freer transformer.+-}+module Control.Monad.Trans.Freer.Church where++import Control.Effect.Class (Instruction, LiftIns (..))+import Control.Freer.Trans (TransFreer (hoistFreer, liftInsT, liftLowerFT, runInterpretF))+import Control.Heftia.Trans (TransHeftia (..), liftSigT)+import Control.Monad.Trans (MonadTrans)+import Control.Monad.Trans.Freer (+    MonadTransFreer (interpretMK, reinterpretMK),+    ViaLiftLower (ViaLiftLower),+ )+import Control.Monad.Trans.Heftia.Church (HeftiaChurchT (HeftiaChurchT))++-- | A Church-encoded Freer transformer.+newtype FreerChurchT (ins :: Instruction) f a = FreerChurchT+    {unFreerChurchT :: HeftiaChurchT (LiftIns ins) f a}++deriving newtype instance Functor (FreerChurchT ins m)+deriving newtype instance Applicative (FreerChurchT ins m)+deriving newtype instance Monad (FreerChurchT ins m)++instance TransFreer Monad FreerChurchT where+    liftInsT = FreerChurchT . liftSigT . LiftIns+    {-# INLINE liftInsT #-}++    liftLowerFT = FreerChurchT . liftLowerHT+    {-# INLINE liftLowerFT #-}++    runInterpretF i = runElaborateH (i . unliftIns) . unFreerChurchT+    {-# INLINE runInterpretF #-}++    hoistFreer phi = FreerChurchT . hoistHeftia phi . unFreerChurchT+    {-# INLINE hoistFreer #-}++deriving via ViaLiftLower FreerChurchT ins instance MonadTrans (FreerChurchT ins)++instance MonadTransFreer FreerChurchT where+    interpretMK f (FreerChurchT (HeftiaChurchT g)) = g $ f . unliftIns+    {-# INLINE interpretMK #-}++    reinterpretMK f = interpretMK f . hoistFreer liftLowerFT+    {-# INLINE reinterpretMK #-}
+ src/Control/Monad/Trans/Freer/Tree.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE DerivingVia #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A tree-structured encoded Freer transformer.+-}+module Control.Monad.Trans.Freer.Tree where++import Control.Applicative (Alternative)+import Control.Effect.Class (type (~>))+import Control.Freer (Freer, interpretF, liftIns)+import Control.Monad (MonadPlus)+import Control.Monad.Base (MonadBase)+import Control.Monad.Identity (Identity, runIdentity)+import Control.Monad.Trans (MonadIO, MonadTrans)+import Control.Monad.Trans.Free (FreeF (Free, Pure), FreeT (FreeT), MonadFree, liftF)+import Data.Functor.Coyoneda (Coyoneda (Coyoneda), liftCoyoneda)++-- | A tree-structured encoded Freer transformer.+newtype FreerTreeT f m a = FreerTreeT {unFreerTreeT :: FreeT (Coyoneda f) m a}+    deriving newtype+        ( Functor+        , Applicative+        , Monad+        , Alternative+        , MonadPlus+        , MonadBase b+        , MonadIO+        , MonadFail+        , Eq+        , Ord+        , Read+        , Show+        , MonadTrans+        )+    deriving stock (Foldable, Traversable)++newtype FreerTreeMonad m f a = FreerTreeMonad {unFreerTreeMonad :: FreerTreeT f m a}+    deriving newtype+        ( Functor+        , Applicative+        , Alternative+        , Monad+        , MonadPlus+        , MonadBase b+        , MonadIO+        , MonadFail+        , Eq+        , Ord+        , Read+        , Show+        )+    deriving stock (Foldable, Traversable)+    deriving (MonadFree (Coyoneda f)) via FreeT (Coyoneda f) m++liftInsTree :: Monad m => ins a -> FreerTreeT ins m a+liftInsTree = FreerTreeT . liftF . liftCoyoneda+{-# INLINE liftInsTree #-}++interpretTTree :: Monad n => (m ~> n) -> (ins ~> n) -> FreerTreeT ins m a -> n a+interpretTTree iLower i (FreerTreeT (FreeT m)) =+    iLower m >>= \case+        Pure x -> pure x+        Free (Coyoneda f e) -> i e >>= interpretTTree iLower i . FreerTreeT . f++type FreerTree = FreerTreeMonad Identity++instance Freer Monad FreerTree where+    liftIns = FreerTreeMonad . liftInsTree+    interpretF i = interpretTTree (pure . runIdentity) i . unFreerTreeMonad+    {-# INLINE liftIns #-}+    {-# INLINE interpretF #-}++-- todo: MonadTransFreer instance
+ src/Control/Monad/Trans/Heftia.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE QuantifiedConstraints #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class to abstract away the encoding details of the Heftia monad transformers.+-}+module Control.Monad.Trans.Heftia where++import Control.Effect.Class (Signature, type (~>))+import Control.Effect.Class.Machinery.HFunctor (HFunctor)+import Control.Heftia.Trans (TransHeftia, elaborateHT, hoistHeftia, liftLowerHT)+import Control.Monad.Cont (ContT)+import Control.Monad.Trans (MonadTrans, lift)+import Data.Coerce (Coercible, coerce)+import Data.Kind (Type)++-- | A type class to abstract away the encoding details of the Heftia monad transformers.+class+    (TransHeftia Monad h, forall sig. HFunctor sig => MonadTrans (h sig)) =>+    MonadTransHeftia h+    where+    elaborateMK ::+        (Monad m, HFunctor sig) =>+        (sig (ContT r m) ~> ContT r m) ->+        h sig m ~> ContT r m+    elaborateMK = elaborateMT+    {-# INLINE elaborateMK #-}++    reelaborateMK ::+        (Monad m, HFunctor sig) =>+        (sig (ContT r (h sig m)) ~> ContT r (h sig m)) ->+        h sig m ~> ContT r (h sig m)+    reelaborateMK = reelaborateMT+    {-# INLINE reelaborateMK #-}++    elaborateMT ::+        (Monad m, MonadTrans t, Monad (t m), HFunctor sig) =>+        (sig (t m) ~> t m) ->+        h sig m ~> t m+    elaborateMT = elaborateHT lift+    {-# INLINE elaborateMT #-}++    reelaborateMT ::+        forall m t n sig.+        (Monad m, MonadTrans t, Coercible n (h sig m), Monad (t n), Monad n, HFunctor sig) =>+        (sig (t n) ~> t n) ->+        h sig m ~> t n+    reelaborateMT f = elaborateMT f . hoistHeftia (coerce . liftLowerHT @Monad @h @sig)+    {-# INLINE reelaborateMT #-}++reinterpretHTTViaFinal ::+    forall h m t n sig.+    ( MonadTransHeftia h+    , Monad m+    , MonadTrans t+    , Coercible n (h sig m)+    , Monad (t n)+    , Monad n+    , HFunctor sig+    ) =>+    (sig (t n) ~> t n) ->+    h sig m ~> t n+reinterpretHTTViaFinal = elaborateHT $ lift . coerce . liftLowerHT @Monad @h @sig+{-# INLINE reinterpretHTTViaFinal #-}++newtype ViaLiftLowerH (h :: Signature -> (Type -> Type) -> Type -> Type) sig m a = ViaLiftLowerH+    {runViaLiftLowerH :: h sig m a}+    deriving newtype (Functor, Applicative, Monad)+    deriving stock (Foldable, Traversable)++instance (TransHeftia Monad h, HFunctor sig) => MonadTrans (ViaLiftLowerH h sig) where+    lift = ViaLiftLowerH . liftLowerHT+    {-# INLINE lift #-}
+ src/Control/Monad/Trans/Heftia/Church.hs view
@@ -0,0 +1,77 @@+-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A Church-encoded Heftia transformer.+-}+module Control.Monad.Trans.Heftia.Church where++import Control.Effect.Class (type (~>))+import Control.Effect.Class.Machinery.HFunctor (hfmap)+import Control.Heftia.Trans (TransHeftia (..))+import Control.Monad (join)+import Control.Monad.Trans (MonadTrans, lift)+import Control.Monad.Trans.Cont (ContT (ContT), runContT)+import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, reelaborateMK)++-- | A Church-encoded Heftia transformer.+newtype HeftiaChurchT h f a = HeftiaChurchT+    {unHeftiaChurchT :: forall r. (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a}+    deriving stock (Functor)++runHeftiaChurchT :: (h (HeftiaChurchT h f) ~> ContT r f) -> HeftiaChurchT h f b -> ContT r f b+runHeftiaChurchT i (HeftiaChurchT f) = f i++instance Applicative (HeftiaChurchT h f) where+    pure x = HeftiaChurchT \_ -> pure x+    {-# INLINE pure #-}++    HeftiaChurchT f <*> HeftiaChurchT g = HeftiaChurchT \i -> f i <*> g i+    {-# INLINE (<*>) #-}++instance Monad (HeftiaChurchT h f) where+    HeftiaChurchT f >>= k =+        HeftiaChurchT \i -> f i >>= runHeftiaChurchT i . k+    {-# INLINE (>>=) #-}++instance TransHeftia Monad HeftiaChurchT where+    liftSigT e = HeftiaChurchT \i -> i e+    {-# INLINE liftSigT #-}++    translateT phi (HeftiaChurchT f) =+        HeftiaChurchT \i ->+            f $ i . phi . hfmap (translateT phi)++    liftLowerHT a = HeftiaChurchT \_ -> lift a+    {-# INLINE liftLowerHT #-}++    hoistHeftia phi (HeftiaChurchT f) =+        HeftiaChurchT \i ->+            ContT \k ->+                join . phi $+                    runContT+                        ( f \e -> ContT \k' ->+                            pure $ runContT (i $ hfmap (hoistHeftia phi) e) (join . phi . k')+                        )+                        (pure . k)++    runElaborateH g (HeftiaChurchT f) =+        runContT (f $ lift . g . hfmap (runElaborateH g)) pure++instance MonadTrans (HeftiaChurchT h) where+    lift m = HeftiaChurchT \_ -> lift m+    {-# INLINE lift #-}++instance MonadTransHeftia HeftiaChurchT where+    elaborateMK f (HeftiaChurchT g) = g $ f . hfmap (elaborateMK f)+    {-# INLINE elaborateMK #-}++    reelaborateMK f = elaborateMK f . hoistHeftia liftLowerHT+    {-# INLINE reelaborateMK #-}
+ src/Control/Monad/Trans/Heftia/Tree.hs view
@@ -0,0 +1,20 @@+-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A tree-structured encoded Heftia transformer.+-}+module Control.Monad.Trans.Heftia.Tree where++import Data.Functor.Coyoneda (Coyoneda)++newtype HCoyoneda h f a = HCoyoneda {unHCoyoneda :: Coyoneda (h f) a}++-- todo
+ src/Control/Monad/Trans/Hefty.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+    Copyright : (c) 2023 Yamada Ryo+                (c) 2023 Casper Bach Poulsen and Cas van der Rest+    License : MPL-2.0 (see the file LICENSE)++    Maintainer : ymdfield@outlook.jp+    Stability : experimental+    Portability : portable++    The data structure of hefty trees.+-}+module Control.Monad.Trans.Hefty where++import Control.Monad (ap)+import Control.Monad.Identity (Identity (Identity), runIdentity)+import Control.Monad.Trans (MonadTrans, lift)+import Control.Monad.Trans.Free (FreeF (Free, Pure))+import Data.Functor ((<&>))++-- | A hefty monad transformer.+newtype HeftyT h m a = HeftyT {runHeftyT :: m (FreeF (h (HeftyT h m)) a (HeftyT h m a))}++instance (Functor m, Functor (h (HeftyT h m))) => Functor (HeftyT h m) where+    fmap f (HeftyT m) =+        HeftyT $+            m <&> \case+                Pure x -> Pure $ f x+                Free h -> Free $ fmap f <$> h++instance (Monad m, Functor (h (HeftyT h m))) => Applicative (HeftyT h m) where+    pure = HeftyT . pure . Pure+    (<*>) = ap++    {-# INLINE pure #-}+    {-# INLINE (<*>) #-}++instance (Monad m, Functor (h (HeftyT h m))) => Monad (HeftyT h m) where+    HeftyT m >>= k =+        HeftyT $+            m >>= \case+                Pure x -> runHeftyT $ k x+                Free h -> return $ Free $ (k =<<) <$> h++instance MonadTrans (HeftyT h) where+    lift = liftHefty+    {-# INLINE lift #-}++{- | Lift a computation to a hefty monad.++     Note that this is less constrained than MonadTrans's lift (this one only+    requires a Functor for underlying monad).+-}+liftHefty :: Functor m => m a -> HeftyT h m a+liftHefty = HeftyT . fmap Pure+{-# INLINE liftHefty #-}++-- | A hefty monad.+type Hefty h = HeftyT h Identity++hefty :: FreeF (h (Hefty h)) a (Hefty h a) -> Hefty h a+hefty = HeftyT . Identity+{-# INLINE hefty #-}++runHefty :: Hefty h a -> FreeF (h (Hefty h)) a (Hefty h a)+runHefty = runIdentity . runHeftyT+{-# INLINE runHefty #-}
+ src/Data/Free/Extensible.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++An implementation of an open union for first-order effects using+the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.+-}+module Data.Free.Extensible where++import Control.Effect.Class (Instruction)+import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)+import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))+import Data.Free.Union (+    Union (+        HasMembership,+        absurdUnion,+        inject,+        inject0,+        project,+        weaken,+        (|+|:)+    ),+ )+import Data.Proxy (Proxy (Proxy))+import GHC.TypeNats (KnownNat, Nat, natVal, type (+))+import Type.Membership (Membership, nextMembership)+import Unsafe.Coerce (unsafeCoerce)++{- |+An implementation of an open union for first-order effects using+the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.+-}+newtype ExtensibleUnion fs a = ExtensibleUnion {unExtensibleUnion :: fs :/ FieldApp a}++newtype FieldApp a (f :: Instruction) = FieldApp {unFieldApp :: f a}++instance Forall Functor fs => Functor (ExtensibleUnion fs) where+    fmap f =+        ExtensibleUnion+            . match+                ( htabulateFor @Functor Proxy \w ->+                    Match \e -> EmbedAt w $ FieldApp $ f <$> unFieldApp e+                )+            . unExtensibleUnion+    {-# INLINE fmap #-}++{- todo:+instance Forall Foldable fs => Foldable (ExtensibleUnion fs) where+instance Forall Traversable fs => Traversable (ExtensibleUnion fs) where+-}++instance Union ExtensibleUnion where+    type HasMembership _ f fs = KnownNat (TypeIndex fs f)++    inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp+    {-# INLINE inject #-}++    project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u+    {-# INLINE project #-}++    absurdUnion = exhaust . unExtensibleUnion+    {-# INLINE absurdUnion #-}++    inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp+    {-# INLINE inject0 #-}++    weaken (ExtensibleUnion (EmbedAt w e)) =+        ExtensibleUnion $ EmbedAt (nextMembership w) e+    {-# INLINE weaken #-}++    f |+|: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion+    {-# INLINE (|+|:) #-}++findFirstMembership :: forall xs x. KnownNat (TypeIndex xs x) => Membership xs x+findFirstMembership = unsafeMkMembership $ fromIntegral $ natVal @(TypeIndex xs x) Proxy+  where+    -- This hack may break if the membership package version gets updated.+    unsafeMkMembership :: Int -> Membership xs x+    unsafeMkMembership = unsafeCoerce++type family TypeIndex (xs :: [k]) (x :: k) :: Nat where+    TypeIndex (x ': xs) x = 0+    TypeIndex (y ': xs) x = 1 + TypeIndex xs x
+ src/Data/Free/Sum.hs view
@@ -0,0 +1,121 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++-- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest.++{- |+Copyright   :  (c) 2023 Yamada Ryo+               (c) 2023 Casper Bach Poulsen and Cas van der Rest+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++An implementation of an open union for first-order effects using recursively nested binary sums.+-}+module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1) where++import Control.Effect.Class (Instruction, NopI, type (~>))+import Data.Free.Union (HasMembership, Union, absurdUnion, comp, decomp, inject, project)+import GHC.Generics (type (:+:) (L1, R1))++infixr 6 +++-- | A type synonym for disambiguation to the sum on the higher-order side.+type (+) = (:+:)++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 :: (NopI + f) ~> f+absurdL = caseF \case {} id+{-# INLINE absurdL #-}++absurdR :: (f + NopI) ~> f+absurdR = caseF id \case {}+{-# INLINE absurdR #-}++swapSum :: (f + g) a -> (g + f) a+swapSum = caseF R1 L1+{-# INLINE swapSum #-}++type family Sum fs where+    Sum '[] = NopI+    Sum (f ': fs) = f :+: Sum fs++{- |+An implementation of an open union for first-order effects using recursively nested binary sums.+-}+newtype SumUnion fs a = SumUnion {unSumUnion :: Sum fs a}++deriving newtype instance Functor (SumUnion '[])+deriving newtype instance (Functor f, Functor (Sum fs)) => Functor (SumUnion (f ': fs))++deriving newtype instance Foldable (SumUnion '[])+deriving newtype instance (Foldable f, Foldable (Sum fs)) => Foldable (SumUnion (f ': fs))++deriving stock instance Traversable (SumUnion '[])+deriving stock instance (Traversable f, Traversable (Sum fs)) => Traversable (SumUnion (f ': fs))++instance Union SumUnion where+    type HasMembership _ f fs = f < Sum fs++    inject sig = SumUnion $ inj sig+    project (SumUnion sig) = proj sig++    absurdUnion = \case {}++    comp =+        SumUnion . \case+            Left x -> L1 x+            Right (SumUnion x) -> R1 x++    decomp (SumUnion sig) = case sig of+        L1 x -> Left x+        R1 x -> Right (SumUnion x)++    {-# INLINE inject #-}+    {-# INLINE project #-}+    {-# INLINE absurdUnion #-}++class isHead ~ f `IsHeadInsOf` g => SumMember isHead (f :: Instruction) g where+    injSum :: f a -> g a+    projSum :: g a -> Maybe (f a)++type family (f :: Instruction) `IsHeadInsOf` g where+    f `IsHeadInsOf` f + g = 'True+    _ `IsHeadInsOf` _ = 'False++type f < g = SumMember (IsHeadInsOf f g) f g++inj :: forall f g. f < g => f ~> g+inj = injSum @(IsHeadInsOf f g)++proj :: forall f g a. f < g => g a -> Maybe (f a)+proj = projSum++instance SumMember 'True f (f + g) where+    injSum = L1++    projSum = \case+        L1 x -> Just x+        R1 _ -> Nothing++    {-# INLINE injSum #-}+    {-# INLINE projSum #-}++instance (f `IsHeadInsOf` (g + h) ~ 'False, f < h) => SumMember 'False f (g + h) where+    injSum = R1 . inj+    projSum = \case+        L1 _ -> Nothing+        R1 x -> projSum x++    {-# INLINE injSum #-}+    {-# INLINE projSum #-}
+ src/Data/Free/Union.hs view
@@ -0,0 +1,150 @@+-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++{- |+Copyright   :  (c) 2023 Yamada Ryo+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++A type class representing a general open union for first-order effects, independent of the internal+implementation.+-}+module Data.Free.Union where++import Control.Effect.Class (Instruction, type (~>))+import Data.Kind (Constraint)++{- |+A type class representing a general open union for first-order effects, independent of the internal+implementation.+-}+class Union (u :: [Instruction] -> Instruction) where+    {-# MINIMAL inject, project, absurdUnion, (comp | (inject0, weaken), decomp | (|+|:)) #-}++    type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint++    inject :: HasMembership u f fs => f ~> u fs+    project :: HasMembership u f fs => u fs a -> Maybe (f a)++    absurdUnion :: u '[] a -> x++    comp :: Either (f a) (u fs a) -> u (f ': fs) a+    comp = \case+        Left x -> inject0 x+        Right x -> weaken x+    {-# INLINE comp #-}++    decomp :: u (f ': fs) a -> Either (f a) (u fs a)+    decomp = Left |+|: Right+    {-# INLINE decomp #-}++    infixr 5 |+|:+    (|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r+    (f |+|: g) u = case decomp u of+        Left x -> f x+        Right x -> g x+    {-# INLINE (|+|:) #-}++    inject0 :: f ~> u (f ': fs)+    inject0 = comp . Left+    {-# INLINE inject0 #-}++    injectUnder :: f2 ~> u (f1 ': f2 ': fs)+    injectUnder = weaken . inject0+    {-# INLINE injectUnder #-}++    injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs)+    injectUnder2 = weaken2 . inject0+    {-# INLINE injectUnder2 #-}++    injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs)+    injectUnder3 = weaken3 . inject0+    {-# INLINE injectUnder3 #-}++    weaken :: u fs a -> u (f ': fs) a+    weaken = comp . Right+    {-# INLINE weaken #-}++    weaken2 :: u fs a -> u (f1 ': f2 ': fs) a+    weaken2 = weaken . weaken+    {-# INLINE weaken2 #-}++    weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a+    weaken3 = weaken2 . weaken+    {-# INLINE weaken3 #-}++    weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a+    weaken4 = weaken3 . weaken+    {-# INLINE weaken4 #-}++    weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs)+    weakenUnder = inject0 |+|: weaken2++    weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs)+    weakenUnder2 = inject0 |+|: injectUnder |+|: weaken3++    weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)+    weakenUnder3 = inject0 |+|: injectUnder |+|: injectUnder2 |+|: weaken4++    weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs)+    weaken2Under = inject0 |+|: weaken3++    weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)+    weaken2Under2 = inject0 |+|: injectUnder |+|: weaken4++    weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)+    weaken3Under = inject0 |+|: weaken4++    flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs)+    flipUnion = injectUnder |+|: inject0 |+|: weaken2++    flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs)+    flipUnion3 = injectUnder2 |+|: injectUnder |+|: inject0 |+|: weaken3++    flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs)+    flipUnionUnder = inject0 |+|: injectUnder2 |+|: injectUnder |+|: weaken3++    rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs)+    rot3 = injectUnder2 |+|: inject0 |+|: injectUnder |+|: weaken3++    rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs)+    rot3' = injectUnder |+|: injectUnder2 |+|: inject0 |+|: weaken3++    bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs)+    bundleUnion2 = inject0 . inject0 |+|: inject0 . injectUnder |+|: weaken++    bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs)+    bundleUnion3 =+        (inject0 . inject0)+            |+|: (inject0 . injectUnder)+            |+|: (inject0 . injectUnder2)+            |+|: weaken++    bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs)+    bundleUnion4 =+        (inject0 . inject0)+            |+|: (inject0 . injectUnder)+            |+|: (inject0 . injectUnder2)+            |+|: (inject0 . injectUnder3)+            |+|: weaken++    unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs)+    unbundleUnion2 = (inject0 |+|: injectUnder |+|: absurdUnion) |+|: weaken2++    unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs)+    unbundleUnion3 = (inject0 |+|: injectUnder |+|: injectUnder2 |+|: absurdUnion) |+|: weaken3++    unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)+    unbundleUnion4 =+        (inject0 |+|: injectUnder |+|: injectUnder2 |+|: injectUnder3 |+|: absurdUnion)+            |+|: weaken4++type family IsMember (f :: Instruction) fs where+    IsMember f (f ': fs) = 'True+    IsMember f (_ ': fs) = IsMember f fs+    IsMember _ '[] = 'False++type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True)
+ src/Data/Hefty/Extensible.hs view
@@ -0,0 +1,79 @@+{-# 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 where++import Control.Effect.Class (Signature)+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)+import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)+import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))+import Data.Free.Extensible (TypeIndex, findFirstMembership)+import Data.Hefty.Union (+    UnionH (+        HasMembershipH,+        absurdUnionH,+        inject0H,+        injectH,+        projectH,+        weakenH,+        (|+:)+    ),+ )+import Data.Proxy (Proxy (Proxy))+import GHC.TypeNats (KnownNat)+import Type.Membership (nextMembership)++{- |+An implementation of an open union for higher-order effects using+the [extensible](https://hackage.haskell.org/package/extensible) package as a backend.+-}+newtype ExtensibleUnionH hs f a = ExtensibleUnionH {unExtensibleUnionH :: hs :/ FieldAppH f a}++newtype FieldAppH f a (h :: Signature) = FieldAppH {unFieldAppH :: h f a}++instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where+    hfmap f =+        ExtensibleUnionH+            . match+                ( htabulateFor @HFunctor Proxy \w ->+                    Match $ EmbedAt w . FieldAppH . hfmap f . unFieldAppH+                )+            . unExtensibleUnionH+    {-# INLINE hfmap #-}++-- todo: Functor, Foldable, Traversable instances++instance UnionH ExtensibleUnionH where+    type HasMembershipH _ h hs = KnownNat (TypeIndex hs h)++    injectH = ExtensibleUnionH . EmbedAt findFirstMembership . FieldAppH+    {-# INLINE injectH #-}++    projectH (ExtensibleUnionH u) = unFieldAppH <$> strikeAt findFirstMembership u+    {-# INLINE projectH #-}++    absurdUnionH = exhaust . unExtensibleUnionH+    {-# INLINE absurdUnionH #-}++    inject0H = ExtensibleUnionH . EmbedAt leadership . FieldAppH+    {-# INLINE inject0H #-}++    weakenH (ExtensibleUnionH (EmbedAt w e)) =+        ExtensibleUnionH $ EmbedAt (nextMembership w) e+    {-# INLINE weakenH #-}++    f |+: g = (f . unFieldAppH <:| g . ExtensibleUnionH) . unExtensibleUnionH+    {-# INLINE (|+:) #-}
+ src/Data/Hefty/Sum.hs view
@@ -0,0 +1,123 @@+{-# LANGUAGE UndecidableInstances #-}++-- This Source Code Form is subject to the terms of the Mozilla Public+-- License, v. 2.0. If a copy of the MPL was not distributed with this+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.++-- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest.++{- |+Copyright   :  (c) 2023 Yamada Ryo+               (c) 2023 Casper Bach Poulsen and Cas van der Rest+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+Stability   :  experimental+Portability :  portable++An implementation of an open union for higher-order effects using recursively nested binary sums.+-}+module Data.Hefty.Sum where++import Control.Effect.Class (NopS, Signature, type (~>))+import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))+import Data.Hefty.Union (HasMembershipH, UnionH, absurdUnionH, compH, decompH, injectH, projectH)++absurdLH :: (NopS :+: h) f ~> h f+absurdLH = caseH \case {} id+{-# INLINE absurdLH #-}++absurdRH :: (h :+: NopS) f ~> h f+absurdRH = caseH id \case {}+{-# INLINE absurdRH #-}++swapSumH :: (h1 :+: h2) f a -> (h2 :+: h1) f a+swapSumH = caseH Inr Inl+{-# INLINE swapSumH #-}++type family SumH hs where+    SumH '[] = NopS+    SumH (h ': hs) = h :+: SumH hs++{- |+An implementation of an open union for higher-order effects using recursively nested binary sums.+-}+newtype SumUnionH hs f a = SumUnionH {unSumUnionH :: SumH hs f a}++deriving newtype instance Functor (SumUnionH '[] f)+deriving newtype instance Foldable (SumUnionH '[] f)+deriving stock instance Traversable (SumUnionH '[] f)++{- Lack of instances of 'Data.Comp.Multi.Ops.:+:'.+ - Should we create a pullreq on the compdata package side?+ -}+{-+deriving newtype instance+    (Functor (h f), Functor (SumH hs f)) =>+    Functor (SumUnionH (h ': hs) f)++deriving newtype instance+    (Foldable (h f), Foldable (SumH hs f)) =>+    Foldable (SumUnionH (h ': hs) f)++deriving stock instance+    (Traversable (h f), Traversable (SumH hs f)) =>+    Traversable (SumUnionH (h ': hs) f)+-}++deriving newtype instance HFunctor (SumH hs) => HFunctor (SumUnionH hs)++instance UnionH SumUnionH where+    type HasMembershipH _ h hs = h << SumH hs++    injectH sig = SumUnionH $ injH sig+    projectH (SumUnionH sig) = projH sig++    absurdUnionH = \case {}++    compH =+        SumUnionH . \case+            Left x -> Inl x+            Right (SumUnionH x) -> Inr x++    decompH (SumUnionH sig) = case sig of+        Inl x -> Left x+        Inr x -> Right (SumUnionH x)++    {-# INLINE injectH #-}+    {-# INLINE projectH #-}+    {-# INLINE absurdUnionH #-}++class isHead ~ h1 `IsHeadSigOf` h2 => SumMemberH isHead (h1 :: Signature) h2 where+    injSumH :: h1 f a -> h2 f a+    projSumH :: h2 f a -> Maybe (h1 f a)++type family (h1 :: Signature) `IsHeadSigOf` h2 where+    f `IsHeadSigOf` f :+: g = 'True+    _ `IsHeadSigOf` _ = 'False++type h1 << h2 = SumMemberH (IsHeadSigOf h1 h2) h1 h2++injH :: forall h1 h2 f. h1 << h2 => h1 f ~> h2 f+injH = injSumH @(IsHeadSigOf h1 h2)++projH :: forall h1 h2 f a. h1 << h2 => h2 f a -> Maybe (h1 f a)+projH = projSumH++instance SumMemberH 'True f (f :+: g) where+    injSumH = Inl++    projSumH = \case+        Inl x -> Just x+        Inr _ -> Nothing++    {-# INLINE injSumH #-}+    {-# INLINE projSumH #-}++instance (f `IsHeadSigOf` (g :+: h) ~ 'False, f << h) => SumMemberH 'False f (g :+: h) where+    injSumH = Inr . injH+    projSumH = \case+        Inl _ -> Nothing+        Inr x -> projSumH x++    {-# INLINE injSumH #-}+    {-# INLINE projSumH #-}
+ src/Data/Hefty/Union.hs view
@@ -0,0 +1,157 @@+{-# 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 representing a general open union for higher-order effects, independent of the internal+implementation.+-}+module Data.Hefty.Union where++import Control.Effect.Class (Signature, type (~>))+import Data.Kind (Constraint)++{- |+A type class representing a general open union for higher-order effects, independent of the internal+implementation.+-}+class UnionH (u :: [Signature] -> Signature) where+    {-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-}++    type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint++    injectH :: HasMembershipH u h hs => h f ~> u hs f+    projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)++    absurdUnionH :: u '[] f a -> x++    compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a+    compH = \case+        Left x -> inject0H x+        Right x -> weakenH x+    {-# INLINE compH #-}++    decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)+    decompH = Left |+: Right+    {-# INLINE decompH #-}++    infixr 5 |+:+    (|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r+    (f |+: g) u = case decompH u of+        Left x -> f x+        Right x -> g x+    {-# INLINE (|+:) #-}++    inject0H :: h f ~> u (h ': hs) f+    inject0H = compH . Left+    {-# INLINE inject0H #-}++    injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f+    injectUnderH = weakenH . inject0H+    {-# INLINE injectUnderH #-}++    injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f+    injectUnder2H = weaken2H . inject0H+    {-# INLINE injectUnder2H #-}++    injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    injectUnder3H = weaken3H . inject0H+    {-# INLINE injectUnder3H #-}++    weakenH :: u hs f ~> u (h ': hs) f+    weakenH = compH . Right+    {-# INLINE weakenH #-}++    weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f+    weaken2H = weakenH . weakenH+    {-# INLINE weaken2H #-}++    weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f+    weaken3H = weaken2H . weakenH+    {-# INLINE weaken3H #-}++    weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    weaken4H = weaken3H . weakenH+    {-# INLINE weaken4H #-}++    weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f+    weakenUnderH = inject0H |+: weaken2H++    weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f+    weakenUnder2H = inject0H |+: injectUnderH |+: weaken3H++    weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    weakenUnder3H = inject0H |+: injectUnderH |+: injectUnder2H |+: weaken4H++    weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f+    weaken2UnderH = inject0H |+: weaken3H++    weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    weaken2Under2H = inject0H |+: injectUnderH |+: weaken4H++    weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    weaken3UnderH = inject0H |+: weaken4H++    flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f+    flipUnionH = injectUnderH |+: inject0H |+: weaken2H++    flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f+    flipUnion3H = injectUnder2H |+: injectUnderH |+: inject0H |+: weaken3H++    flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f+    flipUnionUnderH = inject0H |+: injectUnder2H |+: injectUnderH |+: weaken3H++    rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f+    rot3H = injectUnder2H |+: inject0H |+: injectUnderH |+: weaken3H++    rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f+    rot3H' = injectUnderH |+: injectUnder2H |+: inject0H |+: weaken3H++    bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f+    bundleUnion2H = inject0H . inject0H |+: inject0H . injectUnderH |+: weakenH++    bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f+    bundleUnion3H =+        (inject0H . inject0H)+            |+: (inject0H . injectUnderH)+            |+: (inject0H . injectUnder2H)+            |+: weakenH++    bundleUnion4H ::+        UnionH u' =>+        u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f+    bundleUnion4H =+        (inject0H . inject0H)+            |+: (inject0H . injectUnderH)+            |+: (inject0H . injectUnder2H)+            |+: (inject0H . injectUnder3H)+            |+: weakenH++    unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f+    unbundleUnion2H = (inject0H |+: injectUnderH |+: absurdUnionH) |+: weaken2H++    unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f+    unbundleUnion3H = (inject0H |+: injectUnderH |+: injectUnder2H |+: absurdUnionH) |+: weaken3H++    unbundleUnion4H ::+        UnionH u' =>+        u (u' '[h1, h2, h3, h4] ': hs) f+            ~> u (h1 ': h2 ': h3 ': h4 ': hs) f+    unbundleUnion4H =+        (inject0H |+: injectUnderH |+: injectUnder2H |+: injectUnder3H |+: absurdUnionH)+            |+: weaken4H++type family IsMemberH (h :: Signature) hs where+    IsMemberH h (h ': hs) = 'True+    IsMemberH h (_ ': hs) = IsMemberH h hs+    IsMemberH _ '[] = 'False++type MemberH u h hs = (HasMembershipH u h hs, IsMemberH h hs ~ 'True)
+ test/Driver.hs view
@@ -0,0 +1,5 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}++-- 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/.