mirror of
https://github.com/sayo-hs/heftia.git
synced 2024-11-26 11:32:21 +03:00
[fix] Rewrote the operation functions for the Effectful types using the 'Decomp*' constraints approach.
This commit is contained in:
Yamada Ryo
parent
e60bf7ae05
commit
5502127199
15
README.md
15
README.md
@ -64,22 +64,22 @@ are some examples:
|
||||
```
|
||||
|
||||
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](heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
|
||||
For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/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).
|
||||
|
||||
* Extracting Multi-shot Delimited Continuations
|
||||
|
||||
In handling higher-order effects, it's easy to work with multi-shot delimited continuations.
|
||||
This enables an almost complete emulation of "Algebraic Effects and Handlers".
|
||||
For more details, please refer to
|
||||
[Example 3 - Delimited Continuation](<docs/examples/03 Delimited Continuation.md>) .
|
||||
[Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/develop/docs/examples/03%20Delimited%20Continuation.md>) .
|
||||
|
||||
Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
|
||||
eliminated.
|
||||
|
||||
Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).
|
||||
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/](docs/examples/) directory.
|
||||
Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.
|
||||
|
||||
## Future Plans
|
||||
* Benchmarking
|
||||
@ -90,17 +90,16 @@ Examples with explanations can be found in the [docs/examples/](docs/examples/)
|
||||
and others.
|
||||
|
||||
## License
|
||||
The license is MPL 2.0. Please refer to the [NOTICE](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](CONTRIBUTING.md).
|
||||
Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md).
|
||||
|
||||
## Credits
|
||||
Parts of this project have been adapted or inspired by the following resources:
|
||||
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
|
||||
* **Modifications**: The inspiration for the idea of Heftia. Code was used in the Data.{[Free](https://github.com/sayo-hs/heftia/blob/165a5246ffbf473210bfb26a17da3e37d79a5346/heftia/src/Data/Free/Sum.hs),[Hefty](https://github.com/sayo-hs/heftia/blob/165a5246ffbf473210bfb26a17da3e37d79a5346/heftia/src/Data/Hefty/Sum.hs)}.Sum.
|
||||
|
||||
@ -1 +1 @@
|
||||
../heftia/README.md
|
||||
../README.md
|
||||
@ -1,95 +0,0 @@
|
||||
# Heftia
|
||||
Heftia, a composition of hefty trees and co-Yoneda, is a higher-order effects
|
||||
version of Freer.
|
||||
|
||||
The paper
|
||||
* Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular
|
||||
Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7,
|
||||
POPL, Article 62 (January 2023), 31 pages. <https://doi.org/10.1145/3571255>
|
||||
|
||||
inspires this library.
|
||||
Hefty trees, proposed by the above paper, are extensions of free monads,
|
||||
allowing for a straightforward treatment of higher-order effects.
|
||||
|
||||
This library offers Heftia monads and Freer monads, encoded into data
|
||||
types in several ways to enable tuning in pursuit of high performance.
|
||||
|
||||
Additionally, it's designed to operate as a handler system based
|
||||
on [`classy-effects`](https://github.com/sayo-hs/classy-effects), which aims to
|
||||
standardize and unify the definitions of effects in Haskell.
|
||||
|
||||
Compared to existing Effect System libraries in Haskell that handle higher-order effects, this
|
||||
library's approach allows for a more effortless and flexible handling of higher-order effects. Here
|
||||
are some examples:
|
||||
|
||||
* Two interpretations of the `censor` effect for Writer
|
||||
|
||||
Let's consider the following Writer effectful program:
|
||||
|
||||
```hs
|
||||
hello :: (Writer String m, Monad m) => m ()
|
||||
hello = do
|
||||
tell "Hello"
|
||||
tell " world!"
|
||||
|
||||
censorHello :: (Writer String m, Monad m) => m ()
|
||||
censorHello =
|
||||
censor
|
||||
(\s -> if s == "Hello" then "Goodbye" else s)
|
||||
hello
|
||||
```
|
||||
|
||||
For `censorHello`, should the final written string be `"Goodbye world!"`? Or should it be `"Hello world!"`?
|
||||
With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use.
|
||||
|
||||
```hs
|
||||
main :: IO ()
|
||||
main = runFreerEffects do
|
||||
(s :: String, _) <-
|
||||
interpretTell
|
||||
. runElaborate' (elaborateWriterT @String)
|
||||
$ censorHello
|
||||
|
||||
(sTransactional :: String, _) <-
|
||||
interpretTell
|
||||
. runElaborate' (elaborateWriterTransactionalT @String)
|
||||
$ censorHello
|
||||
|
||||
sendIns $ putStrLn $ "Normal: " <> s
|
||||
sendIns $ putStrLn $ "Transactional: " <> sTransactional
|
||||
```
|
||||
|
||||
Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!".
|
||||
For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
|
||||
|
||||
* Extracting Multi-shot Delimited Continuations
|
||||
|
||||
In handling higher-order effects, it's easy to work with multi-shot delimited continuations.
|
||||
This enables an almost complete emulation of "Algebraic Effects and Handlers".
|
||||
For more details, please refer to
|
||||
[Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/master/docs/examples/03%20Delimited%20Continuation.md>) .
|
||||
|
||||
Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
|
||||
eliminated.
|
||||
|
||||
Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).
|
||||
|
||||
## Documentation
|
||||
Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.
|
||||
|
||||
## Future Plans
|
||||
* Benchmarking
|
||||
* Enriching the documentation
|
||||
* Completing missing definitions such as
|
||||
* the Heftia monad transformer encoded in tree structure
|
||||
* handlers for the `Accum`, `Coroutine`, `Fresh`, `Input`, `Output` effect classes
|
||||
|
||||
and others.
|
||||
|
||||
## License
|
||||
The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/master/NOTICE).
|
||||
Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed
|
||||
under CC BY-SA 4.0.
|
||||
|
||||
## Your contributions are welcome!
|
||||
Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/master/CONTRIBUTING.md).
|
||||
1
heftia/README.md
Symbolic link
1
heftia/README.md
Symbolic link
@ -0,0 +1 @@
|
||||
../README.md
|
||||
@ -35,8 +35,7 @@ maintainer: Yamada Ryo <ymdfield@outlook.jp>
|
||||
|
||||
-- A copyright notice.
|
||||
copyright:
|
||||
2023 Yamada Ryo,
|
||||
2023 Casper Bach Poulsen and Cas van der Rest
|
||||
2023 Yamada Ryo
|
||||
category: Control, Monads
|
||||
|
||||
extra-source-files:
|
||||
@ -59,8 +58,9 @@ library
|
||||
Control.Effect.Free
|
||||
Control.Effect.ExtensibleChurch
|
||||
Control.Effect.ExtensibleTree
|
||||
Control.Effect.ExtensibleTreeA
|
||||
Control.Effect.ExtensibleFastA
|
||||
Control.Hefty
|
||||
Control.Hefty.SFunctor
|
||||
Control.Freer
|
||||
Control.Monad.Freer
|
||||
Control.Monad.Freer.Church
|
||||
|
||||
@ -2,6 +2,15 @@
|
||||
-- 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.Free (EffectfulF)
|
||||
|
||||
27
heftia/src/Control/Effect/ExtensibleFastA.hs
Normal file
27
heftia/src/Control/Effect/ExtensibleFastA.hs
Normal file
@ -0,0 +1,27 @@
|
||||
-- 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.Free (EffectfulF)
|
||||
import Control.Effect.Hefty (Effectful)
|
||||
import Data.Hefty.Extensible (ExtensibleUnion)
|
||||
|
||||
infixr 4 !!
|
||||
infixr 3 !
|
||||
|
||||
type (!!) = Effectful ExtensibleUnion Ap
|
||||
type (!) = EffectfulF ExtensibleUnion Ap
|
||||
@ -2,6 +2,15 @@
|
||||
-- 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.Free (EffectfulF)
|
||||
|
||||
28
heftia/src/Control/Effect/ExtensibleTreeA.hs
Normal file
28
heftia/src/Control/Effect/ExtensibleTreeA.hs
Normal file
@ -0,0 +1,28 @@
|
||||
-- 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.Free (EffectfulF)
|
||||
import Control.Effect.Hefty (Effectful)
|
||||
import Data.Hefty.Extensible (ExtensibleUnion)
|
||||
|
||||
infixr 4 !!
|
||||
infixr 3 !
|
||||
|
||||
type (!!) = Effectful ExtensibleUnion Ap
|
||||
type (!) = EffectfulF ExtensibleUnion Ap
|
||||
@ -6,7 +6,7 @@
|
||||
-- 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
|
||||
@ -18,17 +18,16 @@ on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
|
||||
module Control.Effect.Free where
|
||||
|
||||
import Control.Applicative (Alternative)
|
||||
import Control.Effect.Class (LiftIns (LiftIns), NopS, SendIns, sendIns, type (~>))
|
||||
import Control.Effect.Class (LiftIns (LiftIns), NopS, SendIns, sendIns, unliftIns, type (~>))
|
||||
import Control.Effect.Class.Machinery.HFunctor (caseH, type (:+:) (Inr))
|
||||
import Control.Effect.Hefty (
|
||||
DecompF,
|
||||
EffHeadF,
|
||||
EffUnion (EffUnion),
|
||||
EffTailF,
|
||||
Effectful (Effectful),
|
||||
MemberF,
|
||||
MultiToUnionF,
|
||||
SumToUnionF,
|
||||
unEffUnion,
|
||||
unEffUnionH,
|
||||
unEffectful,
|
||||
)
|
||||
import Control.Freer (Freer, InsClass, interpretFreer, liftIns, retractFreer, transformFreer)
|
||||
@ -58,7 +57,7 @@ import Data.Hefty.Union (
|
||||
)
|
||||
import Data.Kind (Type)
|
||||
|
||||
-- | A common wrapper data type for representing first-order effectful programs.
|
||||
-- | A common wrapper data type for representing first-order extensible effectful programs.
|
||||
newtype
|
||||
EffectfulF
|
||||
(u :: [SigClass] -> SigClass)
|
||||
@ -98,10 +97,10 @@ instance (MemberF u e es, Freer c fr) => SendIns e (EffectfulF u fr es) where
|
||||
|
||||
-- | Interpret the leading first-order effect class.
|
||||
interpretF ::
|
||||
forall er r f u c.
|
||||
(Freer c f, Union u, DecompF u er r) =>
|
||||
(EffHeadF u er ~> EffectfulF u f r) ->
|
||||
EffectfulF u f er ~> EffectfulF u f r
|
||||
forall er f u c.
|
||||
(Freer c f, Union u, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> EffectfulF u f (EffTailF er)) ->
|
||||
EffectfulF u f er ~> EffectfulF u f (EffTailF er)
|
||||
interpretF i =
|
||||
overEffectfulF $ interpretFreer \u ->
|
||||
case decomp u of
|
||||
@ -110,30 +109,34 @@ interpretF i =
|
||||
|
||||
-- | Interpret the leading first-order effect class using a monad transformer.
|
||||
interpretTF ::
|
||||
forall t er r f u.
|
||||
(MonadFreer f, Union u, DecompF u er r, MonadTrans t, Monad (t (EffectfulF u f r))) =>
|
||||
(EffHeadF u er ~> t (EffectfulF u f r)) ->
|
||||
EffectfulF u f er ~> t (EffectfulF u f r)
|
||||
forall t er f u.
|
||||
(MonadFreer f, Union u, DecompF u er, MonadTrans t, Monad (t (EffectfulF u f (EffTailF er)))) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> t (EffectfulF u f (EffTailF er))) ->
|
||||
EffectfulF u f er ~> t (EffectfulF u f (EffTailF er))
|
||||
interpretTF i = retractFreer . transformFreer (caseF i lift) . splitEffF @f
|
||||
{-# INLINE interpretTF #-}
|
||||
|
||||
-- | Interpret the leading first-order effect class using a delimited continuation.
|
||||
interpretKF ::
|
||||
forall er r' a r f u.
|
||||
(MonadFreer f, Union u, DecompF u er r) =>
|
||||
(a -> EffectfulF u f r r') ->
|
||||
(forall x. (x -> EffectfulF u f r r') -> EffHeadF u er x -> EffectfulF u f r r') ->
|
||||
forall er r a f u.
|
||||
(MonadFreer f, Union u, DecompF u er) =>
|
||||
(a -> EffectfulF u f (EffTailF er) r) ->
|
||||
( forall x.
|
||||
(x -> EffectfulF u f (EffTailF er) r) ->
|
||||
MultiToUnionF u (EffHeadF er) x ->
|
||||
EffectfulF u f (EffTailF er) r
|
||||
) ->
|
||||
EffectfulF u f er a ->
|
||||
EffectfulF u f r r'
|
||||
EffectfulF u f (EffTailF er) r
|
||||
interpretKF k i = (`runContT` k) . interpretContTF \e -> ContT (`i` e)
|
||||
{-# INLINE interpretKF #-}
|
||||
|
||||
-- | Interpret the leading first-order effect class using a continuation monad transformer.
|
||||
interpretContTF ::
|
||||
forall er r' r f u.
|
||||
(MonadFreer f, Union u, DecompF u er r) =>
|
||||
(EffHeadF u er ~> ContT r' (EffectfulF u f r)) ->
|
||||
EffectfulF u f er ~> ContT r' (EffectfulF u f r)
|
||||
forall er r f u.
|
||||
(MonadFreer f, Union u, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> ContT r (EffectfulF u f (EffTailF er))) ->
|
||||
EffectfulF u f er ~> ContT r (EffectfulF u f (EffTailF er))
|
||||
interpretContTF i =
|
||||
transCont
|
||||
. interpretFreerK (detransContT . caseF i lift)
|
||||
@ -157,37 +160,37 @@ transformAllF f = overEffectfulF $ transformFreer f
|
||||
{-# INLINE transformAllF #-}
|
||||
|
||||
raiseF ::
|
||||
forall e1 e f u c.
|
||||
(Freer c f, Union u) =>
|
||||
EffectfulF u f e ~> EffectfulF u f (e1 + e)
|
||||
forall er f u c.
|
||||
(Freer c f, Union u, DecompF u er) =>
|
||||
EffectfulF u f (EffTailF er) ~> EffectfulF u f er
|
||||
raiseF = transformAllF weaken
|
||||
{-# INLINE raiseF #-}
|
||||
|
||||
raise2F ::
|
||||
forall e1 e2 e f u c.
|
||||
(Freer c f, Union u) =>
|
||||
EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e)
|
||||
forall e2 e1r f u c.
|
||||
(Freer c f, Union u, DecompF u e1r) =>
|
||||
EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e2 + e1r)
|
||||
raise2F = transformAllF weaken2
|
||||
{-# INLINE raise2F #-}
|
||||
|
||||
raise3F ::
|
||||
forall e1 e2 e3 e f u c.
|
||||
(Freer c f, Union u) =>
|
||||
EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e3 + e)
|
||||
forall e3 e2 e1r f u c.
|
||||
(Freer c f, Union u, DecompF u e1r) =>
|
||||
EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e3 + e2 + e1r)
|
||||
raise3F = transformAllF weaken3
|
||||
{-# INLINE raise3F #-}
|
||||
|
||||
raise4F ::
|
||||
forall e1 e2 e3 e4 e f u c.
|
||||
(Freer c f, Union u) =>
|
||||
EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e3 + e4 + e)
|
||||
forall e4 e3 e2 e1r f u c.
|
||||
(Freer c f, Union u, DecompF u e1r) =>
|
||||
EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e4 + e3 + e2 + e1r)
|
||||
raise4F = transformAllF weaken4
|
||||
{-# INLINE raise4F #-}
|
||||
|
||||
raiseUnderF ::
|
||||
forall e1 e2 e f u c.
|
||||
(Freer c f, Union u) =>
|
||||
EffectfulF u f (e1 + e) ~> EffectfulF u f (e1 + e2 + e)
|
||||
forall e1r e2 f u c.
|
||||
(Freer c f, Union u, DecompF u e1r) =>
|
||||
EffectfulF u f (e2 + EffTailF e1r) ~> EffectfulF u f (e2 + e1r)
|
||||
raiseUnderF = transformAllF weakenUnder
|
||||
{-# INLINE raiseUnderF #-}
|
||||
|
||||
@ -199,18 +202,18 @@ flipEffF = transformAllF flipUnion
|
||||
{-# INLINE flipEffF #-}
|
||||
|
||||
splitEffF ::
|
||||
forall f' er r f u c.
|
||||
(Freer c f', Freer c f, Union u, DecompF u er r) =>
|
||||
EffectfulF u f er ~> f' (EffHeadF u er + EffectfulF u f r)
|
||||
forall f' er f u c.
|
||||
(Freer c f', Freer c f, Union u, DecompF u er) =>
|
||||
EffectfulF u f er ~> f' (MultiToUnionF u (EffHeadF er) + EffectfulF u f (EffTailF er))
|
||||
splitEffF (EffectfulF f) =
|
||||
f & interpretFreer \u -> case decomp u of
|
||||
Left e -> liftIns $ L1 e
|
||||
Right e -> liftIns $ R1 $ EffectfulF $ liftIns e
|
||||
|
||||
mergeEffF ::
|
||||
forall f' e r f u c.
|
||||
(Freer c f', Freer c f, Union u) =>
|
||||
f' (MultiToUnionF u e + EffectfulF u f r) ~> EffectfulF u f (e + r)
|
||||
forall f' er f u c.
|
||||
(Freer c f', Freer c f, Union u, DecompF u er) =>
|
||||
f' (MultiToUnionF u (EffHeadF er) + EffectfulF u f (EffTailF er)) ~> EffectfulF u f er
|
||||
mergeEffF =
|
||||
EffectfulF
|
||||
. interpretFreer
|
||||
@ -219,18 +222,18 @@ mergeEffF =
|
||||
(transformFreer weaken . unEffectfulF)
|
||||
)
|
||||
|
||||
fromEffectful :: forall e f u c. (Freer c f, Union u) => Effectful u f NopS e ~> EffectfulF u f e
|
||||
fromEffectful =
|
||||
toEffectfulF :: forall e f u c. (Freer c f, Union u) => Effectful u f NopS e ~> EffectfulF u f e
|
||||
toEffectfulF =
|
||||
EffectfulF
|
||||
. transformFreer (caseF (absurdUnion . unEffUnionH) id . unEffUnion)
|
||||
. transformFreer (caseH absurdUnion unliftIns)
|
||||
. unHefty
|
||||
. unEffectful
|
||||
{-# INLINE fromEffectful #-}
|
||||
{-# INLINE toEffectfulF #-}
|
||||
|
||||
toEffectful :: forall e f u c. Freer c f => EffectfulF u f e ~> Effectful u f NopS e
|
||||
toEffectful =
|
||||
fromEffectfulF :: forall e f u c. Freer c f => EffectfulF u f e ~> Effectful u f NopS e
|
||||
fromEffectfulF =
|
||||
Effectful
|
||||
. Hefty
|
||||
. transformFreer (EffUnion . R1)
|
||||
. transformFreer (Inr . LiftIns)
|
||||
. unEffectfulF
|
||||
{-# INLINE toEffectful #-}
|
||||
{-# INLINE fromEffectfulF #-}
|
||||
|
||||
@ -5,7 +5,7 @@
|
||||
-- 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
|
||||
@ -17,14 +17,25 @@ on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
|
||||
module Control.Effect.Hefty where
|
||||
|
||||
import Control.Applicative (Alternative)
|
||||
import Control.Effect.Class (LiftIns (LiftIns), NopI, NopS, SendIns, SendSig, sendIns, sendSig)
|
||||
import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:))
|
||||
import Control.Arrow ((>>>))
|
||||
import Control.Effect.Class (
|
||||
LiftIns (LiftIns),
|
||||
NopI,
|
||||
NopS,
|
||||
SendIns,
|
||||
SendSig,
|
||||
sendIns,
|
||||
sendSig,
|
||||
unliftIns,
|
||||
)
|
||||
import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
|
||||
import Control.Freer (Freer, InsClass, interpretFreer, liftIns, transformFreer)
|
||||
import Control.Hefty (Hefty (Hefty), SigClass, overHefty, unHefty)
|
||||
import Control.Monad (MonadPlus)
|
||||
import Control.Monad.Base (MonadBase)
|
||||
import Control.Monad.IO.Class (MonadIO)
|
||||
import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
|
||||
import Data.Coerce (coerce)
|
||||
import Data.Free.Sum (type (+))
|
||||
import Data.Hefty.Union (
|
||||
ForallHFunctor,
|
||||
HFunctorUnion,
|
||||
@ -39,7 +50,8 @@ import Data.Hefty.Union (
|
||||
import Data.Kind (Type)
|
||||
|
||||
{- |
|
||||
A common wrapper data type for representing first-order & higher-order effectful programs.
|
||||
A common wrapper data type for representing first-order & higher-order extensible effectful
|
||||
programs.
|
||||
-}
|
||||
newtype
|
||||
Effectful
|
||||
@ -49,13 +61,8 @@ newtype
|
||||
(ef :: InsClass)
|
||||
(a :: Type) = Effectful {unEffectful :: Hefty f (EffUnion u eh ef) a}
|
||||
|
||||
-- | Open union for higher-order effect classes and first-order effect classes.
|
||||
newtype EffUnion u eh ef f a = EffUnion
|
||||
{unEffUnion :: (EffUnionH u (NormalizeSig eh) f + SumToUnionF u ef) a}
|
||||
|
||||
-- | A wrapper to provide an instance of t'HFunctor' for the open union.
|
||||
newtype EffUnionH (u :: [SigClass] -> SigClass) (e :: SigClass) f a = EffUnionH
|
||||
{unEffUnionH :: SumToUnion u e f a}
|
||||
-- | Open union for first-order & higher-order effect classes.
|
||||
type EffUnion u eh ef = SumToUnion u (NormalizeSig eh) :+: LiftIns (SumToUnionF u ef)
|
||||
|
||||
-- | Manipulate the inside of the t'Effectful' wrapper.
|
||||
overEffectful ::
|
||||
@ -83,12 +90,6 @@ type TailHFunctor u e = ForallHFunctor u (SumToUnionList u (NormalizeSig e))
|
||||
-- | t'HFunctor' constraint for effect classes that are either single or in an open union.
|
||||
type HeadHFunctor u e = HFunctor (MultiToUnionH u e)
|
||||
|
||||
instance HFunctors u eh => HFunctor (EffUnion u eh ef) where
|
||||
hfmap f = EffUnion . caseF (L1 . hfmap f) R1 . unEffUnion
|
||||
{-# INLINE hfmap #-}
|
||||
|
||||
deriving newtype instance HFunctor (SumToUnion u e) => HFunctor (EffUnionH u e)
|
||||
|
||||
{- |
|
||||
Convert a given list of higher-order effect classes into a suitable representation type for each
|
||||
case of being empty, single, or multiple.
|
||||
@ -156,36 +157,81 @@ newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
|
||||
deriving newtype (HFunctor)
|
||||
|
||||
{- |
|
||||
The higher-order effect class @er@ can be decomposed into the sum of t'EffHeadH' @u@ @er@ and @r@
|
||||
(@er ≅ EffHeadH u er :+: r@).
|
||||
The higher-order effect class @er@ can be decomposed into the sum of t'EffHead' @er@ and t'EffTail'
|
||||
@er@ (@er ≅ EffHead er :+: EffTail er@).
|
||||
-}
|
||||
type DecompH u er r =
|
||||
SumToUnionList u (NormalizeSig er) ~ EffHeadH u er ': SumToUnionList u (NormalizeSig r)
|
||||
type DecompH u er =
|
||||
SumToUnionList u (NormalizeSig er)
|
||||
~ MultiToUnionH u (EffHead er)
|
||||
': SumToUnionList u (NormalizeSig (EffTail er))
|
||||
|
||||
{- |
|
||||
The first-order effect class @er@ can be decomposed into the sum of t'EffHeadF' @u@ @er@ and @r@
|
||||
(@er ≅ EffHeadF u er + r@).
|
||||
The first-order effect class @er@ can be decomposed into the sum of t'EffHeadF' @er@ and t'EffTailF'
|
||||
@er@ (@er ≅ EffHeadF er + EffTailF er@).
|
||||
-}
|
||||
type DecompF u er r = DecompH u (LiftIns er) (LiftIns r)
|
||||
type DecompF u er = DecompH u (LiftIns er)
|
||||
|
||||
type family EffHead u e where
|
||||
EffHead u (e :+: r) = MultiToUnion u e
|
||||
EffHead u (SingleSig e) = e
|
||||
type family EffHead e where
|
||||
EffHead (LiftIns e) = LiftIns (EffHeadF e)
|
||||
EffHead (e :+: r) = e
|
||||
EffHead e = e
|
||||
|
||||
type EffHeadH u er = EffHead u (NormalizeSig er)
|
||||
type EffHeadF u er = EffHeadH u (LiftIns er) NopI
|
||||
type family EffHeadF e where
|
||||
EffHeadF (e + r) = e
|
||||
EffHeadF e = e
|
||||
|
||||
type family EffTail e where
|
||||
EffTail (LiftIns e) = LiftIns (EffTailF e)
|
||||
EffTail (e :+: r) = r
|
||||
EffTail e = NopS
|
||||
|
||||
type family EffTailF e where
|
||||
EffTailF (e + r) = r
|
||||
EffTailF e = NopI
|
||||
|
||||
compEff ::
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u er) =>
|
||||
Effectful u f eh (EffHeadF er + EffTailF er) ~> Effectful u f eh er
|
||||
compEff = coerce
|
||||
{-# INLINE compEff #-}
|
||||
|
||||
compEffH ::
|
||||
(Freer c f, Union u, HFunctors u er, DecompH u er) =>
|
||||
Effectful u f (EffHead er :+: EffTail er) ef ~> Effectful u f er ef
|
||||
compEffH = coerce
|
||||
{-# INLINE compEffH #-}
|
||||
|
||||
decompEff ::
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u er) =>
|
||||
Effectful u f eh er ~> Effectful u f eh (EffHeadF er + EffTailF er)
|
||||
decompEff = coerce
|
||||
{-# INLINE decompEff #-}
|
||||
|
||||
decompEffH ::
|
||||
(Freer c f, Union u, HFunctors u er, DecompH u er) =>
|
||||
Effectful u f er ef ~> Effectful u f (EffHead er :+: EffTail er) ef
|
||||
decompEffH = coerce
|
||||
{-# INLINE decompEffH #-}
|
||||
|
||||
deriving newtype instance Functor (Hefty f (EffUnion u eh ef)) => Functor (Effectful u f eh ef)
|
||||
deriving newtype instance Applicative (Hefty f (EffUnion u eh ef)) => Applicative (Effectful u f eh ef)
|
||||
deriving newtype instance Alternative (Hefty f (EffUnion u eh ef)) => Alternative (Effectful u f eh ef)
|
||||
deriving newtype instance
|
||||
Applicative (Hefty f (EffUnion u eh ef)) =>
|
||||
Applicative (Effectful u f eh ef)
|
||||
deriving newtype instance
|
||||
Alternative (Hefty f (EffUnion u eh ef)) =>
|
||||
Alternative (Effectful u f eh ef)
|
||||
deriving newtype instance Monad (Hefty f (EffUnion u eh ef)) => Monad (Effectful u f eh ef)
|
||||
deriving newtype instance MonadPlus (Hefty f (EffUnion u eh ef)) => MonadPlus (Effectful u f eh ef)
|
||||
deriving newtype instance (MonadBase b (Hefty f (EffUnion u eh ef)), Monad b) => MonadBase b (Effectful u f eh ef)
|
||||
deriving newtype instance
|
||||
(MonadBase b (Hefty f (EffUnion u eh ef)), Monad b) =>
|
||||
MonadBase b (Effectful u f eh ef)
|
||||
deriving newtype instance MonadIO (Hefty f (EffUnion u eh ef)) => MonadIO (Effectful u f eh ef)
|
||||
deriving newtype instance MonadFail (Hefty f (EffUnion u eh ef)) => MonadFail (Effectful u f eh ef)
|
||||
|
||||
deriving stock instance Foldable (Hefty f (EffUnion u eh ef)) => Foldable (Effectful u f eh ef)
|
||||
deriving stock instance Traversable (Hefty f (EffUnion u eh ef)) => Traversable (Effectful u f eh ef)
|
||||
deriving stock instance
|
||||
Traversable (Hefty f (EffUnion u eh ef)) =>
|
||||
Traversable (Effectful u f eh ef)
|
||||
|
||||
deriving newtype instance Eq (Hefty f (EffUnion u eh ef) a) => Eq (Effectful u f eh ef a)
|
||||
deriving newtype instance Ord (Hefty f (EffUnion u eh ef) a) => Ord (Effectful u f eh ef a)
|
||||
@ -195,7 +241,7 @@ deriving newtype instance Show (Hefty f (EffUnion u eh ef) a) => Show (Effectful
|
||||
type MemberF u e ef = MemberH u (LiftIns e) (LiftIns ef)
|
||||
|
||||
instance (MemberF u e ef, Freer c fr) => SendIns e (Effectful u fr eh ef) where
|
||||
sendIns = Effectful . Hefty . liftIns . EffUnion . R1 . injectRec . LiftIns
|
||||
sendIns = Effectful . Hefty . liftIns . Inr . LiftIns . injectRec . LiftIns
|
||||
{-# INLINE sendIns #-}
|
||||
|
||||
type MemberH u e eh = MemberRec u e (SumToUnionList u (NormalizeSig eh))
|
||||
@ -203,26 +249,25 @@ type MemberH u e eh = MemberRec u e (SumToUnionList u (NormalizeSig eh))
|
||||
-- enhance: introduce 'HFunctorCoercible' for performance
|
||||
instance (MemberH u e eh, Freer c fr, HFunctor e) => SendSig e (Effectful u fr eh ef) where
|
||||
sendSig =
|
||||
Effectful . Hefty . liftIns . EffUnion . L1 . EffUnionH . injectRec . hfmap unEffectful
|
||||
Effectful . Hefty . liftIns . Inl . injectRec . hfmap unEffectful
|
||||
{-# INLINE sendSig #-}
|
||||
|
||||
-- | Using the provided interpretation function, interpret first-order effects.
|
||||
interpret ::
|
||||
forall e r f u c.
|
||||
(Freer c f, Union u) =>
|
||||
(MultiToUnionF u e ~> Effectful u f NopS r) ->
|
||||
Effectful u f NopS (e + r) ~> Effectful u f NopS r
|
||||
forall er f u c.
|
||||
(Freer c f, Union u, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> Effectful u f NopS (EffTailF er)) ->
|
||||
Effectful u f NopS er ~> Effectful u f NopS (EffTailF er)
|
||||
interpret i =
|
||||
overEffectful
|
||||
. overHefty
|
||||
$ interpretFreer
|
||||
$ caseF
|
||||
(absurdUnion . unEffUnionH)
|
||||
( \u -> case decomp u of
|
||||
$ caseH
|
||||
absurdUnion
|
||||
( unliftIns >>> decomp >>> \case
|
||||
Left e -> unHefty $ unEffectful $ i e
|
||||
Right e -> liftIns $ EffUnion $ R1 e
|
||||
Right e -> liftIns $ Inr $ LiftIns e
|
||||
)
|
||||
. unEffUnion
|
||||
|
||||
{- |
|
||||
Using the provided interpretation function, interpret first-order effects. For actions (scopes)
|
||||
@ -232,25 +277,23 @@ Note that if the interpretation function is stateful (i.e., not a monad morphism
|
||||
maintained across the scopes.
|
||||
-}
|
||||
interpretRec ::
|
||||
forall e eh r f u c.
|
||||
(Freer c f, Union u, HFunctors u eh) =>
|
||||
(MultiToUnionF u e ~> Effectful u f eh r) ->
|
||||
Effectful u f eh (e + r) ~> Effectful u f eh r
|
||||
forall er eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> Effectful u f eh (EffTailF er)) ->
|
||||
Effectful u f eh er ~> Effectful u f eh (EffTailF er)
|
||||
interpretRec i =
|
||||
overEffectful
|
||||
. overHefty
|
||||
$ interpretFreer
|
||||
$ caseF
|
||||
$ caseH
|
||||
( liftIns
|
||||
. EffUnion
|
||||
. L1
|
||||
. hfmap (unEffectful . interpretRec i . Effectful)
|
||||
. Inl
|
||||
. hfmap (unEffectful . interpretRec @er i . Effectful)
|
||||
)
|
||||
( \u -> case decomp u of
|
||||
( unliftIns >>> decomp >>> \case
|
||||
Left e -> unHefty $ unEffectful $ i e
|
||||
Right e -> liftIns $ EffUnion $ R1 e
|
||||
Right e -> liftIns $ Inr $ LiftIns e
|
||||
)
|
||||
. unEffUnion
|
||||
|
||||
{- |
|
||||
Using the provided interpretation function, interpret higher-order effects. For actions (scopes)
|
||||
@ -260,50 +303,54 @@ Note that if the interpretation function is stateful (i.e., not a monad morphism
|
||||
maintained across the scopes.
|
||||
-}
|
||||
interpretRecH ::
|
||||
forall e r ef f u c.
|
||||
(Freer c f, Union u, HeadHFunctor u e, HFunctors u r) =>
|
||||
(MultiToUnionH u e (Effectful u f r ef) ~> Effectful u f r ef) ->
|
||||
Effectful u f (e :+: r) ef ~> Effectful u f r ef
|
||||
forall er ef f u c.
|
||||
(Freer c f, Union u, HeadHFunctor u (EffHead er), HFunctors u (EffTail er), DecompH u er) =>
|
||||
( MultiToUnionH u (EffHead er) (Effectful u f (EffTail er) ef)
|
||||
~> Effectful u f (EffTail er) ef
|
||||
) ->
|
||||
Effectful u f er ef ~> Effectful u f (EffTail er) ef
|
||||
interpretRecH i =
|
||||
overEffectful
|
||||
. overHefty
|
||||
$ interpretFreer
|
||||
$ caseF
|
||||
( \(EffUnionH u) -> case decomp u of
|
||||
Left e ->
|
||||
unHefty $ unEffectful $ i $ hfmap int e
|
||||
Right e ->
|
||||
liftIns $ EffUnion $ L1 $ EffUnionH $ hfmap (unEffectful . int) e
|
||||
$ caseH
|
||||
( decomp >>> \case
|
||||
Left e -> unHefty $ unEffectful $ i $ hfmap int e
|
||||
Right e -> liftIns $ Inl $ hfmap (unEffectful . int) e
|
||||
)
|
||||
(liftIns . EffUnion . R1)
|
||||
. unEffUnion
|
||||
(liftIns . Inr . coerce)
|
||||
where
|
||||
int :: Hefty f (EffUnion u (e :+: r) ef) ~> Effectful u f r ef
|
||||
int = interpretRecH i . Effectful
|
||||
int :: Hefty f (EffUnion u er ef) ~> Effectful u f (EffTail er) ef
|
||||
int = interpretRecH @er i . Effectful
|
||||
{-# INLINE int #-}
|
||||
|
||||
reinterpret ::
|
||||
forall e r f u c.
|
||||
(Freer c f, HFunctorUnion u) =>
|
||||
(MultiToUnionF u e ~> Effectful u f NopS (e + r)) ->
|
||||
Effectful u f NopS (e + r) ~> Effectful u f NopS (e + r)
|
||||
reinterpret f = interpret f . raiseUnder
|
||||
forall er f u c.
|
||||
(Freer c f, HFunctorUnion u, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> Effectful u f NopS er) ->
|
||||
Effectful u f NopS er ~> Effectful u f NopS er
|
||||
reinterpret f = interpret f . raiseUnder . decompEff
|
||||
{-# INLINE reinterpret #-}
|
||||
|
||||
reinterpretRec ::
|
||||
forall e eh r f u c.
|
||||
(Freer c f, Union u, HFunctors u eh) =>
|
||||
(MultiToUnionF u e ~> Effectful u f eh (e + r)) ->
|
||||
Effectful u f eh (e + r) ~> Effectful u f eh (e + r)
|
||||
reinterpretRec f = interpretRec f . raiseUnder
|
||||
forall er eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u er) =>
|
||||
(MultiToUnionF u (EffHeadF er) ~> Effectful u f eh er) ->
|
||||
Effectful u f eh er ~> Effectful u f eh er
|
||||
reinterpretRec f = interpretRec f . raiseUnder . decompEff
|
||||
{-# INLINE reinterpretRec #-}
|
||||
|
||||
reinterpretRecH ::
|
||||
forall e r ef f u c.
|
||||
(Freer c f, HFunctorUnion u, HeadHFunctor u e, TailHFunctor u r) =>
|
||||
(MultiToUnionH u e (Effectful u f (e :+: r) ef) ~> Effectful u f (e :+: r) ef) ->
|
||||
Effectful u f (e :+: r) ef ~> Effectful u f (e :+: r) ef
|
||||
reinterpretRecH f = interpretRecH f . raiseUnderH
|
||||
forall er ef f u c.
|
||||
( Freer c f
|
||||
, HFunctorUnion u
|
||||
, DecompH u er
|
||||
, HeadHFunctor u (EffHead er)
|
||||
, TailHFunctor u (EffTail er)
|
||||
) =>
|
||||
(MultiToUnionH u (EffHead er) (Effectful u f er ef) ~> Effectful u f er ef) ->
|
||||
Effectful u f er ef ~> Effectful u f er ef
|
||||
reinterpretRecH f = interpretRecH f . raiseUnderH . decompEffH
|
||||
{-# INLINE reinterpretRecH #-}
|
||||
|
||||
transformAllFH ::
|
||||
@ -318,16 +365,9 @@ transformAllFH fh ff =
|
||||
overEffectful
|
||||
. overHefty
|
||||
$ transformFreer
|
||||
$ EffUnion
|
||||
. caseF
|
||||
( L1
|
||||
. EffUnionH
|
||||
. fh
|
||||
. hfmap (unEffectful . transformAllFH fh ff . Effectful)
|
||||
. unEffUnionH
|
||||
)
|
||||
(R1 . ff)
|
||||
. unEffUnion
|
||||
$ caseH
|
||||
(Inl . fh . hfmap (unEffectful . transformAllFH @eh' @ef' @eh @ef fh ff . Effectful))
|
||||
(Inr . LiftIns . ff . unliftIns)
|
||||
|
||||
transformAll ::
|
||||
forall ef' ef eh f u c.
|
||||
@ -348,34 +388,34 @@ transformAllH f = transformAllFH f id
|
||||
{-# INLINE transformAllH #-}
|
||||
|
||||
raise ::
|
||||
forall e1 e eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh) =>
|
||||
Effectful u f eh e ~> Effectful u f eh (e1 + e)
|
||||
forall er eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u er) =>
|
||||
Effectful u f eh (EffTailF er) ~> Effectful u f eh er
|
||||
raise = transformAll weaken
|
||||
{-# INLINE raise #-}
|
||||
|
||||
raiseH ::
|
||||
forall e1 e ef f u c.
|
||||
(Freer c f, Union u, HFunctors u e) =>
|
||||
Effectful u f e ef ~> Effectful u f (e1 :+: e) ef
|
||||
forall er ef f u c.
|
||||
(Freer c f, Union u, HFunctors u (EffTail er), DecompH u er) =>
|
||||
Effectful u f (EffTail er) ef ~> Effectful u f er ef
|
||||
raiseH = transformAllH weaken
|
||||
{-# INLINE raiseH #-}
|
||||
|
||||
raiseUnder ::
|
||||
forall e1 e2 e eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh) =>
|
||||
Effectful u f eh (e1 + e) ~> Effectful u f eh (e1 + e2 + e)
|
||||
forall e1r e2 eh f u c.
|
||||
(Freer c f, Union u, HFunctors u eh, DecompF u e1r) =>
|
||||
Effectful u f eh (e2 + EffTailF e1r) ~> Effectful u f eh (e2 + e1r)
|
||||
raiseUnder = transformAll weakenUnder
|
||||
{-# INLINE raiseUnder #-}
|
||||
|
||||
raiseUnderH ::
|
||||
forall e1 e2 e ef f u c.
|
||||
forall e1r e2 ef f u c.
|
||||
( Freer c f
|
||||
, Union u
|
||||
, HeadHFunctor u e1
|
||||
, HFunctors u (e1 :+: e)
|
||||
, HFunctors u (e1 :+: e2 :+: e)
|
||||
, HFunctorUnion u
|
||||
, DecompH u e1r
|
||||
, HeadHFunctor u e2
|
||||
, TailHFunctor u (EffTail e1r)
|
||||
) =>
|
||||
Effectful u f (e1 :+: e) ef ~> Effectful u f (e1 :+: e2 :+: e) ef
|
||||
Effectful u f (e2 :+: EffTail e1r) ef ~> Effectful u f (e2 :+: e1r) ef
|
||||
raiseUnderH = transformAllH weakenUnder
|
||||
{-# INLINE raiseUnderH #-}
|
||||
|
||||
@ -7,9 +7,7 @@
|
||||
module Control.Hefty where
|
||||
|
||||
import Control.Applicative (Alternative)
|
||||
import Control.Effect.Class (type (~>))
|
||||
import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, type (:+:))
|
||||
import Control.Freer (Freer, InsClass, interpretFreer, liftIns)
|
||||
import Control.Freer (InsClass)
|
||||
import Control.Monad (MonadPlus)
|
||||
import Control.Monad.Base (MonadBase)
|
||||
import Control.Monad.IO.Class (MonadIO)
|
||||
@ -46,36 +44,3 @@ overHefty ::
|
||||
Hefty f' e' b
|
||||
overHefty f = Hefty . f . unHefty
|
||||
{-# INLINE overHefty #-}
|
||||
|
||||
interpretRecRWith ::
|
||||
forall r l f c.
|
||||
Freer c f =>
|
||||
((Hefty f (l :+: r) ~> Hefty f l) -> l (Hefty f (l :+: r)) ~> l (Hefty f l)) ->
|
||||
((Hefty f (l :+: r) ~> Hefty f l) -> r (Hefty f (l :+: r)) ~> Hefty f l) ->
|
||||
Hefty f (l :+: r) ~> Hefty f l
|
||||
interpretRecRWith f i =
|
||||
overHefty $
|
||||
interpretFreer $
|
||||
caseH
|
||||
(liftIns . f int)
|
||||
(unHefty . i int)
|
||||
where
|
||||
int :: Hefty f (l :+: r) ~> Hefty f l
|
||||
int = interpretRecRWith f i
|
||||
{-# INLINE int #-}
|
||||
|
||||
interpretRecR ::
|
||||
forall r l f c.
|
||||
(Freer c f, HFunctor l, HFunctor r) =>
|
||||
(r (Hefty f l) ~> Hefty f l) ->
|
||||
Hefty f (l :+: r) ~> Hefty f l
|
||||
interpretRecR i =
|
||||
overHefty $
|
||||
interpretFreer $
|
||||
caseH
|
||||
(liftIns . hfmapInt)
|
||||
(unHefty . i . hfmapInt)
|
||||
where
|
||||
hfmapInt :: HFunctor e => e (Hefty f (l :+: r)) ~> e (Hefty f l)
|
||||
hfmapInt = hfmap $ interpretRecR i
|
||||
{-# INLINE hfmapInt #-}
|
||||
|
||||
@ -1,158 +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/.
|
||||
|
||||
module Control.Hefty.SFunctor where
|
||||
|
||||
import Control.Effect.Class (LiftIns (LiftIns), NopS, unliftIns, type (~>))
|
||||
import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
|
||||
import Control.Freer (Freer, interpretFreer, liftIns, transformFreer)
|
||||
import Control.Hefty (Hefty (Hefty), SigClass, overHefty, unHefty)
|
||||
import Data.Kind (Type)
|
||||
|
||||
class HyperFunctor (h :: SigClass -> Type -> Type) where
|
||||
hyfmap :: (e (h e) ~> e' (h e')) -> h e ~> h e'
|
||||
|
||||
instance Freer c f => HyperFunctor (Hefty f) where
|
||||
hyfmap f = Hefty . transformFreer f . unHefty
|
||||
{-# INLINE hyfmap #-}
|
||||
|
||||
class SFunctor (e :: SigClass) where
|
||||
sfmap ::
|
||||
(HyperFunctor h, SFunctor e1, SFunctor e2) =>
|
||||
(forall ex. SFunctor ex => h (ex :+: e1) ~> h (ex :+: e2)) ->
|
||||
e (h e1) ~> e (h e2)
|
||||
|
||||
interpretRecRWithSFunctor ::
|
||||
forall r l f c.
|
||||
(Freer c f, SFunctor l, SFunctor r) =>
|
||||
(forall ex. SFunctor ex => r (Hefty f (ex :+: l)) ~> Hefty f (ex :+: l)) ->
|
||||
Hefty f (l :+: r) ~> Hefty f l
|
||||
interpretRecRWithSFunctor i =
|
||||
overHefty $
|
||||
interpretFreer $
|
||||
caseH
|
||||
(liftIns . sfmap int)
|
||||
( unHefty
|
||||
. absurdHyperFunctorL
|
||||
. i
|
||||
. sfmap (hyshfmap (caseH Inl (Inr . Inr)) . int)
|
||||
)
|
||||
where
|
||||
int :: SFunctor ex' => Hefty f (ex' :+: (l :+: r)) ~> Hefty f (ex' :+: l)
|
||||
int =
|
||||
interpretRecRWithSFunctor (hyshfmap assocRSumH . i . shysfmap assocLSumH)
|
||||
. hyshfmap assocLSumH
|
||||
|
||||
hyshfmap ::
|
||||
forall e1 e2 h.
|
||||
( HyperFunctor h
|
||||
, SFunctor e1
|
||||
, SFunctor e2
|
||||
) =>
|
||||
(forall ex. e1 (h ex) ~> e2 (h ex)) ->
|
||||
h e1 ~> h e2
|
||||
hyshfmap f = hyfmap $ shysfmap f . f
|
||||
{-# INLINE hyshfmap #-}
|
||||
|
||||
shysfmap ::
|
||||
forall e e1 e2 h.
|
||||
( HyperFunctor h
|
||||
, SFunctor e
|
||||
, SFunctor e1
|
||||
, SFunctor e2
|
||||
) =>
|
||||
(forall ex. e1 (h ex) ~> e2 (h ex)) ->
|
||||
e (h e1) ~> e (h e2)
|
||||
shysfmap f = sfmap $ hyshfmap $ caseH Inl (Inr . f)
|
||||
{-# INLINE shysfmap #-}
|
||||
|
||||
hysfmap ::
|
||||
forall e e' h.
|
||||
(HyperFunctor h, SFunctor e, SFunctor e') =>
|
||||
(forall f. e f ~> e' f) ->
|
||||
h e ~> h e'
|
||||
hysfmap f = hyfmap $ f . sfmap (rightHyperFunctor f)
|
||||
{-# INLINE hysfmap #-}
|
||||
|
||||
rightHyperFunctor ::
|
||||
forall l r r' h.
|
||||
(HyperFunctor h, SFunctor l, SFunctor r, SFunctor r') =>
|
||||
(forall ex. r (h (ex :+: r')) ~> r' (h (ex :+: r'))) ->
|
||||
h (l :+: r) ~> h (l :+: r')
|
||||
rightHyperFunctor f =
|
||||
hyfmap $ caseH (Inl . sfmapR f) (Inr . f . sfmapR f)
|
||||
|
||||
sfmapR ::
|
||||
forall e l r r' h.
|
||||
(HyperFunctor h, SFunctor e, SFunctor l, SFunctor r, SFunctor r') =>
|
||||
(forall ex. r (h (ex :+: r')) ~> r' (h (ex :+: r'))) ->
|
||||
e (h (l :+: r)) ~> e (h (l :+: r'))
|
||||
sfmapR f =
|
||||
sfmap $
|
||||
assocHyperFunctorR
|
||||
. rightHyperFunctor f
|
||||
. assocHyperFunctorL
|
||||
|
||||
assocHyperFunctorL ::
|
||||
forall e1 e2 e3 h.
|
||||
(HyperFunctor h, SFunctor e1, SFunctor e2, SFunctor e3) =>
|
||||
h (e1 :+: (e2 :+: e3)) ~> h ((e1 :+: e2) :+: e3)
|
||||
assocHyperFunctorL = hyshfmap assocLSumH
|
||||
|
||||
assocHyperFunctorR ::
|
||||
forall e1 e2 e3 h.
|
||||
(HyperFunctor h, SFunctor e1, SFunctor e2, SFunctor e3) =>
|
||||
h ((e1 :+: e2) :+: e3) ~> h (e1 :+: (e2 :+: e3))
|
||||
assocHyperFunctorR = hyshfmap assocRSumH
|
||||
|
||||
instance SFunctor (LiftIns e) where
|
||||
sfmap _ = LiftIns . unliftIns
|
||||
{-# INLINE sfmap #-}
|
||||
|
||||
instance
|
||||
(SFunctor e1, SFunctor e2) =>
|
||||
SFunctor (e1 :+: e2)
|
||||
where
|
||||
sfmap f = caseH (Inl . sfmap f) (Inr . sfmap f)
|
||||
{-# INLINE sfmap #-}
|
||||
|
||||
newtype ViaHFunctor (e :: SigClass) f a = ViaHFunctor {unViaHFunctor :: e f a}
|
||||
deriving (HFunctor)
|
||||
|
||||
instance HFunctor e => SFunctor (ViaHFunctor e) where
|
||||
sfmap f = hfmap $ absurdHyperFunctorL . f . weakenHyperFunctorL
|
||||
{-# INLINE sfmap #-}
|
||||
|
||||
absurdHyperFunctorL ::
|
||||
forall e h.
|
||||
(HyperFunctor h, SFunctor e) =>
|
||||
h (NopS :+: e) ~> h e
|
||||
absurdHyperFunctorL = hysfmap $ caseH (\case {}) id
|
||||
{-# INLINE absurdHyperFunctorL #-}
|
||||
|
||||
weakenHyperFunctorL ::
|
||||
forall l r h.
|
||||
(HyperFunctor h, SFunctor l, SFunctor r) =>
|
||||
h r ~> h (l :+: r)
|
||||
weakenHyperFunctorL = hysfmap Inr
|
||||
{-# INLINE weakenHyperFunctorL #-}
|
||||
|
||||
assocLSumH :: (e1 :+: (e2 :+: e3)) f ~> ((e1 :+: e2) :+: e3) f
|
||||
assocLSumH = caseH (Inl . Inl) (caseH (Inl . Inr) Inr)
|
||||
|
||||
assocRSumH :: ((e1 :+: e2) :+: e3) f ~> (e1 :+: (e2 :+: e3)) f
|
||||
assocRSumH = caseH (caseH Inl (Inr . Inl)) (Inr . Inr)
|
||||
|
||||
data ((e :: SigClass) +# (f :: Type -> Type)) (a :: Type) where
|
||||
HyperFunctorPlusT :: h (e :+: r) a -> (e +# h r) a
|
||||
|
||||
deriving stock instance Functor (h (e :+: r)) => Functor (e +# h r)
|
||||
deriving stock instance Foldable (h (e :+: r)) => Foldable (e +# h r)
|
||||
deriving stock instance Traversable (h (e :+: r)) => Traversable (e +# h r)
|
||||
|
||||
instance SFunctor e => SFunctor ((+#) e) where
|
||||
sfmap f (HyperFunctorPlusT a) = HyperFunctorPlusT $ f a
|
||||
{-# INLINE sfmap #-}
|
||||
@ -61,8 +61,6 @@ interpretTreeK i (FreerTree m) =
|
||||
(i e)
|
||||
((`runCont` runIdentity . k) . interpretTreeK i . FreerTree . f)
|
||||
|
||||
-- ContT \k -> f k \k' e -> Identity $ runCont (i e) (runIdentity . k')
|
||||
|
||||
instance Freer Monad FreerTree where
|
||||
liftIns = liftInsTree
|
||||
interpretFreer = interpretTree
|
||||
|
||||
@ -4,7 +4,6 @@
|
||||
|
||||
{- |
|
||||
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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user