data-effects-core 0.2.0.0 → 0.4.0.0

raw patch · 14 files changed

+1717/−328 lines, 14 filesdep +freedep +hspecdep +kan-extensionsdep −compdatadep −tasty-hunitdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: free, hspec, kan-extensions, primitive, tasty-hspec, unliftio

Dependencies removed: compdata, tasty-hunit

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• data-effects-core.cabal +29/−17
• src/Control/Effect.hs +330/−24
• src/Control/Effect/Interpret.hs +197/−0
• src/Control/Effect/Key.hs +0/−66
• src/Control/Effect/Tag.hs +0/−70
• src/Control/Effect/Transform.hs +215/−0
• src/Data/Effect.hs +280/−22
• src/Data/Effect/HFunctor.hs +8/−41
• src/Data/Effect/HFunctor/HCont.hs +5/−6
• src/Data/Effect/Key.hs +0/−48
• src/Data/Effect/OpenUnion.hs +564/−0
• src/Data/Effect/Tag.hs +14/−34
• test/OpenUnion.hs +69/−0

@@ -9,3 +9,9 @@ * Remove the type operator for HCont. * Rename the terms "instruction" and "signature" to the simpler "FOE" and "HOE". * Support for GHC 9.8.2.++## 0.4.0.0 -- 2025-04-16++* The new v4 interface.+    * Unified first-order and higher-order effect interfaces.+    * Added a generic `Eff` carrier type.

@@ -1,6 +1,6 @@-cabal-version:      2.4+cabal-version:      3.0 name:               data-effects-core-version:            0.2.0.0+version:            0.4.0.0  -- A short (one-line) description of the package. synopsis: A basic framework for effect systems based on effects represented by GADTs.@@ -15,12 +15,12 @@ -- The license under which the package is released. license:            MPL-2.0 license-file:       LICENSE-author:             Sayo Koyoneda <ymdfield@outlook.jp>-maintainer:         Sayo Koyoneda <ymdfield@outlook.jp>+author:             Sayo contributors <ymdfield@outlook.jp>+maintainer:         ymdfield <ymdfield@outlook.jp>  -- A copyright notice. copyright:-    2023-2024 Sayo Koyoneda+    2023-2025 Sayo contributors  category: Control, Effect @@ -29,27 +29,30 @@     NOTICE     README.md -tested-with:-    GHC == 9.8.2-    GHC == 9.4.1-    GHC == 9.2.8+tested-with: GHC == {9.2.8, 9.4.8, 9.6.7, 9.8.4, 9.10.1, 9.12.2} +common warnings+    ghc-options: -Wall -Wredundant-constraints+ source-repository head     type: git     location: https://github.com/sayo-hs/data-effects-    tag: v0.2.0+    tag: v0.4.0     subdir: data-effects-core  library+    import: warnings+     exposed-modules:         Data.Effect+        -- Data.Effect.OpenUnion         Data.Effect.Tag-        Data.Effect.Key         Data.Effect.HFunctor         Data.Effect.HFunctor.HCont+        Data.Effect.OpenUnion         Control.Effect-        Control.Effect.Tag-        Control.Effect.Key+        Control.Effect.Interpret+        Control.Effect.Transform      -- Modules included in this executable, other than Main.     -- other-modules:@@ -57,9 +60,12 @@     -- LANGUAGE extensions used by modules in this package.     -- other-extensions:     build-depends:-        base                          >= 4.16.4 && < 4.21,-        compdata                      >= 0.13.1 && < 0.14,+        base                          >= 4.16.4 && < 4.22,         mtl                           >= 2.2.2 && < 2.4,+        kan-extensions,+        free,+        unliftio,+        primitive,      hs-source-dirs:   src     ghc-options:      -Wall@@ -75,16 +81,21 @@         RecordWildCards,         DefaultSignatures - test-suite test+    import: warnings+     main-is: Driver.hs     hs-source-dirs: test     build-depends:         data-effects-core,         base,         tasty                         >= 1.4 && < 1.6,-        tasty-hunit                   ^>= 0.10,+        tasty-hspec                   ^>= 1.2,+        hspec                         >= 2.5 && < 2.12, +    other-modules:+        OpenUnion+     type: exitcode-stdio-1.0      build-tool-depends:@@ -101,3 +112,4 @@         FunctionalDependencies,         RecordWildCards,         DefaultSignatures+

