diff --git a/data-effects-core.cabal b/data-effects-core.cabal
--- a/data-effects-core.cabal
+++ b/data-effects-core.cabal
@@ -1,6 +1,6 @@
cabal-version: 3.0
name: data-effects-core
-version: 0.4.1.0
+version: 0.4.2.0
-- A short (one-line) description of the package.
synopsis: A basic framework for effect systems based on effects represented by GADTs.
@@ -37,7 +37,7 @@
source-repository head
type: git
location: https://github.com/sayo-hs/data-effects
- tag: v0.4.1.0
+ tag: v0.4.2.0
subdir: data-effects-core
library
diff --git a/src/Control/Effect/Transform.hs b/src/Control/Effect/Transform.hs
--- a/src/Control/Effect/Transform.hs
+++ b/src/Control/Effect/Transform.hs
@@ -19,10 +19,12 @@
KnownLength,
KnownOrder,
Membership,
+ RemoveExps,
RemoveHOEs,
Suffix,
SuffixUnder,
Union,
+ WeakenExps,
WeakenHOEs,
hfmapUnion,
identityMembership,
@@ -34,6 +36,7 @@
prefixFor1,
suffixFor,
weaken,
+ weakenExps,
weakenFor,
weakenHOEs,
weakens,
@@ -68,6 +71,10 @@
onlyFOEs :: forall es a ff c. (Free c ff, WeakenHOEs es) => Eff ff (RemoveHOEs es) a -> Eff ff es a
onlyFOEs = transAll weakenHOEs
{-# INLINE onlyFOEs #-}
+
+onlyPolys :: forall es a ff c. (Free c ff, WeakenExps es) => Eff ff (RemoveExps es) a -> Eff ff es a
+onlyPolys = transAll weakenExps
+{-# INLINE onlyPolys #-}
raisePrefix
:: forall es' es a ff c
diff --git a/src/Data/Effect.hs b/src/Data/Effect.hs
--- a/src/Data/Effect.hs
+++ b/src/Data/Effect.hs
@@ -23,10 +23,19 @@
type family OrderOf (e :: Effect) :: EffectOrder
-type family OrderCase (e :: EffectOrder) a b where
+type family OrderCase (o :: EffectOrder) a b where
OrderCase 'FirstOrder a b = a
OrderCase 'HigherOrder a b = b
+data EffectForm = Polynomial | Exponential
+ deriving (Show, Eq, Ord)
+
+type family FormOf (e :: Effect) :: EffectForm
+
+type family FormCase (f :: EffectForm) a b where
+ FormCase 'Polynomial a b = a
+ FormCase 'Exponential a b = b
+
type family LabelOf (e :: Effect)
class
@@ -36,7 +45,7 @@
FirstOrder (e :: Effect)
-- | A higher-order polynomial functor.
-class PolyHFunctor (e :: Effect)
+class (FormOf e ~ 'Polynomial) => PolyHFunctor (e :: Effect)
-- * Nop Effect
@@ -50,6 +59,7 @@
instance HFunctor Nop where
hfmap _ = \case {}
{-# INLINE hfmap #-}
+type instance FormOf Nop = 'Polynomial
instance PolyHFunctor Nop
-- * Embedding Effect
@@ -65,6 +75,7 @@
instance HFunctor (Emb e) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (Emb e) = 'Polynomial
instance PolyHFunctor (Emb e)
newtype Unemb e a = Unemb {getUnemb :: forall f. e f a}
@@ -83,6 +94,7 @@
instance HFunctor (Ask r) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (Ask r) = 'Polynomial
instance PolyHFunctor (Ask r)
-- | An effect that locally modifies the value held in the environment.
@@ -101,6 +113,7 @@
instance HFunctor (Local r) where
hfmap phi (Local f a) = Local f (phi a)
{-# INLINE hfmap #-}
+type instance FormOf (Local r) = 'Polynomial
instance PolyHFunctor (Local r)
-- * State Effect
@@ -119,6 +132,7 @@
instance HFunctor (State s) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (State s) = 'Polynomial
instance PolyHFunctor (State s)
-- * Writer Effects
@@ -135,6 +149,7 @@
instance HFunctor (Tell w) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (Tell w) = 'Polynomial
instance PolyHFunctor (Tell w)
-- | An effect that performs local operations on accumulations in the context on a per-scope basis.
@@ -160,6 +175,7 @@
Listen a -> Listen $ phi a
Censor f a -> Censor f (phi a)
{-# INLINE hfmap #-}
+type instance FormOf (WriterH w) = 'Polynomial
instance PolyHFunctor (WriterH w)
-- * Exception Effects
@@ -176,6 +192,7 @@
instance HFunctor (Throw e) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (Throw e) = 'Polynomial
instance PolyHFunctor (Throw e)
-- | An effect to catch exceptions.
@@ -194,6 +211,7 @@
instance HFunctor (Catch e) where
hfmap phi (Catch a hdl) = Catch (phi a) (phi . hdl)
{-# INLINE hfmap #-}
+type instance FormOf (Catch e) = 'Polynomial
instance PolyHFunctor (Catch e)
-- * Non-Determinism Effects
@@ -210,6 +228,7 @@
instance HFunctor Empty where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf Empty = 'Polynomial
instance PolyHFunctor Empty
-- | An effect that splits the computation into two branches.
@@ -225,6 +244,7 @@
instance HFunctor Choose where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf Choose = 'Polynomial
instance PolyHFunctor Choose
{- |
@@ -242,6 +262,7 @@
instance HFunctor ChooseH where
hfmap phi (ChooseH a b) = ChooseH (phi a) (phi b)
{-# INLINE hfmap #-}
+type instance FormOf ChooseH = 'Polynomial
instance PolyHFunctor ChooseH
-- * Fail Effect
@@ -256,6 +277,7 @@
instance HFunctor Fail where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf Fail = 'Polynomial
instance PolyHFunctor Fail
-- * Fix Effect
@@ -269,6 +291,7 @@
instance HFunctor Fix where
hfmap phi (Efix f) = Efix $ phi . f
{-# INLINE hfmap #-}
+type instance FormOf Fix = 'Polynomial
instance PolyHFunctor Fix
-- * Unlift Effect
@@ -284,8 +307,7 @@
instance HFunctor (UnliftBase b) where
hfmap phi (WithRunInBase f) = WithRunInBase \run -> f $ run . phi
{-# INLINE hfmap #-}
-
--- The Unlift effect is not polynomial.
+type instance FormOf (UnliftBase b) = 'Exponential
-- * CallCC Effect (Sub/Jump-based)
@@ -300,4 +322,5 @@
instance HFunctor (CC ref) where
hfmap _ = coerce
{-# INLINE hfmap #-}
+type instance FormOf (CC ref) = 'Polynomial
instance PolyHFunctor (CC ref)
diff --git a/src/Data/Effect/OpenUnion.hs b/src/Data/Effect/OpenUnion.hs
--- a/src/Data/Effect/OpenUnion.hs
+++ b/src/Data/Effect/OpenUnion.hs
@@ -16,7 +16,7 @@
import Control.Arrow ((&&&))
import Data.Coerce (coerce)
import Data.Data (Proxy (Proxy), (:~:) (Refl))
-import Data.Effect (Effect, EffectOrder (FirstOrder, HigherOrder), FirstOrder, LabelOf, OrderCase, OrderOf, PolyHFunctor)
+import Data.Effect (Effect, EffectForm (Exponential, Polynomial), EffectOrder (FirstOrder, HigherOrder), FirstOrder, FormCase, FormOf, LabelOf, OrderCase, OrderOf, PolyHFunctor)
import Data.Effect.HFunctor (HFunctor, hfmap)
import Data.Effect.Tag (type (#))
import Data.Kind (Constraint, Type)
@@ -47,13 +47,13 @@
{-# INLINE hfmapUnion #-}
-- | The list @es@ consists only of first-order effects.
-class FOEs es
+class FOEs (es :: [Effect])
instance FOEs '[]
instance (FirstOrder e, FOEs es) => FOEs (e ': es)
-- | The list @es@ consists only of polynomial effects.
-class PolyHFunctors es
+class PolyHFunctors (es :: [Effect])
instance PolyHFunctors '[]
instance (PolyHFunctor e, PolyHFunctors es) => PolyHFunctors (e ': es)
@@ -77,7 +77,12 @@
There (UnsafeMembership n) = UnsafeMembership (n + 1)
{-# INLINE There #-}
-{-# COMPLETE Here, There #-}
+infixr 5 !:>
+(!:>) :: forall e e' es r. ((e :~: e') -> r) -> (Membership e es -> r) -> Membership e (e' ': es) -> r
+(f !:> g) (UnsafeMembership n)
+ | n == 0 = f $ unsafeCoerce Refl
+ | otherwise = g $ UnsafeMembership $ n - 1
+{-# INLINE (!:>) #-}
weakenFor :: Membership e es -> Membership e (e' ': es)
weakenFor (UnsafeMembership n) = UnsafeMembership $ n + 1
@@ -428,6 +433,36 @@
else shiftedIx + 1
{-# INLINE foldHoeIndexShifter #-}
+type family RemoveExps (es :: [Effect]) where
+ RemoveExps '[] = '[]
+ RemoveExps (e ': es) =
+ FormCase (FormOf e) (e ': RemoveExps es) (RemoveExps es)
+
+type WeakenExps es = (WeakenExps_ es 0 (FormOf (HeadOf es)), PolyHFunctors (RemoveExps es))
+
+class (formOfHead ~ FormOf (HeadOf es)) => WeakenExps_ es (countP :: Natural) formOfHead where
+ foldExpIndexShifter :: (Int -> Int) -> (Int -> Int)
+
+instance (FormOf (HeadOf '[]) ~ formOfHead) => WeakenExps_ '[] countP formOfHead where
+ foldExpIndexShifter = id
+ {-# INLINE foldExpIndexShifter #-}
+
+instance (PolyHFunctor e, WeakenExps_ es (countP + 1) _formOfHead) => WeakenExps_ (e ': es) countP 'Polynomial where
+ foldExpIndexShifter = foldExpIndexShifter @es @(countP + 1)
+ {-# INLINE foldExpIndexShifter #-}
+
+instance
+ (FormOf e ~ 'Exponential, WeakenExps_ es countP _formOfHead, KnownNat countP)
+ => WeakenExps_ (e ': es) countP 'Exponential
+ where
+ foldExpIndexShifter shifterAcc =
+ foldExpIndexShifter @es @countP \ix ->
+ let shiftedIx = shifterAcc ix
+ in if ix < intVal @countP
+ then shiftedIx
+ else shiftedIx + 1
+ {-# INLINE foldExpIndexShifter #-}
+
weaken :: Union es f a -> Union (e ': es) f a
weaken = mapUnion weakenFor
{-# INLINE weaken #-}
@@ -448,6 +483,14 @@
weakenHOEs = mapUnion weakenHOEsFor
{-# INLINE weakenHOEs #-}
+weakenExpsFor :: forall es e. (WeakenExps es) => Membership e (RemoveExps es) -> Membership e es
+weakenExpsFor = UnsafeMembership . foldExpIndexShifter @es @0 id . unMembership
+{-# INLINE weakenExpsFor #-}
+
+weakenExps :: forall es f a. (WeakenExps es) => Union (RemoveExps es) f a -> Union es f a
+weakenExps = mapUnion weakenExpsFor
+{-# INLINE weakenExps #-}
+
type KnownLength :: forall {k}. [k] -> Constraint
class KnownLength xs where
reifyLength :: Int
@@ -515,6 +558,26 @@
Right u -> mapUnion (prefixFor @es) u
{-# INLINE mergeUnion #-}
+splitUnion1
+ :: forall fs x es es' f a
+ . (KnownLength fs)
+ => (forall e. Membership e (Each fs x) -> Membership e es')
+ -> (forall e. Membership e es -> Membership e es')
+ -> Union (Each fs x ++ es) f a
+ -> Union es' f a
+splitUnion1 injL injR = mapUnion $ splitFor1 @fs @x @es injL injR
+{-# INLINE splitUnion1 #-}
+
+mergeUnion1
+ :: forall fs x es f a
+ . (KnownLength fs)
+ => Either (Union (Each fs x) f a) (Union es f a)
+ -> Union (Each fs x ++ es) f a
+mergeUnion1 = \case
+ Left u -> mapUnion (suffixFor @es) u
+ Right u -> mapUnion (prefixFor1 @fs @x) u
+{-# INLINE mergeUnion1 #-}
+
splitFor
:: forall es es' e r
. (KnownLength es)
@@ -528,6 +591,20 @@
where
l = reifyLength @es
{-# INLINE splitFor #-}
+
+splitFor1
+ :: forall fs x es e r
+ . (KnownLength fs)
+ => (Membership e (Each fs x) -> r)
+ -> (Membership e es -> r)
+ -> Membership e (Each fs x ++ es)
+ -> r
+splitFor1 f g (UnsafeMembership n)
+ | n < l = f $ UnsafeMembership n
+ | otherwise = g $ UnsafeMembership $ n - l
+ where
+ l = reifyLength @fs
+{-# INLINE splitFor1 #-}
suffixFor :: forall es' es e. Membership e es -> Membership e (es ++ es')
suffixFor = coerce
diff --git a/test/OpenUnion.hs b/test/OpenUnion.hs
--- a/test/OpenUnion.hs
+++ b/test/OpenUnion.hs
@@ -8,8 +8,8 @@
module OpenUnion where
import Control.Effect (Eff, Free, perform)
-import Data.Effect (Catch, Effect, LabelOf, Throw (Throw))
-import Data.Effect.OpenUnion (Membership (UnsafeMembership), labelMembership, membershipAt, weakenHOEsFor, (:>))
+import Data.Effect (Catch, Effect, LabelOf, Throw (Throw), UnliftIO)
+import Data.Effect.OpenUnion (Membership (UnsafeMembership), labelMembership, membershipAt, weakenExpsFor, weakenHOEsFor, (:>))
import Data.Proxy (Proxy (Proxy))
import GHC.TypeNats (KnownNat, Natural, natVal)
import Test.Hspec (Spec, describe, it, shouldBe)
@@ -60,6 +60,29 @@
shiftIx = weakenHOEsFor
ix0, ix1, ix2, ix3 :: Membership F '[F, F, F, F]
+ ix0 = membershipAt @0
+ ix1 = membershipAt @1
+ ix2 = membershipAt @2
+ ix3 = membershipAt @3
+
+type P = Catch ()
+type E = UnliftIO
+
+spec_onlyPolys :: Spec
+spec_onlyPolys = describe "onlyPolys index shift" do
+ it "'[, P , P , P ] -> '[ E ,
, P , E , E , P , E , P ]" $
+ shiftIx ix0 `shouldBe` UnsafeMembership 1
+ it "'[ P ,
, P , P ] -> '[ E , P ,
, E , E , P , E , P ]" $
+ shiftIx ix1 `shouldBe` UnsafeMembership 2
+ it "'[ P , P ,
, P ] -> '[ E , P , P , E , E ,
, E , P ]" $
+ shiftIx ix2 `shouldBe` UnsafeMembership 5
+ it "'[ P , P , P ,
] -> '[ E , P , P , E , E , P , E ,
]" $
+ shiftIx ix3 `shouldBe` UnsafeMembership 7
+ where
+ shiftIx :: Membership e '[P, P, P, P] -> Membership e '[E, P, P, E, E, P, E, P]
+ shiftIx = weakenExpsFor
+
+ ix0, ix1, ix2, ix3 :: Membership P '[P, P, P, P]
ix0 = membershipAt @0
ix1 = membershipAt @1
ix2 = membershipAt @2