diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -3,3 +3,8 @@ ## 0.1.0.0 -- 2023-09-18 * Initial public release. + +## 0.2.0.0 -- 2024-07-17 + +* Redesign from scratch. +* Released as a beta version. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,13 @@ -# Heftia -Heftia, a composition of hefty trees and co-Yoneda, is a higher-order effects -version of Freer. +# Heftia: higher-order effects done right for Haskell +[![Hackage](https://img.shields.io/hackage/v/heftia.svg?logo=haskell&label=heftia)](https://hackage.haskell.org/package/heftia) +[![Hackage](https://img.shields.io/hackage/v/heftia-effects.svg?logo=haskell&label=heftia-effects)](https://hackage.haskell.org/package/heftia-effects) + +Heftia is a higher-order effects version of Freer. + +This library provides "[continuation-based semantics](https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md)" for higher-order effects, the same as [lexi-lambda's eff](https://github.com/lexi-lambda/eff). +Instead of using the `IO` monad to implement delimited continuations for effects, Heftia internally uses `Freer` monad. + The paper * Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7, @@ -11,85 +17,205 @@ Hefty trees, proposed by the above paper, are extensions of free monads, allowing for a straightforward treatment of higher-order effects. -This library offers Heftia monads and Freer monads, encoded into data +This library offers Hefty monads and Freer monads, encoded into data types in several ways to enable tuning in pursuit of high performance. -Additionally, it's designed to operate as a handler system based -on [`classy-effects`](https://github.com/sayo-hs/classy-effects), which aims to -standardize and unify the definitions of effects in Haskell. +## Status +This library is currently in the beta stage. +There may be significant changes and potential bugs. + +**We are looking forward to your feedback!** + +## Getting Started +To run the [SemanticsZoo example](heftia-effects/Example/SemanticsZoo/Main.hs): +```console +$ git clone https://github.com/sayo-hs/heftia +$ cd heftia/heftia-effects +$ cabal run exe:SemanticsZoo +... +# State + Except +( evalState . runThrow . runCatch $ action ) = Right True +( runThrow . evalState . runCatch $ action ) = Right True + +# NonDet + Except +( runNonDet . runThrow . runCatch . runChooseH $ action1 ) = [Right True,Right False] +( runThrow . runNonDet . runCatch . runChooseH $ action1 ) = Right [True,False] +( runNonDet . runThrow . runCatch . runChooseH $ action2 ) = [Right False,Right True] +( runThrow . runNonDet . runCatch . runChooseH $ action2 ) = Right [False,True] + +# NonDet + Writer +( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = [(3,(3,True)),(4,(4,False))] +( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = (6,[(3,True),(4,False)]) + +[Note] All other permutations will cause type errors. +$ +``` + +## Example + Compared to existing Effect System libraries in Haskell that handle higher-order effects, this library's approach allows for a more effortless and flexible handling of higher-order effects. Here are some examples: -* Two interpretations of the `censor` effect for Writer +### Extracting Multi-shot Delimited Continuations - Let's consider the following Writer effectful program: +In handling higher-order effects, it's easy to work with **multi-shot delimited continuations**. +This enables an almost complete emulation of "Algebraic Effects and Handlers". +For more details, please refer to +the [example code](heftia-effects/Example/Continuation/Main.hs). - ```hs - hello :: (Writer String m, Monad m) => m () - hello = do - tell "Hello" - tell " world!" +### Two interpretations of the `censor` effect for Writer - censorHello :: (Writer String m, Monad m) => m () - censorHello = - censor - (\s -> if s == "Hello" then "Goodbye" else s) - hello - ``` +Let's consider the following Writer effectful program: - For `censorHello`, should the final written string be `"Goodbye world!"`? Or should it be `"Hello world!"`? - With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use. +```hs +hello :: (Tell String <: m, Monad m) => m () +hello = do + tell "Hello" + tell " world!" - ```hs - main :: IO () - main = runFreerEffects do - (s :: String, _) <- - interpretTell - . runElaborate' (elaborateWriterT @String) - $ censorHello +censorHello :: (Tell String <: m, WriterH String <<: m, Monad m) => m () +censorHello = + censor + ( \s -> + if s == "Hello" then + "Goodbye" + else if s == "Hello world!" then + "Hello world!!" + else + s + ) + hello +``` - (sTransactional :: String, _) <- - interpretTell - . runElaborate' (elaborateWriterTransactionalT @String) - $ censorHello +For `censorHello`, should the final written string be `"Goodbye world!"` (Pre-applying behavior) ? +Or should it be `"Hello world!!"` (Post-applying behavior) ? +With Heftia, **you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use**. - sendIns $ putStrLn $ "Normal: " <> s - sendIns $ putStrLn $ "Transactional: " <> sTransactional - ``` +```hs +main :: IO () +main = runEff do + (sPre, _) <- + runTell + . interpretRecH (elabWriterPre @String) + $ censorHello - Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!". - For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs). + (sPost, _) <- + runTell + . interpretRecH (elabWriterPost @String) + $ censorHello -* Extracting Multi-shot Delimited Continuations + liftIO $ putStrLn $ "Pre-applying: " <> sPre + liftIO $ putStrLn $ "Post-applying: " <> sPost +``` - In handling higher-order effects, it's easy to work with multi-shot delimited continuations. - This enables an almost complete emulation of "Algebraic Effects and Handlers". - For more details, please refer to - [Example 3 - Delimited Continuation]() . +Using the `elabWriterPre` elaborator, you'll get "Goodbye world!", whereas with the `elabWriterPost` elaborator, you'll get "Hello world!!". +``` +Pre-applying: Goodbye world! +Post-applying: Hello world!! +``` +For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs). + Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being eliminated. -Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs). +Additionally, Heftia supports not only monadic effectful programs but also **applicative effectful programs**. +This may be useful when writing concurrent effectful code. +Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs). + ## Documentation -Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory. +The example codes are located in the [heftia-effects/Example/](heftia-effects/Example/) directory. +Also, the following *HeftWorld* example: https://github.com/sayo-hs/HeftWorld +~~Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.~~ Documents have become outdated. +Please wait for the documentation for the new version to be written. + +## Limitation and how to avoid it +### The *reset* behavior of the scopes held by unhandled higher-order effects +When attempting to interpret an effect while there are unhandled higher-order effects present, you cannot obtain delimited continuations beyond the action scope held by these unhandled higher-order effects. +It appears as if a *reset* (in the sense of *shift/reset*) is applied to each of the scopes still held by the remaining unhandled higher-order effects. + +In other words, to obtain delimited continuations beyond their scope, it is necessary to first handle and eliminate all higher-order effects that hold those scopes, +and then handle the effect targeted for stateful interpretation in that order. +For this purpose, it might sometimes be possible to use *multi-layering*. For an example of multi-layering, +see `handleReaderThenShift` defined in [Example/Continuation2](https://github.com/sayo-hs/heftia/blob/8f71a2d4e6125018b64cbbacd32151565a29046d/heftia-effects/Example/Continuation2/Main.hs) +(particularly, the type signature of `prog` within it). +For more details, please refer to the documentation of the `interpretRec` family of functions. + +## Comparison + +* Higher-Order Effects: Does it support higher-order effects? +* Delimited Continuation: The ability to manipulate delimited continuations. +* Statically Typed Set of Effects: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce? +* Purely Monadic: Is an effectful program represented as a transparent data structure that is a monad, and can it be interpreted into other data types using only pure operations without side effects or `unsafePerformIO`? +* Dynamic Effect Rewriting: Can an effectful program have its internal effects altered afterwards (by functions typically referred to as `handle with`, `intercept`, `interpose`, `transform`, `translate`, or `rewrite`) ? +* Performance: Time complexity or space complexity. + +| Library or Language | Higher-Order Effects | Delimited Continuation | Statically Typed Set of Effects | Purely Monadic | Dynamic Effect Rewriting | Performance (TODO) | +| ------------------- | -------------------- | ---------------------- | ----------------------------------------------- | --------------------------------- | ------------------------ | ------------------ | +| Heftia | Yes [^1] | Multi-shot | Yes | Yes (also Applicative and others) | Yes | ? | +| freer-simple | No | Multi-shot | Yes | Yes | Yes | ? | +| Polysemy | Yes | No | Yes | Yes | Yes | ? | +| Effectful | Yes | No | Yes | No (based on the `IO` monad) | Yes | ? | +| eff | Yes | Multi-shot? | Yes | No (based on the `IO` monad) | Yes | Fast | +| mtl | Yes | Multi-shot (`ContT`) | Yes | Yes | No | ? | +| fused-effects | Yes | No? | Yes | Yes | No | ? | +| koka-lang | No? | Multi-shot | Yes | No (language built-in) | ? | ? | +| OCaml-lang 5 | Yes | One-shot | No [^2] | No (language built-in) | ? | ? | + +[^1]: limitation: https://github.com/sayo-hs/heftia?tab=readme-ov-file#the-reset-behavior-of-the-scopes-held-by-unhandled-higher-order-effects +[^2]: potential for 'unhandled' runtime errors + +Heftia can simply be described as a higher-order version of freer-simple. +This is indeed true in terms of its internal mechanisms as well. + +### Compatibility with other libraries +#### Representation of effects +* Heftia Effects relies on [data-effects](https://github.com/sayo-hs/data-effects) for the definitions of standard effects such as `Reader`, `Writer`, and `State`. + +* It is generally recommended to use effects defined with automatic derivation provided by [data-effects-th](https://github.com/sayo-hs/data-effects/tree/develop/data-effects-th). + +* The representation of first-order effects is compatible with freer-simple. + Therefore, effects defined for freer-simple can be used as is in this library. + However, to avoid confusion between redundantly defined effects, + it is recommended to use the effects defined in [data-effects](https://github.com/sayo-hs/data-effects). + +* GADTs for higher-order effects need to be instances of the [HFunctor](https://hackage.haskell.org/package/compdata-0.13.1/docs/Data-Comp-Multi-HFunctor.html#t:HFunctor) type class for convenient usage. + While it is still possible to use them without being instances of `HFunctor`, + the `interpretRec` family of functions cannot be used when higher-order effects that are not `HFunctor` are unhandled. + If this issue is not a concern, the GADT representation of higher-order effects is compatible with Polysemy and fused-effects. + It is not compatible with Effectful and eff. + +#### About mtl +* Since the representation of effectful programs in Heftia is simply a monad (`Eff`), it can be used as the base monad for transformers. + This means you can stack any transformer on top of it. + +* The `Eff` monad is an instance of `MonadIO`, `MonadError`, `MonadRWS`, etc., and these behave as the senders for the embedded `IO` or the effect GADTs defined in [data-effects](https://github.com/sayo-hs/data-effects). + ## Future Plans -* Benchmarking -* Enriching the documentation +* Enriching the documentation and tests * Completing missing definitions such as - * the Heftia monad transformer encoded in tree structure - * handlers for the `Accum`, `Coroutine`, `Fresh`, `Input`, `Output` effect classes + * `raise`, `raiseUnder`, and `subsume` for arbitrary numbers of effects by type classes. + * more patterns of interpret & transform function-families. + * handlers for the `Accum` and others effect classes and others. +* Benchmarking ## License -The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/master/NOTICE). +The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/develop/NOTICE). Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed under CC BY-SA 4.0. ## Your contributions are welcome! -Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/master/CONTRIBUTING.md). +Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md). + +## Credits +Parts of this project have been inspired by the following resources: + +* **[Hefty Algebras -- The Artifact](https://github.com/heft-lang/POPL2023)** + * **Copyright** (c) 2023 Casper Bach Poulsen and Cas van der Rest + * **License**: MIT diff --git a/heftia.cabal b/heftia.cabal --- a/heftia.cabal +++ b/heftia.cabal @@ -1,15 +1,19 @@ cabal-version: 2.4 name: heftia -version: 0.1.0.0 +version: 0.2.0.0 -- A short (one-line) description of the package. -synopsis: Higher-order version of Freer. +synopsis: higher-order effects done right -- A longer description of the package. description: - Heftia, a composition of hefty trees and co-Yoneda, is a higher-order - effects version of Freer. + Heftia is a higher-order effects version of Freer. . + This library provides "[continuation-based semantics](https://github.com/lexi-lambda/eff/blob/master/notes/semantics-zoo.md)" + for higher-order effects, the same as [lexi-lambda's eff](https://github.com/lexi-lambda/eff). + Instead of using the @IO@ monad to implement delimited continuations for effects, + Heftia internally uses @Freer@ monad. + . The paper . * Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular @@ -20,7 +24,7 @@ Hefty trees, proposed by the above paper, are extensions of free monads, allowing for a straightforward treatment of higher-order effects. . - This library provides Heftia monads and Freer monads, encoded into data + This library provides Hefty monads and Freer monads, encoded into data types in several ways to enable tuning in pursuit of high performance. . @@ -35,8 +39,7 @@ -- A copyright notice. copyright: - 2023 Yamada Ryo, - 2023 Casper Bach Poulsen and Cas van der Rest + 2023-2024 Yamada Ryo category: Control, Monads extra-source-files: @@ -50,31 +53,42 @@ source-repository head type: git location: https://github.com/sayo-hs/heftia - tag: v0.1.0 + tag: v0.2.0 subdir: heftia library exposed-modules: + Control.Effect.Hefty + Control.Effect.Free + Control.Effect.ExtensibleFinal + Control.Effect.ExtensibleChurch + Control.Effect.ExtensibleTree + Control.Effect.ExtensibleFinalA + Control.Effect.ExtensibleTreeA + Control.Effect.ExtensibleFastA + Control.Hefty Control.Freer - Control.Freer.Trans - Control.Heftia - Control.Heftia.Trans - Control.Monad.Trans.Freer - Control.Monad.Trans.Freer.Tree - Control.Monad.Trans.Freer.Church - Control.Monad.Trans.Heftia - Control.Monad.Trans.Heftia.Tree - Control.Monad.Trans.Heftia.Church - Control.Monad.Trans.Hefty - Control.Effect.Freer - Control.Effect.Heftia - Data.Free.Union - Data.Free.Extensible - Data.Free.Sum + Control.Freer.Final + Control.Monad.Freer + Control.Monad.Freer.Church + Control.Monad.Freer.Tree Data.Hefty.Union Data.Hefty.Extensible - Data.Hefty.Sum + Data.Free.Sum + reexported-modules: + Data.Effect, + Data.Effect.TH, + Data.Effect.Tag, + Data.Effect.Key, + Data.Effect.Key.TH, + Data.Effect.HFunctor, + Data.Effect.HFunctor.HCont, + Data.Effect.HFunctor.TH, + Control.Effect, + Control.Effect.Tag, + Control.Effect.Key, + -- Modules included in this executable, other than Main. -- other-modules: @@ -82,7 +96,7 @@ -- other-extensions: build-depends: base ^>= 4.16.4.0, - classy-effects-base ^>= 0.1, + data-effects ^>= 0.1, mtl ^>= 2.2.2, free ^>= 5.2, kan-extensions ^>= 5.2.5, @@ -91,6 +105,9 @@ transformers ^>= 0.5.6, extensible ^>= 0.9, membership == 0.0.1, + singletons-base ^>= 3.1, + singletons-th ^>= 3.1, + unliftio ^>= 0.2, hs-source-dirs: src ghc-options: -Wall diff --git a/src/Control/Effect/ExtensibleChurch.hs b/src/Control/Effect/ExtensibleChurch.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleChurch.hs @@ -0,0 +1,43 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the Church-encoded Freer monad. +-} +module Control.Effect.ExtensibleChurch where + +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Control.Monad.Freer.Church (FreerChurch) +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion FreerChurch eh ef +type (!) ef = EffectfulF ExtensibleUnion FreerChurch ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion FreerChurch ehs efs +type (:!) efs = EffF ExtensibleUnion FreerChurch efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Monad f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Monad f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/ExtensibleFastA.hs b/src/Control/Effect/ExtensibleFastA.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleFastA.hs @@ -0,0 +1,45 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the fast-encoded free applicative. + +See "Control.Applicative.Free.Fast". +-} +module Control.Effect.ExtensibleFastA where + +import Control.Applicative.Free.Fast (Ap) +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion Ap eh ef +type (!) ef = EffectfulF ExtensibleUnion Ap ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion Ap ehs efs +type (:!) efs = EffF ExtensibleUnion Ap efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Applicative f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/ExtensibleFinal.hs b/src/Control/Effect/ExtensibleFinal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleFinal.hs @@ -0,0 +1,43 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the final-encoded Freer monad. +-} +module Control.Effect.ExtensibleFinal where + +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Control.Freer.Final (FreerFinal) +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion (FreerFinal Monad) eh ef +type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Monad) ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Monad) ehs efs +type (:!) efs = EffF ExtensibleUnion (FreerFinal Monad) efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Monad f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Monad f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/ExtensibleFinalA.hs b/src/Control/Effect/ExtensibleFinalA.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleFinalA.hs @@ -0,0 +1,43 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the final-encoded Freer applicative. +-} +module Control.Effect.ExtensibleFinalA where + +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Control.Freer.Final (FreerFinal) +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion (FreerFinal Applicative) eh ef +type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Applicative) ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Applicative) ehs efs +type (:!) efs = EffF ExtensibleUnion (FreerFinal Applicative) efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Applicative f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/ExtensibleTree.hs b/src/Control/Effect/ExtensibleTree.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleTree.hs @@ -0,0 +1,43 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the tree-structured encoded Freer monad. +-} +module Control.Effect.ExtensibleTree where + +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Control.Monad.Freer.Tree (FreerTree) +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion FreerTree eh ef +type (!) ef = EffectfulF ExtensibleUnion FreerTree ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion FreerTree ehs efs +type (:!) efs = EffF ExtensibleUnion FreerTree efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Monad f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Monad f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/ExtensibleTreeA.hs b/src/Control/Effect/ExtensibleTreeA.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/ExtensibleTreeA.hs @@ -0,0 +1,46 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +Type operators for extensible effectful programs based on the tree-structured encoded free +applicative. + +See "Control.Applicative.Free". +-} +module Control.Effect.ExtensibleTreeA where + +import Control.Applicative.Free (Ap) +import Control.Effect (type (~>)) +import Control.Effect.Free (EffF, EffectfulF) +import Control.Effect.Free qualified as F +import Control.Effect.Hefty (Eff, Effectful) +import Control.Effect.Hefty qualified as H +import Data.Effect (LiftIns) +import Data.Hefty.Extensible (ExtensibleUnion) + +type eh !! ef = Effectful ExtensibleUnion Ap eh ef +type (!) ef = EffectfulF ExtensibleUnion Ap ef + +infixr 5 !! +infixr 4 ! + +type ehs :!! efs = Eff ExtensibleUnion Ap ehs efs +type (:!) efs = EffF ExtensibleUnion Ap efs + +infixr 4 :!! +infixr 3 :! + +runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f +runEff = H.runEff +{-# INLINE runEff #-} + +runEffF :: Applicative f => (:!) '[LiftIns f] ~> f +runEffF = F.runEffF +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/Free.hs b/src/Control/Effect/Free.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/Free.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +A Freer carrier that can be used as a handler for effect systems based +on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). +-} +module Control.Effect.Free where + +import Control.Effect (type (~>)) + +import Control.Effect.Hefty (Eff, EffUnion (EffUnion), caseHF) +import Control.Freer (Freer, InjectIns, ViaFreer (ViaFreer), injectIns, interpretFreer, transformFreer, viaFreer) +import Control.Hefty (Hefty (Hefty), unHefty) +import Data.Effect (LiftIns (LiftIns), Nop, SigClass) +import Data.Free.Sum (pattern R1) +import Data.Hefty.Union (Member, U, Union, exhaust, injectRec, (|+)) + +{- | +A common type for representing first-order extensible effectful programs that can issue effects +belonging to the specified sum of effect classes. +-} +type EffectfulF u fr e = EffF u fr (U u e) + +{- | +A common type for representing first-order extensible effectful programs that can issue effects +belonging to the specified list of effect classes. +-} +type EffF u fr es = ViaFreer fr (EffUnionF u es) + +-- | A common wrapper data type for representing first-order extensible effect union. +newtype EffUnionF (u :: [SigClass] -> SigClass) es a = EffUnionF {unEffUnionF :: u es Nop a} + +instance Member u e es => InjectIns e (EffUnionF u es) where + injectIns = EffUnionF . injectRec . LiftIns + {-# INLINE injectIns #-} + +toEffF :: forall es fr u c. (Freer c fr, Union u) => Eff u fr '[] es ~> EffF u fr es +toEffF = + ViaFreer + . transformFreer (caseHF exhaust EffUnionF) + . unHefty +{-# INLINE toEffF #-} + +fromEffF :: forall es fr u c. Freer c fr => EffF u fr es ~> Eff u fr '[] es +fromEffF = + Hefty + . transformFreer (EffUnion . R1 . unEffUnionF) + . viaFreer +{-# INLINE fromEffF #-} + +{- all types of interpret-family functions: + - interpret : e ~> E r -> E (e + r) ~> E r + - reinterpret : e1 ~> E (e2 + r) -> E (e1 + r) ~> E (e2 + r) + - interpose : e <| es => e ~> E es -> E es ~> E es + + all possible suffix patterns of interpret-family functions: + - + - K + - ContT + - Fin + - T + + all types of transform-family functions: + - transform : e1 ~> e2 -> E (e1 + r) ~> E (e2 + r) + - translate : e2 <| r => e1 ~> e2 -> E (e1 + r) ~> E r + - rewrite : e <| es => e ~> e -> E es ~> E es + + todo patterns: all ( 5x3 + 3 = 18 functions ) + + + *By (for keyed effects) in interpose/translate/rewrite ( 5 + 2 = 7 functions ) +-} + +runEffF :: forall f fr u c. (Freer c fr, Union u, c f) => EffF u fr '[LiftIns f] ~> f +runEffF (ViaFreer f) = interpretFreer ((id |+ exhaust) . unEffUnionF) f +{-# INLINE runEffF #-} diff --git a/src/Control/Effect/Freer.hs b/src/Control/Effect/Freer.hs deleted file mode 100644 --- a/src/Control/Effect/Freer.hs +++ /dev/null @@ -1,632 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE PartialTypeSignatures #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE UndecidableInstances #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A Freer carrier that can be used as a handler for effect systems based -on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). --} -module Control.Effect.Freer where - -import Control.Applicative (Alternative) -import Control.Effect.Class ( - EffectDataHandler, - EffectsVia (EffectsVia), - Instruction, - SendIns, - Tag, - getTag, - runEffectsVia, - sendIns, - type (~>), - ) -import Control.Freer.Trans ( - TransFreer, - hoistFreer, - interposeLowerT, - interpretFT, - liftInsT, - liftLowerFT, - reinterpretFT, - runInterpretF, - transformT, - ) -import Control.Monad (MonadPlus) -import Control.Monad.Cont (ContT (ContT), runContT) -import Control.Monad.IO.Class (MonadIO, liftIO) -import Control.Monad.Trans (MonadTrans, lift) -import Control.Monad.Trans.Freer (MonadTransFreer, interpretMK, interpretMT, reinterpretMK, reinterpretMT) -import Control.Monad.Trans.Freer.Church (FreerChurchT) -import Data.Coerce (Coercible, coerce) -import Data.Free.Extensible (ExtensibleUnion) -import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+)) -import Data.Free.Union ( - IsMember, - Member, - Union ( - absurdUnion, - bundleUnion2, - bundleUnion3, - bundleUnion4, - decomp, - flipUnion, - flipUnion3, - flipUnionUnder, - inject, - inject0, - project, - rot3, - rot3', - unbundleUnion2, - unbundleUnion3, - unbundleUnion4, - weaken, - weaken2, - weaken2Under, - weaken2Under2, - weaken3, - weaken3Under, - weaken4, - weakenUnder, - weakenUnder2, - weakenUnder3 - ), - (|+|:), - ) -import Data.Function ((&)) -import Data.Kind (Type) - -{- | -A data type that wraps Freer with any encoding to become an instance of 'SendIns' based on the -`liftInsT` from the `TransFreer` type class. --} -newtype - FreerUnion - (fr :: Instruction -> (Type -> Type) -> Type -> Type) - u - (es :: [Instruction]) - f - a = FreerUnion {runFreerUnion :: fr (u es) f a} - deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus) - deriving stock (Foldable, Traversable) - -{- | -A Freer carrier that can be used as a handler for effect systems based -on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). --} -type FreerEffects fr u es f = EffectsVia EffectDataHandler (FreerUnion fr u es f) - --- | Unwrap the `FreerEffects` wrapper. -unFreerEffects :: FreerEffects fr u es f ~> fr (u es) f -unFreerEffects = runFreerUnion . runEffectsVia -{-# INLINE unFreerEffects #-} - --- | Wrap with `FreerEffects`. -freerEffects :: fr (u es) f ~> FreerEffects fr u es f -freerEffects = EffectsVia . FreerUnion -{-# INLINE freerEffects #-} - -{- | -A wrapper data type designed to induce instance resolution to delegate the search for effect classes -to a lower carrier @f@ even when there are no target effect classes in the effect class list @es@. - -When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it -doesn't exist, it's induced to be @'False@. --} -newtype FreerUnionForSend handleHere fr u es f a = FreerUnionForSend - {runFreerUnionForSend :: FreerUnion fr u es f a} - deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus) - deriving stock (Foldable, Traversable) - -instance - SendIns e (FreerUnionForSend (e `IsMember` es) fr u es f) => - SendIns e (FreerUnion fr u es f) - where - sendIns = runFreerUnionForSend @(e `IsMember` es) . sendIns - {-# INLINE sendIns #-} - -instance - (TransFreer c fr, Union u, Member u e es) => - SendIns e (FreerUnionForSend 'True fr u es f) - where - sendIns = FreerUnionForSend . FreerUnion . liftInsT . inject - {-# INLINE sendIns #-} - -instance (TransFreer c fr, SendIns e f, c f) => SendIns e (FreerUnionForSend 'False fr u es f) where - sendIns = FreerUnionForSend . FreerUnion . liftLowerFT . sendIns - {-# INLINE sendIns #-} - --- | Interpret the leading effect class in the effect class list. -interpret :: - (TransFreer c fr, Union u, c f) => - (e ~> FreerEffects fr u es f) -> - FreerEffects fr u (e ': es) f ~> FreerEffects fr u es f -interpret i = - overFreerEffects $ interpretFT liftLowerFT \u -> - case decomp u of - Left e -> unFreerEffects $ i e - Right e -> liftInsT e - --- | Interpret the leading effect class in the effect class list using a monad transformer. -interpretT :: - forall t fr u e es f. - (MonadTransFreer fr, Union u, MonadTrans t, Monad f, Monad (t (FreerEffects fr u es f))) => - (e ~> t (FreerEffects fr u es f)) -> - FreerEffects fr u (e ': es) f ~> t (FreerEffects fr u es f) -interpretT i = interpretMT i . splitFreerEffects @_ @fr -{-# INLINE interpretT #-} - --- | Interpret the leading effect class in the effect class list using a delimited continuation. -interpretK :: - (MonadTransFreer fr, Union u, Monad f) => - (a -> FreerEffects fr u es f r) -> - (forall x. (x -> FreerEffects fr u es f r) -> e x -> FreerEffects fr u es f r) -> - FreerEffects fr u (e ': es) f a -> - FreerEffects fr u es f r -interpretK k i = (`runContT` k) . interpretContT \e -> ContT (`i` e) -{-# INLINE interpretK #-} - -{- | -Interpret the leading effect class in the effect class list using a continuation monad transformer. --} -interpretContT :: - forall r fr u e es f. - (MonadTransFreer fr, Union u, Monad f) => - (e ~> ContT r (FreerEffects fr u es f)) -> - FreerEffects fr u (e ': es) f ~> ContT r (FreerEffects fr u es f) -interpretContT i = interpretMK i . splitFreerEffects @_ @fr -{-# INLINE interpretContT #-} - -{- | -Interpret not only the leading effect class but also all the remaining effect classes and the -underlying carrier simultaneously, transforming them into any carrier @g@. --} -interpretAll :: - (TransFreer c fr, Union u, c f, c g) => - (f ~> g) -> - (u es ~> g) -> - (e ~> g) -> - FreerEffects fr u (e ': es) f ~> g -interpretAll iLower iOther iTarget a = - unFreerEffects a & interpretFT iLower \u -> - case decomp u of - Left e -> iTarget e - Right e -> iOther e - --- | Reinterpret the leading effect class in the effect class list. -reinterpret :: - (TransFreer c fr, Union u, c f) => - (e ~> FreerEffects fr u (e ': es) f) -> - FreerEffects fr u (e ': es) f ~> FreerEffects fr u (e ': es) f -reinterpret i = - overFreerEffects $ reinterpretFT \u -> - case decomp u of - Left e -> unFreerEffects $ i e - Right e -> liftInsT $ weaken e - --- | Transform all effect classes in the effect class list into another union of effect classes. -transformAll :: - (TransFreer c fr, Union u, Union u', c f) => - (u es ~> u' es') -> - FreerEffects fr u es f ~> FreerEffects fr u' es' f -transformAll f = overFreerEffects $ transformT f -{-# INLINE transformAll #-} - --- | Transform the leading effect class in the effect class list into another effect class. -transform :: - forall e' e fr u r f c. - (TransFreer c fr, Union u, c f) => - (e ~> e') -> - FreerEffects fr u (e ': r) f ~> FreerEffects fr u (e' ': r) f -transform f = - overFreerEffects $ transformT \u -> - case decomp u of - Left e -> inject0 $ f e - Right e -> weaken e - --- | Remove the tag attached to the effect class. -untag :: - forall tag e fr u r f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (Tag e tag ': r) f ~> FreerEffects fr u (e ': r) f -untag = transform getTag - --- | Interpose the effect class that exists within the effect class list. -interpose :: - forall e fr u es f c. - (TransFreer c fr, Union u, Member u e es, c f) => - (e ~> FreerEffects fr u es f) -> - FreerEffects fr u es f ~> FreerEffects fr u es f -interpose f = - overFreerEffects $ reinterpretFT \u -> - case project @_ @e u of - Just e -> unFreerEffects $ f e - Nothing -> liftInsT u - --- | Interpose the effect class that exists within the effect class list using a monad transformer. -interposeT :: - forall e t fr u es m. - ( MonadTransFreer fr - , Union u - , Member u e es - , Monad m - , MonadTrans t - , forall m1 m2 x. Coercible m1 m2 => Coercible (t m1 x) (t m2 x) - , Monad (t (fr (u es) m)) - ) => - (e ~> t (FreerEffects fr u es m)) -> - FreerEffects fr u es m ~> t (FreerEffects fr u es m) -interposeT f a = - hoistT @(fr (u es) m) $ - unFreerEffects a & reinterpretMT \u -> - case project @_ @e u of - Just e -> hoistT $ f e - Nothing -> lift $ liftInsT u - where - hoistT :: Coercible (t m1 a) (t m2 a) => t m1 a -> t m2 a - hoistT = coerce - {-# INLINE hoistT #-} - -{- | -Transform all other effect classes in the effect class list and the underlying carrier, along -with the effect class that exists within the effect class list, into any carrier @g@. --} -interposeAll :: - forall e g fr u es f c. - ( TransFreer c fr - , Union u - , Member u e es - , c f - , c g - ) => - (f ~> g) -> - (u es ~> g) -> - (e ~> g) -> - FreerEffects fr u es f ~> g -interposeAll iLower iOther iTarget a = - unFreerEffects a & interpretFT iLower \u -> - case project @_ @e u of - Just e -> iTarget e - Nothing -> iOther u - -{- | -Interpose the effect class that exists within the effect class list using a delimited continuation. --} -interposeK :: - (MonadTransFreer fr, Union u, Member u e es, Monad m) => - (a -> FreerEffects fr u es m r) -> - (forall x. (x -> FreerEffects fr u es m r) -> e x -> FreerEffects fr u es m r) -> - FreerEffects fr u es m a -> - FreerEffects fr u es m r -interposeK k i = (`runContT` k) . interposeContT \e -> ContT (`i` e) -{-# INLINE interposeK #-} - -{- | -Interpose the effect class that exists within the effect class list using a continuation monad -transformer. --} -interposeContT :: - forall e r fr u es m. - (MonadTransFreer fr, Union u, Member u e es, Monad m) => - (e ~> ContT r (FreerEffects fr u es m)) -> - FreerEffects fr u es m ~> ContT r (FreerEffects fr u es m) -interposeContT f a = - hoistContT $ - unFreerEffects a & reinterpretMK \u -> - case project @_ @e u of - Just e -> hoistContT $ f e - Nothing -> lift $ liftInsT u - where - hoistContT :: Coercible m1 m2 => ContT r m1 a -> ContT r m2 a - hoistContT = coerce - {-# INLINE hoistContT #-} - --- | Transform the effect of the effect class that exists within the effect class list. -intercept :: - forall e fr u es f c. - (TransFreer c fr, Union u, Member u e es, c f) => - (e ~> e) -> - FreerEffects fr u es f ~> FreerEffects fr u es f -intercept f = - overFreerEffects $ transformT \u -> - case project @_ @e u of - Just e -> inject $ f e - Nothing -> u - --- | Insert an arbitrary effect class at the beginning of the effect class list. -raise :: - forall e es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u es f ~> FreerEffects fr u (e ': es) f -raise = transformAll weaken -{-# INLINE raise #-} - --- | Insert two arbitrary effect classes at the beginning of the effect class list. -raise2 :: - forall e1 e2 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': es) f -raise2 = transformAll weaken2 -{-# INLINE raise2 #-} - --- | Insert three arbitrary effect classes at the beginning of the effect class list. -raise3 :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f -raise3 = transformAll weaken3 -{-# INLINE raise3 #-} - --- | Insert four arbitrary effect classes at the beginning of the effect class list. -raise4 :: - forall e1 e2 e3 e4 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f -raise4 = transformAll weaken4 -{-# INLINE raise4 #-} - --- | Insert an arbitrary effect class below the leading effect class in the effect class list. -raiseUnder :: - forall e1 e2 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f -raiseUnder = transformAll weakenUnder -{-# INLINE raiseUnder #-} - -{- | -Insert an arbitrary effect class below the first two leading effect classes in the effect class -list. --} -raiseUnder2 :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f -raiseUnder2 = transformAll weakenUnder2 -{-# INLINE raiseUnder2 #-} - -{- | -Insert an arbitrary effect class below the first three leading effect classes in the effect class list. --} -raiseUnder3 :: - forall e1 e2 e3 e4 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f -raiseUnder3 = transformAll weakenUnder3 -{-# INLINE raiseUnder3 #-} - --- | Insert two arbitrary effect classes below the leading effect class in the effect class list. -raise2Under :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f -raise2Under = transformAll weaken2Under -{-# INLINE raise2Under #-} - -{- | -Insert two arbitrary effect classes below the first two leading effect classes in the effect class list. --} -raise2Under2 :: - forall e1 e2 e3 e4 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f -raise2Under2 = transformAll weaken2Under2 -{-# INLINE raise2Under2 #-} - --- | Inserts three arbitrary effect classes under the top effect class in the effect class list. -raise3Under :: - forall e1 e2 e3 e4 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f -raise3Under = transformAll weaken3Under -{-# INLINE raise3Under #-} - --- | Swaps the top two effect classes in the effect class list. -flipFreer :: - forall e1 e2 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e2 ': e1 ': es) f -flipFreer = transformAll flipUnion -{-# INLINE flipFreer #-} - --- | Reverses the order of the top three effect classes in the effect class list. -flipFreer3 :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e2 ': e1 ': es) f -flipFreer3 = transformAll flipUnion3 -{-# INLINE flipFreer3 #-} - --- | Swaps the second and third effect classes from the top in the effect class list. -flipFreerUnder :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e3 ': e2 ': es) f -flipFreerUnder = transformAll flipUnionUnder -{-# INLINE flipFreerUnder #-} - --- | Rotates the top three effect classes in the effect class list to the left. -rotate3 :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e2 ': e3 ': e1 ': es) f -rotate3 = transformAll rot3 -{-# INLINE rotate3 #-} - --- | Rotates the top three effect classes in the effect class list to the left twice. -rotate3' :: - forall e1 e2 e3 es fr u f c. - (TransFreer c fr, Union u, c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e1 ': e2 ': es) f -rotate3' = transformAll rot3' -{-# INLINE rotate3' #-} - --- | Bundles the top two effect classes in the effect class list into any open union. -bundle2 :: - forall e1 e2 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (u' '[e1, e2] ': es) f -bundle2 = transformAll bundleUnion2 -{-# INLINE bundle2 #-} - --- | Bundles the top three effect classes in the effect class list into any open union. -bundle3 :: - forall e1 e2 e3 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3] ': es) f -bundle3 = transformAll bundleUnion3 -{-# INLINE bundle3 #-} - --- | Bundles the top four effect classes in the effect class list into any open union. -bundle4 :: - forall e1 e2 e3 e4 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f -bundle4 = transformAll bundleUnion4 -{-# INLINE bundle4 #-} - --- | Expands the open union at the top of the effect class list. -unbundle2 :: - forall e1 e2 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (u' '[e1, e2] ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f -unbundle2 = transformAll unbundleUnion2 -{-# INLINE unbundle2 #-} - --- | Expands the open union at the top of the effect class list. -unbundle3 :: - forall e1 e2 e3 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (u' '[e1, e2, e3] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f -unbundle3 = transformAll unbundleUnion3 -{-# INLINE unbundle3 #-} - --- | Expands the open union at the top of the effect class list. -unbundle4 :: - forall e1 e2 e3 e4 es fr u f c u'. - (TransFreer c fr, Union u, Union u', c f) => - FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f -unbundle4 = transformAll unbundleUnion4 -{-# INLINE unbundle4 #-} - -{- | -Transforms the lower carrier. - -__Warning__: The given natural transformation must be a monad morphism -(see ). -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 ). -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 diff --git a/src/Control/Effect/Heftia.hs b/src/Control/Effect/Heftia.hs deleted file mode 100644 --- a/src/Control/Effect/Heftia.hs +++ /dev/null @@ -1,760 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE UndecidableInstances #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A Heftia carrier that can be used as a handler for effect systems based -on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). --} -module Control.Effect.Heftia where - -import Control.Applicative (Alternative) -import Control.Arrow ((>>>)) -import Control.Effect.Class ( - EffectDataHandler, - EffectsVia (EffectsVia), - LiftIns (LiftIns), - SendIns, - SendSig, - Signature, - TagH, - getTagH, - runEffectsVia, - sendIns, - sendSig, - unliftIns, - type (~>), - ) -import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap) -import Control.Effect.Freer (FreerEffects, freerEffects, interpose, unFreerEffects) -import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT) -import Control.Heftia.Trans ( - TransHeftia, - elaborateHT, - hoistHeftia, - interpretLowerHT, - liftLowerHT, - liftSigT, - reelaborateHT, - runElaborateH, - transformHT, - translateT, - ) -import Control.Monad (MonadPlus) -import Control.Monad.Cont (ContT (ContT), MonadTrans, runContT) -import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, elaborateMT) -import Control.Monad.Trans.Heftia.Church (HeftiaChurchT) -import Data.Extensible.Class (Forall) -import Data.Free.Union (Member, Union, project) -import Data.Hefty.Extensible (ExtensibleUnionH) -import Data.Hefty.Union ( - IsMemberH, - MemberH, - UnionH ( - absurdUnionH, - bundleUnion2H, - bundleUnion3H, - bundleUnion4H, - decompH, - flipUnion3H, - flipUnionH, - flipUnionUnderH, - inject0H, - injectH, - projectH, - rot3H, - rot3H', - unbundleUnion2H, - unbundleUnion3H, - unbundleUnion4H, - weaken2H, - weaken2Under2H, - weaken2UnderH, - weaken3H, - weaken3UnderH, - weaken4H, - weakenH, - weakenUnder2H, - weakenUnder3H, - weakenUnderH - ), - (|+:), - ) -import Data.Kind (Type) - -{- | -A data type that wraps Heftia with any encoding to become an instance of 'SendIns'/'SendSig' based -on the `liftInsT` or `liftSigT` from the `TransFreer` or `TransHeftia` type class. --} -newtype - HeftiaUnion - (h :: Signature -> (Type -> Type) -> Type -> Type) - u - (es :: [Signature]) - f - a = HeftiaUnion {runHeftiaUnion :: h (u es) f a} - deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus) - deriving stock (Foldable, Traversable) - -{- | -A Heftia carrier that can be used as a handler for effect systems based -on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). --} -type HeftiaEffects h u es f = EffectsVia EffectDataHandler (HeftiaUnion h u es f) - --- | Unwrap the `HeftiaEffects` wrapper. -unHeftiaEffects :: HeftiaEffects h u es f ~> h (u es) f -unHeftiaEffects = runHeftiaUnion . runEffectsVia -{-# INLINE unHeftiaEffects #-} - --- | Wrap with `HeftiaEffects`. -heftiaEffects :: h (u es) f ~> HeftiaEffects h u es f -heftiaEffects = EffectsVia . HeftiaUnion -{-# INLINE heftiaEffects #-} - -{- | -A wrapper data type designed to induce instance resolution to delegate the search for first-order -effect classes to a lower carrier @f@ even when there are no target effect classes in the effect -class list @es@. - -When a target effect class exists within @es@, @handleHere@ is induced to be @'True@; when it -doesn't exist, it's induced to be @'False@. --} -newtype HeftiaUnionForSendIns handleHere h u es f a = HeftiaUnionForSendIns - {runHeftiaUnionForSendIns :: HeftiaUnion h u es f a} - deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus) - deriving stock (Foldable, Traversable) - -instance - SendIns e (HeftiaUnionForSendIns (LiftIns e `IsMemberH` es) h u es f) => - SendIns e (HeftiaUnion h u es f) - where - sendIns = runHeftiaUnionForSendIns @(LiftIns e `IsMemberH` es) . sendIns - {-# INLINE sendIns #-} - -instance - (TransHeftia c h, UnionH u, MemberH u (LiftIns e) es, HFunctor (u es)) => - SendIns e (HeftiaUnionForSendIns 'True h u es f) - where - sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftSigT . injectH . LiftIns - {-# INLINE sendIns #-} - -instance - (TransHeftia c h, SendIns e f, c f, HFunctor (u es)) => - SendIns e (HeftiaUnionForSendIns 'False h u es f) - where - sendIns = HeftiaUnionForSendIns . HeftiaUnion . liftLowerHT . sendIns - {-# INLINE sendIns #-} - -instance - (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es)) => - SendSig e (HeftiaUnion h u es f) - where - sendSig = HeftiaUnion . liftSigT . hfmap runHeftiaUnion . injectH - {-# INLINE sendSig #-} - --- | Elaborate all effects in the effect class list at once. -runElaborate :: - (TransHeftia c h, HFunctor (u es), c f, UnionH u) => - (u es f ~> f) -> - HeftiaEffects h u es f ~> f -runElaborate f = runElaborateH f . unHeftiaEffects -{-# INLINE runElaborate #-} - --- | Elaborate all effects in the effect class list using a delimited continuation. -runElaborateK :: - (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) => - (a -> m r) -> - (forall x. (x -> m r) -> u es (ContT r m) x -> m r) -> - HeftiaEffects h u es m a -> - m r -runElaborateK k f = (`runContT` k) . runElaborateContT \e -> ContT (`f` e) -{-# INLINE runElaborateK #-} - -{- | -Elaborate all effects in the effect class list using a continuation monad transformer. --} -runElaborateContT :: - (MonadTransHeftia h, HFunctor (u es), UnionH u, Monad m) => - (u es (ContT r m) ~> ContT r m) -> - HeftiaEffects h u es m ~> ContT r m -runElaborateContT f = elaborateMK f . unHeftiaEffects -{-# INLINE runElaborateContT #-} - -{- | -Elaborate all effects in the effect class list using a monad transformer. --} -runElaborateT :: - (MonadTransHeftia h, HFunctor (u es), UnionH u, MonadTrans t, Monad m, Monad (t m)) => - (u es (t m) ~> t m) -> - HeftiaEffects h u es m ~> t m -runElaborateT f = elaborateMT f . unHeftiaEffects -{-# INLINE runElaborateT #-} - -{- | -Elaborate all effects in the effect class list and the underlying carrier simultaneously, -transforming them into any carrier @g@. --} -elaborate :: - (TransHeftia c h, HFunctor (u es), c f, UnionH u, c g) => - (f ~> g) -> - (u es g ~> g) -> - HeftiaEffects h u es f ~> g -elaborate f g = elaborateHT f g . unHeftiaEffects -{-# INLINE elaborate #-} - --- | Elaborate the leading effect class in the effect class list. -interpretH :: - (TransHeftia c h, UnionH u, HFunctor (u es), HFunctor (u (e : es)), HFunctor e, c f) => - (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) -> - HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u es f -interpretH i = - overHeftiaEffects $ elaborateHT liftLowerHT \u -> - case decompH u of - Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e - Right e -> liftSigT e - --- | Re-elaborate the leading effect class in the effect class list. -reinterpretH :: - (TransHeftia c h, UnionH u, HFunctor (u (e : es)), HFunctor e, c f) => - (e (HeftiaEffects h u (e ': es) f) ~> HeftiaEffects h u (e ': es) f) -> - HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u (e ': es) f -reinterpretH i = - overHeftiaEffects $ reelaborateHT \u -> - case decompH u of - Left e -> unHeftiaEffects $ i $ hfmap heftiaEffects e - Right e -> liftSigT $ weakenH e - --- | Transform all effect classes in the effect class list into another union of effect classes. -transformAllH :: - ( TransHeftia c h - , UnionH u - , UnionH u' - , HFunctor (u es) - , HFunctor (u' es') - , c f - ) => - (forall g. u es g ~> u' es' g) -> - HeftiaEffects h u es f ~> HeftiaEffects h u' es' f -transformAllH f = overHeftiaEffects $ transformHT f -{-# INLINE transformAllH #-} - --- | Transform the leading effect class in the effect class list into another effect class. -transformH :: - forall e' e h u r f c. - ( TransHeftia c h - , UnionH u - , c f - , HFunctor (u (e : r)) - , HFunctor (u (e' : r)) - ) => - (forall g. e g ~> e' g) -> - HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f -transformH f = overHeftiaEffects $ translateT \u -> - case decompH u of - Left e -> inject0H $ f e - Right e -> weakenH e - --- | Remove the tag attached to the effect class. -untagH :: - forall tag e h u r f c. - ( TransHeftia c h - , UnionH u - , c f - , HFunctor (u (e : r)) - , HFunctor (u (TagH e tag : r)) - ) => - HeftiaEffects h u (TagH e tag ': r) f ~> HeftiaEffects h u (e ': r) f -untagH = transformH getTagH - --- | Transform the leading effect class in the effect class list into another effect class. -translate :: - forall e' e h u r f c. - ( TransHeftia c h - , UnionH u - , HFunctor (u (e : r)) - , HFunctor (u (e' : r)) - , HFunctor e - , HFunctor e' - , c f - ) => - (e (HeftiaEffects h u (e' ': r) f) ~> e' (HeftiaEffects h u (e' ': r) f)) -> - HeftiaEffects h u (e ': r) f ~> HeftiaEffects h u (e' ': r) f -translate f = - overHeftiaEffects $ translateT \u -> - case decompH u of - Left e -> inject0H $ hfmap unHeftiaEffects $ f $ hfmap heftiaEffects e - Right e -> weakenH e - --- | Transform all effect classes in the effect class list into another union of effect classes. -translateAll :: - ( TransHeftia c h - , UnionH u - , UnionH u' - , HFunctor (u es) - , HFunctor (u' es') - , c f - ) => - (u es (HeftiaEffects h u' es' f) ~> u' es' (HeftiaEffects h u' es' f)) -> - HeftiaEffects h u es f ~> HeftiaEffects h u' es' f -translateAll f = - overHeftiaEffects $ translateT (hfmap unHeftiaEffects . f . hfmap heftiaEffects) -{-# INLINE translateAll #-} - --- | Interpose the effect class that exists within the effect class list using a monad transformer. -interposeH :: - forall e h u es f c. - (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), c f) => - (e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f) -> - HeftiaEffects h u es f ~> HeftiaEffects h u es f -interposeH f = - overHeftiaEffects $ reelaborateHT \u -> - let u' = hfmap (interposeH f . heftiaEffects) u - in case projectH @_ @e u' of - Just e -> unHeftiaEffects $ f e - Nothing -> liftSigT $ hfmap unHeftiaEffects u' - --- | Transform the effect of the effect class that exists within the effect class list. -interceptH :: - forall e h u es f c. - (TransHeftia c h, UnionH u, MemberH u e es, HFunctor (u es), HFunctor e, c f) => - (e (HeftiaEffects h u es f) ~> e (HeftiaEffects h u es f)) -> - HeftiaEffects h u es f ~> HeftiaEffects h u es f -interceptH f = - overHeftiaEffects $ translateT \u -> - let u' = hfmap (interceptH f . heftiaEffects) u - in case projectH @_ @e u' of - Just e -> injectH $ hfmap unHeftiaEffects $ f e - Nothing -> hfmap unHeftiaEffects u' - --- | Insert an arbitrary effect class at the beginning of the effect class list. -raiseH :: - forall e hs h u f c. - ( TransHeftia c h - , HFunctor (u hs) - , HFunctor (u (e ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u hs f ~> HeftiaEffects h u (e ': hs) f -raiseH = transformAllH weakenH -{-# INLINE raiseH #-} - --- | Insert two arbitrary effect classes at the beginning of the effect class list. -raise2H :: - forall e1 e2 hs h u f c. - ( TransHeftia c h - , HFunctor (u hs) - , HFunctor (u (e1 ': e2 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': hs) f -raise2H = transformAllH weaken2H -{-# INLINE raise2H #-} - --- | Insert three arbitrary effect classes at the beginning of the effect class list. -raise3H :: - forall e1 e2 e3 hs h u f c. - ( TransHeftia c h - , HFunctor (u hs) - , HFunctor (u (e1 ': e2 ': e3 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f -raise3H = transformAllH weaken3H -{-# INLINE raise3H #-} - --- | Insert four arbitrary effect classes at the beginning of the effect class list. -raise4H :: - forall e1 e2 e3 e4 hs h u f c. - ( TransHeftia c h - , HFunctor (u hs) - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f -raise4H = transformAllH weaken4H -{-# INLINE raise4H #-} - --- | Insert an arbitrary effect class below the leading effect class in the effect class list. -raiseUnderH :: - forall e1 e2 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': hs)) - , HFunctor (u (e1 ': e2 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': hs) f -raiseUnderH = transformAllH weakenUnderH -{-# INLINE raiseUnderH #-} - -{- | -Insert an arbitrary effect class below the first two leading effect classes in the effect class -list. --} -raiseUnder2H :: - forall e1 e2 e3 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': hs)) - , HFunctor (u (e1 ': e2 ': e3 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f -raiseUnder2H = transformAllH weakenUnder2H -{-# INLINE raiseUnder2H #-} - -{- | -Insert an arbitrary effect class below the first three leading effect classes in the effect class list. --} -raiseUnder3H :: - forall e1 e2 e3 e4 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': hs)) - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f -raiseUnder3H = transformAllH weakenUnder3H -{-# INLINE raiseUnder3H #-} - --- | Insert two arbitrary effect classes below the leading effect class in the effect class list. -raise2UnderH :: - forall e1 e2 e3 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': hs)) - , HFunctor (u (e1 ': e2 ': e3 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f -raise2UnderH = transformAllH weaken2UnderH -{-# INLINE raise2UnderH #-} - -{- | -Insert two arbitrary effect classes below the first two leading effect classes in the effect class list. --} -raise2Under2H :: - forall e1 e2 e3 e4 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': hs)) - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f -raise2Under2H = transformAllH weaken2Under2H -{-# INLINE raise2Under2H #-} - --- | Inserts three arbitrary effect classes under the top effect class in the effect class list. -raise3UnderH :: - forall e1 e2 e3 e4 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': hs)) - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f -raise3UnderH = transformAllH weaken3UnderH -{-# INLINE raise3UnderH #-} - --- | Swaps the top two effect classes in the effect class list. -flipHeftia :: - forall e1 e2 hs h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': hs)) - , HFunctor (u (e2 ': e1 ': hs)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e2 ': e1 ': hs) f -flipHeftia = transformAllH flipUnionH -{-# INLINE flipHeftia #-} - --- | Reverses the order of the top three effect classes in the effect class list. -flipHeftia3 :: - forall e1 e2 e3 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (e3 : e2 : e1 : es)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e2 ': e1 ': es) f -flipHeftia3 = transformAllH flipUnion3H -{-# INLINE flipHeftia3 #-} - --- | Swaps the second and third effect classes from the top in the effect class list. -flipHeftiaUnder :: - forall e1 e2 e3 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (e1 : e3 : e2 : es)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e1 ': e3 ': e2 ': es) f -flipHeftiaUnder = transformAllH flipUnionUnderH -{-# INLINE flipHeftiaUnder #-} - --- | Rotates the top three effect classes in the effect class list to the left. -rotate3H :: - forall e1 e2 e3 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (e2 : e3 : e1 : es)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e2 ': e3 ': e1 ': es) f -rotate3H = transformAllH rot3H -{-# INLINE rotate3H #-} - --- | Rotates the top three effect classes in the effect class list to the left twice. -rotate3H' :: - forall e1 e2 e3 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (e3 : e1 : e2 : es)) - , c f - , UnionH u - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e1 ': e2 ': es) f -rotate3H' = transformAllH rot3H' -{-# INLINE rotate3H' #-} - --- | Bundles the top two effect classes in the effect class list into any open union. -bundle2H :: - forall u' e1 e2 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': es)) - , HFunctor (u (u' '[e1, e2] ': es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (e1 ': e2 ': es) f ~> HeftiaEffects h u (u' '[e1, e2] ': es) f -bundle2H = transformAllH bundleUnion2H -{-# INLINE bundle2H #-} - --- | Bundles the top three effect classes in the effect class list into any open union. -bundle3H :: - forall u' e1 e2 e3 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (u' '[e1, e2, e3] : es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (u' '[e1, e2, e3] ': es) f -bundle3H = transformAllH bundleUnion3H -{-# INLINE bundle3H #-} - --- | Bundles the top four effect classes in the effect class list into any open union. -bundle4H :: - forall u' e1 e2 e3 e4 es h u f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es)) - , HFunctor (u (u' '[e1, e2, e3, e4] : es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f - ~> HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f -bundle4H = transformAllH bundleUnion4H -{-# INLINE bundle4H #-} - --- | Expands the open union at the top of the effect class list. -unbundle2H :: - forall e1 e2 es h u u' f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': es)) - , HFunctor (u (u' '[e1, e2] ': es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (u' '[e1, e2] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': es) f -unbundle2H = transformAllH unbundleUnion2H -{-# INLINE unbundle2H #-} - --- | Expands the open union at the top of the effect class list. -unbundle3H :: - forall e1 e2 e3 es h u u' f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': es)) - , HFunctor (u (u' '[e1, e2, e3] ': es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (u' '[e1, e2, e3] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': es) f -unbundle3H = transformAllH unbundleUnion3H -{-# INLINE unbundle3H #-} - --- | Expands the open union at the top of the effect class list. -unbundle4H :: - forall e1 e2 e3 e4 es h u u' f c. - ( TransHeftia c h - , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es)) - , HFunctor (u (u' '[e1, e2, e3, e4] ': es)) - , c f - , UnionH u - , UnionH u' - ) => - HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f - ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f -unbundle4H = transformAllH unbundleUnion4H -{-# INLINE unbundle4H #-} - -{- | -Transforms the lower carrier. - -__Warning__: The given natural transformation must be a monad morphism -(see ). -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 ). -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 ). -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 ). -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 diff --git a/src/Control/Effect/Hefty.hs b/src/Control/Effect/Hefty.hs new file mode 100644 --- /dev/null +++ b/src/Control/Effect/Hefty.hs @@ -0,0 +1,1114 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023-2024 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +A Heftia carrier that can be used as a handler for effect systems based +on [@classy-effects@](https://hackage.haskell.org/package/classy-effects). +-} +module Control.Effect.Hefty where + +import Control.Effect (type (~>)) +import Control.Effect.Key (sendInsBy, sendSigBy) +import Control.Freer (Freer, InjectIns, InjectInsBy, injectIns, injectInsBy, interpretFreer, liftIns, transformFreer) +import Control.Hefty (Hefty (Hefty), InjectSig, InjectSigBy, injectSig, injectSigBy, overHefty, unHefty) +import Control.Monad.Cont (Cont, ContT (ContT), lift, runContT) +import Control.Monad.Freer (MonadFreer, interpretFreerK) +import Control.Monad.Identity (Identity (Identity), runIdentity) +import Control.Monad.Trans (MonadTrans) +import Data.Coerce (coerce) +import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns) +import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:)) +import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>)) +import Data.Effect.Tag (Tag (unTag), TagH (unTagH), type (#), type (##)) +import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+)) +import Data.Hefty.Union ( + HFunctorUnion, + HFunctorUnion_ (ForallHFunctor), + HeadIns, + LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle), + Lookup, + Member, + MemberBy, + MemberH, + MemberHBy, + MemberRec, + U, + UH, + Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)), + UnliftIfSingle, + flipUnion, + flipUnion3, + flipUnionUnder, + inject, + injectRec, + projectRec, + weaken2, + weaken2Under, + weaken2Under2, + weaken3Under, + weakenUnder2, + weakenUnder3, + (|+), + ) +import Data.Kind (Type) +import Data.Maybe.Singletons (FromJust) + +{- | +A common type for representing first-order and higher-order extensible effectful programs that can +issue effects belonging to the specified list of effect classes. +-} +type Eff u fr ehs efs = Hefty fr (EffUnion u ehs efs) + +{- | +A common type for representing first-order and higher-order extensible effectful programs that can +issue effects belonging to the specified sum of effect classes. +-} +type Effectful u fr eh ef = Eff u fr (UH u eh) (U u ef) + +{- | +A common wrapper data type for representing first-order and higher-order extensible effect union. +-} +newtype EffUnion (u :: [SigClass] -> SigClass) ehs efs f a = EffUnion + {unEffUnion :: (u ehs f + u efs Nop) a} + +caseHF :: (u ehs f a -> r) -> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r +caseHF f g = caseF f g . unEffUnion + +instance HFunctor (u ehs) => HFunctor (EffUnion u ehs efs) where + hfmap f = EffUnion . caseF (L1 . hfmap f) R1 . unEffUnion + {-# INLINE hfmap #-} + +instance MemberRec u (LiftIns e) efs => InjectIns e (EffUnion u ehs efs f) where + injectIns = EffUnion . R1 . injectRec . LiftIns + {-# INLINE injectIns #-} + +instance MemberRec u e ehs => InjectSig e (EffUnion u ehs efs) where + injectSig = EffUnion . L1 . injectRec + {-# INLINE injectSig #-} + +type HasMembershipF u e efs = HasMembership u (LiftIns e) efs + +infixr 3 $ +infixr 4 $$ + +-- | Type-level infix applcation for functors. +type (f :: Type -> Type) $ a = f a + +-- | Type-level infix applcation for higher-order functors. +type (h :: (Type -> Type) -> Type -> Type) $$ f = h f + +type Elab e f = e f ~> f + +injectH :: (Freer c f, HFunctor (u ehs)) => u ehs (Eff u f ehs efs) ~> Eff u f ehs efs +injectH = Hefty . liftIns . EffUnion . L1 +{-# INLINE injectH #-} + +injectF :: Freer c f => u efs Nop ~> Eff u f ehs efs +injectF = Hefty . liftIns . EffUnion . R1 +{-# INLINE injectF #-} + +{- all types of interpret-family functions: + - interpret : e ~> E r -> E (e + r) ~> E r + - reinterpret : e1 ~> E (e2 + r) -> E (e1 + r) ~> E (e2 + r) + - interpose : e <| es => e ~> E es -> E es ~> E es + + all possible suffix patterns of interpret functions: + { , K , ContT , Fin , T } x { , H , FH } + - Rec + - RecH + - RecFH + + all possible suffix patterns of interpret-family functions (except 'interpret'): + - + - K + - ContT + - Fin ('interpose' only) + - T + - Rec + - RecH + - RecFH + + all types of transform-family functions: + - transform : e1 ~> e2 -> E (e1 + r) ~> E (e2 + r) + - translate : e2 <| r => e1 ~> e2 -> E (e1 + r) ~> E r + - rewrite : e <| es => e ~> e -> E es ~> E es + + all possible suffix patterns of transform-family functions: + - + - H + - FH + + todo patterns: + - *FH in interpret-family ( (5+1) + 2 = 8 functions ) + + + *By (for keyed effects) in interpose/translate/rewrite ( 8 + 2x3 = 14 functions ) +-} + +-- | Using the provided interpretation function, interpret first-order effects. +interpret :: + forall e r ehs fr u c. + (Freer c fr, Union u, HeadIns e) => + UnliftIfSingle e ~> Eff u fr ehs r -> + Eff u fr '[] (e ': r) ~> Eff u fr ehs r +interpret i = interpretAllE $ i . unliftInsIfSingle |+: injectF +{-# INLINE interpret #-} + +interpretH :: + forall eh ehs efs fr u c. + (Freer c fr, Union u) => + eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs -> + Eff u fr '[eh] efs ~> Eff u fr ehs efs +interpretH i = interpretAllH $ i |+: exhaust +{-# INLINE interpretH #-} + +-- | Interpret the leading first-order effect class using delimited continuations. +interpretK :: + forall e rs r a ehs fr u c. + (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) => + (a -> Eff u fr ehs rs r) -> + (forall x. (x -> Eff u fr ehs rs r) -> UnliftIfSingle e x -> Eff u fr ehs rs r) -> + Eff u fr '[] (e ': rs) a -> + Eff u fr ehs rs r +interpretK = toInterpretKFromContT interpretContT +{-# INLINE interpretK #-} + +interpretKH :: + forall e r ehs efs a fr u c. + (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) => + (a -> Eff u fr ehs efs r) -> + (forall x. (x -> Eff u fr ehs efs r) -> e (Eff u fr '[e] efs) x -> Eff u fr ehs efs r) -> + Eff u fr '[e] efs a -> + Eff u fr ehs efs r +interpretKH = toInterpretKFromContT interpretContTH +{-# INLINE interpretKH #-} + +-- | Interpret the leading first-order effect class using a continuation monad transformer. +interpretContT :: + forall e rs r ehs fr u c. + (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) => + (UnliftIfSingle e ~> ContT r (Eff u fr ehs rs)) -> + Eff u fr '[] (e ': rs) ~> ContT r (Eff u fr ehs rs) +interpretContT i = + interpretContTAll $ i . unliftInsIfSingle |+: lift . injectF +{-# INLINE interpretContT #-} + +interpretContTH :: + forall e r ehs efs fr u c. + (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) => + (e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs)) -> + Eff u fr '[e] efs ~> ContT r (Eff u fr ehs efs) +interpretContTH i = interpretContTAllH $ i |+: exhaust +{-# INLINE interpretContTH #-} + +-- | Interpret the leading first-order effect class into the carrier @f@. +interpretFin :: + forall e r f fr u c. + (Freer c fr, Union u, HeadIns e, c f) => + (u r Nop ~> f) -> + UnliftIfSingle e ~> f -> + Eff u fr '[] (e ': r) ~> f +interpretFin liftFin i = interpretAll $ i . unliftInsIfSingle |+: liftFin +{-# INLINE interpretFin #-} + +interpretFinH :: + forall e f efs fr u c. + (Freer c fr, Union u, c f) => + (u efs Nop ~> f) -> + e (Eff u fr '[e] efs) ~> f -> + Eff u fr '[e] efs ~> f +interpretFinH liftFin i = interpretAllFH (i |+: exhaust) liftFin +{-# INLINE interpretFinH #-} + +-- | Interpret the leading first-order effect class using a monad transformer. +interpretT :: + forall e r t ehs fr u c. + ( Freer c fr + , Union u + , MonadTrans t + , HeadIns e + , Monad (Eff u fr ehs r) + , c (t (Eff u fr ehs r)) + ) => + UnliftIfSingle e ~> t (Eff u fr ehs r) -> + Eff u fr '[] (e ': r) ~> t (Eff u fr ehs r) +interpretT = interpretFin $ lift . injectF +{-# INLINE interpretT #-} + +interpretTH :: + forall e t ehs efs fr u c. + (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs efs), c (t (Eff u fr ehs efs))) => + e (Eff u fr '[e] efs) ~> t (Eff u fr ehs efs) -> + Eff u fr '[e] efs ~> t (Eff u fr ehs efs) +interpretTH = interpretFinH $ lift . injectF +{-# INLINE interpretTH #-} + +{- | +Using the provided interpretation function, interpret first-order effects. For actions (scopes) +within higher-order effects that are currently unhandled, interpretation is applied recursively. + +Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not +maintained across the scopes. +-} +interpretRec :: + forall e rs ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), HeadIns e) => + UnliftIfSingle e ~> Eff u fr ehs rs -> + Eff u fr ehs (e ': rs) ~> Eff u fr ehs rs +interpretRec i = interpretAllRec $ i . unliftInsIfSingle |+: injectF +{-# INLINE interpretRec #-} + +{- | +Using the provided interpretation function, interpret higher-order effects. For actions (scopes) +within higher-order effects that are currently unhandled, interpretation is applied recursively. + +Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not +maintained across the scopes. +-} +interpretRecH :: + forall e rs efs fr u c. + (Freer c fr, Union u, HFunctor e, HFunctor (u rs), HFunctor (u (e ': rs))) => + e (Eff u fr rs efs) ~> Eff u fr rs efs -> + Eff u fr (e ': rs) efs ~> Eff u fr rs efs +interpretRecH i = interpretAllRecH $ i |+: injectH +{-# INLINE interpretRecH #-} + +reinterpret :: + forall e2 e1 r ehs fr u c. + (Freer c fr, Union u, HeadIns e1, HFunctor (u '[])) => + UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) -> + Eff u fr '[] (e1 ': r) ~> Eff u fr ehs (e2 ': r) +reinterpret f = interpret f . raiseUnder +{-# INLINE reinterpret #-} + +reinterpretK :: + forall e2 e1 rs r a ehs fr u c. + (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) => + (a -> Eff u fr ehs (e2 ': rs) r) -> + ( forall x. + (x -> Eff u fr ehs (e2 ': rs) r) -> + UnliftIfSingle e1 x -> + Eff u fr ehs (e2 ': rs) r + ) -> + Eff u fr '[] (e1 ': rs) a -> + Eff u fr ehs (e2 ': rs) r +reinterpretK = toInterpretKFromContT reinterpretContT +{-# INLINE reinterpretK #-} + +reinterpretContT :: + forall e2 e1 rs r ehs fr u c. + (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) => + (UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 ': rs))) -> + Eff u fr '[] (e1 ': rs) ~> ContT r (Eff u fr ehs (e2 ': rs)) +reinterpretContT i = interpretContT i . raiseUnder +{-# INLINE reinterpretContT #-} + +reinterpretT :: + forall e2 e1 t r ehs fr u c. + ( Freer c fr + , Union u + , MonadTrans t + , HeadIns e1 + , HFunctor (u '[]) + , Monad (Eff u fr ehs (e2 ': r)) + , c (t (Eff u fr ehs (e2 ': r))) + ) => + UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 ': r)) -> + Eff u fr '[] (e1 ': r) ~> t (Eff u fr ehs (e2 ': r)) +reinterpretT i = interpretT i . raiseUnder +{-# INLINE reinterpretT #-} + +reinterpretRec :: + forall e2 e1 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) => + UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) -> + Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r) +reinterpretRec i = interpretRec i . raiseUnder +{-# INLINE reinterpretRec #-} + +reinterpretRecH :: + forall e2 e1 r efs fr u c. + (Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2, ForallHFunctor u r) => + e1 (Eff u fr (e2 ': r) efs) ~> Eff u fr (e2 ': r) efs -> + Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs +reinterpretRecH i = interpretRecH i . raiseUnderH +{-# INLINE reinterpretRecH #-} + +interpose :: + forall e efs fr u c. + (Freer c fr, Union u, Member u e efs) => + e ~> Eff u fr '[] efs -> + Eff u fr '[] efs ~> Eff u fr '[] efs +interpose f = + interpretAllE + \u -> case projectRec u of + Just (LiftIns e) -> f e + Nothing -> injectF u + +interposeK :: + forall e efs r a fr u c. + (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) => + (a -> Eff u fr '[] efs r) -> + (forall x. (x -> Eff u fr '[] efs r) -> e x -> Eff u fr '[] efs r) -> + Eff u fr '[] efs a -> + Eff u fr '[] efs r +interposeK = toInterpretKFromContT interposeContT +{-# INLINE interposeK #-} + +interposeContT :: + forall e efs r fr u c. + (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) => + (e ~> ContT r (Eff u fr '[] efs)) -> + Eff u fr '[] efs ~> ContT r (Eff u fr '[] efs) +interposeContT f = + interpretContTAll + \u -> case projectRec u of + Just (LiftIns e) -> f e + Nothing -> lift $ injectF u +{-# INLINE interposeContT #-} + +interposeFin :: + forall e f efs fr u c. + (Freer c fr, Union u, Member u e efs, c f) => + u efs Nop ~> f -> + e ~> f -> + Eff u fr '[] efs ~> f +interposeFin liftFin f = + interpretAll + \u -> case projectRec u of + Just (LiftIns e) -> f e + Nothing -> liftFin u +{-# INLINE interposeFin #-} + +interposeT :: + forall e t efs fr u c. + ( Freer c fr + , Union u + , MonadTrans t + , Member u e efs + , Monad (Eff u fr '[] efs) + , c (t (Eff u fr '[] efs)) + ) => + e ~> t (Eff u fr '[] efs) -> + Eff u fr '[] efs ~> t (Eff u fr '[] efs) +interposeT = interposeFin $ lift . injectF +{-# INLINE interposeT #-} + +interposeRec :: + forall e ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), Member u e efs) => + e ~> Eff u fr ehs efs -> + Eff u fr ehs efs ~> Eff u fr ehs efs +interposeRec f = + interpretAllRec + \u -> case projectRec u of + Just (LiftIns e) -> f e + Nothing -> injectF u +{-# INLINE interposeRec #-} + +interposeRecH :: + forall e ehs efs fr u c. + (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u ehs, MemberH u e ehs) => + e (Eff u fr ehs efs) ~> Eff u fr ehs efs -> + Eff u fr ehs efs ~> Eff u fr ehs efs +interposeRecH f = + interpretAllH + \u -> case projectRec u of + Just e -> f e + Nothing -> injectH u +{-# INLINE interposeRecH #-} + +interpretAll :: + forall g efs fr u c. + (Freer c fr, Union u, c g) => + u efs Nop ~> g -> + Eff u fr '[] efs ~> g +interpretAll = interpretAllFH exhaust +{-# INLINE interpretAll #-} + +interpretAllE :: + forall ehs' efs' efs fr u c. + (Freer c fr, Union u) => + u efs Nop ~> Eff u fr ehs' efs' -> + Eff u fr '[] efs ~> Eff u fr ehs' efs' +interpretAllE = interpretAllFHE exhaust +{-# INLINE interpretAllE #-} + +interpretAllRecH :: + forall ehs' ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs -> + Eff u fr ehs efs ~> Eff u fr ehs' efs +interpretAllRecH fh = + interpretAllH $ fh . hfmap (interpretAllRecH fh) + +interpretAllH :: + forall ehs' ehs efs fr u c. + (Freer c fr, Union u) => + u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs -> + Eff u fr ehs efs ~> Eff u fr ehs' efs +interpretAllH fh = interpretAllFHE fh injectF +{-# INLINE interpretAllH #-} + +interpretAllRecFH :: + forall g ehs efs fr u c. + (Freer c fr, Union u, c g, HFunctor (u ehs)) => + u ehs g ~> g -> + u efs Nop ~> g -> + Eff u fr ehs efs ~> g +interpretAllRecFH fh ff = + interpretAllFH (fh . hfmap (interpretAllRecFH fh ff)) ff + +interpretAllFH :: + forall g ehs efs fr u c. + (Freer c fr, Union u, c g) => + u ehs (Eff u fr ehs efs) ~> g -> + u efs Nop ~> g -> + Eff u fr ehs efs ~> g +interpretAllFH fh ff = interpretFreer (caseHF fh ff) . unHefty +{-# INLINE interpretAllFH #-} + +interpretAllRecFHE :: + forall ehs' efs' ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs' -> + u efs Nop ~> Eff u fr ehs' efs' -> + Eff u fr ehs efs ~> Eff u fr ehs' efs' +interpretAllRecFHE fh ff = + interpretAllFHE (fh . hfmap (interpretAllRecFHE fh ff)) ff +{-# INLINE interpretAllRecFHE #-} + +interpretAllFHE :: + forall ehs' efs' ehs efs fr u c. + (Freer c fr, Union u) => + u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs' -> + u efs Nop ~> Eff u fr ehs' efs' -> + Eff u fr ehs efs ~> Eff u fr ehs' efs' +interpretAllFHE fh ff = + overHefty $ interpretFreer $ unHefty . caseHF fh ff + +interpretKAll :: + forall r a efs fr u c. + (MonadFreer c fr, Union u) => + (a -> Eff u fr '[] efs r) -> + (forall x. (x -> Eff u fr '[] efs r) -> u efs Nop x -> Eff u fr '[] efs r) -> + Eff u fr '[] efs a -> + Eff u fr '[] efs r +interpretKAll = toInterpretKFromContT interpretContTAll +{-# INLINE interpretKAll #-} + +interpretKAllRecH :: + forall ehs' r a ehs efs fr u c. + (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) => + (a -> Eff u fr ehs' efs r) -> + ( forall x. + (x -> Eff u fr ehs' efs r) -> + u ehs (ContT r (Eff u fr ehs' efs)) x -> + Eff u fr ehs' efs r + ) -> + Eff u fr ehs efs a -> + Eff u fr ehs' efs r +interpretKAllRecH = toInterpretKFromContT interpretContTAllRecH +{-# INLINE interpretKAllRecH #-} + +interpretKAllH :: + forall ehs' r a ehs efs fr u c. + (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) => + (a -> Eff u fr ehs' efs r) -> + ( forall x. + (x -> Eff u fr ehs' efs r) -> + u ehs (Eff u fr ehs efs) x -> + Eff u fr ehs' efs r + ) -> + Eff u fr ehs efs a -> + Eff u fr ehs' efs r +interpretKAllH = toInterpretKFromContT interpretContTAllH +{-# INLINE interpretKAllH #-} + +interpretKAllRecFH :: + forall g r a ehs efs fr u c. + (MonadFreer c fr, Union u, HFunctor (u ehs)) => + (a -> g r) -> + (forall x. (x -> g r) -> u ehs (ContT r g) x -> g r) -> + (forall x. (x -> g r) -> u efs Nop x -> g r) -> + Eff u fr ehs efs a -> + g r +interpretKAllRecFH = toInterpretKFromContT2 interpretContTAllRecFH +{-# INLINE interpretKAllRecFH #-} + +interpretKAllFH :: + forall g r a ehs efs fr u c. + (MonadFreer c fr, Union u) => + (a -> g r) -> + (forall x. (x -> g r) -> u ehs (Eff u fr ehs efs) x -> g r) -> + (forall x. (x -> g r) -> u efs Nop x -> g r) -> + Eff u fr ehs efs a -> + g r +interpretKAllFH = toInterpretKFromContT2 interpretContTAllFH +{-# INLINE interpretKAllFH #-} + +interpretContTAll :: + forall g r efs fr u c. + (MonadFreer c fr, Union u) => + u efs Nop ~> ContT r g -> + Eff u fr '[] efs ~> ContT r g +interpretContTAll f = + transCont + . interpretFreerK (caseHF exhaust (detransContT . f)) + . unHefty + +interpretContTAllRecH :: + forall ehs' r ehs efs fr u c. + (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) => + u ehs (ContT r (Eff u fr ehs' efs)) ~> ContT r (Eff u fr ehs' efs) -> + Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs) +interpretContTAllRecH fh = interpretContTAllRecFH fh (lift . injectF) +{-# INLINE interpretContTAllRecH #-} + +interpretContTAllH :: + forall ehs' r ehs efs fr u c. + (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) => + u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs) -> + Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs) +interpretContTAllH fh = interpretContTAllFH fh (lift . injectF) +{-# INLINE interpretContTAllH #-} + +interpretContTAllRecFH :: + forall g r ehs efs fr u c. + (MonadFreer c fr, Union u, HFunctor (u ehs)) => + u ehs (ContT r g) ~> ContT r g -> + u efs Nop ~> ContT r g -> + Eff u fr ehs efs ~> ContT r g +interpretContTAllRecFH fh ff = + transCont + . interpretFreerK (detransContT . caseHF (fh . hfmap (interpretContTAllRecFH fh ff)) ff) + . unHefty + +interpretContTAllFH :: + forall g r ehs efs fr u c. + (MonadFreer c fr, Union u) => + u ehs (Eff u fr ehs efs) ~> ContT r g -> + u efs Nop ~> ContT r g -> + Eff u fr ehs efs ~> ContT r g +interpretContTAllFH fh ff = + transCont + . interpretFreerK (detransContT . caseHF fh ff) + . unHefty + +transCont :: Cont (m r) ~> ContT r m +transCont (ContT f) = ContT \k -> coerce $ f $ coerce . k +{-# INLINE transCont #-} + +detransContT :: ContT r m ~> Cont (m r) +detransContT (ContT f) = ContT \k -> coerce $ f $ coerce . k +{-# INLINE detransContT #-} + +toInterpretKFromContT :: + ((e ~> ContT r m) -> f ~> ContT r m') -> + (a -> m' r) -> + (forall x. (x -> m r) -> e x -> m r) -> + f a -> + m' r +toInterpretKFromContT intContT k i = (`runContT` k) . intContT \e -> ContT (`i` e) +{-# INLINE toInterpretKFromContT #-} + +toInterpretKFromContT2 :: + ((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m') -> + (a -> m' r) -> + (forall x. (x -> m r) -> e1 x -> m r) -> + (forall x. (x -> m r) -> e2 x -> m r) -> + f a -> + m' r +toInterpretKFromContT2 intContT k i1 i2 = + (`runContT` k) . intContT (\e -> ContT (`i1` e)) (\e -> ContT (`i2` e)) +{-# INLINE toInterpretKFromContT2 #-} + +interpretTAll :: + forall t g efs fr u c. + (Freer c fr, Union u, c (t g)) => + u efs Nop ~> t g -> + Eff u fr '[] efs ~> t g +interpretTAll = interpretAll +{-# INLINE interpretTAll #-} + +interpretTAllRecH :: + forall ehs' t ehs efs fr u c. + ( Freer c fr + , Union u + , MonadTrans t + , HFunctor (u ehs) + , Monad (Eff u fr ehs' efs) + , c (t (Eff u fr ehs' efs)) + ) => + u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs) -> + Eff u fr ehs efs ~> t (Eff u fr ehs' efs) +interpretTAllRecH i = interpretAllRecFH i (lift . injectF) +{-# INLINE interpretTAllRecH #-} + +interpretTAllH :: + forall ehs' t ehs efs fr u c. + (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs' efs), c (t (Eff u fr ehs' efs))) => + u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs) -> + Eff u fr ehs efs ~> t (Eff u fr ehs' efs) +interpretTAllH i = interpretAllFH i (lift . injectF) +{-# INLINE interpretTAllH #-} + +interpretAllRec :: + forall efs' ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u efs Nop ~> Eff u fr ehs efs' -> + Eff u fr ehs efs ~> Eff u fr ehs efs' +interpretAllRec = interpretAllRecFHE injectH +{-# INLINE interpretAllRec #-} + +transform :: + forall e2 e1 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) => + (UnliftIfSingle e1 ~> UnliftIfSingle e2) -> + Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r) +transform f = + transformAll $ + inject0 . liftInsIfSingle . f . unliftInsIfSingle |+: weaken +{-# INLINE transform #-} + +transformH :: + forall e2 e1 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e1 ': r))) => + (e1 (Eff u fr (e2 ': r) efs) ~> e2 (Eff u fr (e2 ': r) efs)) -> + Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs +transformH f = transformAllH $ inject0 . f |+: weaken +{-# INLINE transformH #-} + +transformFH :: + forall e2h e2f e1h e1f rh rf fr u c. + (Freer c fr, Union u, HFunctor (u (e1h ': rh)), HeadIns e1f, HeadIns e2f) => + (e1h (Eff u fr (e2h ': rh) (e2f ': rf)) ~> e2h (Eff u fr (e2h ': rh) (e2f ': rf))) -> + (UnliftIfSingle e1f ~> UnliftIfSingle e2f) -> + Eff u fr (e1h ': rh) (e1f ': rf) ~> Eff u fr (e2h ': rh) (e2f ': rf) +transformFH fh ff = + transformAllFH + (inject0 . fh |+: weaken) + (inject0 . liftInsIfSingle . ff . unliftInsIfSingle |+: weaken) +{-# INLINE transformFH #-} + +translate :: + forall e2 e1 es ehs fr u c. + (Freer c fr, Union u, Member u e2 es, HFunctor (u ehs), HeadIns e1) => + (UnliftIfSingle e1 ~> e2) -> + Eff u fr ehs (e1 ': es) ~> Eff u fr ehs es +translate f = + transformAll $ + injectRec . LiftIns . f . unliftInsIfSingle |+: id +{-# INLINE translate #-} + +translateH :: + forall e2 e1 es efs fr u c. + (Freer c fr, Union u, MemberH u e2 es, HFunctor (u (e1 ': es))) => + (e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs)) -> + Eff u fr (e1 ': es) efs ~> Eff u fr es efs +translateH f = transformAllH $ injectRec . f |+: id +{-# INLINE translateH #-} + +translateFH :: + forall e2h e2f e1h e1f ehs efs fr u c. + ( Freer c fr + , Union u + , MemberH u e2h ehs + , Member u e2f efs + , HFunctor (u (e1h ': ehs)) + , HeadIns e1f + ) => + (e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs)) -> + (UnliftIfSingle e1f ~> e2f) -> + Eff u fr (e1h ': ehs) (e1f ': efs) ~> Eff u fr ehs efs +translateFH fh ff = + transformAllFH + (injectRec . fh |+: id) + (injectRec . LiftIns . ff . unliftInsIfSingle |+: id) +{-# INLINE translateFH #-} + +rewrite :: + forall e efs ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), Member u e efs) => + (e ~> e) -> + Eff u fr ehs efs ~> Eff u fr ehs efs +rewrite f = + transformAll + \u -> case projectRec u of + Just (LiftIns e) -> injectRec $ LiftIns $ f e + Nothing -> u +{-# INLINE rewrite #-} + +rewriteH :: + forall e efs ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), MemberH u e ehs) => + (e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)) -> + Eff u fr ehs efs ~> Eff u fr ehs efs +rewriteH f = + transformAllH + \u -> case projectRec u of + Just e -> injectRec $ f e + Nothing -> u +{-# INLINE rewriteH #-} + +rewriteFH :: + forall eh ef efs ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), MemberH u eh ehs, Member u ef efs) => + (eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)) -> + (ef ~> ef) -> + Eff u fr ehs efs ~> Eff u fr ehs efs +rewriteFH fh ff = + transformAllFH + ( \u -> case projectRec u of + Just e -> injectRec $ fh e + Nothing -> u + ) + ( \u -> case projectRec u of + Just (LiftIns e) -> injectRec $ LiftIns $ ff e + Nothing -> u + ) +{-# INLINE rewriteFH #-} + +transformAll :: + forall efs' efs ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u efs Nop ~> u efs' Nop -> + Eff u fr ehs efs ~> Eff u fr ehs efs' +transformAll = transformAllFH id +{-# INLINE transformAll #-} + +transformAllH :: + forall ehs' ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs) -> + Eff u fr ehs efs ~> Eff u fr ehs' efs +transformAllH f = transformAllFH f id +{-# INLINE transformAllH #-} + +transformAllFH :: + forall ehs' efs' ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs') -> + (u efs Nop ~> u efs' Nop) -> + Eff u fr ehs efs ~> Eff u fr ehs' efs' +transformAllFH fh ff = + overHefty $ + transformFreer $ + EffUnion + . caseHF + (L1 . fh . hfmap (transformAllFH fh ff)) + (R1 . ff) + +raise :: + forall e r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs r ~> Eff u fr ehs (e ': r) +raise = transformAll weaken +{-# INLINE raise #-} + +raiseH :: + forall e r efs fr u c. + (Freer c fr, Union u, HFunctor (u r)) => + Eff u fr r efs ~> Eff u fr (e ': r) efs +raiseH = transformAllH weaken +{-# INLINE raiseH #-} + +raise2H :: + forall e2 e1 r efs fr u c. + (Freer c fr, Union u, HFunctor (u r)) => + Eff u fr r efs ~> Eff u fr (e2 ': e1 ': r) efs +raise2H = transformAllH weaken2 +{-# INLINE raise2H #-} + +raiseUnder :: + forall e1 e2 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r) +raiseUnder = transformAll weakenUnder +{-# INLINE raiseUnder #-} + +raiseUnder2 :: + forall e1 e2 e3 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e3 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r) +raiseUnder2 = transformAll weakenUnder2 +{-# INLINE raiseUnder2 #-} + +raiseUnder3 :: + forall e1 e2 e3 e4 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e4 ': e3 ': e2 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r) +raiseUnder3 = transformAll weakenUnder3 +{-# INLINE raiseUnder3 #-} + +raise2Under2 :: + forall e1 e2 e3 e4 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e4 ': e3 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r) +raise2Under2 = transformAll weaken2Under2 +{-# INLINE raise2Under2 #-} + +raise2Under :: + forall e1 e2 e3 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r) +raise2Under = transformAll weaken2Under +{-# INLINE raise2Under #-} + +raise3Under :: + forall e1 e2 e3 e4 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e4 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r) +raise3Under = transformAll weaken3Under +{-# INLINE raise3Under #-} + +raiseUnderH :: + forall e1 e2 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e2 ': r))) => + Eff u fr (e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs +raiseUnderH = transformAllH weakenUnder +{-# INLINE raiseUnderH #-} + +raiseUnder2H :: + forall e1 e2 e3 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e3 ': e2 ': r))) => + Eff u fr (e3 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs +raiseUnder2H = transformAllH weakenUnder2 +{-# INLINE raiseUnder2H #-} + +raiseUnder3H :: + forall e1 e2 e3 e4 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': e2 ': r))) => + Eff u fr (e4 ': e3 ': e2 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs +raiseUnder3H = transformAllH weakenUnder3 +{-# INLINE raiseUnder3H #-} + +raise2Under2H :: + forall e1 e2 e3 e4 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': r))) => + Eff u fr (e4 ': e3 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs +raise2Under2H = transformAllH weaken2Under2 +{-# INLINE raise2Under2H #-} + +raise2UnderH :: + forall e1 e2 e3 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e3 ': r))) => + Eff u fr (e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs +raise2UnderH = transformAllH weaken2Under +{-# INLINE raise2UnderH #-} + +raise3UnderH :: + forall e1 e2 e3 e4 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e4 ': r))) => + Eff u fr (e4 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs +raise3UnderH = transformAllH weaken3Under +{-# INLINE raise3UnderH #-} + +raiseAll :: + forall ehs efs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs '[] ~> Eff u fr ehs efs +raiseAll = transformAll exhaust +{-# INLINE raiseAll #-} + +raiseAllH :: + forall ehs efs fr u c. + (Freer c fr, Union u) => + Eff u fr '[] efs ~> Eff u fr ehs efs +raiseAllH = overHefty $ transformFreer $ EffUnion . caseHF exhaust R1 +{-# INLINE raiseAllH #-} + +flipEff :: + forall e1 e2 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e1 ': e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r) +flipEff = transformAll flipUnion +{-# INLINE flipEff #-} + +flipEff3 :: + forall e1 e2 e3 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e1 ': e2 ': e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r) +flipEff3 = transformAll flipUnion3 +{-# INLINE flipEff3 #-} + +flipEffUnder :: + forall e1 e2 e3 r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (e3 ': e1 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r) +flipEffUnder = transformAll flipUnionUnder +{-# INLINE flipEffUnder #-} + +flipEffH :: + forall e1 e2 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': r))) => + Eff u fr (e1 ': e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs +flipEffH = transformAllH flipUnion +{-# INLINE flipEffH #-} + +flipEff3H :: + forall e1 e2 e3 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': e3 ': r))) => + Eff u fr (e1 ': e2 ': e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs +flipEff3H = transformAllH flipUnion3 +{-# INLINE flipEff3H #-} + +flipEffUnderH :: + forall e1 e2 e3 r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e3 ': e1 ': e2 ': r))) => + Eff u fr (e3 ': e1 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs +flipEffUnderH = transformAllH flipUnionUnder +{-# INLINE flipEffUnderH #-} + +subsume :: + forall e r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), HasMembership u e r) => + Eff u fr ehs (e ': r) ~> Eff u fr ehs r +subsume = transformAll $ inject |+: id +{-# INLINE subsume #-} + +subsumeH :: + forall e r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembership u e r) => + Eff u fr (e ': r) efs ~> Eff u fr r efs +subsumeH = transformAllH $ inject |+: id +{-# INLINE subsumeH #-} + +liftInsEff :: + forall e eh ef fr u c. + (Freer c fr, Union u, HFunctor (u eh), HFunctor e) => + Eff u fr eh (e ': ef) ~> Eff u fr (e ': eh) ef +liftInsEff = + overHefty $ + transformFreer $ + EffUnion + . caseHF + (L1 . weaken . hfmap liftInsEff) + (L1 . inject0 . hfmap \case {} |+: R1) + +splitEff :: + forall fr' e r ehs fr u c. + (Freer c fr', Freer c fr, Union u, HeadIns e) => + Eff u fr '[] (e ': r) ~> fr' (UnliftIfSingle e + Eff u fr ehs r) +splitEff = interpretAll $ liftIns . (L1 . unliftInsIfSingle |+: R1 . injectF) +{-# INLINE splitEff #-} + +mergeEff :: + forall fr' e r ehs fr u c. + (Freer c fr', Freer c fr, Union u, HeadIns e, c (Eff u fr ehs (e ': r)), HFunctor (u ehs)) => + fr' (UnliftIfSingle e + Eff u fr ehs r) ~> Eff u fr ehs (e ': r) +mergeEff = interpretFreer $ caseF send0 raise +{-# INLINE mergeEff #-} + +mergeEffH :: + forall fr' e r efs fr u c. + ( Freer c fr' + , Freer c fr + , Union u + , c (Eff u fr (e ': r) efs) + , HFunctor (u r) + , HFunctor e + ) => + Hefty fr' (e :+: LiftIns (Eff u fr r efs)) ~> Eff u fr (e ': r) efs +mergeEffH = + interpretFreer + ( caseH + (send0H . hfmap mergeEffH) + (raiseH . unliftIns) + ) + . unHefty + +send0 :: (Freer c fr, Union u, HeadIns e) => UnliftIfSingle e ~> Eff u fr eh (e ': r) +send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle +{-# INLINE send0 #-} + +send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r) +send1 = Hefty . liftIns . EffUnion . R1 . weaken . inject0 . liftInsIfSingle +{-# INLINE send1 #-} + +send0H :: (Freer c fr, Union u) => e (Eff u fr (e ': r) ef) ~> Eff u fr (e ': r) ef +send0H = Hefty . liftIns . EffUnion . L1 . inject0 +{-# INLINE send0H #-} + +send1H :: (Freer c fr, Union u) => e1 (Eff u fr (e2 ': e1 ': r) ef) ~> Eff u fr (e2 ': e1 ': r) ef +send1H = Hefty . liftIns . EffUnion . L1 . weaken . inject0 +{-# INLINE send1H #-} + +runEff :: forall f fr u c. (Freer c fr, Union u, c f) => Eff u fr '[] '[LiftIns f] ~> f +runEff = interpretAll $ id |+ exhaust +{-# INLINE runEff #-} + +runPure :: forall a fr u c. (Freer c fr, Union u, c Identity) => Eff u fr '[] '[] a -> a +runPure = runIdentity . interpretAll exhaust +{-# INLINE runPure #-} + +untagEff :: + forall tag e r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (LiftIns (e # tag) ': r) ~> Eff u fr ehs (LiftIns e ': r) +untagEff = transform unTag +{-# INLINE untagEff #-} + +untagEffH :: + forall tag e r efs fr u c. + (Freer c fr, Union u, HFunctor (u (e ## tag ': r))) => + Eff u fr (e ## tag ': r) efs ~> Eff u fr (e ': r) efs +untagEffH = transformH unTagH +{-# INLINE untagEffH #-} + +-- keyed effects + +instance + (MemberRec u (LiftIns (key #> e)) efs, LiftIns (key #> e) ~ FromJust (Lookup key efs)) => + InjectInsBy key e (EffUnion u ehs efs f) + where + injectInsBy = EffUnion . R1 . injectRec . LiftIns . Key @key + {-# INLINE injectInsBy #-} + +instance + (MemberRec u (key ##> e) ehs, key ##> e ~ FromJust (Lookup key ehs)) => + InjectSigBy key e (EffUnion u ehs efs) + where + injectSigBy = EffUnion . L1 . injectRec . KeyH @key + {-# INLINE injectSigBy #-} + +unkeyEff :: + forall key e r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs)) => + Eff u fr ehs (LiftIns (key #> e) ': r) ~> Eff u fr ehs (LiftIns e ': r) +unkeyEff = transform unKey +{-# INLINE unkeyEff #-} + +unkeyEffH :: + forall key e r efs fr u c. + (Freer c fr, Union u, HFunctor (u (key ##> e ': r))) => + Eff u fr (key ##> e ': r) efs ~> Eff u fr (e ': r) efs +unkeyEffH = transformH unKeyH +{-# INLINE unkeyEffH #-} + +keySubsume :: + forall key e r ehs fr u c. + (Freer c fr, Union u, HFunctor (u ehs), MemberBy u key e r) => + Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs r +keySubsume = interpretRec $ sendInsBy @key +{-# INLINE keySubsume #-} + +keySubsumeH :: + forall key e r efs fr u c. + (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u r, MemberHBy u key e r) => + Eff u fr (e ': r) efs ~> Eff u fr r efs +keySubsumeH = interpretRecH $ sendSigBy @key +{-# INLINE keySubsumeH #-} + +end :: Union u => u '[] f a -> x +end = exhaust +{-# INLINE end #-} diff --git a/src/Control/Freer.hs b/src/Control/Freer.hs --- a/src/Control/Freer.hs +++ b/src/Control/Freer.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} -- This Source Code Form is subject to the terms of the Mozilla Public -- License, v. 2.0. If a copy of the MPL was not distributed with this @@ -15,45 +17,147 @@ -} module Control.Freer where +import Control.Applicative (Alternative, empty, (<|>)) import Control.Applicative.Free (Ap, liftAp, runAp) -import Control.Effect.Class (type (~>)) +import Control.Applicative.Free.Fast qualified as Fast +import Control.Effect (SendIns, sendIns, type (~>)) +import Control.Effect.Key (SendInsBy, sendInsBy) +import Control.Monad (MonadPlus) +import Control.Monad.Base (MonadBase) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.State.Class (MonadState, get, put) +import Data.Bool (bool) +import Data.Effect (InsClass) +import Data.Effect.Fail (Fail (Fail)) +import Data.Effect.NonDet (Choose, Empty, choose) +import Data.Effect.NonDet qualified as NonDet +import Data.Effect.State (State, get'', put'') import Data.Functor.Coyoneda (Coyoneda, hoistCoyoneda, liftCoyoneda, lowerCoyoneda) +import Data.Kind (Type) -- | A type class to abstract away the encoding details of the Freer carrier. -class (forall ins. c (f ins)) => Freer c f | f -> c where - {-# MINIMAL liftIns, (interpretF | retract, transformF) #-} +class (forall e. c (f e)) => Freer c f | f -> c where + {-# MINIMAL liftIns, (interpretFreer | retractFreer, transformFreer) #-} -- | Lift a /instruction/ into a Freer carrier. - liftIns :: ins a -> f ins a + liftIns :: e a -> f e a - interpretF :: c m => (ins ~> m) -> f ins a -> m a - interpretF i = retract . transformF i - {-# INLINE interpretF #-} + interpretFreer :: c m => (e ~> m) -> f e a -> m a + interpretFreer i = retractFreer . transformFreer i + {-# INLINE interpretFreer #-} - retract :: c m => f m a -> m a - retract = interpretF id - {-# INLINE retract #-} + retractFreer :: c m => f m a -> m a + retractFreer = interpretFreer id + {-# INLINE retractFreer #-} -- | Translate /instruction/s embedded in a Freer carrier. - transformF :: - (ins ~> ins') -> - f ins a -> - f ins' a - transformF phi = interpretF $ liftIns . phi - {-# INLINE transformF #-} + transformFreer :: + (e ~> e') -> + f e a -> + f e' a + transformFreer phi = interpretFreer $ liftIns . phi + {-# INLINE transformFreer #-} - reinterpretF :: (ins ~> f ins) -> f ins a -> f ins a - reinterpretF = interpretF - {-# INLINE reinterpretF #-} + reinterpretFreer :: (e ~> f e) -> f e a -> f e a + reinterpretFreer = interpretFreer + {-# INLINE reinterpretFreer #-} instance Freer Functor Coyoneda where liftIns = liftCoyoneda - interpretF i = lowerCoyoneda . hoistCoyoneda i + interpretFreer i = lowerCoyoneda . hoistCoyoneda i {-# INLINE liftIns #-} - {-# INLINE interpretF #-} + {-# INLINE interpretFreer #-} instance Freer Applicative Ap where liftIns = liftAp - interpretF = runAp + interpretFreer = runAp {-# INLINE liftIns #-} - {-# INLINE interpretF #-} + {-# INLINE interpretFreer #-} + +instance Freer Applicative Fast.Ap where + liftIns = Fast.liftAp + interpretFreer = Fast.runAp + {-# INLINE liftIns #-} + {-# INLINE interpretFreer #-} + +newtype + ViaFreer + (fr :: InsClass -> Type -> Type) + (e :: InsClass) + (a :: Type) = ViaFreer + {viaFreer :: fr e a} + +deriving newtype instance Functor (fr e) => Functor (ViaFreer fr e) +deriving newtype instance Applicative (fr e) => Applicative (ViaFreer fr e) +deriving newtype instance Monad (fr e) => Monad (ViaFreer fr e) +deriving newtype instance (MonadBase b (fr e), Monad b) => MonadBase b (ViaFreer fr e) + +deriving newtype instance Foldable (fr e) => Foldable (ViaFreer fr e) +deriving stock instance Traversable (fr e) => Traversable (ViaFreer fr e) +deriving newtype instance Eq (fr e a) => Eq (ViaFreer fr e a) +deriving newtype instance Ord (fr e a) => Ord (ViaFreer fr e a) +deriving newtype instance Read (fr e a) => Read (ViaFreer fr e a) +deriving newtype instance Show (fr e a) => Show (ViaFreer fr e a) + +deriving newtype instance (Freer c fr, forall e. c (ViaFreer fr e)) => Freer c (ViaFreer fr) + +instance (Freer c fr, InjectIns e e') => SendIns e (ViaFreer fr e') where + sendIns = ViaFreer . liftIns . injectIns + {-# INLINE sendIns #-} + +class InjectIns e (e' :: InsClass) where + injectIns :: e ~> e' + +instance (Freer c fr, InjectInsBy key e e') => SendInsBy key e (ViaFreer fr e') where + sendInsBy = ViaFreer . liftIns . injectInsBy @key + {-# INLINE sendInsBy #-} + +class InjectInsBy key e (e' :: InsClass) | key e' -> e where + injectInsBy :: e ~> e' + +overFreer :: (fr e a -> fr' e' b) -> ViaFreer fr e a -> ViaFreer fr' e' b +overFreer f = ViaFreer . f . viaFreer +{-# INLINE overFreer #-} + +reencodeFreer :: (Freer c fr, Freer c' fr', c (fr' f)) => fr f ~> fr' f +reencodeFreer = interpretFreer liftIns +{-# INLINE reencodeFreer #-} + +instance (Freer c fr, InjectInsBy StateKey (State s) e, Monad (fr e)) => MonadState s (ViaFreer fr e) where + get = get'' @StateKey + put = put'' @StateKey + {-# INLINE get #-} + {-# INLINE put #-} + +data StateKey + +instance + ( Freer c fr + , InjectIns Empty e + , InjectIns Choose e + , Monad (fr e) + ) => + Alternative (ViaFreer fr e) + where + empty = NonDet.empty + a <|> b = do + world <- choose + bool a b world + {-# INLINE empty #-} + {-# INLINE (<|>) #-} + +instance + ( Freer c fr + , InjectIns Empty e + , InjectIns Choose e + , Monad (fr e) + ) => + MonadPlus (ViaFreer fr e) + +instance (Freer c fr, InjectIns IO e, Monad (fr e)) => MonadIO (ViaFreer fr e) where + liftIO = ViaFreer . liftIns . injectIns + {-# INLINE liftIO #-} + +instance (Freer c fr, InjectIns Fail e, Monad (fr e)) => MonadFail (ViaFreer fr e) where + fail = ViaFreer . liftIns . injectIns . Fail + {-# INLINE fail #-} diff --git a/src/Control/Freer/Final.hs b/src/Control/Freer/Final.hs new file mode 100644 --- /dev/null +++ b/src/Control/Freer/Final.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Use fmap" #-} +{-# HLINT ignore "Use const" #-} +{-# HLINT ignore "Avoid lambda" #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +A final-encoded generic Freer carrier. +-} +module Control.Freer.Final where + +import Control.Applicative (Alternative, empty, liftA2, many, some, (<|>)) +import Control.Effect (type (~>)) +import Control.Freer (Freer, interpretFreer, liftIns) +import Control.Monad (MonadPlus, mplus, mzero) +import Control.Monad.Freer (MonadFreer) + +-- | A final-encoded generic Freer carrier. +newtype FreerFinal c f a = FreerFinal {unFreerFinal :: forall m. c m => (f ~> m) -> m a} + +deriving stock instance (forall f. c f => Functor f) => Functor (FreerFinal c e) + +instance + (forall f. c f => Applicative f, Functor (FreerFinal c e)) => + Applicative (FreerFinal c e) + where + pure x = FreerFinal \_ -> pure x + + FreerFinal f <*> FreerFinal g = + FreerFinal \i -> f i <*> g i + + liftA2 f (FreerFinal fa) (FreerFinal fb) = + FreerFinal \i -> liftA2 f (fa i) (fb i) + + FreerFinal f *> FreerFinal g = + FreerFinal \i -> f i *> g i + + FreerFinal f <* FreerFinal g = + FreerFinal \i -> f i <* g i + + {-# INLINE pure #-} + {-# INLINE (<*>) #-} + {-# INLINE liftA2 #-} + {-# INLINE (*>) #-} + {-# INLINE (<*) #-} + +instance + (forall f. c f => Alternative f, Applicative (FreerFinal c e)) => + Alternative (FreerFinal c e) + where + empty = FreerFinal \_ -> empty + + FreerFinal f <|> FreerFinal g = + FreerFinal \i -> f i <|> g i + + some (FreerFinal f) = FreerFinal \i -> some (f i) + many (FreerFinal f) = FreerFinal \i -> many (f i) + + {-# INLINE empty #-} + {-# INLINE (<|>) #-} + {-# INLINE some #-} + {-# INLINE many #-} + +instance (forall m. c m => Monad m, Applicative (FreerFinal c f)) => Monad (FreerFinal c f) where + FreerFinal f >>= k = + FreerFinal \i -> + f i >>= interpretFreerFinal i . k + + (>>) = (*>) + return = pure + + {-# INLINE (>>=) #-} + {-# INLINE (>>) #-} + {-# INLINE return #-} + +instance + (forall m. c m => MonadPlus m, Alternative (FreerFinal c f), Monad (FreerFinal c f)) => + MonadPlus (FreerFinal c f) + where + mzero = FreerFinal \_ -> mzero + + FreerFinal f `mplus` FreerFinal g = + FreerFinal \i -> f i `mplus` g i + + {-# INLINE mzero #-} + {-# INLINE mplus #-} + +interpretFreerFinal :: c f => (e ~> f) -> FreerFinal c e a -> f a +interpretFreerFinal i (FreerFinal f) = f i +{-# INLINE interpretFreerFinal #-} + +liftInsFinal :: ins a -> FreerFinal c ins a +liftInsFinal e = FreerFinal \i -> i e +{-# INLINE liftInsFinal #-} + +instance (forall e. c (FreerFinal c e)) => Freer c (FreerFinal c) where + liftIns = liftInsFinal + interpretFreer = interpretFreerFinal + {-# INLINE liftIns #-} + {-# INLINE interpretFreer #-} + +instance MonadFreer Monad (FreerFinal Monad) diff --git a/src/Control/Freer/Trans.hs b/src/Control/Freer/Trans.hs deleted file mode 100644 --- a/src/Control/Freer/Trans.hs +++ /dev/null @@ -1,70 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class to abstract away the encoding details of the Freer carrier transformers. --} -module Control.Freer.Trans where - -import Control.Effect.Class (type (~>)) -import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT) -import Data.Free.Sum (pattern L1, pattern R1, type (+)) - --- | A type class to abstract away the encoding details of the Freer carrier transformers. -class (forall ins f. c f => c (fr ins f)) => TransFreer c fr | fr -> c where - {-# MINIMAL liftInsT, liftLowerFT, (hoistFreer, runInterpretF | interpretFT) #-} - - -- | Lift a /instruction/ into a Freer carrier transformer. - liftInsT :: ins ~> fr ins f - - liftLowerFT :: forall ins f. c f => f ~> fr ins f - - -- | Translate /instruction/s embedded in a Freer carrier transformer. - transformT :: c f => (ins ~> ins') -> fr ins f ~> fr ins' f - transformT f = interpretFT liftLowerFT (liftInsT . f) - {-# INLINE transformT #-} - - -- | Translate an underlying carrier. - hoistFreer :: (c f, c g) => (f ~> g) -> fr ins f ~> fr ins g - hoistFreer f = interpretFT (liftLowerFT . f) liftInsT - {-# INLINE hoistFreer #-} - - interposeLowerT :: (c f, c g) => (f ~> fr ins g) -> fr ins f ~> fr ins g - interposeLowerT f = interpretFT f liftInsT - {-# INLINE interposeLowerT #-} - - runInterpretF :: c f => (ins ~> f) -> fr ins f a -> f a - default runInterpretF :: (c f, c (IdentityT f)) => (ins ~> f) -> fr ins f a -> f a - runInterpretF f = runIdentityT . interpretFT IdentityT (IdentityT . f) - {-# INLINE runInterpretF #-} - - interpretFT :: (c f, c g) => (f ~> g) -> (ins ~> g) -> fr ins f ~> g - interpretFT f i = runInterpretF i . hoistFreer f - {-# INLINE interpretFT #-} - - reinterpretFT :: c f => (ins ~> fr ins f) -> fr ins f ~> fr ins f - reinterpretFT = interpretFT liftLowerFT - {-# INLINE reinterpretFT #-} - -mergeFreer :: - forall fr m ins ins' c. - (TransFreer c fr, c m) => - fr ins (fr ins' m) ~> fr (ins + ins') m -mergeFreer = interpretFT (transformT @c R1) (liftInsT @c . L1) - -splitFreer :: - forall fr m ins ins' c. - (TransFreer c fr, c m) => - fr (ins + ins') m ~> fr ins (fr ins' m) -splitFreer = interpretFT (liftLowerFT . liftLowerFT) \case - L1 e -> liftInsT e - R1 e -> liftLowerFT $ liftInsT e diff --git a/src/Control/Heftia.hs b/src/Control/Heftia.hs deleted file mode 100644 --- a/src/Control/Heftia.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class to abstract away the encoding details of the Heftia carriers. --} -module Control.Heftia where - -import Control.Effect.Class (LiftIns, unliftIns, type (~>)) -import Control.Effect.Class.Machinery.HFunctor (HFunctor) - --- | A type class to abstract away the encoding details of the Heftia carrier. -class (forall sig. HFunctor sig => c (h sig)) => Heftia c h | h -> c where - {-# MINIMAL liftSig, interpretHH #-} - - -- | Lift a /signature/ into a Heftia carrier. - liftSig :: HFunctor sig => sig (h sig) a -> h sig a - - interpretHH :: (c m, HFunctor sig) => (sig m ~> m) -> h sig a -> m a - - -- | Translate /signature/s embedded in a Heftia carrier. - translateHH :: - (HFunctor sig, HFunctor sig') => - (sig (h sig') ~> sig' (h sig')) -> - h sig a -> - h sig' a - translateHH phi = interpretHH $ liftSig . phi - {-# INLINE translateHH #-} - - reinterpretHH :: HFunctor sig => (sig (h sig) ~> h sig) -> h sig a -> h sig a - reinterpretHH = interpretHH - {-# INLINE reinterpretHH #-} - -retractH :: (Heftia c h, c m) => h (LiftIns m) a -> m a -retractH = interpretHH unliftIns -{-# INLINE retractH #-} diff --git a/src/Control/Heftia/Trans.hs b/src/Control/Heftia/Trans.hs deleted file mode 100644 --- a/src/Control/Heftia/Trans.hs +++ /dev/null @@ -1,89 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} - -{-# HLINT ignore "Eta reduce" #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class to abstract away the encoding details of the Heftia carrier transformers. --} -module Control.Heftia.Trans where - -import Control.Effect.Class (LiftIns (LiftIns), unliftIns, type (~>)) -import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr)) -import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT) -import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT) - --- | A type class to abstract away the encoding details of the Heftia carrier transformers. -class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where - {-# MINIMAL liftSigT, liftLowerHT, (hoistHeftia, runElaborateH | elaborateHT) #-} - - -- | Lift a /signature/ into a Heftia carrier transformer. - liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a - - transformHT :: - (c f, HFunctor sig, HFunctor sig') => - (forall g. sig g ~> sig' g) -> - h sig f ~> h sig' f - transformHT f = translateT f - {-# INLINE transformHT #-} - - -- | Translate /signature/s embedded in a Heftia carrier transformer. - translateT :: - (c f, HFunctor sig, HFunctor sig') => - (sig (h sig' f) ~> sig' (h sig' f)) -> - h sig f ~> h sig' f - translateT f = elaborateHT liftLowerHT (liftSigT . f) - {-# INLINE translateT #-} - - liftLowerHT :: forall sig f. (c f, HFunctor sig) => f ~> h sig f - - -- | Translate an underlying monad. - hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f ~> h sig g - hoistHeftia phi = elaborateHT (liftLowerHT . phi) liftSigT - {-# INLINE hoistHeftia #-} - - interpretLowerHT :: (HFunctor sig, c f, c g) => (f ~> h sig g) -> h sig f ~> h sig g - interpretLowerHT f = elaborateHT f liftSigT - {-# INLINE interpretLowerHT #-} - - runElaborateH :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f ~> f - default runElaborateH :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f ~> f - runElaborateH f = runIdentityT . elaborateHT IdentityT (IdentityT . f . hfmap runIdentityT) - {-# INLINE runElaborateH #-} - - elaborateHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f ~> g - elaborateHT f i = runElaborateH i . hoistHeftia f - {-# INLINE elaborateHT #-} - - reelaborateHT :: (c f, HFunctor sig) => (sig (h sig f) ~> h sig f) -> h sig f ~> h sig f - reelaborateHT = elaborateHT liftLowerHT - {-# INLINE reelaborateHT #-} - -heftiaToFreer :: - (TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) => - h (LiftIns ins) f ~> fr ins f -heftiaToFreer = elaborateHT liftLowerFT (liftInsT . unliftIns) -{-# INLINE heftiaToFreer #-} - -freerToHeftia :: - (TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f), c' (h (LiftIns ins) f), c f) => - fr ins f ~> h (LiftIns ins) f -freerToHeftia = interpretFT liftLowerHT (liftSigT . LiftIns) -{-# INLINE freerToHeftia #-} - -mergeHeftia :: - forall h m sig sig' a c. - (HFunctor sig, HFunctor sig', TransHeftia c h, c m) => - h sig (h sig' m) a -> - h (sig :+: sig') m a -mergeHeftia = elaborateHT (translateT @c Inr) (liftSigT @c . Inl) diff --git a/src/Control/Hefty.hs b/src/Control/Hefty.hs new file mode 100644 --- /dev/null +++ b/src/Control/Hefty.hs @@ -0,0 +1,182 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +module Control.Hefty where + +import Control.Applicative (Alternative, empty, (<|>)) +import Control.Effect (SendIns (..), SendSig (..), type (~>)) +import Control.Effect.Key (ByKey (ByKey), SendInsBy, SendSigBy, key, sendInsBy, sendSigBy) +import Control.Freer (Freer (liftIns), InjectIns, InjectInsBy, StateKey, injectIns, injectInsBy) +import Control.Monad (MonadPlus) +import Control.Monad.Base (MonadBase) +import Control.Monad.Fix (MonadFix, mfix) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.RWS.Class (MonadRWS) +import Control.Monad.Reader.Class (MonadReader, ask, local) +import Control.Monad.State.Class (MonadState, get, put) +import Control.Monad.Writer.Class (MonadWriter, listen, pass, tell) +import Data.Effect (InsClass, SigClass) +import Data.Effect.Fail (Fail) +import Data.Effect.Fail qualified as E +import Data.Effect.Fix (Fix) +import Data.Effect.Fix qualified as E +import Data.Effect.NonDet (ChooseH, Empty, chooseH) +import Data.Effect.NonDet qualified as NonDet +import Data.Effect.Reader (Ask, Local, ask'', local'') +import Data.Effect.State (State, get'', put'') +import Data.Effect.Unlift (UnliftIO, pattern WithRunInIO) +import Data.Effect.Writer (Tell, WriterH, listen'', tell'') +import Data.Function ((&)) +import Data.Kind (Type) +import Data.Tuple (swap) +import UnliftIO (MonadUnliftIO, withRunInIO) + +newtype + Hefty + (f :: InsClass -> Type -> Type) + (e :: SigClass) + (a :: Type) = Hefty + {unHefty :: f (e (Hefty f e)) a} + +deriving newtype instance Functor (f (e (Hefty f e))) => Functor (Hefty f e) +deriving newtype instance Applicative (f (e (Hefty f e))) => Applicative (Hefty f e) +deriving newtype instance Monad (f (e (Hefty f e))) => Monad (Hefty f e) +deriving newtype instance (MonadBase b (f (e (Hefty f e))), Monad b) => MonadBase b (Hefty f e) + +deriving newtype instance Foldable (f (e (Hefty f e))) => Foldable (Hefty f e) +deriving stock instance Traversable (f (e (Hefty f e))) => Traversable (Hefty f e) +deriving newtype instance Eq (f (e (Hefty f e)) a) => Eq (Hefty f e a) +deriving newtype instance Ord (f (e (Hefty f e)) a) => Ord (Hefty f e a) +deriving newtype instance Read (f (e (Hefty f e)) a) => Read (Hefty f e a) +deriving newtype instance Show (f (e (Hefty f e)) a) => Show (Hefty f e a) + +overHefty :: + (f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b) -> + Hefty f e a -> + Hefty f' e' b +overHefty f = Hefty . f . unHefty +{-# INLINE overHefty #-} + +instance (Freer c fr, InjectIns e (e' (Hefty fr e'))) => SendIns e (Hefty fr e') where + sendIns = Hefty . liftIns . injectIns + {-# INLINE sendIns #-} + +instance (Freer c fr, InjectSig e e') => SendSig e (Hefty fr e') where + sendSig = Hefty . liftIns . injectSig + {-# INLINE sendSig #-} + +class InjectSig e (e' :: SigClass) where + injectSig :: e f ~> e' f + +instance (Freer c fr, InjectInsBy key e (e' (Hefty fr e'))) => SendInsBy key e (Hefty fr e') where + sendInsBy = Hefty . liftIns . injectInsBy @key + {-# INLINE sendInsBy #-} + +instance (Freer c fr, InjectSigBy key e e') => SendSigBy key e (Hefty fr e') where + sendSigBy = Hefty . liftIns . injectSigBy @key + {-# INLINE sendSigBy #-} + +class InjectSigBy key e (e' :: SigClass) | key e' -> e where + injectSigBy :: e f ~> e' f + +instance + ( Freer c fr + , InjectInsBy ReaderKey (Ask r) (e (Hefty fr e)) + , InjectSigBy ReaderKey (Local r) e + , Monad (fr (e (Hefty fr e))) + ) => + MonadReader r (Hefty fr e) + where + ask = ask'' @ReaderKey + local = local'' @ReaderKey + {-# INLINE ask #-} + {-# INLINE local #-} + +data ReaderKey + +instance + ( Freer c fr + , InjectInsBy WriterKey (Tell w) (e (Hefty fr e)) + , InjectSigBy WriterKey (WriterH w) e + , Monoid w + , Monad (fr (e (Hefty fr e))) + ) => + MonadWriter w (Hefty fr e) + where + tell = tell'' @WriterKey + listen = fmap swap . listen'' @WriterKey + pass m = pass (ByKey m) & key @WriterKey + {-# INLINE tell #-} + {-# INLINE listen #-} + +data WriterKey + +instance + (Freer c fr, InjectInsBy StateKey (State s) (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) => + MonadState s (Hefty fr e) + where + get = get'' @StateKey + put = put'' @StateKey + {-# INLINE get #-} + {-# INLINE put #-} + +instance + ( Freer c fr + , InjectInsBy ReaderKey (Ask r) (e (Hefty fr e)) + , InjectSigBy ReaderKey (Local r) e + , InjectInsBy WriterKey (Tell w) (e (Hefty fr e)) + , InjectSigBy WriterKey (WriterH w) e + , InjectInsBy StateKey (State s) (e (Hefty fr e)) + , Monoid w + , Monad (fr (e (Hefty fr e))) + ) => + MonadRWS r w s (Hefty fr e) + +instance + ( Freer c fr + , InjectIns Empty (e (Hefty fr e)) + , InjectSig ChooseH e + , Applicative (fr (e (Hefty fr e))) + ) => + Alternative (Hefty fr e) + where + empty = NonDet.empty + a <|> b = chooseH a b + {-# INLINE empty #-} + {-# INLINE (<|>) #-} + +instance + ( Freer c fr + , InjectIns Empty (e (Hefty fr e)) + , InjectSig ChooseH e + , Monad (fr (e (Hefty fr e))) + ) => + MonadPlus (Hefty fr e) + +instance (Freer c fr, InjectIns IO (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) => MonadIO (Hefty fr e) where + liftIO = sendIns + {-# INLINE liftIO #-} + +instance (Freer c fr, InjectIns Fail (e (Hefty fr e)), Monad (fr (e (Hefty fr e)))) => MonadFail (Hefty fr e) where + fail = E.fail + {-# INLINE fail #-} + +instance (Freer c fr, InjectSig Fix e, Monad (fr (e (Hefty fr e)))) => MonadFix (Hefty fr e) where + mfix = E.mfix + {-# INLINE mfix #-} + +instance + ( Freer c fr + , InjectIns IO (e (Hefty fr e)) + , InjectSig UnliftIO e + , Monad (fr (e (Hefty fr e))) + ) => + MonadUnliftIO (Hefty fr e) + where + withRunInIO f = Hefty . liftIns . injectSig $ WithRunInIO f + {-# INLINE withRunInIO #-} diff --git a/src/Control/Monad/Freer.hs b/src/Control/Monad/Freer.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Freer.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Eta reduce" #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +module Control.Monad.Freer where + +import Control.Effect (type (~>)) +import Control.Freer (Freer, interpretFreer) +import Control.Monad.Cont (Cont) + +class (Freer c fr, forall f. c f => Monad f) => MonadFreer c fr where + interpretFreerK :: (e ~> Cont r) -> fr e ~> Cont r + default interpretFreerK :: c (Cont r) => (e ~> Cont r) -> fr e ~> Cont r + interpretFreerK i = interpretFreer i + {-# INLINE interpretFreerK #-} diff --git a/src/Control/Monad/Freer/Church.hs b/src/Control/Monad/Freer/Church.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Freer/Church.hs @@ -0,0 +1,58 @@ +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +A Church-encoded Freer monad. +-} +module Control.Monad.Freer.Church where + +import Control.Effect (type (~>)) +import Control.Freer (Freer, interpretFreer, liftIns, retractFreer, transformFreer) +import Control.Monad.Cont (Cont, ContT (ContT), runCont) +import Control.Monad.Freer (MonadFreer, interpretFreerK) +import Control.Monad.Identity (Identity (Identity), runIdentity) +import Control.Monad.Trans.Free.Church (FT (FT), retract, transFT) + +-- | A Church encoded Freer monad. +newtype FreerChurch f a = FreerChurch {unFreerChurch :: FT f Identity a} + deriving newtype + ( Functor + , Applicative + , Monad + , Eq + , Ord + ) + deriving stock (Foldable, Traversable) + +liftInsChurch :: ins a -> FreerChurch ins a +liftInsChurch e = FreerChurch $ FT \k f -> f k e +{-# INLINE liftInsChurch #-} + +interpretChurch :: Monad m => (ins ~> m) -> FreerChurch ins a -> m a +interpretChurch i = retract . transFT i . unFreerChurch +{-# INLINE interpretChurch #-} + +interpretChurchK :: (e ~> Cont r) -> FreerChurch e ~> Cont r +interpretChurchK i (FreerChurch (FT f)) = + ContT \k -> f k \k' e -> Identity $ runCont (i e) (runIdentity . k') + +instance Freer Monad FreerChurch where + liftIns = liftInsChurch + interpretFreer = interpretChurch + retractFreer = retract . unFreerChurch + transformFreer phi = FreerChurch . transFT phi . unFreerChurch + {-# INLINE liftIns #-} + {-# INLINE interpretFreer #-} + {-# INLINE retractFreer #-} + {-# INLINE transformFreer #-} + +instance MonadFreer Monad FreerChurch where + interpretFreerK = interpretChurchK + {-# INLINE interpretFreerK #-} diff --git a/src/Control/Monad/Freer/Tree.hs b/src/Control/Monad/Freer/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Freer/Tree.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE DerivingVia #-} + +-- This Source Code Form is subject to the terms of the Mozilla Public +-- License, v. 2.0. If a copy of the MPL was not distributed with this +-- file, You can obtain one at https://mozilla.org/MPL/2.0/. + +{- | +Copyright : (c) 2023 Yamada Ryo +License : MPL-2.0 (see the file LICENSE) +Maintainer : ymdfield@outlook.jp +Stability : experimental +Portability : portable + +A tree-structured encoded Freer monad. +-} +module Control.Monad.Freer.Tree where + +import Control.Applicative (Alternative) +import Control.Effect (type (~>)) +import Control.Freer (Freer, interpretFreer, liftIns, transformFreer) +import Control.Monad (MonadPlus) +import Control.Monad.Cont (Cont, ContT (ContT), runCont) +import Control.Monad.Free (Free (Free, Pure), hoistFree, liftF) +import Control.Monad.Freer (MonadFreer, interpretFreerK) +import Control.Monad.Identity (Identity (Identity), runIdentity) +import Data.Functor.Coyoneda (Coyoneda (Coyoneda), hoistCoyoneda, liftCoyoneda) + +-- | A tree-structured encoded Freer monad. +newtype FreerTree f a = FreerTree {unFreerTree :: Free (Coyoneda f) a} + deriving newtype + ( Functor + , Applicative + , Monad + , Alternative + , MonadPlus + , Eq + , Ord + , Read + , Show + ) + deriving stock (Foldable, Traversable) + +liftInsTree :: ins a -> FreerTree ins a +liftInsTree = FreerTree . liftF . liftCoyoneda +{-# INLINE liftInsTree #-} + +interpretTree :: Monad m => (ins ~> m) -> FreerTree ins a -> m a +interpretTree i (FreerTree m) = + case m of + Pure x -> pure x + Free (Coyoneda f e) -> i e >>= interpretTree i . FreerTree . f + +interpretTreeK :: (e ~> Cont r) -> FreerTree e ~> Cont r +interpretTreeK i (FreerTree m) = + case m of + Pure x -> pure x + Free (Coyoneda f e) -> + ContT \k -> + Identity $ + runCont + (i e) + ((`runCont` runIdentity . k) . interpretTreeK i . FreerTree . f) + +instance Freer Monad FreerTree where + liftIns = liftInsTree + interpretFreer = interpretTree + transformFreer phi = FreerTree . hoistFree (hoistCoyoneda phi) . unFreerTree + {-# INLINE liftIns #-} + {-# INLINE interpretFreer #-} + {-# INLINE transformFreer #-} + +instance MonadFreer Monad FreerTree where + interpretFreerK = interpretTreeK + {-# INLINE interpretFreerK #-} diff --git a/src/Control/Monad/Trans/Freer.hs b/src/Control/Monad/Trans/Freer.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Freer.hs +++ /dev/null @@ -1,71 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class to abstract away the encoding details of the Freer monad transformers. --} -module Control.Monad.Trans.Freer where - -import Control.Effect.Class (Instruction, type (~>)) -import Control.Freer.Trans (TransFreer, hoistFreer, interpretFT, liftLowerFT) -import Control.Monad.Cont (ContT) -import Control.Monad.Trans (MonadTrans, lift) -import Data.Coerce (Coercible, coerce) -import Data.Kind (Type) - --- | A type class to abstract away the encoding details of the Freer monad transformers. -class - (TransFreer Monad fr, forall ins. MonadTrans (fr ins)) => - MonadTransFreer fr - where - interpretMK :: Monad m => (ins ~> ContT r m) -> fr ins m ~> ContT r m - interpretMK = interpretMT - {-# INLINE interpretMK #-} - - reinterpretMK :: Monad m => (ins ~> ContT r (fr ins m)) -> fr ins m ~> ContT r (fr ins m) - reinterpretMK = reinterpretMT - {-# INLINE reinterpretMK #-} - - interpretMT :: (Monad m, MonadTrans t, Monad (t m)) => (ins ~> t m) -> fr ins m ~> t m - interpretMT = interpretFT lift - {-# INLINE interpretMT #-} - - reinterpretMT :: - forall m t n ins. - (Monad m, MonadTrans t, Coercible n (fr ins m), Monad (t n), Monad n) => - (ins ~> t n) -> - fr ins m ~> t n - reinterpretMT f = interpretMT f . hoistFreer (coerce . liftLowerFT @Monad @fr @ins) - {-# INLINE reinterpretMT #-} - -reinterpretTTViaFinal :: - forall fr m t n ins. - ( MonadTransFreer fr - , Monad m - , MonadTrans t - , Coercible n (fr ins m) - , Monad (t n) - , Monad n - ) => - (ins ~> t n) -> - fr ins m ~> t n -reinterpretTTViaFinal = interpretFT $ lift . coerce . liftLowerFT @Monad @fr @ins -{-# INLINE reinterpretTTViaFinal #-} - -newtype ViaLiftLower (fr :: Instruction -> (Type -> Type) -> Type -> Type) ins m a = ViaLiftLower - {runViaLiftLower :: fr ins m a} - deriving newtype (Functor, Applicative, Monad) - deriving stock (Foldable, Traversable) - -instance TransFreer Monad h => MonadTrans (ViaLiftLower h ins) where - lift = ViaLiftLower . liftLowerFT - {-# INLINE lift #-} diff --git a/src/Control/Monad/Trans/Freer/Church.hs b/src/Control/Monad/Trans/Freer/Church.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Freer/Church.hs +++ /dev/null @@ -1,56 +0,0 @@ -{-# LANGUAGE DerivingVia #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A Church-encoded Freer transformer. --} -module Control.Monad.Trans.Freer.Church where - -import Control.Effect.Class (Instruction, LiftIns (..)) -import Control.Freer.Trans (TransFreer (hoistFreer, liftInsT, liftLowerFT, runInterpretF)) -import Control.Heftia.Trans (TransHeftia (..), liftSigT) -import Control.Monad.Trans (MonadTrans) -import Control.Monad.Trans.Freer ( - MonadTransFreer (interpretMK, reinterpretMK), - ViaLiftLower (ViaLiftLower), - ) -import Control.Monad.Trans.Heftia.Church (HeftiaChurchT (HeftiaChurchT)) - --- | A Church-encoded Freer transformer. -newtype FreerChurchT (ins :: Instruction) f a = FreerChurchT - {unFreerChurchT :: HeftiaChurchT (LiftIns ins) f a} - -deriving newtype instance Functor (FreerChurchT ins m) -deriving newtype instance Applicative (FreerChurchT ins m) -deriving newtype instance Monad (FreerChurchT ins m) - -instance TransFreer Monad FreerChurchT where - liftInsT = FreerChurchT . liftSigT . LiftIns - {-# INLINE liftInsT #-} - - liftLowerFT = FreerChurchT . liftLowerHT - {-# INLINE liftLowerFT #-} - - runInterpretF i = runElaborateH (i . unliftIns) . unFreerChurchT - {-# INLINE runInterpretF #-} - - hoistFreer phi = FreerChurchT . hoistHeftia phi . unFreerChurchT - {-# INLINE hoistFreer #-} - -deriving via ViaLiftLower FreerChurchT ins instance MonadTrans (FreerChurchT ins) - -instance MonadTransFreer FreerChurchT where - interpretMK f (FreerChurchT (HeftiaChurchT g)) = g $ f . unliftIns - {-# INLINE interpretMK #-} - - reinterpretMK f = interpretMK f . hoistFreer liftLowerFT - {-# INLINE reinterpretMK #-} diff --git a/src/Control/Monad/Trans/Freer/Tree.hs b/src/Control/Monad/Trans/Freer/Tree.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Freer/Tree.hs +++ /dev/null @@ -1,83 +0,0 @@ -{-# LANGUAGE DerivingVia #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A tree-structured encoded Freer transformer. --} -module Control.Monad.Trans.Freer.Tree where - -import Control.Applicative (Alternative) -import Control.Effect.Class (type (~>)) -import Control.Freer (Freer, interpretF, liftIns) -import Control.Monad (MonadPlus) -import Control.Monad.Base (MonadBase) -import Control.Monad.Identity (Identity, runIdentity) -import Control.Monad.Trans (MonadIO, MonadTrans) -import Control.Monad.Trans.Free (FreeF (Free, Pure), FreeT (FreeT), MonadFree, liftF) -import Data.Functor.Coyoneda (Coyoneda (Coyoneda), liftCoyoneda) - --- | A tree-structured encoded Freer transformer. -newtype FreerTreeT f m a = FreerTreeT {unFreerTreeT :: FreeT (Coyoneda f) m a} - deriving newtype - ( Functor - , Applicative - , Monad - , Alternative - , MonadPlus - , MonadBase b - , MonadIO - , MonadFail - , Eq - , Ord - , Read - , Show - , MonadTrans - ) - deriving stock (Foldable, Traversable) - -newtype FreerTreeMonad m f a = FreerTreeMonad {unFreerTreeMonad :: FreerTreeT f m a} - deriving newtype - ( Functor - , Applicative - , Alternative - , Monad - , MonadPlus - , MonadBase b - , MonadIO - , MonadFail - , Eq - , Ord - , Read - , Show - ) - deriving stock (Foldable, Traversable) - deriving (MonadFree (Coyoneda f)) via FreeT (Coyoneda f) m - -liftInsTree :: Monad m => ins a -> FreerTreeT ins m a -liftInsTree = FreerTreeT . liftF . liftCoyoneda -{-# INLINE liftInsTree #-} - -interpretTTree :: Monad n => (m ~> n) -> (ins ~> n) -> FreerTreeT ins m a -> n a -interpretTTree iLower i (FreerTreeT (FreeT m)) = - iLower m >>= \case - Pure x -> pure x - Free (Coyoneda f e) -> i e >>= interpretTTree iLower i . FreerTreeT . f - -type FreerTree = FreerTreeMonad Identity - -instance Freer Monad FreerTree where - liftIns = FreerTreeMonad . liftInsTree - interpretF i = interpretTTree (pure . runIdentity) i . unFreerTreeMonad - {-# INLINE liftIns #-} - {-# INLINE interpretF #-} - --- todo: MonadTransFreer instance diff --git a/src/Control/Monad/Trans/Heftia.hs b/src/Control/Monad/Trans/Heftia.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Heftia.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-# LANGUAGE QuantifiedConstraints #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class to abstract away the encoding details of the Heftia monad transformers. --} -module Control.Monad.Trans.Heftia where - -import Control.Effect.Class (Signature, type (~>)) -import Control.Effect.Class.Machinery.HFunctor (HFunctor) -import Control.Heftia.Trans (TransHeftia, elaborateHT, hoistHeftia, liftLowerHT) -import Control.Monad.Cont (ContT) -import Control.Monad.Trans (MonadTrans, lift) -import Data.Coerce (Coercible, coerce) -import Data.Kind (Type) - --- | A type class to abstract away the encoding details of the Heftia monad transformers. -class - (TransHeftia Monad h, forall sig. HFunctor sig => MonadTrans (h sig)) => - MonadTransHeftia h - where - elaborateMK :: - (Monad m, HFunctor sig) => - (sig (ContT r m) ~> ContT r m) -> - h sig m ~> ContT r m - elaborateMK = elaborateMT - {-# INLINE elaborateMK #-} - - reelaborateMK :: - (Monad m, HFunctor sig) => - (sig (ContT r (h sig m)) ~> ContT r (h sig m)) -> - h sig m ~> ContT r (h sig m) - reelaborateMK = reelaborateMT - {-# INLINE reelaborateMK #-} - - elaborateMT :: - (Monad m, MonadTrans t, Monad (t m), HFunctor sig) => - (sig (t m) ~> t m) -> - h sig m ~> t m - elaborateMT = elaborateHT lift - {-# INLINE elaborateMT #-} - - reelaborateMT :: - forall m t n sig. - (Monad m, MonadTrans t, Coercible n (h sig m), Monad (t n), Monad n, HFunctor sig) => - (sig (t n) ~> t n) -> - h sig m ~> t n - reelaborateMT f = elaborateMT f . hoistHeftia (coerce . liftLowerHT @Monad @h @sig) - {-# INLINE reelaborateMT #-} - -reinterpretHTTViaFinal :: - forall h m t n sig. - ( MonadTransHeftia h - , Monad m - , MonadTrans t - , Coercible n (h sig m) - , Monad (t n) - , Monad n - , HFunctor sig - ) => - (sig (t n) ~> t n) -> - h sig m ~> t n -reinterpretHTTViaFinal = elaborateHT $ lift . coerce . liftLowerHT @Monad @h @sig -{-# INLINE reinterpretHTTViaFinal #-} - -newtype ViaLiftLowerH (h :: Signature -> (Type -> Type) -> Type -> Type) sig m a = ViaLiftLowerH - {runViaLiftLowerH :: h sig m a} - deriving newtype (Functor, Applicative, Monad) - deriving stock (Foldable, Traversable) - -instance (TransHeftia Monad h, HFunctor sig) => MonadTrans (ViaLiftLowerH h sig) where - lift = ViaLiftLowerH . liftLowerHT - {-# INLINE lift #-} diff --git a/src/Control/Monad/Trans/Heftia/Church.hs b/src/Control/Monad/Trans/Heftia/Church.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Heftia/Church.hs +++ /dev/null @@ -1,77 +0,0 @@ --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A Church-encoded Heftia transformer. --} -module Control.Monad.Trans.Heftia.Church where - -import Control.Effect.Class (type (~>)) -import Control.Effect.Class.Machinery.HFunctor (hfmap) -import Control.Heftia.Trans (TransHeftia (..)) -import Control.Monad (join) -import Control.Monad.Trans (MonadTrans, lift) -import Control.Monad.Trans.Cont (ContT (ContT), runContT) -import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, reelaborateMK) - --- | A Church-encoded Heftia transformer. -newtype HeftiaChurchT h f a = HeftiaChurchT - {unHeftiaChurchT :: forall r. (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a} - deriving stock (Functor) - -runHeftiaChurchT :: (h (HeftiaChurchT h f) ~> ContT r f) -> HeftiaChurchT h f b -> ContT r f b -runHeftiaChurchT i (HeftiaChurchT f) = f i - -instance Applicative (HeftiaChurchT h f) where - pure x = HeftiaChurchT \_ -> pure x - {-# INLINE pure #-} - - HeftiaChurchT f <*> HeftiaChurchT g = HeftiaChurchT \i -> f i <*> g i - {-# INLINE (<*>) #-} - -instance Monad (HeftiaChurchT h f) where - HeftiaChurchT f >>= k = - HeftiaChurchT \i -> f i >>= runHeftiaChurchT i . k - {-# INLINE (>>=) #-} - -instance TransHeftia Monad HeftiaChurchT where - liftSigT e = HeftiaChurchT \i -> i e - {-# INLINE liftSigT #-} - - translateT phi (HeftiaChurchT f) = - HeftiaChurchT \i -> - f $ i . phi . hfmap (translateT phi) - - liftLowerHT a = HeftiaChurchT \_ -> lift a - {-# INLINE liftLowerHT #-} - - hoistHeftia phi (HeftiaChurchT f) = - HeftiaChurchT \i -> - ContT \k -> - join . phi $ - runContT - ( f \e -> ContT \k' -> - pure $ runContT (i $ hfmap (hoistHeftia phi) e) (join . phi . k') - ) - (pure . k) - - runElaborateH g (HeftiaChurchT f) = - runContT (f $ lift . g . hfmap (runElaborateH g)) pure - -instance MonadTrans (HeftiaChurchT h) where - lift m = HeftiaChurchT \_ -> lift m - {-# INLINE lift #-} - -instance MonadTransHeftia HeftiaChurchT where - elaborateMK f (HeftiaChurchT g) = g $ f . hfmap (elaborateMK f) - {-# INLINE elaborateMK #-} - - reelaborateMK f = elaborateMK f . hoistHeftia liftLowerHT - {-# INLINE reelaborateMK #-} diff --git a/src/Control/Monad/Trans/Heftia/Tree.hs b/src/Control/Monad/Trans/Heftia/Tree.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Heftia/Tree.hs +++ /dev/null @@ -1,20 +0,0 @@ --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A tree-structured encoded Heftia transformer. --} -module Control.Monad.Trans.Heftia.Tree where - -import Data.Functor.Coyoneda (Coyoneda) - -newtype HCoyoneda h f a = HCoyoneda {unHCoyoneda :: Coyoneda (h f) a} - --- todo diff --git a/src/Control/Monad/Trans/Hefty.hs b/src/Control/Monad/Trans/Hefty.hs deleted file mode 100644 --- a/src/Control/Monad/Trans/Hefty.hs +++ /dev/null @@ -1,72 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | - Copyright : (c) 2023 Yamada Ryo - (c) 2023 Casper Bach Poulsen and Cas van der Rest - License : MPL-2.0 (see the file LICENSE) - - Maintainer : ymdfield@outlook.jp - Stability : experimental - Portability : portable - - The data structure of hefty trees. --} -module Control.Monad.Trans.Hefty where - -import Control.Monad (ap) -import Control.Monad.Identity (Identity (Identity), runIdentity) -import Control.Monad.Trans (MonadTrans, lift) -import Control.Monad.Trans.Free (FreeF (Free, Pure)) -import Data.Functor ((<&>)) - --- | A hefty monad transformer. -newtype HeftyT h m a = HeftyT {runHeftyT :: m (FreeF (h (HeftyT h m)) a (HeftyT h m a))} - -instance (Functor m, Functor (h (HeftyT h m))) => Functor (HeftyT h m) where - fmap f (HeftyT m) = - HeftyT $ - m <&> \case - Pure x -> Pure $ f x - Free h -> Free $ fmap f <$> h - -instance (Monad m, Functor (h (HeftyT h m))) => Applicative (HeftyT h m) where - pure = HeftyT . pure . Pure - (<*>) = ap - - {-# INLINE pure #-} - {-# INLINE (<*>) #-} - -instance (Monad m, Functor (h (HeftyT h m))) => Monad (HeftyT h m) where - HeftyT m >>= k = - HeftyT $ - m >>= \case - Pure x -> runHeftyT $ k x - Free h -> return $ Free $ (k =<<) <$> h - -instance MonadTrans (HeftyT h) where - lift = liftHefty - {-# INLINE lift #-} - -{- | Lift a computation to a hefty monad. - - Note that this is less constrained than MonadTrans's lift (this one only - requires a Functor for underlying monad). --} -liftHefty :: Functor m => m a -> HeftyT h m a -liftHefty = HeftyT . fmap Pure -{-# INLINE liftHefty #-} - --- | A hefty monad. -type Hefty h = HeftyT h Identity - -hefty :: FreeF (h (Hefty h)) a (Hefty h a) -> Hefty h a -hefty = HeftyT . Identity -{-# INLINE hefty #-} - -runHefty :: Hefty h a -> FreeF (h (Hefty h)) a (Hefty h a) -runHefty = runIdentity . runHeftyT -{-# INLINE runHefty #-} diff --git a/src/Data/Free/Extensible.hs b/src/Data/Free/Extensible.hs deleted file mode 100644 --- a/src/Data/Free/Extensible.hs +++ /dev/null @@ -1,92 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -An implementation of an open union for first-order effects using -the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. --} -module Data.Free.Extensible where - -import Control.Effect.Class (Instruction) -import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match) -import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt)) -import Data.Free.Union ( - Union ( - HasMembership, - absurdUnion, - inject, - inject0, - project, - weaken, - (|+|:) - ), - ) -import Data.Proxy (Proxy (Proxy)) -import GHC.TypeNats (KnownNat, Nat, natVal, type (+)) -import Type.Membership (Membership, nextMembership) -import Unsafe.Coerce (unsafeCoerce) - -{- | -An implementation of an open union for first-order effects using -the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. --} -newtype ExtensibleUnion fs a = ExtensibleUnion {unExtensibleUnion :: fs :/ FieldApp a} - -newtype FieldApp a (f :: Instruction) = FieldApp {unFieldApp :: f a} - -instance Forall Functor fs => Functor (ExtensibleUnion fs) where - fmap f = - ExtensibleUnion - . match - ( htabulateFor @Functor Proxy \w -> - Match \e -> EmbedAt w $ FieldApp $ f <$> unFieldApp e - ) - . unExtensibleUnion - {-# INLINE fmap #-} - -{- todo: -instance Forall Foldable fs => Foldable (ExtensibleUnion fs) where -instance Forall Traversable fs => Traversable (ExtensibleUnion fs) where --} - -instance Union ExtensibleUnion where - type HasMembership _ f fs = KnownNat (TypeIndex fs f) - - inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp - {-# INLINE inject #-} - - project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u - {-# INLINE project #-} - - absurdUnion = exhaust . unExtensibleUnion - {-# INLINE absurdUnion #-} - - inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp - {-# INLINE inject0 #-} - - weaken (ExtensibleUnion (EmbedAt w e)) = - ExtensibleUnion $ EmbedAt (nextMembership w) e - {-# INLINE weaken #-} - - f |+|: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion - {-# INLINE (|+|:) #-} - -findFirstMembership :: forall xs x. KnownNat (TypeIndex xs x) => Membership xs x -findFirstMembership = unsafeMkMembership $ fromIntegral $ natVal @(TypeIndex xs x) Proxy - where - -- This hack may break if the membership package version gets updated. - unsafeMkMembership :: Int -> Membership xs x - unsafeMkMembership = unsafeCoerce - -type family TypeIndex (xs :: [k]) (x :: k) :: Nat where - TypeIndex (x ': xs) x = 0 - TypeIndex (y ': xs) x = 1 + TypeIndex xs x diff --git a/src/Data/Free/Sum.hs b/src/Data/Free/Sum.hs --- a/src/Data/Free/Sum.hs +++ b/src/Data/Free/Sum.hs @@ -1,32 +1,24 @@ -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE UndecidableInstances #-} - -- This Source Code Form is subject to the terms of the Mozilla Public -- License, v. 2.0. If a copy of the MPL was not distributed with this -- file, You can obtain one at https://mozilla.org/MPL/2.0/. --- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest. - {- | -Copyright : (c) 2023 Yamada Ryo - (c) 2023 Casper Bach Poulsen and Cas van der Rest +Copyright : (c) 2023-2024 Yamada Ryo License : MPL-2.0 (see the file LICENSE) Maintainer : ymdfield@outlook.jp Stability : experimental Portability : portable -An implementation of an open union for first-order effects using recursively nested binary sums. +Binary sums for first-order effects. -} module Data.Free.Sum (module Data.Free.Sum, pattern L1, pattern R1) where -import Control.Effect.Class (Instruction, NopI, type (~>)) -import Data.Free.Union (HasMembership, Union, absurdUnion, comp, decomp, inject, project) +import Control.Effect (type (~>)) +import Data.Effect (Nop) import GHC.Generics (type (:+:) (L1, R1)) -infixr 6 + - --- | A type synonym for disambiguation to the sum on the higher-order side. type (+) = (:+:) +infixr 5 + caseF :: (f a -> r) -> (g a -> r) -> (f + g) a -> r caseF f g = \case @@ -34,88 +26,14 @@ R1 x -> g x {-# INLINE caseF #-} -absurdL :: (NopI + f) ~> f +absurdL :: Nop + f ~> f absurdL = caseF \case {} id {-# INLINE absurdL #-} -absurdR :: (f + NopI) ~> f +absurdR :: f + Nop ~> f absurdR = caseF id \case {} {-# INLINE absurdR #-} swapSum :: (f + g) a -> (g + f) a swapSum = caseF R1 L1 {-# INLINE swapSum #-} - -type family Sum fs where - Sum '[] = NopI - Sum (f ': fs) = f :+: Sum fs - -{- | -An implementation of an open union for first-order effects using recursively nested binary sums. --} -newtype SumUnion fs a = SumUnion {unSumUnion :: Sum fs a} - -deriving newtype instance Functor (SumUnion '[]) -deriving newtype instance (Functor f, Functor (Sum fs)) => Functor (SumUnion (f ': fs)) - -deriving newtype instance Foldable (SumUnion '[]) -deriving newtype instance (Foldable f, Foldable (Sum fs)) => Foldable (SumUnion (f ': fs)) - -deriving stock instance Traversable (SumUnion '[]) -deriving stock instance (Traversable f, Traversable (Sum fs)) => Traversable (SumUnion (f ': fs)) - -instance Union SumUnion where - type HasMembership _ f fs = f < Sum fs - - inject sig = SumUnion $ inj sig - project (SumUnion sig) = proj sig - - absurdUnion = \case {} - - comp = - SumUnion . \case - Left x -> L1 x - Right (SumUnion x) -> R1 x - - decomp (SumUnion sig) = case sig of - L1 x -> Left x - R1 x -> Right (SumUnion x) - - {-# INLINE inject #-} - {-# INLINE project #-} - {-# INLINE absurdUnion #-} - -class isHead ~ f `IsHeadInsOf` g => SumMember isHead (f :: Instruction) g where - injSum :: f a -> g a - projSum :: g a -> Maybe (f a) - -type family (f :: Instruction) `IsHeadInsOf` g where - f `IsHeadInsOf` f + g = 'True - _ `IsHeadInsOf` _ = 'False - -type f < g = SumMember (IsHeadInsOf f g) f g - -inj :: forall f g. f < g => f ~> g -inj = injSum @(IsHeadInsOf f g) - -proj :: forall f g a. f < g => g a -> Maybe (f a) -proj = projSum - -instance SumMember 'True f (f + g) where - injSum = L1 - - projSum = \case - L1 x -> Just x - R1 _ -> Nothing - - {-# INLINE injSum #-} - {-# INLINE projSum #-} - -instance (f `IsHeadInsOf` (g + h) ~ 'False, f < h) => SumMember 'False f (g + h) where - injSum = R1 . inj - projSum = \case - L1 _ -> Nothing - R1 x -> projSum x - - {-# INLINE injSum #-} - {-# INLINE projSum #-} diff --git a/src/Data/Free/Union.hs b/src/Data/Free/Union.hs deleted file mode 100644 --- a/src/Data/Free/Union.hs +++ /dev/null @@ -1,150 +0,0 @@ --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - -{- | -Copyright : (c) 2023 Yamada Ryo -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -A type class representing a general open union for first-order effects, independent of the internal -implementation. --} -module Data.Free.Union where - -import Control.Effect.Class (Instruction, type (~>)) -import Data.Kind (Constraint) - -{- | -A type class representing a general open union for first-order effects, independent of the internal -implementation. --} -class Union (u :: [Instruction] -> Instruction) where - {-# MINIMAL inject, project, absurdUnion, (comp | (inject0, weaken), decomp | (|+|:)) #-} - - type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint - - inject :: HasMembership u f fs => f ~> u fs - project :: HasMembership u f fs => u fs a -> Maybe (f a) - - absurdUnion :: u '[] a -> x - - comp :: Either (f a) (u fs a) -> u (f ': fs) a - comp = \case - Left x -> inject0 x - Right x -> weaken x - {-# INLINE comp #-} - - decomp :: u (f ': fs) a -> Either (f a) (u fs a) - decomp = Left |+|: Right - {-# INLINE decomp #-} - - infixr 5 |+|: - (|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r - (f |+|: g) u = case decomp u of - Left x -> f x - Right x -> g x - {-# INLINE (|+|:) #-} - - inject0 :: f ~> u (f ': fs) - inject0 = comp . Left - {-# INLINE inject0 #-} - - injectUnder :: f2 ~> u (f1 ': f2 ': fs) - injectUnder = weaken . inject0 - {-# INLINE injectUnder #-} - - injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs) - injectUnder2 = weaken2 . inject0 - {-# INLINE injectUnder2 #-} - - injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs) - injectUnder3 = weaken3 . inject0 - {-# INLINE injectUnder3 #-} - - weaken :: u fs a -> u (f ': fs) a - weaken = comp . Right - {-# INLINE weaken #-} - - weaken2 :: u fs a -> u (f1 ': f2 ': fs) a - weaken2 = weaken . weaken - {-# INLINE weaken2 #-} - - weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a - weaken3 = weaken2 . weaken - {-# INLINE weaken3 #-} - - weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a - weaken4 = weaken3 . weaken - {-# INLINE weaken4 #-} - - weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs) - weakenUnder = inject0 |+|: weaken2 - - weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs) - weakenUnder2 = inject0 |+|: injectUnder |+|: weaken3 - - weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs) - weakenUnder3 = inject0 |+|: injectUnder |+|: injectUnder2 |+|: weaken4 - - weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs) - weaken2Under = inject0 |+|: weaken3 - - weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs) - weaken2Under2 = inject0 |+|: injectUnder |+|: weaken4 - - weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs) - weaken3Under = inject0 |+|: weaken4 - - flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs) - flipUnion = injectUnder |+|: inject0 |+|: weaken2 - - flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs) - flipUnion3 = injectUnder2 |+|: injectUnder |+|: inject0 |+|: weaken3 - - flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs) - flipUnionUnder = inject0 |+|: injectUnder2 |+|: injectUnder |+|: weaken3 - - rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs) - rot3 = injectUnder2 |+|: inject0 |+|: injectUnder |+|: weaken3 - - rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs) - rot3' = injectUnder |+|: injectUnder2 |+|: inject0 |+|: weaken3 - - bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs) - bundleUnion2 = inject0 . inject0 |+|: inject0 . injectUnder |+|: weaken - - bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs) - bundleUnion3 = - (inject0 . inject0) - |+|: (inject0 . injectUnder) - |+|: (inject0 . injectUnder2) - |+|: weaken - - bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs) - bundleUnion4 = - (inject0 . inject0) - |+|: (inject0 . injectUnder) - |+|: (inject0 . injectUnder2) - |+|: (inject0 . injectUnder3) - |+|: weaken - - unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs) - unbundleUnion2 = (inject0 |+|: injectUnder |+|: absurdUnion) |+|: weaken2 - - unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs) - unbundleUnion3 = (inject0 |+|: injectUnder |+|: injectUnder2 |+|: absurdUnion) |+|: weaken3 - - unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs) - unbundleUnion4 = - (inject0 |+|: injectUnder |+|: injectUnder2 |+|: injectUnder3 |+|: absurdUnion) - |+|: weaken4 - -type family IsMember (f :: Instruction) fs where - IsMember f (f ': fs) = 'True - IsMember f (_ ': fs) = IsMember f fs - IsMember _ '[] = 'False - -type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True) diff --git a/src/Data/Hefty/Extensible.hs b/src/Data/Hefty/Extensible.hs --- a/src/Data/Hefty/Extensible.hs +++ b/src/Data/Hefty/Extensible.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE UndecidableInstances #-} -- This Source Code Form is subject to the terms of the Mozilla Public @@ -14,66 +15,113 @@ An implementation of an open union for higher-order effects using the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. -} -module Data.Hefty.Extensible where +module Data.Hefty.Extensible ( + module Data.Hefty.Extensible, + Forall, +) where -import Control.Effect.Class (Signature) -import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap) -import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match) -import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt)) -import Data.Free.Extensible (TypeIndex, findFirstMembership) +import Data.Effect (SigClass) +import Data.Effect.HFunctor (HFunctor, hfmap) +import Data.Extensible (Forall, Match (Match), htabulateFor, match) +import Data.Extensible.Sum (strikeAt, (<:|), type (:/) (EmbedAt)) +import Data.Extensible.Sum qualified as E import Data.Hefty.Union ( - UnionH ( - HasMembershipH, - absurdUnionH, - inject0H, - injectH, - projectH, - weakenH, + ClassIndex, + HFunctorUnion_ (ForallHFunctor), + Union ( + HasMembership, + exhaust, + inject, + inject0, + project, + weaken, (|+:) ), ) +import Data.Hefty.Union qualified as U +import Data.Hefty.Union qualified as Union import Data.Proxy (Proxy (Proxy)) +import Data.Type.Equality ((:~:) (Refl)) import GHC.TypeNats (KnownNat) -import Type.Membership (nextMembership) +import Type.Membership.Internal ( + Elaborate, + Elaborated (Expecting), + FindType, + Membership, + leadership, + membership, + nextMembership, + ) +import Unsafe.Coerce (unsafeCoerce) {- | An implementation of an open union for higher-order effects using the [extensible](https://hackage.haskell.org/package/extensible) package as a backend. -} -newtype ExtensibleUnionH hs f a = ExtensibleUnionH {unExtensibleUnionH :: hs :/ FieldAppH f a} +newtype ExtensibleUnion es f a = ExtensibleUnion {unExtensibleUnion :: es :/ FieldApp f a} -newtype FieldAppH f a (h :: Signature) = FieldAppH {unFieldAppH :: h f a} +newtype FieldApp f a (e :: SigClass) = FieldApp {unFieldApp :: e f a} -instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where +instance Forall HFunctor es => HFunctor (ExtensibleUnion es) where hfmap f = - ExtensibleUnionH + ExtensibleUnion . match ( htabulateFor @HFunctor Proxy \w -> - Match $ EmbedAt w . FieldAppH . hfmap f . unFieldAppH + Match $ EmbedAt w . FieldApp . hfmap f . unFieldApp ) - . unExtensibleUnionH + . unExtensibleUnion {-# INLINE hfmap #-} -- todo: Functor, Foldable, Traversable instances -instance UnionH ExtensibleUnionH where - type HasMembershipH _ h hs = KnownNat (TypeIndex hs h) +instance Union ExtensibleUnion where + type HasMembership _ e es = KnownNat (ClassIndex es e) - injectH = ExtensibleUnionH . EmbedAt findFirstMembership . FieldAppH - {-# INLINE injectH #-} + inject = ExtensibleUnion . EmbedAt findFirstMembership . FieldApp + {-# INLINE inject #-} - projectH (ExtensibleUnionH u) = unFieldAppH <$> strikeAt findFirstMembership u - {-# INLINE projectH #-} + project (ExtensibleUnion u) = unFieldApp <$> strikeAt findFirstMembership u + {-# INLINE project #-} - absurdUnionH = exhaust . unExtensibleUnionH - {-# INLINE absurdUnionH #-} + exhaust = E.exhaust . unExtensibleUnion + {-# INLINE exhaust #-} - inject0H = ExtensibleUnionH . EmbedAt leadership . FieldAppH - {-# INLINE inject0H #-} + inject0 = ExtensibleUnion . EmbedAt leadership . FieldApp + {-# INLINE inject0 #-} - weakenH (ExtensibleUnionH (EmbedAt w e)) = - ExtensibleUnionH $ EmbedAt (nextMembership w) e - {-# INLINE weakenH #-} + weaken (ExtensibleUnion (EmbedAt w e)) = + ExtensibleUnion $ EmbedAt (nextMembership w) e + {-# INLINE weaken #-} - f |+: g = (f . unFieldAppH <:| g . ExtensibleUnionH) . unExtensibleUnionH + f |+: g = (f . unFieldApp <:| g . ExtensibleUnion) . unExtensibleUnion {-# INLINE (|+:) #-} + +findFirstMembership :: forall xs x. KnownNat (ClassIndex xs x) => Membership xs x +findFirstMembership = unsafeMkMembership @(ClassIndex xs x) Proxy + where + -- This hack may break if the membership package version gets updated. + unsafeMkMembership :: forall pos. Proxy pos -> KnownNat pos => Membership xs x + unsafeMkMembership _ = case hackedEquality of Refl -> membership + where + hackedEquality :: Elaborate x (FindType x xs) :~: 'Expecting pos + hackedEquality = unsafeCoerce Refl + +instance HFunctorUnion_ (Forall HFunctor) ExtensibleUnion where + type ForallHFunctor _ = Forall HFunctor + +type e <| es = U.Member ExtensibleUnion e es +type e <<| es = U.MemberH ExtensibleUnion e es + +type MemberBy key e efs = U.MemberBy ExtensibleUnion key e efs +type MemberHBy key e ehs = U.MemberHBy ExtensibleUnion key e ehs + +infix 3 <| +infix 3 <<| + +type ForallHFunctor = Forall HFunctor + +type U ef = Union.U ExtensibleUnion ef +type UH eh = Union.UH ExtensibleUnion eh + +type S ef = Union.S ExtensibleUnion ef +type SH eh = Union.SH ExtensibleUnion eh diff --git a/src/Data/Hefty/Sum.hs b/src/Data/Hefty/Sum.hs deleted file mode 100644 --- a/src/Data/Hefty/Sum.hs +++ /dev/null @@ -1,123 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- This Source Code Form is subject to the terms of the Mozilla Public --- License, v. 2.0. If a copy of the MPL was not distributed with this --- file, You can obtain one at https://mozilla.org/MPL/2.0/. - --- The code before modification is MIT licensed; (c) 2023 Casper Bach Poulsen and Cas van der Rest. - -{- | -Copyright : (c) 2023 Yamada Ryo - (c) 2023 Casper Bach Poulsen and Cas van der Rest -License : MPL-2.0 (see the file LICENSE) -Maintainer : ymdfield@outlook.jp -Stability : experimental -Portability : portable - -An implementation of an open union for higher-order effects using recursively nested binary sums. --} -module Data.Hefty.Sum where - -import Control.Effect.Class (NopS, Signature, type (~>)) -import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr)) -import Data.Hefty.Union (HasMembershipH, UnionH, absurdUnionH, compH, decompH, injectH, projectH) - -absurdLH :: (NopS :+: h) f ~> h f -absurdLH = caseH \case {} id -{-# INLINE absurdLH #-} - -absurdRH :: (h :+: NopS) f ~> h f -absurdRH = caseH id \case {} -{-# INLINE absurdRH #-} - -swapSumH :: (h1 :+: h2) f a -> (h2 :+: h1) f a -swapSumH = caseH Inr Inl -{-# INLINE swapSumH #-} - -type family SumH hs where - SumH '[] = NopS - SumH (h ': hs) = h :+: SumH hs - -{- | -An implementation of an open union for higher-order effects using recursively nested binary sums. --} -newtype SumUnionH hs f a = SumUnionH {unSumUnionH :: SumH hs f a} - -deriving newtype instance Functor (SumUnionH '[] f) -deriving newtype instance Foldable (SumUnionH '[] f) -deriving stock instance Traversable (SumUnionH '[] f) - -{- Lack of instances of 'Data.Comp.Multi.Ops.:+:'. - - Should we create a pullreq on the compdata package side? - -} -{- -deriving newtype instance - (Functor (h f), Functor (SumH hs f)) => - Functor (SumUnionH (h ': hs) f) - -deriving newtype instance - (Foldable (h f), Foldable (SumH hs f)) => - Foldable (SumUnionH (h ': hs) f) - -deriving stock instance - (Traversable (h f), Traversable (SumH hs f)) => - Traversable (SumUnionH (h ': hs) f) --} - -deriving newtype instance HFunctor (SumH hs) => HFunctor (SumUnionH hs) - -instance UnionH SumUnionH where - type HasMembershipH _ h hs = h << SumH hs - - injectH sig = SumUnionH $ injH sig - projectH (SumUnionH sig) = projH sig - - absurdUnionH = \case {} - - compH = - SumUnionH . \case - Left x -> Inl x - Right (SumUnionH x) -> Inr x - - decompH (SumUnionH sig) = case sig of - Inl x -> Left x - Inr x -> Right (SumUnionH x) - - {-# INLINE injectH #-} - {-# INLINE projectH #-} - {-# INLINE absurdUnionH #-} - -class isHead ~ h1 `IsHeadSigOf` h2 => SumMemberH isHead (h1 :: Signature) h2 where - injSumH :: h1 f a -> h2 f a - projSumH :: h2 f a -> Maybe (h1 f a) - -type family (h1 :: Signature) `IsHeadSigOf` h2 where - f `IsHeadSigOf` f :+: g = 'True - _ `IsHeadSigOf` _ = 'False - -type h1 << h2 = SumMemberH (IsHeadSigOf h1 h2) h1 h2 - -injH :: forall h1 h2 f. h1 << h2 => h1 f ~> h2 f -injH = injSumH @(IsHeadSigOf h1 h2) - -projH :: forall h1 h2 f a. h1 << h2 => h2 f a -> Maybe (h1 f a) -projH = projSumH - -instance SumMemberH 'True f (f :+: g) where - injSumH = Inl - - projSumH = \case - Inl x -> Just x - Inr _ -> Nothing - - {-# INLINE injSumH #-} - {-# INLINE projSumH #-} - -instance (f `IsHeadSigOf` (g :+: h) ~ 'False, f << h) => SumMemberH 'False f (g :+: h) where - injSumH = Inr . injH - projSumH = \case - Inl _ -> Nothing - Inr x -> projSumH x - - {-# INLINE injSumH #-} - {-# INLINE projSumH #-} diff --git a/src/Data/Hefty/Union.hs b/src/Data/Hefty/Union.hs --- a/src/Data/Hefty/Union.hs +++ b/src/Data/Hefty/Union.hs @@ -1,11 +1,16 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} -- This Source Code Form is subject to the terms of the Mozilla Public -- License, v. 2.0. If a copy of the MPL was not distributed with this -- file, You can obtain one at https://mozilla.org/MPL/2.0/. {- | -Copyright : (c) 2023 Yamada Ryo +Copyright : (c) 2023-2024 Yamada Ryo License : MPL-2.0 (see the file LICENSE) Maintainer : ymdfield@outlook.jp Stability : experimental @@ -16,142 +21,511 @@ -} module Data.Hefty.Union where -import Control.Effect.Class (Signature, type (~>)) +import Control.Effect (type (~>)) +import Control.Monad ((<=<)) +import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns) +import Data.Effect.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr)) +import Data.Effect.Key (type (##>), type (#>)) +import Data.Free.Sum (type (+)) import Data.Kind (Constraint) +import Data.Singletons (SingI, sing) +import Data.Singletons.TH (singletons) +import Data.Type.Bool (If) +import Data.Type.Equality ((:~:) (Refl)) +import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), Nat, TypeError) +import GHC.TypeNats qualified as N {- | A type class representing a general open union for higher-order effects, independent of the internal implementation. -} -class UnionH (u :: [Signature] -> Signature) where - {-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-} +class Union (u :: [SigClass] -> SigClass) where + {-# MINIMAL inject, project, exhaust, (comp | (inject0, weaken), decomp | (|+:)) #-} - type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint + type HasMembership u (e :: SigClass) (es :: [SigClass]) :: Constraint - injectH :: HasMembershipH u h hs => h f ~> u hs f - projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a) + inject :: HasMembership u e es => e f ~> u es f + project :: HasMembership u e es => u es f a -> Maybe (e f a) - absurdUnionH :: u '[] f a -> x + exhaust :: u '[] f a -> x - compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a - compH = \case - Left x -> inject0H x - Right x -> weakenH x - {-# INLINE compH #-} + comp :: Either (e f a) (u es f a) -> u (e ': es) f a + comp = \case + Left x -> inject0 x + Right x -> weaken x + {-# INLINE comp #-} - decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a) - decompH = Left |+: Right - {-# INLINE decompH #-} + decomp :: u (e ': es) f a -> (e :+: u es) f a + decomp = Inl |+: Inr + {-# INLINE decomp #-} infixr 5 |+: - (|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r - (f |+: g) u = case decompH u of - Left x -> f x - Right x -> g x + (|+:) :: (e f a -> r) -> (u es f a -> r) -> u (e ': es) f a -> r + f |+: g = caseH f g . decomp {-# INLINE (|+:) #-} - inject0H :: h f ~> u (h ': hs) f - inject0H = compH . Left - {-# INLINE inject0H #-} + inject0 :: e f ~> u (e ': es) f + inject0 = comp . Left + {-# INLINE inject0 #-} - injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f - injectUnderH = weakenH . inject0H - {-# INLINE injectUnderH #-} + injectUnder :: h2 f ~> u (h1 ': h2 ': es) f + injectUnder = weaken . inject0 + {-# INLINE injectUnder #-} - injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f - injectUnder2H = weaken2H . inject0H - {-# INLINE injectUnder2H #-} + injectUnder2 :: h3 f ~> u (h1 ': h2 ': h3 ': es) f + injectUnder2 = weaken2 . inject0 + {-# INLINE injectUnder2 #-} - injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - injectUnder3H = weaken3H . inject0H - {-# INLINE injectUnder3H #-} + injectUnder3 :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': es) f + injectUnder3 = weaken3 . inject0 + {-# INLINE injectUnder3 #-} - weakenH :: u hs f ~> u (h ': hs) f - weakenH = compH . Right - {-# INLINE weakenH #-} + weaken :: u es f ~> u (e ': es) f + weaken = comp . Right + {-# INLINE weaken #-} - weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f - weaken2H = weakenH . weakenH - {-# INLINE weaken2H #-} + weaken2 :: u es f ~> u (e1 ': e2 ': es) f + weaken2 = weaken . weaken + {-# INLINE weaken2 #-} - weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f - weaken3H = weaken2H . weakenH - {-# INLINE weaken3H #-} + weaken3 :: u es f ~> u (e1 ': e2 ': e3 ': es) f + weaken3 = weaken2 . weaken + {-# INLINE weaken3 #-} - weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - weaken4H = weaken3H . weakenH - {-# INLINE weaken4H #-} + weaken4 :: u es f ~> u (e1 ': e2 ': e3 ': e4 ': es) f + weaken4 = weaken3 . weaken + {-# INLINE weaken4 #-} - weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f - weakenUnderH = inject0H |+: weaken2H + weakenUnder :: u (e1 ': es) f ~> u (e1 ': e2 ': es) f + weakenUnder = inject0 |+: weaken2 - weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f - weakenUnder2H = inject0H |+: injectUnderH |+: weaken3H + weakenUnder2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': es) f + weakenUnder2 = inject0 |+: injectUnder |+: weaken3 - weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - weakenUnder3H = inject0H |+: injectUnderH |+: injectUnder2H |+: weaken4H + weakenUnder3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f + weakenUnder3 = inject0 |+: injectUnder |+: injectUnder2 |+: weaken4 - weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f - weaken2UnderH = inject0H |+: weaken3H + weaken2Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': es) f + weaken2Under = inject0 |+: weaken3 - weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - weaken2Under2H = inject0H |+: injectUnderH |+: weaken4H + weaken2Under2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f + weaken2Under2 = inject0 |+: injectUnder |+: weaken4 - weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - weaken3UnderH = inject0H |+: weaken4H + weaken3Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f + weaken3Under = inject0 |+: weaken4 - flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f - flipUnionH = injectUnderH |+: inject0H |+: weaken2H + flipUnion :: u (e1 ': e2 ': es) f ~> u (e2 ': e1 ': es) f + flipUnion = injectUnder |+: inject0 |+: weaken2 - flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f - flipUnion3H = injectUnder2H |+: injectUnderH |+: inject0H |+: weaken3H + flipUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e2 ': e1 ': es) f + flipUnion3 = injectUnder2 |+: injectUnder |+: inject0 |+: weaken3 - flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f - flipUnionUnderH = inject0H |+: injectUnder2H |+: injectUnderH |+: weaken3H + flipUnionUnder :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e3 ': e2 ': es) f + flipUnionUnder = inject0 |+: injectUnder2 |+: injectUnder |+: weaken3 - rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f - rot3H = injectUnder2H |+: inject0H |+: injectUnderH |+: weaken3H + rot3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e2 ': e3 ': e1 ': es) f + rot3 = injectUnder2 |+: inject0 |+: injectUnder |+: weaken3 - rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f - rot3H' = injectUnderH |+: injectUnder2H |+: inject0H |+: weaken3H + rot3' :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e1 ': e2 ': es) f + rot3' = injectUnder |+: injectUnder2 |+: inject0 |+: weaken3 - bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f - bundleUnion2H = inject0H . inject0H |+: inject0H . injectUnderH |+: weakenH + bundleUnion2 :: u (e1 ': e2 ': es) f ~> u (u '[e1, e2] ': es) f + bundleUnion2 = inject0 . inject0 |+: inject0 . injectUnder |+: weaken - bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f - bundleUnion3H = - (inject0H . inject0H) - |+: (inject0H . injectUnderH) - |+: (inject0H . injectUnder2H) - |+: weakenH + bundleUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (u '[e1, e2, e3] ': es) f + bundleUnion3 = + (inject0 . inject0) + |+: (inject0 . injectUnder) + |+: (inject0 . injectUnder2) + |+: weaken - bundleUnion4H :: - UnionH u' => - u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f - bundleUnion4H = - (inject0H . inject0H) - |+: (inject0H . injectUnderH) - |+: (inject0H . injectUnder2H) - |+: (inject0H . injectUnder3H) - |+: weakenH + bundleUnion4 :: + u (e1 ': e2 ': e3 ': e4 ': es) f ~> u (u '[e1, e2, e3, e4] ': es) f + bundleUnion4 = + (inject0 . inject0) + |+: (inject0 . injectUnder) + |+: (inject0 . injectUnder2) + |+: (inject0 . injectUnder3) + |+: weaken - unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f - unbundleUnion2H = (inject0H |+: injectUnderH |+: absurdUnionH) |+: weaken2H + unbundleUnion2 :: u (u '[e1, e2] ': es) f ~> u (e1 ': e2 ': es) f + unbundleUnion2 = (inject0 |+: injectUnder |+: exhaust) |+: weaken2 - unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f - unbundleUnion3H = (inject0H |+: injectUnderH |+: injectUnder2H |+: absurdUnionH) |+: weaken3H + unbundleUnion3 :: u (u '[e1, e2, e3] ': es) f ~> u (e1 ': e2 ': e3 ': es) f + unbundleUnion3 = (inject0 |+: injectUnder |+: injectUnder2 |+: exhaust) |+: weaken3 - unbundleUnion4H :: - UnionH u' => - u (u' '[h1, h2, h3, h4] ': hs) f - ~> u (h1 ': h2 ': h3 ': h4 ': hs) f - unbundleUnion4H = - (inject0H |+: injectUnderH |+: injectUnder2H |+: injectUnder3H |+: absurdUnionH) - |+: weaken4H + unbundleUnion4 :: + u (u '[e1, e2, e3, e4] ': es) f + ~> u (e1 ': e2 ': e3 ': e4 ': es) f + unbundleUnion4 = + (inject0 |+: injectUnder |+: injectUnder2 |+: injectUnder3 |+: exhaust) + |+: weaken4 -type family IsMemberH (h :: Signature) hs where - IsMemberH h (h ': hs) = 'True - IsMemberH h (_ ': hs) = IsMemberH h hs - IsMemberH _ '[] = 'False +type HFunctorUnion u = HFunctorUnion_ (ForallHFunctor u) u -type MemberH u h hs = (HasMembershipH u h hs, IsMemberH h hs ~ 'True) +-- A hack to avoid the "Quantified predicate must have a class or type variable head" error. +class + ( Union u + , forall e es. (HFunctor e, forallHFunctor es) => forallHFunctor (e ': es) + , forall es. forallHFunctor es => HFunctor (u es) + , forallHFunctor ~ ForallHFunctor u + , forallHFunctor '[] + ) => + HFunctorUnion_ forallHFunctor u + | u -> forallHFunctor + where + type ForallHFunctor u :: [SigClass] -> Constraint + +$( singletons + [d| + data SearchResult = FoundIn FoundLevel | NotFound + + data FoundLevel = CurrentLevel | LowerLevel + |] + ) + +type family FoundLevelOf found :: FoundLevel where + FoundLevelOf ( 'FoundIn l) = l + +type MemberH u e ehs = HasMembershipRec u e ehs +type Member u e efs = MemberH u (LiftIns e) efs + +class MemberRec (u :: [SigClass] -> SigClass) e es where + injectRec :: e f ~> u es f + projectRec :: u es f a -> Maybe (e f a) + +type HasMembershipRec u e es = + ( SearchMemberRec es u e es + , HasMembershipRec1_ u e es (Search u es e) + ) + +type HasMembershipRec1_ u e es searchResult = + ( HasMembershipRec2_ u e es (CurrentLevelSearchResult searchResult) + , SingI (HeadLowerSearchResult searchResult) + ) +type HasMembershipRec2_ u e es found = HasMembershipRec3_ u e es found (FoundLevelOf found) +type HasMembershipRec3_ u e es found lvl = + ( found ~ 'FoundIn lvl + , SingI lvl + , HasMembershipWhenCurrentLevel lvl u e es + , SearchMemberRecWhenLowerLevel lvl es u e + ) + +instance + ( SearchMemberRec es u e es + , MemberFound e es (CurrentLevelSearchResult searchResult) + , searchResult ~ Search u es e + , SingI (HeadLowerSearchResult searchResult) + , found ~ CurrentLevelSearchResult searchResult + ) => + MemberRec u e es + where + injectRec = withFound @e @es @found $ injectSMR @es Refl sing sing + projectRec = withFound @e @es @found $ projectSMR @es Refl sing sing + {-# INLINE injectRec #-} + {-# INLINE projectRec #-} + +class MemberFound e es found where + withFound :: (forall lvl. (found ~ 'FoundIn lvl, SingI lvl) => a) -> a + +instance SingI lvl => MemberFound e es ( 'FoundIn lvl) where + withFound a = a + {-# INLINE withFound #-} + +-- A stopgap until upgrading to base-4.19. +-- https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeError.html#t:Unsatisfiable +instance + TypeError + ( 'Text "The effect class: " ':<>: 'ShowType e + ':$$: 'Text " was not found in the union:" + ':$$: 'Text " " ':<>: 'ShowType es + ) => + MemberFound e es 'NotFound + where + withFound _ = error "unreachable" + +type SearchMemberRec rest u e = SearchMemberRec_ (NextSearchMemberRecAction rest u e) rest u e + +class + SearchMemberRec_ + (act :: SearchMemberRecAction) + (rest :: [SigClass]) + (u :: [SigClass] -> SigClass) + (e :: SigClass) + (es :: [SigClass]) + where + type Search_ act u rest e :: SearchResults + + injectSMR_ :: + searchResult ~ Search_ act u rest e => + CurrentLevelSearchResult searchResult :~: 'FoundIn lvl -> + SSearchResult ( 'FoundIn lvl) -> + SSearchResult (HeadLowerSearchResult searchResult) -> + e f ~> u es f + + projectSMR_ :: + searchResult ~ Search_ act u rest e => + CurrentLevelSearchResult searchResult :~: 'FoundIn lvl -> + SSearchResult ( 'FoundIn lvl) -> + SSearchResult (HeadLowerSearchResult searchResult) -> + u es f a -> + Maybe (e f a) + +type Search u rest e = Search_ (NextSearchMemberRecAction rest u e) u rest e + +injectSMR :: + forall rest u e es searchResult lvl f. + (SearchMemberRec rest u e es, searchResult ~ Search u rest e) => + CurrentLevelSearchResult searchResult :~: 'FoundIn lvl -> + SSearchResult ( 'FoundIn lvl) -> + SSearchResult (HeadLowerSearchResult searchResult) -> + e f ~> u es f +injectSMR = injectSMR_ @(NextSearchMemberRecAction rest u e) @rest +{-# INLINE injectSMR #-} + +projectSMR :: + forall rest u e es searchResult lvl f a. + (SearchMemberRec rest u e es, searchResult ~ Search u rest e) => + CurrentLevelSearchResult searchResult :~: 'FoundIn lvl -> + SSearchResult ( 'FoundIn lvl) -> + SSearchResult (HeadLowerSearchResult searchResult) -> + u es f a -> + Maybe (e f a) +projectSMR = projectSMR_ @(NextSearchMemberRecAction rest u e) @rest +{-# INLINE projectSMR #-} + +data SearchResults = SearchResults SearchResult SearchResult +type family CurrentLevelSearchResult a where + CurrentLevelSearchResult ( 'SearchResults a _) = a + +type family HeadLowerSearchResult a where + HeadLowerSearchResult ( 'SearchResults _ a) = a + +data SearchMemberRecAction = SmrStop | SmrRight | SmrDown + +type family NextSearchMemberRecAction rest (u :: [SigClass] -> SigClass) e where + NextSearchMemberRecAction (e ': _) u e = 'SmrStop + NextSearchMemberRecAction (u _ ': _) u e = 'SmrDown + NextSearchMemberRecAction _ _ _ = 'SmrRight + +instance + (HasMembership u e es, Union u) => + SearchMemberRec_ 'SmrStop (e ': _tail) u e es + where + type Search_ _ _ (e ': _tail) e = 'SearchResults ( 'FoundIn 'CurrentLevel) 'NotFound + + injectSMR_ _ _ _ = inject + projectSMR_ _ _ _ = project + {-# INLINE injectSMR_ #-} + {-# INLINE projectSMR_ #-} + +type family IsFound found where + IsFound ( 'FoundIn _) = 'True + IsFound 'NotFound = 'False + +instance + ( SearchMemberRec es' u e es' + , headSearchResults ~ Search u es' e + , tailSearchResults ~ Search u tail e + , isFoundInHead ~ IsFound (CurrentLevelSearchResult headSearchResults) + , If isFoundInHead (HasMembership u (u es') es) (() :: Constraint) + , SearchMemberRec (If isFoundInHead '[] tail) u e es + , Union u + , SingI (HeadLowerSearchResult headSearchResults) + , SingI (HeadLowerSearchResult tailSearchResults) + ) => + SearchMemberRec_ 'SmrDown (u es' ': tail) u e es + where + type + Search_ _ _ (u es' ': tail) e = + SearchResultsOnSmrDown + u + es' + tail + e + (CurrentLevelSearchResult (Search u es' e)) + (CurrentLevelSearchResult (Search u tail e)) + + injectSMR_ Refl found = \case + SFoundIn lvl -> inject . injectSMR @es' @u @_ @es' Refl (SFoundIn lvl) sing + SNotFound -> injectSMR @tail Refl found sing + + projectSMR_ Refl found = \case + SFoundIn lvl -> projectSMR @es' @u @_ @es' Refl (SFoundIn lvl) sing <=< project + SNotFound -> projectSMR @tail Refl found sing + + {-# INLINE injectSMR_ #-} + {-# INLINE projectSMR_ #-} + +type SearchResultsOnSmrDown u es' tail e foundInHead foundInTail = + 'SearchResults + (If (IsFound foundInHead) ( 'FoundIn 'LowerLevel) foundInTail) + foundInHead + +instance + ( HasMembershipWhenCurrentLevel lvl u e (_e ': rest) + , SearchMemberRecWhenLowerLevel lvl rest u e + , SingI (HeadLowerSearchResult searchResult) + , Union u + , searchResult ~ Search u rest e + , lvl ~ FoundLevelOf (CurrentLevelSearchResult searchResult) + ) => + SearchMemberRec_ 'SmrRight (_e ': rest) u e (_e ': rest) + where + type Search_ _ u (_ ': rest) e = 'SearchResults (CurrentLevelSearchResult (Search u rest e)) 'NotFound + + injectSMR_ Refl (SFoundIn lvl) _ = case lvl of + SCurrentLevel -> inject + SLowerLevel -> weaken . injectSMR @rest Refl sing sing + + projectSMR_ Refl (SFoundIn lvl) _ = case lvl of + SCurrentLevel -> project + SLowerLevel -> const Nothing |+: projectSMR @rest Refl sing sing + + {-# INLINE injectSMR_ #-} + {-# INLINE projectSMR_ #-} + +instance SearchMemberRec_ act '[] u e es where + type Search_ _ _ _ _ = 'SearchResults 'NotFound 'NotFound + injectSMR_ = \case {} + projectSMR_ = \case {} + {-# INLINE injectSMR_ #-} + {-# INLINE projectSMR_ #-} + +-- A hack to avoid the "Quantified predicate must have a class or type variable head" error. + +type HasMembershipWhenCurrentLevel lvl u e es = + HasMembershipWhenCurrentLevel_ (HasMembership u e es) lvl u e es +class + (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) => + HasMembershipWhenCurrentLevel_ c lvl u e es + | u e es -> c +instance + (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) => + HasMembershipWhenCurrentLevel_ c lvl u e es + +type SearchMemberRecWhenLowerLevel lvl rest u e = + SearchMemberRecWhenLowerLevel_ (SearchMemberRec rest u e rest) lvl rest u e +class + (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) => + SearchMemberRecWhenLowerLevel_ c lvl rest u e + | rest u e -> c +instance + (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) => + SearchMemberRecWhenLowerLevel_ c lvl rest u e + +infixr 5 |+ +(|+) :: Union u => (e a -> r) -> (u es f a -> r) -> u (LiftIns e ': es) f a -> r +f |+ g = f . unliftIns |+: g +{-# INLINE (|+) #-} + +{- | +Recursively decompose the sum of first-order effects into a list, following the direction of right +association, with normalization. +-} +type U u ef = UH u (LiftIns ef) + +{- | +Recursively decompose the sum of higher-order effects into a list, following the direction of right +association, with normalization. +-} +type UH u eh = SumToUnionList u (NormalizeSig eh) + +{- | +Recursively decompose the sum of higher-order effects into a list, following the direction of right +association. +-} +type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where + SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2 + SumToUnionList u LNop = '[] + SumToUnionList u (SingleSig e) = '[e] + +{- | +Convert a given list of higher-order effect classes into a suitable representation type for each +case of being empty, single, or multiple. +-} +type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where + MultiListToUnion u '[] = LNop + MultiListToUnion u '[e] = e + MultiListToUnion u es = u es + +{- | +Normalization in preparation for decomposing the sum of effect classes into a list. + +In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it. +-} +type family NormalizeSig e where + NormalizeSig LNop = LNop + NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2) + NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2 + NormalizeSig e = SingleSig e + +{- | +A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as +a sum. +-} +newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a} + deriving newtype (HFunctor) + +type family UnionListToSum (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where + UnionListToSum u '[e] = UnionToSum u e + UnionListToSum u '[] = LNop + UnionListToSum u (e ': r) = UnionToSum u e :+: UnionListToSum u r + +type family UnionToSum (u :: [SigClass] -> SigClass) (e :: SigClass) :: SigClass where + UnionToSum u (u es) = UnionListToSum u es + UnionToSum u e = e + +type S u es = UnionListToSum u es Nop +type SH u es = UnionListToSum u es + +type NormalFormUnionList u es = U u (S u es) ~ es +type NormalFormUnionListH u es = UH u (SH u es) ~ es + +type NFU u es = NormalFormUnionList u es +type NFUH u es = NormalFormUnionListH u es + +type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le + +type family UnliftIfSingle e where + UnliftIfSingle (LiftIns e) = e + UnliftIfSingle e = e Nop + +class LiftInsIfSingle e le where + liftInsIfSingle :: e ~> le Nop + unliftInsIfSingle :: le Nop ~> e + +instance LiftInsIfSingle (e Nop) e where + liftInsIfSingle = id + unliftInsIfSingle = id + {-# INLINE liftInsIfSingle #-} + {-# INLINE unliftInsIfSingle #-} + +instance LiftInsIfSingle e (LiftIns e) where + liftInsIfSingle = LiftIns + unliftInsIfSingle = unliftIns + {-# INLINE liftInsIfSingle #-} + {-# INLINE unliftInsIfSingle #-} + +type family ClassIndex (es :: [SigClass]) (e :: SigClass) :: Nat where + ClassIndex (e ': es) e = 0 + ClassIndex (_ ': es) e = 1 N.+ ClassIndex es e + ClassIndex '[] e = + TypeError + ( 'Text "The effect class ‘" ':<>: 'ShowType e ':<>: 'Text "’ was not found in the list.") + +-- keyed effects + +type MemberBy u key e efs = (Member u (key #> e) efs, Lookup key efs ~ 'Just (LiftIns (key #> e))) +type MemberHBy u key e ehs = (MemberH u (key ##> e) ehs, Lookup key ehs ~ 'Just (key ##> e)) + +type family Lookup (key :: k) es :: Maybe SigClass where + Lookup key (key ##> e ': _) = 'Just (key ##> e) + Lookup key (LiftIns (key #> e) ': _) = 'Just (LiftIns (key #> e)) + Lookup key (u es ': es') = Lookup key es `OrElse` Lookup key es' + Lookup key (_ ': es) = Lookup key es + Lookup key '[] = 'Nothing + +type family OrElse (a :: Maybe k) (b :: Maybe k) :: Maybe k where + OrElse ( 'Just a) _ = 'Just a + OrElse 'Nothing a = a