@@ -1,44 +1,350 @@--- 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/.+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-} +-- SPDX-License-Identifier: MPL-2.0+ {- |-Copyright   :  (c) 2023-2024 Sayo Koyoneda+Copyright   :  (c) 2023-2025 Sayo contributors License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable -} module Control.Effect where -import Data.Effect (EffectF, EffectH, LiftFOE (unliftFOE))+import Control.Alternative.Free qualified as Tree+import Control.Alternative.Free.Final qualified as Final+import Control.Applicative (Alternative, empty, (<|>))+import Control.Applicative.Free qualified as Tree+import Control.Applicative.Free.Fast qualified as Fast+import Control.Applicative.Free.Final qualified as Final+import Control.Monad (MonadPlus)+import Control.Monad.Cont qualified as Cont+import Control.Monad.Except (MonadError, catchError, throwError)+import Control.Monad.Fix (MonadFix, mfix)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.RWS (MonadRWS)+import Control.Monad.Reader (MonadReader (ask), local)+import Control.Monad.State (MonadState, get, put)+import Control.Monad.Writer (MonadWriter, listen, tell)+import Control.Monad.Writer qualified as Writer+import Data.Effect (+    Ask (Ask),+    AskLabel,+    CC (Jump, SubFork),+    Catch (Catch),+    ChooseH (ChooseH),+    Emb (Emb),+    Empty (Empty),+    Fail (Fail),+    Fix (Efix),+    Local (Local),+    State (Get, Put),+    StateLabel,+    Tell (Tell),+    TellLabel,+    Throw (Throw),+    ThrowLabel,+    UnliftBase (WithRunInBase),+    UnliftIO,+    WriterH (Listen),+ )+import Data.Effect.OpenUnion (+    At,+    FindByLabel,+    Has,+    IdentityResolver,+    In,+    KeyDiscriminator,+    KeyResolver,+    KnownIndex,+    KnownOrder,+    LabelResolver,+    Membership,+    Union,+    hfmapUnion,+    inject,+    membership,+    membershipAt,+    type (:>),+ )+import Data.Effect.Tag (Tagged (Tag), type (#))+import Data.Functor.Coyoneda (Coyoneda (Coyoneda), hoistCoyoneda, liftCoyoneda, lowerCoyoneda) import Data.Kind (Type)+import Data.Tuple (swap)+import UnliftIO qualified as IO --- | A type class that represents the ability to send an first-order effect @ins@ to carrier @f@.-class SendFOE (ins :: EffectF) f where-    -- | Send an /instruction/ @ins@ to carrier @f@.-    sendFOE :: ins a -> f a+newtype Eff ff es a = Eff {unEff :: ff (Union es (Eff ff es)) a} --- | The operator version of `SendFOE`.-type (<:) = SendFOE+perform :: forall e es ff a c. (e :> es, Free c ff) => e (Eff ff es) a -> Eff ff es a+perform = sendFor $ membership @LabelResolver+{-# INLINE perform #-} -infix 2 <:+perform' :: forall key e es ff a c. (Has key e es, Free c ff) => e (Eff ff es) a -> Eff ff es a+perform' = sendFor (membership @KeyResolver @(KeyDiscriminator key)) . Tag+{-# INLINE perform' #-} --- | A type class that represents the ability to send a higher-order effect @sig@ to carrier @f@.-class SendHOE (sig :: EffectH) f where-    -- | Send a higher-order effect @sig@ to carrier @f@.-    sendHOE :: sig f a -> f a+perform'' :: forall tag e es ff a c. (e # tag :> es, Free c ff) => e (Eff ff es) a -> Eff ff es a+perform'' = perform . Tag @tag+{-# INLINE perform'' #-} --- | The operator version of `SendHOE`.-type (<<:) = SendHOE+send :: forall e es ff a c. (e `In` es, Free c ff) => e (Eff ff es) a -> Eff ff es a+send = sendFor $ membership @IdentityResolver+{-# INLINE send #-} -infix 2 <<:+sendAt :: forall i es ff a c. (KnownIndex i es, Free c ff) => At i es (Eff ff es) a -> Eff ff es a+sendAt = sendFor $ membershipAt @i+{-# INLINE sendAt #-} -instance (SendFOE ins f) => SendHOE (LiftFOE ins) f where-    sendHOE = sendFOE . unliftFOE-    {-# INLINE sendHOE #-}+sendFor+    :: forall e es ff a c+     . (KnownOrder e, Free c ff)+    => Membership e es+    -> e (Eff ff es) a+    -> Eff ff es a+sendFor i = Eff . liftFree . inject i+{-# INLINE sendFor #-} +emb :: forall f es ff a c. (Emb f :> es, Free c ff) => f a -> Eff ff es a+emb = perform . Emb+{-# INLINE emb #-}+ -- | A natural transformation. type f ~> g = forall (x :: Type). f x -> g x  infixr 2 ~>++type e ~~> f = e f ~> f++infix 2 ~~>++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++instance+    (FindByLabel AskLabel (Ask r) es, Local r :> es, Monad (Eff ff es), Free c ff)+    => MonadReader r (Eff ff es)+    where+    ask = perform Ask+    local f a = perform $ Local f a+    {-# INLINE ask #-}+    {-# INLINE local #-}++instance+    (FindByLabel TellLabel (Tell w) es, WriterH w :> es, Monoid w, Monad (Eff ff es), Free c ff)+    => MonadWriter w (Eff ff es)+    where+    tell = perform . Tell+    listen a = fmap swap $ perform $ Listen a+    pass = pass . fmap swap+    {-# INLINE tell #-}+    {-# INLINE listen #-}++{- |+For a given scope, uses the function (the first component of the pair returned+by that scope) to modify the accumulated value of that scope, and then+accumulates the result into the current outer scope.++@+pass m = do+    (w, (f, a)) <- listen m+    tell $ f w+    pure a+@+-}+pass+    :: forall w a es ff c+     . (Tell w :> es, WriterH w :> es, Monad (Eff ff es), Free c ff)+    => Eff ff es (w -> w, a)+    -> Eff ff es a+pass m = do+    (w, (f, a)) <- perform $ Listen m+    perform $ Tell $ f w+    pure a+{-# INLINE pass #-}++instance (FindByLabel StateLabel (State s) es, Monad (Eff ff es), Free c ff) => MonadState s (Eff ff es) where+    get = perform Get+    put = perform . Put+    {-# INLINE get #-}+    {-# INLINE put #-}++instance+    ( FindByLabel AskLabel (Ask r) es+    , Local r :> es+    , FindByLabel TellLabel (Tell w) es+    , WriterH w :> es+    , FindByLabel StateLabel (State s) es+    , Monoid w+    , Monad (Eff ff es)+    , Free c ff+    )+    => MonadRWS r w s (Eff ff es)++instance+    (FindByLabel ThrowLabel (Throw e) es, Catch e :> es, Monad (Eff ff es), Free c ff)+    => MonadError e (Eff ff es)+    where+    throwError = perform . Throw+    catchError a hdl = perform $ Catch a hdl+    {-# INLINE throwError #-}+    {-# INLINE catchError #-}++instance+    (Empty :> es, ChooseH :> es, Applicative (Eff ff es), Free c ff)+    => Alternative (Eff ff es)+    where+    empty = perform Empty+    a <|> b = perform $ ChooseH a b+    {-# INLINE empty #-}+    {-# INLINE (<|>) #-}++instance (Empty :> es, ChooseH :> es, Monad (Eff ff es), Free c ff) => MonadPlus (Eff ff es)++instance (CC ref :> es, Monad (Eff ff es), Free c ff) => Cont.MonadCont (Eff ff es) where+    callCC = callCC_+    {-# INLINE callCC #-}++sub+    :: forall ref a b es ff c+     . (CC ref :> es, Monad (Eff ff es), Free c ff)+    => (ref a -> Eff ff es b)+    -> (a -> Eff ff es b)+    -> Eff ff es b+sub p q = perform SubFork >>= either p q+{-# INLINE sub #-}++callCC_+    :: forall ref a b es ff c+     . (CC ref :> es, Monad (Eff ff es), Free c ff)+    => ((a -> Eff ff es b) -> Eff ff es a)+    -> Eff ff es a+callCC_ f = sub (f . jump) pure+  where+    jump ref x = perform $ Jump ref x+{-# INLINE callCC_ #-}++instance (Emb IO :> es, Monad (Eff ff es), Free c ff) => MonadIO (Eff ff es) where+    liftIO = emb+    {-# INLINE liftIO #-}++instance (Fail :> es, Monad (Eff ff es), Free c ff) => MonadFail (Eff ff es) where+    fail = perform . Fail+    {-# INLINE fail #-}++instance (Fix :> es, Monad (Eff ff es), Free c ff) => MonadFix (Eff ff es) where+    mfix = perform . Efix+    {-# INLINE mfix #-}++instance+    (UnliftIO :> es, Emb IO :> es, Monad (Eff ff es), Free c ff)+    => IO.MonadUnliftIO (Eff ff es)+    where+    withRunInIO f = perform $ WithRunInBase f+    {-# INLINE withRunInIO #-}++-- Free++class (forall f. c (ff f)) => Free c (ff :: (Type -> Type) -> Type -> Type) | ff -> c where+    {-# MINIMAL liftFree, (runFree | (retract, hoist)) #-}++    liftFree :: f a -> ff f a+    runFree :: (c g) => (forall x. f x -> g x) -> ff f a -> g a+    retract :: (c f) => ff f a -> f a+    hoist :: (forall x. f x -> g x) -> ff f a -> ff g a++    runFree f = retract . hoist f+    retract = runFree id++    default hoist :: (c (ff g)) => (forall x. f x -> g x) -> ff f a -> ff g a+    hoist phi = runFree $ liftFree . phi++    {-# INLINE runFree #-}+    {-# INLINE retract #-}+    {-# INLINE hoist #-}++convertEff+    :: forall ff gg es a c c'+     . (Free c ff, Free c' gg, forall r. c (gg r))+    => Eff ff es a+    -> Eff gg es a+convertEff = go+  where+    go :: Eff ff es ~> Eff gg es+    go = Eff . hoist (hfmapUnion go) . convertFree . unEff+{-# INLINE convertEff #-}++convertFree :: (Free c ff, Free c' gg, c (gg r)) => ff r a -> gg r a+convertFree = runFree liftFree+{-# INLINE convertFree #-}++deriving instance (forall f. Functor (ff f)) => Functor (Eff ff es)+deriving instance (forall r. Applicative (ff r)) => Applicative (Eff ff es)+deriving instance (forall r. Monad (ff r)) => Monad (Eff ff es)++instance Free Functor Coyoneda where+    liftFree = liftCoyoneda+    runFree f (Coyoneda g x) = g <$> f x+    retract = lowerCoyoneda+    hoist = hoistCoyoneda++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE retract #-}+    {-# INLINE hoist #-}++instance Free Applicative Tree.Ap where+    liftFree = Tree.liftAp+    runFree = Tree.runAp+    retract = Tree.retractAp+    hoist = Tree.hoistAp++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE retract #-}+    {-# INLINE hoist #-}++instance Free Applicative Fast.Ap where+    liftFree = Fast.liftAp+    runFree = Fast.runAp+    retract = Fast.retractAp+    hoist = Fast.hoistAp++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE retract #-}+    {-# INLINE hoist #-}++instance Free Applicative Final.Ap where+    liftFree = Final.liftAp+    runFree = Final.runAp+    retract = Final.retractAp+    hoist = Final.hoistAp++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE retract #-}+    {-# INLINE hoist #-}++instance Free Alternative Tree.Alt where+    liftFree = Tree.liftAlt+    runFree = Tree.runAlt+    hoist = Tree.hoistAlt++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE hoist #-}++instance Free Alternative Final.Alt where+    liftFree = Final.liftAlt+    runFree = Final.runAlt+    hoist = Final.hoistAlt++    {-# INLINE liftFree #-}+    {-# INLINE runFree #-}+    {-# INLINE hoist #-}

@@ -0,0 +1,197 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Avoid lambda" #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2025 Sayo contributors+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+-}+module Control.Effect.Interpret where++import Control.Effect (+    Eff (..),+    Free (liftFree),+    hoist,+    runFree,+    type (~>),+    type (~~>),+ )+import Data.Effect (Emb, getEmb)+import Data.Effect.OpenUnion (+    Has,+    In,+    KnownLength,+    KnownOrder,+    Membership,+    Suffix,+    Union,+    hfmapUnion,+    identityMembership,+    keyMembership,+    labelMembership,+    nil,+    project,+    weakens,+    (!++),+    (!:),+    (:>),+    type (++),+ )+import Data.Effect.Tag (unTag)+import Data.Functor.Identity (Identity, runIdentity)++runEff :: (Free c ff, c f) => Eff ff '[Emb f] a -> f a+runEff = runFree (getEmb !: nil) . unEff+{-# INLINE runEff #-}++runPure :: (Free c ff, c Identity) => Eff ff '[] a -> a+runPure = runIdentity . runFree nil . unEff+{-# INLINE runPure #-}++interpret+    :: forall e es ff a c+     . (KnownOrder e, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff (e ': es) a+    -> Eff ff es a+interpret i = interpretAll $ i !: Eff . liftFree+{-# INLINE interpret #-}++reinterpret+    :: forall e es es' ff a c+     . (Suffix es es', KnownOrder e, Free c ff)+    => e ~~> Eff ff es'+    -> Eff ff (e ': es) a+    -> Eff ff es' a+reinterpret i = interpretAll $ i !: Eff . liftFree . weakens+{-# INLINE reinterpret #-}++interprets+    :: forall es r ff a c+     . (KnownLength es, Free c ff)+    => Union es ~~> Eff ff r+    -> Eff ff (es ++ r) a+    -> Eff ff r a+interprets i = interpretAll $ i !++ Eff . liftFree+{-# INLINE interprets #-}++reinterprets+    :: forall es r r' ff a c+     . (Suffix r r', KnownLength es, Free c ff)+    => (Union es (Eff ff r') ~> Eff ff r')+    -> Eff ff (es ++ r) a+    -> Eff ff r' a+reinterprets i = interpretAll $ i !++ Eff . liftFree . weakens @r+{-# INLINE reinterprets #-}++interpose+    :: forall e es ff a c+     . (e :> es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+interpose = interposeFor labelMembership+{-# INLINE interpose #-}++interposeOn+    :: forall key e es ff a c+     . (Has key e es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+interposeOn f = interposeFor (keyMembership @key) (f . unTag)+{-# INLINE interposeOn #-}++interposeIn+    :: forall e es ff a c+     . (e `In` es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+interposeIn = interposeFor identityMembership+{-# INLINE interposeIn #-}++interposeFor+    :: forall e es ff a c+     . (KnownOrder e, Free c ff)+    => Membership e es+    -> e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+interposeFor i f =+    interpretAll \u ->+        case project i u of+            Just e -> f e+            Nothing -> Eff $ liftFree u+{-# INLINE interposeFor #-}++preinterpose+    :: forall e es ff a c+     . (e :> es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+preinterpose = preinterposeFor labelMembership+{-# INLINE preinterpose #-}++preinterposeOn+    :: forall key e es ff a c+     . (Has key e es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+preinterposeOn f = preinterposeFor (keyMembership @key) (f . unTag)+{-# INLINE preinterposeOn #-}++preinterposeIn+    :: forall e es ff a c+     . (e `In` es, Free c ff)+    => e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+preinterposeIn = preinterposeFor identityMembership+{-# INLINE preinterposeIn #-}++preinterposeFor+    :: forall e es ff a c+     . (KnownOrder e, Free c ff)+    => Membership e es+    -> e ~~> Eff ff es+    -> Eff ff es a+    -> Eff ff es a+preinterposeFor i f = go+  where+    go :: Eff ff es ~> Eff ff es+    go (Eff a) = Eff $ (`runFree` a) \u ->+        hoist (hfmapUnion go) $ case project i u of+            Just e -> unEff $ f e+            Nothing -> liftFree u+{-# INLINE preinterposeFor #-}++interpretAll+    :: forall es es' ff a c+     . (Free c ff)+    => (Union es ~~> Eff ff es')+    -> Eff ff es a+    -> Eff ff es' a+interpretAll i = go+  where+    go :: Eff ff es ~> Eff ff es'+    go = Eff . runFree (unEff . i . hfmapUnion go) . unEff+{-# INLINE interpretAll #-}++iterAllEff+    :: forall es f ff a c+     . (Free c ff, c f)+    => Union es ~~> f+    -> Eff ff es a+    -> f a+iterAllEff i = go+  where+    go :: Eff ff es ~> f+    go = runFree (i . hfmapUnion go) . unEff+{-# INLINE iterAllEff #-}

@@ -1,66 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}---- 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 Sayo Koyoneda-License     :  MPL-2.0 (see the file LICENSE)-Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--}-module Control.Effect.Key where--import Control.Applicative (Alternative)-import Control.Effect (SendFOE (sendFOE), SendHOE (sendHOE))-import Control.Monad (MonadPlus)-import Control.Monad.Except (MonadError)-import Control.Monad.Fix (MonadFix)-import Control.Monad.IO.Class (MonadIO)-import Control.Monad.RWS (MonadRWS)-import Control.Monad.Reader (MonadReader)-import Control.Monad.State (MonadState)-import Control.Monad.Writer (MonadWriter)-import Data.Coerce (coerce)-import Data.Effect (EffectF, EffectH)-import Data.Effect.HFunctor (HFunctor, hfmap)-import Data.Kind (Type)--class SendFOEBy key (ins :: EffectF) f | key f -> ins where-    sendFOEBy :: ins a -> f a--class SendHOEBy key (sig :: EffectH) f | key f -> sig where-    sendHOEBy :: sig f a -> f a---- | A wrapper data type to represent sending an effect to the carrier @f@ with the specified key.-newtype ByKey key (f :: Type -> Type) a = ByKey {runByKey :: f a}-    deriving newtype-        ( Functor-        , Applicative-        , Alternative-        , Monad-        , MonadPlus-        , MonadFix-        , MonadIO-        , MonadFail-        , MonadReader r-        , MonadWriter w-        , MonadState s-        , MonadRWS r w s-        , MonadError e-        )---- | Send all effects within the scope, keyed, to carrier @f@.-key :: forall key f a. ByKey key f a -> f a-key = runByKey-{-# INLINE key #-}--instance (SendFOEBy key ins f) => SendFOE ins (ByKey key f) where-    sendFOE = ByKey . sendFOEBy @key-    {-# INLINE sendFOE #-}--instance (SendHOEBy key sig f, HFunctor sig) => SendHOE sig (ByKey key f) where-    sendHOE = ByKey . sendHOEBy @key . hfmap coerce-    {-# INLINE sendHOE #-}

@@ -1,70 +0,0 @@-{-# 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/.--{- |-Copyright   :  (c) 2023-2024 Sayo Koyoneda-License     :  MPL-2.0 (see the file LICENSE)-Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--}-module Control.Effect.Tag where--import Control.Applicative (Alternative)-import Control.Effect (SendFOE (sendFOE), SendHOE (sendHOE))-import Control.Effect.Key (SendFOEBy, SendHOEBy, sendFOEBy, sendHOEBy)-import Control.Monad (MonadPlus)-import Control.Monad.Except (MonadError)-import Control.Monad.Fix (MonadFix)-import Control.Monad.IO.Class (MonadIO)-import Control.Monad.RWS (MonadRWS)-import Control.Monad.Reader (MonadReader)-import Control.Monad.State (MonadState)-import Control.Monad.Writer (MonadWriter)-import Data.Coerce (coerce)-import Data.Effect.HFunctor (HFunctor, hfmap)-import Data.Effect.Tag (pattern T, pattern TH, type (#), type (##))-import Data.Kind (Type)---- | A wrapper data type to represent sending an effect to the carrier @f@ with the specified tag.-newtype ViaTag tag (f :: Type -> Type) a = ViaTag {runViaTag :: f a}-    deriving newtype-        ( Functor-        , Applicative-        , Alternative-        , Monad-        , MonadPlus-        , MonadFix-        , MonadIO-        , MonadFail-        , MonadReader r-        , MonadWriter w-        , MonadState s-        , MonadRWS r w s-        , MonadError e-        )---- | Send all effects within the scope, tagged, to carrier @f@.-tag :: forall tag f a. ViaTag tag f a -> f a-tag = runViaTag-{-# INLINE tag #-}--instance (SendFOE (ins # tag) f) => SendFOE ins (ViaTag tag f) where-    sendFOE = ViaTag . sendFOE . T @tag-    {-# INLINE sendFOE #-}--instance (SendHOE (sig ## tag) f, HFunctor sig) => SendHOE sig (ViaTag tag f) where-    sendHOE = ViaTag . sendHOE . TH @tag . hfmap coerce-    {-# INLINE sendHOE #-}--instance (SendFOEBy key (ins # tag) f) => SendFOEBy key ins (ViaTag tag f) where-    sendFOEBy = ViaTag . sendFOEBy @key . T @tag-    {-# INLINE sendFOEBy #-}--instance (SendHOEBy key (sig ## tag) f, HFunctor sig) => SendHOEBy key sig (ViaTag tag f) where-    sendHOEBy = ViaTag . sendHOEBy @key . TH @tag . hfmap coerce-    {-# INLINE sendHOEBy #-}

@@ -0,0 +1,215 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PatternSynonyms #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2025 Sayo contributors+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+-}+module Control.Effect.Transform where++import Control.Effect (Eff (..), Free, hoist, sendFor, type (~>))+import Control.Effect.Interpret (interposeFor, interpret, reinterpret)+import Data.Effect.OpenUnion (+    Each,+    Has,+    In,+    KnownLength,+    KnownOrder,+    Membership,+    RemoveHOEs,+    Suffix,+    SuffixUnder,+    Union,+    WeakenHOEs,+    hfmapUnion,+    identityMembership,+    inject,+    keyMembership,+    labelMembership,+    mapUnion,+    prefixFor,+    prefixFor1,+    suffixFor,+    weaken,+    weakenFor,+    weakenHOEs,+    weakens,+    weakensUnder,+    (!:),+    pattern Here,+    type (++),+    type (:>),+ )+import Data.Effect.Tag (Tagged (Tag), unTag, type (#))++raise :: forall e es a ff c. (Free c ff) => Eff ff es a -> Eff ff (e ': es) a+raise = raises+{-# INLINE raise #-}++raises :: forall es es' a ff c. (Suffix es es', Free c ff) => Eff ff es a -> Eff ff es' a+raises = transAll weakens+{-# INLINE raises #-}++raiseUnder :: forall e0 e1 es a ff c. (Free c ff) => Eff ff (e0 ': es) a -> Eff ff (e0 ': e1 ': es) a+raiseUnder = raisesUnder+{-# INLINE raiseUnder #-}++raisesUnder :: forall e es es' a ff c. (Suffix es es', Free c ff) => Eff ff (e ': es) a -> Eff ff (e ': es') a+raisesUnder = transAll weakensUnder+{-# INLINE raisesUnder #-}++raisesUnders :: forall es es' a ff c. (SuffixUnder es es', Free c ff) => Eff ff es a -> Eff ff es' a+raisesUnders = transAll weakensUnder+{-# INLINE raisesUnders #-}++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 #-}++raisePrefix+    :: forall es' es a ff c+     . (KnownLength es', Free c ff)+    => Eff ff es a+    -> Eff ff (es' ++ es) a+raisePrefix = transAll $ mapUnion $ prefixFor @es'+{-# INLINE raisePrefix #-}++raiseSuffix+    :: forall es' es a ff c+     . (Free c ff)+    => Eff ff es a+    -> Eff ff (es ++ es') a+raiseSuffix = transAll $ mapUnion $ suffixFor @es'+{-# INLINE raiseSuffix #-}++raisePrefix1+    :: forall fs x es a ff c+     . (KnownLength fs, Free c ff)+    => Eff ff es a+    -> Eff ff (Each fs x ++ es) a+raisePrefix1 = transAll $ mapUnion $ prefixFor1 @fs @x+{-# INLINE raisePrefix1 #-}++subsume :: forall e es a ff c. (e `In` es, Free c ff) => Eff ff (e ': es) a -> Eff ff es a+subsume = transAll $ inject identityMembership !: id+{-# INLINE subsume #-}++subsumeUnder :: forall e1 e0 es a ff c. (e1 `In` es, KnownOrder e0, Free c ff) => Eff ff (e0 ': e1 ': es) a -> Eff ff (e0 ': es) a+subsumeUnder = transAll $ inject Here !: inject (weakenFor identityMembership) !: weaken+{-# INLINE subsumeUnder #-}++-- todo: generalize subsume by type-class++transform+    :: forall e e' es a ff c+     . (KnownOrder e, KnownOrder e', Free c ff)+    => (e (Eff ff (e' ': es)) ~> e' (Eff ff (e' ': es)))+    -> Eff ff (e ': es) a+    -> Eff ff (e' ': es) a+transform f = reinterpret $ sendFor Here . f+{-# INLINE transform #-}++translate+    :: forall e e' es a ff c+     . (KnownOrder e, e' :> es, Free c ff)+    => (e (Eff ff es) ~> e' (Eff ff es))+    -> Eff ff (e ': es) a+    -> Eff ff es a+translate = translateFor labelMembership+{-# INLINE translate #-}++translateOn+    :: forall key e e' es a ff c+     . (KnownOrder e, Has key e' es, Free c ff)+    => (e (Eff ff es) ~> e' (Eff ff es))+    -> Eff ff (e ': es) a+    -> Eff ff es a+translateOn f = translateFor (keyMembership @key) (Tag . f)+{-# INLINE translateOn #-}++translateIn+    :: forall e e' es a ff c+     . (KnownOrder e, e' `In` es, Free c ff)+    => (e (Eff ff es) ~> e' (Eff ff es))+    -> Eff ff (e ': es) a+    -> Eff ff es a+translateIn = translateFor identityMembership+{-# INLINE translateIn #-}++translateFor+    :: forall e e' es a ff c+     . (KnownOrder e, KnownOrder e', Free c ff)+    => Membership e' es+    -> (e (Eff ff es) ~> e' (Eff ff es))+    -> Eff ff (e ': es) a+    -> Eff ff es a+translateFor i f = interpret $ sendFor i . f+{-# INLINE translateFor #-}++rewrite+    :: forall e es a ff c+     . (e :> es, Free c ff)+    => (e (Eff ff es) ~> e (Eff ff es))+    -> Eff ff es a+    -> Eff ff es a+rewrite = rewriteFor labelMembership+{-# INLINE rewrite #-}++rewriteOn+    :: forall key e es a ff c+     . (Has key e es, Free c ff)+    => (e (Eff ff es) ~> e (Eff ff es))+    -> Eff ff es a+    -> Eff ff es a+rewriteOn f = rewriteFor (keyMembership @key) (Tag . f . unTag)+{-# INLINE rewriteOn #-}++rewriteIn+    :: forall e es a ff c+     . (e `In` es, Free c ff)+    => (e (Eff ff es) ~> e (Eff ff es))+    -> Eff ff es a+    -> Eff ff es a+rewriteIn = rewriteFor identityMembership+{-# INLINE rewriteIn #-}++rewriteFor+    :: forall e es a ff c+     . (KnownOrder e, Free c ff)+    => Membership e es+    -> (e (Eff ff es) ~> e (Eff ff es))+    -> Eff ff es a+    -> Eff ff es a+rewriteFor i f = interposeFor i (sendFor i . f)+{-# INLINE rewriteFor #-}++transAll+    :: forall es es' ff a c+     . (Free c ff)+    => (Union es (Eff ff es') ~> Union es' (Eff ff es'))+    -> Eff ff es a+    -> Eff ff es' a+transAll f = go+  where+    go :: Eff ff es ~> Eff ff es'+    go (Eff a) = Eff $ hoist (f . hfmapUnion go) a+{-# INLINE transAll #-}++tag+    :: forall tag e es a ff c+     . (KnownOrder e, KnownOrder (e # tag), Free c ff)+    => Eff ff (e ': es) a+    -> Eff ff (e # tag ': es) a+tag = transform Tag+{-# INLINE tag #-}++untag+    :: forall tag e es a ff c+     . (KnownOrder e, KnownOrder (e # tag), Free c ff)+    => Eff ff (e # tag ': es) a+    -> Eff ff (e ': es) a+untag = transform unTag+{-# INLINE untag #-}

@@ -1,40 +1,298 @@--- 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/.+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE QuantifiedConstraints #-} +-- SPDX-License-Identifier: MPL-2.0+ {- |-Copyright   :  (c) 2023-2024 Sayo Koyoneda-               (c) 2023 Casper Bach Poulsen and Cas van der Rest+Copyright   :  (c) 2023-2024 Sayo contributors License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable -} module Data.Effect where +import Data.Coerce (Coercible, coerce) import Data.Effect.HFunctor (HFunctor, hfmap) import Data.Kind (Type) --- | The kind of first-order effects.-type EffectF = Type -> Type+-- | The kind for effects.+type Effect = (Type -> Type) -> Type -> Type --- | The kind of higher-order effects.-type EffectH = (Type -> Type) -> Type -> Type+-- | An order of effect.+data EffectOrder = FirstOrder | HigherOrder+    deriving (Show, Eq, Ord) -{- | Lift first-order effects to higher-order effects.+type family OrderOf (e :: Effect) :: EffectOrder -     Come from [heft-lang\/POPL2023\/haskell\/src\/Elab.hs]-    (https://github.com/heft-lang/POPL2023/blob/74afe1d5ce0b491cffe40cc5c73a2a5ee6a94d9c/haskell/src/Elab.hs#L9-L10).+type family OrderCase (e :: EffectOrder) a b where+    OrderCase 'FirstOrder a b = a+    OrderCase 'HigherOrder a b = b++type family LabelOf (e :: Effect)++class+    ( OrderOf e ~ 'FirstOrder+    , forall f g a. Coercible (e f a) (e g a)+    ) =>+    FirstOrder (e :: Effect)++-- * Nop Effect++-- | A effect with no operations.+data Nop :: Effect+    deriving anyclass (FirstOrder)++data NopLabel+type instance LabelOf Nop = NopLabel+type instance OrderOf Nop = 'FirstOrder+instance HFunctor Nop where+    hfmap _ = \case {}+    {-# INLINE hfmap #-}++-- * Embedding Effect++newtype Emb e (f :: Type -> Type) (a :: Type) = Emb {getEmb :: e a}+    deriving anyclass (FirstOrder)+    deriving newtype (Functor, Applicative, Monad, Foldable)+    deriving stock (Traversable)++data EmbLabel (e :: Type -> Type)+type instance LabelOf (Emb e) = EmbLabel e+type instance OrderOf (Emb e) = 'FirstOrder+instance HFunctor (Emb e) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++newtype Unemb e a = Unemb {getUnemb :: forall f. e f a}++-- * Reader Effects++-- | An effect that holds a value of type @r@ in the context (environment).+data Ask r :: Effect where+    -- | Obtain a value from the environment.+    Ask :: Ask r f r++data AskLabel+type instance LabelOf (Ask r) = AskLabel+type instance OrderOf (Ask r) = 'FirstOrder+instance FirstOrder (Ask r)+instance HFunctor (Ask r) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- | An effect that locally modifies the value held in the environment.+data Local r :: Effect where+    -- | Locally modifies the value held in the environment.+    Local+        :: (r -> r)+        -- ^ A function that transforms the original value to the modified value.+        -> f a+        -- ^ The local scope where the modification is applied.+        -> Local r f a++data LocalLabel+type instance LabelOf (Local r) = LocalLabel+type instance OrderOf (Local r) = 'HigherOrder+instance HFunctor (Local r) where+    hfmap phi (Local f a) = Local f (phi a)+    {-# INLINE hfmap #-}++-- * State Effect++-- | An effect for holding mutable state values in the context.+data State s :: Effect where+    -- | Retrieves the current state value from the context.+    Get :: State s f s+    -- | Overwrites the state value in the context.+    Put :: s -> State s f ()++data StateLabel+type instance LabelOf (State s) = StateLabel+type instance OrderOf (State s) = 'FirstOrder+instance FirstOrder (State s)+instance HFunctor (State s) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- * Writer Effects++-- | An effect that can accumulate values monoidally in a context.+data Tell w :: Effect where+    -- | Accumulates new values to the cumulative value held in the context.+    Tell :: w -> Tell w f ()++data TellLabel+type instance LabelOf (Tell w) = TellLabel+type instance OrderOf (Tell w) = 'FirstOrder+instance FirstOrder (Tell w)+instance HFunctor (Tell w) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- | An effect that performs local operations on accumulations in the context on a per-scope basis.+data WriterH w :: Effect where+    -- | Obtains the accumulated value in the scope and returns it together as a pair.+    Listen+        :: f a+        -- ^ The scope from which to obtain the accumulation.+        -> WriterH w f (w, a)+    -- | Modifies the accumulation in the scope based on the given function.+    Censor+        :: (w -> w)+        -- ^ A function for modifying the accumulated value.+        -> f a+        -- ^ The scope where the modification is applied.+        -> WriterH w f a++data WriterHLabel+type instance LabelOf (WriterH w) = WriterHLabel+type instance OrderOf (WriterH w) = 'HigherOrder+instance HFunctor (WriterH w) where+    hfmap phi = \case+        Listen a -> Listen $ phi a+        Censor f a -> Censor f (phi a)+    {-# INLINE hfmap #-}++-- * Exception Effects++-- | An effect to escape from the normal control structure with an exception value of type @e@ in the middle of a context.+data Throw e :: Effect where+    -- | Throws an exception; that is, escapes from the normal control structure with an exception value in the middle of a context.+    Throw :: e -> Throw e f a++data ThrowLabel+type instance LabelOf (Throw e) = ThrowLabel+type instance OrderOf (Throw e) = 'FirstOrder+instance FirstOrder (Throw e)+instance HFunctor (Throw e) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- | An effect to catch exceptions.+data Catch e :: Effect where+    -- | Catches exceptions within a scope and processes them according to the given exception handler.+    Catch+        :: f a+        -- ^ The scope in which to catch exceptions.+        -> (e -> f a)+        -- ^ Exception handler. Defines the processing to perform when an exception is thrown within the scope.+        -> Catch e f a++data CatchLabel+type instance LabelOf (Catch w) = CatchLabel+type instance OrderOf (Catch w) = 'HigherOrder+instance HFunctor (Catch w) where+    hfmap phi (Catch a hdl) = Catch (phi a) (phi . hdl)+    {-# INLINE hfmap #-}++-- * Non-Determinism Effects++-- | An effect that eliminates a branch by causing the current branch context of a non-deterministic computation to fail.+data Empty :: Effect where+    -- | Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.+    Empty :: Empty f a++data EmptyLabel+type instance LabelOf Empty = EmptyLabel+type instance OrderOf Empty = 'FirstOrder+instance FirstOrder Empty+instance HFunctor Empty where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- | An effect that splits the computation into two branches.+data Choose :: Effect where+    -- | Splits the computation into two branches.+    -- As a result of executing @choose@, the world branches into one where `False` is returned and one where `True` is returned.+    Choose :: Choose f Bool++data ChooseLabel+type instance LabelOf Choose = ChooseLabel+type instance OrderOf Choose = 'FirstOrder+instance FirstOrder Choose+instance HFunctor Choose where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++{- |+An effect that executes two branches as scopes.+A higher-order version of the t`Choose` effect. -}-newtype LiftFOE (ins :: EffectF) (f :: Type -> Type) a = LiftFOE {unliftFOE :: ins a}-    deriving stock (Functor, Foldable, Traversable)+data ChooseH :: Effect where+    -- | Executes the given two scopes as branches.+    -- Even if one fails due to the `empty` operation, the whole does not fail as long as the other does not fail.+    ChooseH :: f a -> f a -> ChooseH f a -instance HFunctor (LiftFOE ins) where-    hfmap _ (LiftFOE e) = LiftFOE e+data ChooseHLabel+type instance LabelOf ChooseH = ChooseHLabel+type instance OrderOf ChooseH = 'HigherOrder+instance HFunctor ChooseH where+    hfmap phi (ChooseH a b) = ChooseH (phi a) (phi b)     {-# INLINE hfmap #-} --- | A first-order effect with no operations.-data Nop :: EffectF+-- * Fail Effect --- | A higher-order effect with no operations.-type LNop = LiftFOE Nop+data Fail :: Effect where+    Fail :: String -> Fail f a++data FailLabel+type instance LabelOf Fail = FailLabel+type instance OrderOf Fail = 'FirstOrder+instance FirstOrder Fail+instance HFunctor Fail where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- * Fix Effect++data Fix :: Effect where+    Efix :: (a -> f a) -> Fix f a++data FixLabel+type instance LabelOf Fix = FixLabel+type instance OrderOf Fix = 'HigherOrder+instance HFunctor Fix where+    hfmap phi (Efix f) = Efix $ phi . f+    {-# INLINE hfmap #-}++-- * Unlift Effect++data UnliftBase b f (a :: Type) where+    WithRunInBase :: ((forall x. f x -> b x) -> b a) -> UnliftBase b f a++type UnliftIO = UnliftBase IO++data UnliftBaseLabel (b :: Type -> Type)+type instance LabelOf (UnliftBase b) = UnliftBaseLabel b+type instance OrderOf (UnliftBase b) = 'HigherOrder+instance HFunctor (UnliftBase b) where+    hfmap phi (WithRunInBase f) = WithRunInBase \run -> f $ run . phi+    {-# INLINE hfmap #-}++-- * CallCC Effect (Sub/Jump-based)++data CC ref :: Effect where+    SubFork :: CC ref f (Either (ref a) a)+    Jump :: ref a -> a -> CC ref f b++data CCLabel+type instance LabelOf (CC ref) = CCLabel+type instance OrderOf (CC ref) = 'FirstOrder+instance FirstOrder (CC ref)+instance HFunctor (CC ref) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}++-- * Shift Effect++data Shift ans ref :: Effect where+    SubShiftFork :: Shift ans ref f (Either (ref a) a)+    Call :: ref a -> a -> Shift ans ref f ans+    Abort :: ans -> Shift ans ref f a++data ShiftLabel+type instance LabelOf (Shift ans ref) = ShiftLabel+type instance OrderOf (Shift ans ref) = 'FirstOrder+instance FirstOrder (Shift ans ref)+instance HFunctor (Shift ans ref) where+    hfmap _ = coerce+    {-# INLINE hfmap #-}

@@ -1,46 +1,13 @@--- 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/.+-- SPDX-License-Identifier: MPL-2.0  {- |-Copyright   :  (c) 2023 Sayo Koyoneda-License     :  MPL-2.0 (see the file LICENSE)+Copyright   :  (c) 2025 Sayo contributors+License     :  MPL-2.0 (see the LICENSE file) Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--This module re-exports the `HFunctor` type class and related definitions from the `compdata`-package. For more details, please refer to the-    [`compdata` documentation](https://hackage.haskell.org/package/compdata-0.13.0/docs/Data-Comp-Multi-HFunctor.html). -}-module Data.Effect.HFunctor (-    HFunctor (..),-    RemA (..),-    DistAnn (..),-    (:&:) (..),-    (:=:),-    (:<:),-    Subsume (..),-    Elem,-    (:+:) (..),-    caseH,-    inj,-    proj,-    spl,-) where+module Data.Effect.HFunctor where -import Data.Comp.Multi.HFunctor (HFunctor (hfmap))-import Data.Comp.Multi.Ops (-    DistAnn (injectA, projectA),-    Elem,-    RemA (remA),-    Subsume (..),-    caseH,-    inj,-    proj,-    spl,-    type (:&:) ((:&:)),-    type (:+:) (Inl, Inr),-    type (:<:),-    type (:=:),- )+import Data.Kind (Type)++class HFunctor (ff :: (Type -> Type) -> Type -> Type) where+    hfmap :: (forall x. f x -> g x) -> ff f a -> ff g a

@@ -1,25 +1,24 @@ {-# 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/.+-- SPDX-License-Identifier: MPL-2.0  {- |-Copyright   :  (c) 2024 Sayo Koyoneda+Copyright   :  (c) 2024 Sayo contributors License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable -} module Data.Effect.HFunctor.HCont where  import Control.Effect (type (~>))+import Data.Effect (EffectOrder (HigherOrder), OrderOf) import Data.Effect.HFunctor (HFunctor, hfmap) import Data.Kind (Type)  -- | This represents that the effect @ff@ is finally interpreted as the base carrier @b@. newtype HCont ff b f (a :: Type) = HCont {unHCont :: (f ~> b) -> ff b a}     deriving stock (Functor)++type instance OrderOf (HCont ff b) = 'HigherOrder  instance HFunctor (HCont ff g) where     hfmap phi (HCont f) = HCont \k -> f $ k . phi

@@ -1,48 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}---- 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 Sayo Koyoneda-License     :  MPL-2.0 (see the file LICENSE)-Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable--}-module Data.Effect.Key where--import Data.Comp.Multi.HFunctor (HFunctor)-import Data.Effect (EffectF, EffectH)---- | Keyed first-order effect.-newtype Key key (ins :: EffectF) a = Key {unKey :: ins a}-    deriving stock (Functor, Foldable, Traversable)---- | Keyed first-order effect.-type (#>) = Key--infixr 7 #>---- | Keyed first-order effect.-pattern K :: forall key ins a. ins a -> Key key ins a-pattern K e = Key e--{-# COMPLETE K #-}---- | Keyed higher-order effect.-newtype KeyH key (sig :: EffectH) f a = KeyH {unKeyH :: sig f a}-    deriving stock (Functor, Foldable, Traversable)-    deriving newtype (HFunctor)---- | Keyed higher-order effect.-type (##>) = KeyH--infixr 7 ##>---- | Keyed higher-order effect.-pattern KH :: forall key sig f a. sig f a -> KeyH key sig f a-pattern KH e = KeyH e--{-# COMPLETE KH #-}

@@ -0,0 +1,564 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++-- SPDX-License-Identifier: MPL-2.0++{- |+Copyright   :  (c) 2024-2025 Sayo contributors+License     :  MPL-2.0 (see the file LICENSE)+Maintainer  :  ymdfield@outlook.jp+-}+module Data.Effect.OpenUnion where++import Control.Arrow ((&&&))+import Data.Coerce (coerce)+import Data.Data (Proxy (Proxy), (:~:) (Refl))+import Data.Effect (Effect, EffectOrder (FirstOrder, HigherOrder), FirstOrder, LabelOf, OrderCase, OrderOf)+import Data.Effect.HFunctor (HFunctor, hfmap)+import Data.Effect.Tag (type (#))+import Data.Kind (Constraint, Type)+import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), KnownNat, Symbol, TypeError, natVal, type (+), type (-))+import Unsafe.Coerce (unsafeCoerce)++data Union (es :: [Effect]) (f :: Type -> Type) (a :: Type) where+    UnsafeUnion+        :: {-# UNPACK #-} !Int+        -- ^ A natural number tag to identify the element of the union.+        -> e g a+        -> {-# UNPACK #-} !EffectOrder+        -> (forall x. g x -> f x)+        -> Union es f a++instance HFunctor (Union es) where+    hfmap phi u@(UnsafeUnion n e order koi) =+        case order of+            FirstOrder -> unsafeCoerce u+            HigherOrder -> UnsafeUnion n e HigherOrder (phi . koi)+    {-# INLINE hfmap #-}++hfmapUnion :: (forall x. f x -> g x) -> Union es f a -> Union es g a+hfmapUnion phi u@(UnsafeUnion n e order koi) =+    case order of+        FirstOrder -> unsafeCoerce u+        HigherOrder -> UnsafeUnion n e HigherOrder (phi . koi)+{-# INLINE hfmapUnion #-}++class FOEs es+instance FOEs '[]+instance (FirstOrder e, FOEs es) => FOEs (e ': es)++coerceFOEs :: (FOEs es) => Union es f a -> Union es g a+coerceFOEs = unsafeCoerce+{-# INLINE coerceFOEs #-}++type instance OrderOf (Union es) = 'HigherOrder++newtype Membership (e :: Effect) (es :: [Effect]) = UnsafeMembership {unMembership :: Int}+    deriving stock (Eq, Show)++pattern Here :: Membership e (e ': es)+pattern Here = UnsafeMembership 0+{-# INLINE Here #-}++pattern There :: Membership e es -> Membership e (e ': es)+pattern There i <- ((UnsafeMembership . (`subtract` 1) &&& (/= 0)) . unMembership -> (i, True))+    where+        There (UnsafeMembership n) = UnsafeMembership (n + 1)+{-# INLINE There #-}++{-# COMPLETE Here, There #-}++weakenFor :: Membership e es -> Membership e (e' ': es)+weakenFor (UnsafeMembership n) = UnsafeMembership $ n + 1+{-# INLINE weakenFor #-}++mapUnion+    :: forall es es' f a+     . (forall e. Membership e es -> Membership e es')+    -> Union es f a+    -> Union es' f a+mapUnion f (UnsafeUnion n e order koi) =+    UnsafeUnion (unMembership $ f $ UnsafeMembership n) e order koi+{-# INLINE mapUnion #-}++membershipAt :: forall i es. (KnownNat i) => Membership (At i es) es+membershipAt = UnsafeMembership $ intVal @i+{-# INLINE membershipAt #-}++compareMembership :: Membership e es -> Membership e' es -> Maybe (e :~: e')+compareMembership (UnsafeMembership m) (UnsafeMembership n)+    | m == n = Just $ unsafeCoerce Refl+    | otherwise = Nothing++type family At i es where+    At 0 (e ': es) = e+    At n (e ': es) = At (n - 1) es+    At _ '[] = TypeError ('Text "Effect index out of range")++intVal :: forall n. (KnownNat n) => Int+intVal = fromIntegral $ natVal @n Proxy+{-# INLINE intVal #-}++data LabelResolver+data KeyResolver+data IdentityResolver++data KeyDiscriminator key+data NoKeyDiscriminator++data IdentityDiscriminator (e :: Effect)++type family Discriminator resolver (e :: Effect)+type instance Discriminator LabelResolver e = LabelOf e+type instance Discriminator KeyResolver e = KeyOf e+type instance Discriminator IdentityResolver e = IdentityDiscriminator e++type family KeyOf e where+    KeyOf (e # key) = KeyDiscriminator key+    KeyOf e = NoKeyDiscriminator++type family ResolverName resolver :: Symbol+type instance ResolverName LabelResolver = "label"+type instance ResolverName KeyResolver = "key"+type instance ResolverName IdentityResolver = "identity"++infix 4 :>+infix 4 `In`++type e :> es = MemberBy LabelResolver (Discriminator LabelResolver e) e es+type Has key e es = MemberBy KeyResolver (KeyDiscriminator key) (e # key) es+type e `In` es = MemberBy IdentityResolver (IdentityDiscriminator e) e es+type KnownIndex i es = (KnownNat i, KnownOrder (At i es))++type FindByLabel label e es = MemberBy LabelResolver label e es++type MemberBy resolver dscr e es =+    ( FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es+    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf es)) e es es+    , KnownOrder e+    )++class+    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>+    FindBy resolver dscr dscr' e r+        | resolver dscr dscr' r -> e+    where+    findBy :: Membership e r++instance+    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')+    => FindBy resolver dscr dscr e (e' ': r)+    where+    findBy = Here+    {-# INLINE findBy #-}++instance+    {-# OVERLAPPABLE #-}+    ( dscr ~ Discriminator resolver e+    , dscr' ~ Discriminator resolver e'+    , FindBy resolver dscr (Discriminator resolver (HeadOf r)) e r+    )+    => FindBy resolver dscr dscr' e (e' ': r)+    where+    findBy = weakenFor $ findBy @resolver @dscr @(Discriminator resolver (HeadOf r)) @e @r+    {-# INLINE findBy #-}++membership+    :: forall resolver dscr e es+     . (FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es)+    => Membership e es+membership = findBy @resolver @dscr @(Discriminator resolver (HeadOf es)) @e @es+{-# INLINE membership #-}++labelMembership+    :: forall e es+     . (FindBy LabelResolver (LabelOf e) (LabelOf (HeadOf es)) e es)+    => Membership e es+labelMembership = membership @LabelResolver+{-# INLINE labelMembership #-}++keyMembership+    :: forall key e es+     . (FindBy KeyResolver (KeyDiscriminator key) (KeyOf (HeadOf es)) (e # key) es)+    => Membership (e # key) es+keyMembership = membership @KeyResolver+{-# INLINE keyMembership #-}++identityMembership+    :: forall e es+     . (FindBy IdentityResolver (IdentityDiscriminator e) (IdentityDiscriminator (HeadOf es)) e es)+    => Membership e es+identityMembership = membership @IdentityResolver+{-# INLINE identityMembership #-}+class+    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>+    ErrorIfNotFound resolver dscr dscr' (e :: Effect) (r :: [Effect]) (w :: [Effect])++instance+    ( TypeError+        ( 'Text "The effect ‘"+            ':<>: 'ShowType e+            ':<>: 'Text "’ does not exist within the effect list"+            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"+            ':$$: 'Text "Resolver: " ':<>: 'Text (ResolverName resolver)+            ':$$: 'Text "Discriminator: " ':<>: 'ShowType dscr+        )+    , dscr ~ Discriminator resolver e+    , dscr' ~ Discriminator resolver (HeadOf '[])+    )+    => ErrorIfNotFound resolver dscr dscr' e '[] w++instance+    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')+    => ErrorIfNotFound resolver dscr dscr e (e' ': r) w++instance+    {-# OVERLAPPABLE #-}+    ( dscr ~ Discriminator resolver e+    , dscr' ~ Discriminator resolver e'+    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf r)) e r w+    )+    => ErrorIfNotFound resolver dscr dscr' e (e' ': r) w++instance+    {-# INCOHERENT #-}+    ( dscr ~ Discriminator resolver e+    , dscr' ~ Discriminator resolver (HeadOf r)+    )+    => ErrorIfNotFound resolver dscr dscr' e r w++type family HeadOf es where+    HeadOf (e ': es) = e++type KnownOrder e = Elem e (OrderOf e)++class (order ~ OrderOf e) => Elem e order where+    inject :: Membership e es -> e f a -> Union es f a+    project :: Membership e es -> Union es f a -> Maybe (e f a)+    (!:) :: (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r+    extract :: Union '[e] f a -> e f a++    infixr 5 !:++decomp :: (KnownOrder e, HFunctor e) => Union (e ': es) f a -> Either (e f a) (Union es f a)+decomp = Left !: Right+{-# INLINE decomp #-}++instance (FirstOrder e) => Elem e 'FirstOrder where+    inject :: forall es f a. Membership e es -> e f a -> Union es f a+    inject i = mkUnion i firstOrdership++    project+        :: forall es f a+         . Membership e es+        -> Union es f a+        -> Maybe (e f a)+    project i (UnsafeUnion n e _ _) =+        if n == unMembership i+            then Just $ unsafeCoerce e+            else Nothing++    (f !: g) (UnsafeUnion n e koi order) =+        if n == 0+            then f $ unsafeCoerce e+            else g $ UnsafeUnion (n - 1) e koi order++    extract (UnsafeUnion _ e _ _) = unsafeCoerce e++    {-# INLINE inject #-}+    {-# INLINE project #-}+    {-# INLINE (!:) #-}+    {-# INLINE extract #-}++instance (OrderOf e ~ 'HigherOrder, HFunctor e) => Elem e 'HigherOrder where+    inject :: forall es f a. Membership e es -> e f a -> Union es f a+    inject i = mkUnion i (higherOrdership id)++    project :: forall es f a. Membership e es -> Union es f a -> Maybe (e f a)+    project i (UnsafeUnion n e _ koi) =+        if n == unMembership i+            then Just $ hfmap koi (unsafeCoerce e)+            else Nothing++    (f !: g) (UnsafeUnion n e _ koi) =+        if n == 0+            then f $ hfmap koi (unsafeCoerce e)+            else g $ UnsafeUnion (n - 1) e HigherOrder koi++    extract (UnsafeUnion _ e _ koi) = hfmap koi (unsafeCoerce e)++    {-# INLINE inject #-}+    {-# INLINE project #-}+    {-# INLINE (!:) #-}+    {-# INLINE extract #-}++projectAnyOrder :: forall e es f a. (HFunctor e) => Membership e es -> Union es f a -> Maybe (e f a)+projectAnyOrder i (UnsafeUnion n e order koi) =+    if n == unMembership i+        then Just $ hfmapDynUnsafeCoerce order koi e+        else Nothing++infixr 5 `caseAnyOrder`++caseAnyOrder :: (HFunctor e) => (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r+(f `caseAnyOrder` g) (UnsafeUnion n e order koi) =+    if n == 0+        then f $ hfmapDynUnsafeCoerce order koi e+        else g $ UnsafeUnion (n - 1) e order koi++extractAnyOrder :: (HFunctor e) => Union es f a -> e f a+extractAnyOrder (UnsafeUnion _ e order koi) = hfmapDynUnsafeCoerce order koi e++{-# INLINE projectAnyOrder #-}+{-# INLINE caseAnyOrder #-}+{-# INLINE extractAnyOrder #-}++hfmapDynUnsafeCoerce :: (HFunctor e') => EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a+hfmapDynUnsafeCoerce order phi e = case order of+    FirstOrder -> unsafeCoerce e+    HigherOrder -> hfmap phi (unsafeCoerce e)+{-# INLINE hfmapDynUnsafeCoerce #-}++nil :: Union '[] f a -> r+nil _ = error "Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."++nilMembership :: Membership e '[] -> r+nilMembership _ = error "Effect system internal error: nil - An empty effect union membership, which should not be possible to create, has been created."++weakensFor :: forall es es' e. (Suffix es es') => Membership e es -> Membership e es'+weakensFor (UnsafeMembership n) = UnsafeMembership $ n + prefixLen @es @es'+{-# INLINE weakensFor #-}++class Suffix (es :: [Effect]) (es' :: [Effect]) where+    prefixLen :: Int++instance Suffix es es where+    prefixLen = 0+    {-# INLINE prefixLen #-}++instance {-# INCOHERENT #-} (Suffix es es') => Suffix es (e ': es') where+    prefixLen = prefixLen @es @es' + 1+    {-# INLINE prefixLen #-}++class SuffixUnder (es :: [Effect]) (es' :: [Effect]) where+    prefixLenUnder :: Int+    offset :: Int++instance (Suffix es es') => SuffixUnder es es' where+    prefixLenUnder = prefixLen @es @es'+    offset = 0++    {-# INLINE prefixLenUnder #-}+    {-# INLINE offset #-}++instance {-# INCOHERENT #-} (SuffixUnder es es') => SuffixUnder (e ': es) (e ': es') where+    prefixLenUnder = prefixLenUnder @es @es'+    offset = offset @es @es' + 1++    {-# INLINE prefixLenUnder #-}+    {-# INLINE offset #-}++weakensUnderFor :: forall es es' e. (SuffixUnder es es') => Membership e es -> Membership e es'+weakensUnderFor (UnsafeMembership n) =+    UnsafeMembership+        if n < offset @es @es'+            then n+            else n + prefixLenUnder @es @es'+{-# INLINE weakensUnderFor #-}++type family RemoveHOEs (es :: [Effect]) where+    RemoveHOEs '[] = '[]+    RemoveHOEs (e ': es) =+        OrderCase (OrderOf e) (e ': RemoveHOEs es) (RemoveHOEs es)++type WeakenHOEs es = (WeakenHOEs_ es 0 (OrderOf (HeadOf es)), FOEs (RemoveHOEs es))++class (orderOfHead ~ OrderOf (HeadOf es)) => WeakenHOEs_ es countF orderOfHead where+    -- | Example for '[H,F,F,H,H,F,H,F]+    --+    -- +----+-------+--------+----------------------++    -- | ix | order | countF | shifter accumulation |+    -- +====+=======+========+======================++    -- |  0 |     H |      0 | 01234... -> 12345... |+    -- |  1 |     F |      0 | 01234... -> 12345... |+    -- |  2 |     F |      1 | 01234... -> 12345... |+    -- |  3 |     H |      2 | 01234... -> 12456... |+    -- |  4 |     H |      2 | 01234... -> 12567... |+    -- |  5 |     F |      2 | 01234... -> 12567... |+    -- |  6 |     H |      3 | 01234... -> 12578... |+    -- |  7 |     F |      3 | 01234... -> 12578... |+    -- +----+-------+--------+----------------------++    foldHoeIndexShifter :: (Int -> Int) -> (Int -> Int)++instance (OrderOf (HeadOf '[]) ~ orderOfHead) => WeakenHOEs_ '[] countF orderOfHead where+    foldHoeIndexShifter = id+    {-# INLINE foldHoeIndexShifter #-}++instance (FirstOrder e, WeakenHOEs_ es (countF + 1) _orderOfHead) => WeakenHOEs_ (e ': es) countF 'FirstOrder where+    foldHoeIndexShifter = foldHoeIndexShifter @es @(countF + 1)+    {-# INLINE foldHoeIndexShifter #-}++instance+    (OrderOf e ~ 'HigherOrder, WeakenHOEs_ es countF _orderOfHead, KnownNat countF)+    => WeakenHOEs_ (e ': es) countF 'HigherOrder+    where+    foldHoeIndexShifter shifterAcc =+        foldHoeIndexShifter @es @countF \ix ->+            let shiftedIx = shifterAcc ix+             in if ix < intVal @countF+                    then shiftedIx+                    else shiftedIx + 1+    {-# INLINE foldHoeIndexShifter #-}++weaken :: Union es f a -> Union (e ': es) f a+weaken = mapUnion weakenFor+{-# INLINE weaken #-}++weakens :: (Suffix es es') => Union es f a -> Union es' f a+weakens = mapUnion weakensFor+{-# INLINE weakens #-}++weakensUnder :: (SuffixUnder es es') => Union es f a -> Union es' f a+weakensUnder = mapUnion weakensUnderFor+{-# INLINE weakensUnder #-}++weakenHOEsFor :: forall es e. (WeakenHOEs es) => Membership e (RemoveHOEs es) -> Membership e es+weakenHOEsFor = UnsafeMembership . foldHoeIndexShifter @es @0 id . unMembership+{-# INLINE weakenHOEsFor #-}++weakenHOEs :: forall es f a. (WeakenHOEs es) => Union (RemoveHOEs es) f a -> Union es f a+weakenHOEs = mapUnion weakenHOEsFor+{-# INLINE weakenHOEs #-}++type KnownLength :: forall {k}. [k] -> Constraint+class KnownLength xs where+    reifyLength :: Int++instance KnownLength '[] where+    reifyLength = 0+    {-# INLINE reifyLength #-}++instance (KnownLength xs) => KnownLength (x ': xs) where+    reifyLength = 1 + reifyLength @xs+    {-# INLINE reifyLength #-}++infixr 5 ++++type family (es :: [Effect]) ++ (es' :: [Effect]) where+    '[] ++ es = es+    (e ': es) ++ es' = e ': (es ++ es')++infixr 5 !++++(!++) :: forall es es' f a r. (KnownLength es) => (Union es f a -> r) -> (Union es' f a -> r) -> Union (es ++ es') f a -> r+(h !++ h') (UnsafeUnion n e o koi) =+    if n < reifyLength @es+        then h $ UnsafeUnion n e o koi+        else h' $ UnsafeUnion (n - reifyLength @es) e o koi+{-# INLINE (!++) #-}++bundleUnion+    :: forall es es' f a+     . (KnownLength es)+    => Union (es ++ es') f a+    -> Union (Union es ': es') f a+bundleUnion = union \i o e ->+    splitFor @es @es'+        (\j -> mkUnion Here (higherOrdership id) (mkUnion j o e))+        (\j -> mkUnion (weakenFor j) o e)+        i+{-# INLINE bundleUnion #-}++unbundleUnion+    :: forall es es' f a+     . (KnownLength es)+    => Union (Union es ': es') f a+    -> Union (es ++ es') f a+unbundleUnion = mapUnion (suffixFor @es') !: mapUnion (prefixFor @es)+{-# INLINE unbundleUnion #-}++splitUnion+    :: forall es es' es'' f a+     . (KnownLength es)+    => (forall e. Membership e es -> Membership e es'')+    -> (forall e. Membership e es' -> Membership e es'')+    -> Union (es ++ es') f a+    -> Union es'' f a+splitUnion injL injR = mapUnion $ splitFor @es @es' injL injR+{-# INLINE splitUnion #-}++mergeUnion+    :: forall es es' f a+     . (KnownLength es)+    => Either (Union es f a) (Union es' f a)+    -> Union (es ++ es') f a+mergeUnion = \case+    Left u -> mapUnion (suffixFor @es') u+    Right u -> mapUnion (prefixFor @es) u+{-# INLINE mergeUnion #-}++splitFor+    :: forall es es' e r+     . (KnownLength es)+    => (Membership e es -> r)+    -> (Membership e es' -> r)+    -> Membership e (es ++ es')+    -> r+splitFor f g (UnsafeMembership n)+    | n < l = f $ UnsafeMembership n+    | otherwise = g $ UnsafeMembership $ n - l+  where+    l = reifyLength @es+{-# INLINE splitFor #-}++suffixFor :: forall es' es e. Membership e es -> Membership e (es ++ es')+suffixFor = coerce+{-# INLINE suffixFor #-}++prefixFor :: forall es' es e. (KnownLength es') => Membership e es -> Membership e (es' ++ es)+prefixFor (UnsafeMembership n) = UnsafeMembership $ reifyLength @es' + n+{-# INLINE prefixFor #-}++type family Each (fs :: [k -> Effect]) x where+    Each (f ': fs) x = (f x ': Each fs x)+    Each '[] x = '[]++prefixFor1 :: forall fs x es e. (KnownLength fs) => Membership e es -> Membership e (Each fs x ++ es)+prefixFor1 (UnsafeMembership n) = UnsafeMembership $ reifyLength @fs + n+{-# INLINE prefixFor1 #-}++data Ordership (o :: EffectOrder) (e :: Effect) (f :: Type -> Type) (g :: Type -> Type) where+    UnsafeFirst :: Ordership 'FirstOrder e f g+    UnsafeHigher :: (forall x. g x -> f x) -> Ordership 'HigherOrder e f g++union :: (forall e o g. Membership e es -> Ordership o e f g -> e g a -> r) -> Union es f a -> r+union f (UnsafeUnion n e o koi) =+    let i = UnsafeMembership n+     in case o of+            FirstOrder -> f i UnsafeFirst e+            HigherOrder -> f i (UnsafeHigher koi) e+{-# INLINE union #-}++mkUnion :: Membership e es -> Ordership o e f g -> e g a -> Union es f a+mkUnion (UnsafeMembership i) o e = case o of+    UnsafeFirst -> UnsafeUnion i e FirstOrder undefined+    UnsafeHigher koi -> UnsafeUnion i e HigherOrder koi+{-# INLINE mkUnion #-}++firstOrdership :: (FirstOrder e) => Ordership 'FirstOrder e f g+firstOrdership = UnsafeFirst+{-# INLINE firstOrdership #-}++higherOrdership :: (OrderOf e ~ 'HigherOrder) => (forall x. g x -> f x) -> Ordership 'HigherOrder e f g+higherOrdership = UnsafeHigher+{-# INLINE higherOrdership #-}++shrinkOrdership :: Ordership o e f g -> Ordership (OrderOf e) e f g+shrinkOrdership = unsafeCoerce++continuationOfInterpretation :: Ordership 'HigherOrder e f g -> (forall x. g x -> f x)+continuationOfInterpretation (UnsafeHigher koi) = koi+{-# INLINE continuationOfInterpretation #-}

@@ -1,48 +1,28 @@-{-# LANGUAGE PatternSynonyms #-}---- 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/.+-- SPDX-License-Identifier: MPL-2.0  {- |-Copyright   :  (c) 2023-2024 Sayo Koyoneda+Copyright   :  (c) 2023-2024 Sayo contributors License     :  MPL-2.0 (see the file LICENSE) Maintainer  :  ymdfield@outlook.jp-Stability   :  experimental-Portability :  portable -} module Data.Effect.Tag where -import Data.Comp.Multi.HFunctor (HFunctor)-import Data.Effect (EffectF, EffectH)---- | Tagged first-order effect.-newtype Tag (ins :: EffectF) tag a = Tag {unTag :: ins a}-    deriving stock (Functor, Foldable, Traversable)---- | Tagged first-order effect.-type (#) = Tag--infixl 8 #---- | Tagged first-order effect.-pattern T :: forall tag ins a. ins a -> Tag ins tag a-pattern T e = Tag e--{-# COMPLETE T #-}+import Data.Effect (Effect, FirstOrder, LabelOf, OrderOf)+import Data.Effect.HFunctor (HFunctor)+import Data.Kind (Type) --- | Tagged higher-order effect.-newtype TagH (sig :: EffectH) tag f a = TagH {unTagH :: sig f a}+-- | Tagged effect.+newtype Tagged tag (e :: Effect) f a = Tag {unTag :: e f a}     deriving stock (Functor, Foldable, Traversable)     deriving newtype (HFunctor) --- | Tagged higher-order effect.-type (##) = TagH+type instance OrderOf (Tagged tag e) = OrderOf e+instance (FirstOrder e) => FirstOrder (Tagged tag e) -infixl 8 ##+type instance LabelOf (Tagged tag e) = TaggedLabel tag (LabelOf e)+data TaggedLabel tag (label :: Type) --- | Tagged higher-order effect.-pattern TH :: forall tag sig f a. sig f a -> TagH sig tag f a-pattern TH e = TagH e+-- | Tagged effect.+type e # tag = Tagged tag e -{-# COMPLETE TH #-}+infixl 7 #

@@ -0,0 +1,69 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_GHC -fconstraint-solver-iterations=16 #-}++-- SPDX-License-Identifier: MPL-2.0++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.Proxy (Proxy (Proxy))+import GHC.TypeNats (KnownNat, Natural, natVal)+import Test.Hspec (Spec, describe, it, shouldBe)++data A x :: Effect+data ALabel+type instance LabelOf (A x) = ALabel++data B x y :: Effect+data BLabel x+type instance LabelOf (B x y) = BLabel x++spec_membership :: Spec+spec_membership = describe "Open-Union Membership" do+    it "Membership (A 0) '[B 1 2, A 0] -> 1" $+        label1 `shouldBe` UnsafeMembership 1++    it "Membership (B 5 6) '[B 1 2, B 3 4, A 1, B 5 6, A 0] -> 3" $+        label2 `shouldBe` UnsafeMembership 3++    it "Membership (B 5 ?) '[B 1 2, B 3 4, A 1, B 5 6, A 0] --infer--> ?=6" $+        infer1 labelMembership `shouldBe` 6+  where+    label1 :: Membership (A 0) '[B 1 2, A 0]+    label1 = labelMembership++    label2 :: Membership (B 5 6) '[B 1 2, B 3 4, A 1, B 5 6, A 0]+    label2 = labelMembership++    infer1 :: forall x. (KnownNat x) => Membership (B 5 x) '[B 1 2, B 3 4, A 1, B 5 6, A 0] -> Natural+    infer1 _ = natVal @x Proxy++type F = Throw ()+type H = Catch ()++spec_onlyFOEs :: Spec+spec_onlyFOEs = describe "onlyFOEs index shift" do+    it "'[<F>, F , F , F ] -> '[ H ,<F>, F , H , H , F , H , F ]" $+        shiftIx ix0 `shouldBe` UnsafeMembership 1+    it "'[ F ,<F>, F , F ] -> '[ H , F ,<F>, H , H , F , H , F ]" $+        shiftIx ix1 `shouldBe` UnsafeMembership 2+    it "'[ F , F ,<F>, F ] -> '[ H , F , F , H , H ,<F>, H , F ]" $+        shiftIx ix2 `shouldBe` UnsafeMembership 5+    it "'[ F , F , F ,<F>] -> '[ H , F , F , H , H , F , H ,<F>]" $+        shiftIx ix3 `shouldBe` UnsafeMembership 7+  where+    shiftIx :: Membership e '[F, F, F, F] -> Membership e '[H, F, F, H, H, F, H, F]+    shiftIx = weakenHOEsFor++    ix0, ix1, ix2, ix3 :: Membership F '[F, F, F, F]+    ix0 = membershipAt @0+    ix1 = membershipAt @1+    ix2 = membershipAt @2+    ix3 = membershipAt @3++inferCompileTest :: (Throw () :> es, Catch () :> es, Free Monad ff) => Eff ff es a+inferCompileTest = perform $ Throw mempty