[add] Sum notation of effect sets.

This commit is contained in:
Yamada Ryo 2024-10-04 07:35:26 +09:00
parent 46163053f8
commit 06eb380d0b
No known key found for this signature in database
GPG Key ID: AAE3C7A542B02DBF
7 changed files with 58 additions and 7 deletions

View File

@ -9,9 +9,17 @@ import Control.Effect.Interpreter.Heftia.ShiftReset (evalShift, runShift_)
import Control.Effect.Interpreter.Heftia.State (evalState)
import Control.Effect.Key (key)
import Control.Monad.Extra (whenM)
import Control.Monad.Hefty.Interpret (runEff)
import Control.Monad.Hefty.Transform (unkey)
import Control.Monad.Hefty.Types (Eff, send, sendN)
import Control.Monad.Hefty (
Eff,
runEff,
send,
sendN,
unkey,
type (!!),
type ($),
type (+),
type (:+:),
)
import Control.Monad.IO.Class (liftIO)
import Data.Effect.Key (type (#>))
import Data.Effect.Reader (Ask, Local, ask, local)
@ -88,7 +96,7 @@ handleShiftThenReader = do
& (evalState 0 . unkey)
& runEff
where
prog :: Eff '[Shift_, Local Int] '[Ask Int, "counter" #> State Int, IO] ()
prog :: Shift_ :+: Local Int !! Ask Int + "counter" #> State Int + IO $ ()
prog = do
k <- getCC_
env <- ask @Int

View File

@ -13,6 +13,7 @@ import Control.Effect (type (<:), type (<<:), type (~>))
import Control.Effect.Interpreter.Heftia.Reader (runReader)
import Control.Effect.Interpreter.Heftia.State (evalState)
import Control.Monad (when)
import Control.Monad.Hefty (type (+))
import Control.Monad.Hefty.Interpret (
interposeRec,
interposeRecH,
@ -27,7 +28,7 @@ import Control.Monad.Hefty.Transform (
raiseUnder,
subsume,
)
import Control.Monad.Hefty.Types (Eff, Elab, type (:!!))
import Control.Monad.Hefty.Types (Elab, type (!!), type (:!!))
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.Effect.OpenUnion.Internal.FO (type (<|))
import Data.Effect.OpenUnion.Internal.HO (HFunctors, type (<<|))
@ -187,7 +188,7 @@ limitThenSave =
& saveLogChunk
& runApp
runApp :: Eff '[LogChunk] '[FileSystem, Time, Log, IO] ~> IO
runApp :: LogChunk !! FileSystem + Time + Log + IO ~> IO
runApp =
runLogChunk
>>> runDummyFS

View File

@ -68,6 +68,7 @@ library
Data.Effect.OpenUnion.Internal
Data.Effect.OpenUnion.Internal.FO
Data.Effect.OpenUnion.Internal.HO
Data.Effect.OpenUnion.Sum
reexported-modules:
Data.Effect,

View File

@ -6,6 +6,7 @@ module Control.Monad.Hefty (
module Control.Monad.Hefty.Interpret.State,
module Control.Monad.Hefty.Transform,
module Data.Effect.OpenUnion,
module Data.Effect.HFunctor,
) where
import Control.Monad.Hefty.Interpret (
@ -134,8 +135,10 @@ import Control.Monad.Hefty.Types (
sendUnionBy,
sendUnionH,
sendUnionHBy,
type (!!),
type ($),
type ($$),
type (:!!),
)
import Data.Effect.HFunctor (HFunctor, type (:+:))
import Data.Effect.OpenUnion

View File

@ -27,6 +27,7 @@ import Data.Effect.NonDet qualified as E
import Data.Effect.OpenUnion.Internal (ElemAt)
import Data.Effect.OpenUnion.Internal.FO (MemberBy, Union, inj, inj0, injN, type (<|))
import Data.Effect.OpenUnion.Internal.HO (MemberHBy, UnionH, inj0H, injH, injNH, type (<<|))
import Data.Effect.OpenUnion.Sum (SumToRecUnionList)
import Data.Effect.Reader (Ask, Local, ask'', local'')
import Data.Effect.State (State, get'', put'')
import Data.Effect.Unlift (UnliftIO)
@ -58,6 +59,9 @@ Allows writing @eh :!! ef@ instead of @Eff eh ef@.
-}
type (:!!) = Eff
infixr 5 !!
type eh !! ef = SumToRecUnionList UnionH eh :!! SumToRecUnionList Union ef
instance Functor (Eff eh ef) where
fmap f = \case
Val x -> Val (f x)

View File

@ -10,6 +10,7 @@ module Data.Effect.OpenUnion (
module Data.Effect.OpenUnion.Internal,
module Data.Effect.OpenUnion.Internal.HO,
module Data.Effect.OpenUnion.Internal.FO,
module Data.Effect.OpenUnion.Sum,
) where
import Data.Effect.OpenUnion.Internal (
@ -121,5 +122,12 @@ import Data.Effect.OpenUnion.Internal.HO (
(!!+.),
type (<<|),
)
import Data.Effect.OpenUnion.Sum (
SumToRecUnion,
SumToRecUnionList,
U,
UL,
type (+),
)
-- TODO: add injN/prjN/move/swap/insert/rotate functions.
-- TODO: add move/swap/insert/rotate functions.

View File

@ -0,0 +1,26 @@
-- SPDX-License-Identifier: MPL-2.0
module Data.Effect.OpenUnion.Sum where
import Data.Effect (LNop, Nop)
import Data.Effect.HFunctor ((:+:))
import Data.Effect.OpenUnion.Internal.FO (Union)
import Data.Effect.OpenUnion.Internal.HO (UnionH)
import GHC.Generics qualified as G
infixr 5 +
type (+) = (G.:+:)
type U u e = SumToRecUnion u e
type UL u e = SumToRecUnionList u e
type SumToRecUnion u e = u (SumToRecUnionList u e)
type SumToRecUnionList :: forall k. ([k] -> k) -> k -> [k]
type family SumToRecUnionList u e where
SumToRecUnionList Union Nop = '[]
SumToRecUnionList Union (e + r) = e ': SumToRecUnionList Union r
SumToRecUnionList Union e = '[e]
SumToRecUnionList UnionH LNop = '[]
SumToRecUnionList UnionH (e :+: r) = e ': SumToRecUnionList UnionH r
SumToRecUnionList UnionH e = '[e]