This "direct style" approach to defining effects seems simpler than the one in the "Defining effects section". It avoids the GADT whose only purpose is to provide "hooks" onto which to hang the effectful operations. Instead, why not just define the effectful operations directly?
What do you think? Is this a viable approach?
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
import Cleff
import Cleff.Fail (Fail)
import Cleff.State (State, gets, modify)
import Data.Kind (Type)
import Data.Map (Map, lookup, insert)
import Prelude hiding (lookup)
-- Direct encoding of the effects we want in our filesystem
data Filesystem m = MkFilesystem
{ readFileFS :: FilePath -> m String,
writeFileFS :: FilePath -> String -> m ()
}
-- A type class for such direct-style effects
class EffectDirect (e :: (Type -> Type) -> Type) where
fmapEffect :: (m ~> n) -> e m -> e n
-- Instance for the filesystem effect
instance EffectDirect Filesystem where
fmapEffect f MkFilesystem {readFileFS = r, writeFileFS = w} =
MkFilesystem {readFileFS = f . r, writeFileFS = \s -> f . w s}
-- Adapt direct effects for the existing cleff type-level encoding
data Direct f (m :: Type -> Type) (a :: Type) = Direct (f m -> m a)
-- Direct version of send
sendDirect ::
(Direct f :> es) => (f (Eff es) -> Eff es a) -> Eff es a
sendDirect = send . Direct
-- Define the effectful operations using sendDirect
readFile' ::
Direct Filesystem :> es => FilePath -> Eff es String
readFile' x = sendDirect (\f -> readFileFS f x)
writeFile' ::
Direct Filesystem :> es => FilePath -> String -> Eff es ()
writeFile' x y = sendDirect (\f -> writeFileFS f x y)
-- To run in IO, just define the effects directly
runFilesystemIO ::
(IOE :> es) =>
Eff (Direct Filesystem : es) a ->
Eff es a
runFilesystemIO =
interpretDirectIO
MkFilesystem
{ readFileFS = readFile,
writeFileFS = writeFile
}
-- To run in State, just define the effects directly
filesystemToState ::
(Fail :> es) =>
Eff (Direct Filesystem : es) a ->
Eff (State (Map FilePath String) : es) a
filesystemToState =
reinterpretDirect
MkFilesystem
{ readFileFS = \path ->
gets (lookup path) >>= \case
Nothing -> fail ("File not found: " ++ show path)
Just contents -> pure contents,
writeFileFS = \path contents ->
modify (insert path contents)
}
interpretDirectIO ::
(IOE :> es, EffectDirect f) =>
f IO ->
Eff (Direct f : es) a ->
Eff es a
interpretDirectIO = interpretDirect . fmapEffect liftIO
interpretDirect ::
(EffectDirect f) =>
f (Eff es) ->
Eff (Direct f : es) a ->
Eff es a
interpretDirect p = interpret \(Direct f) ->
withFromEff (\k -> f (fmapEffect k p))
reinterpretDirect ::
(EffectDirect f) =>
f (Eff (e' : es)) ->
Eff (Direct f : es) a ->
Eff (e' : es) a
reinterpretDirect p = reinterpret \(Direct f) ->
withFromEff (\k -> f (fmapEffect k p))
This "direct style" approach to defining effects seems simpler than the one in the "Defining effects section". It avoids the GADT whose only purpose is to provide "hooks" onto which to hang the effectful operations. Instead, why not just define the effectful operations directly?
What do you think? Is this a viable approach?
{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE GHC2021 #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} import Cleff import Cleff.Fail (Fail) import Cleff.State (State, gets, modify) import Data.Kind (Type) import Data.Map (Map, lookup, insert) import Prelude hiding (lookup) -- Direct encoding of the effects we want in our filesystem data Filesystem m = MkFilesystem { readFileFS :: FilePath -> m String, writeFileFS :: FilePath -> String -> m () } -- A type class for such direct-style effects class EffectDirect (e :: (Type -> Type) -> Type) where fmapEffect :: (m ~> n) -> e m -> e n -- Instance for the filesystem effect instance EffectDirect Filesystem where fmapEffect f MkFilesystem {readFileFS = r, writeFileFS = w} = MkFilesystem {readFileFS = f . r, writeFileFS = \s -> f . w s} -- Adapt direct effects for the existing cleff type-level encoding data Direct f (m :: Type -> Type) (a :: Type) = Direct (f m -> m a) -- Direct version of send sendDirect :: (Direct f :> es) => (f (Eff es) -> Eff es a) -> Eff es a sendDirect = send . Direct -- Define the effectful operations using sendDirect readFile' :: Direct Filesystem :> es => FilePath -> Eff es String readFile' x = sendDirect (\f -> readFileFS f x) writeFile' :: Direct Filesystem :> es => FilePath -> String -> Eff es () writeFile' x y = sendDirect (\f -> writeFileFS f x y) -- To run in IO, just define the effects directly runFilesystemIO :: (IOE :> es) => Eff (Direct Filesystem : es) a -> Eff es a runFilesystemIO = interpretDirectIO MkFilesystem { readFileFS = readFile, writeFileFS = writeFile } -- To run in State, just define the effects directly filesystemToState :: (Fail :> es) => Eff (Direct Filesystem : es) a -> Eff (State (Map FilePath String) : es) a filesystemToState = reinterpretDirect MkFilesystem { readFileFS = \path -> gets (lookup path) >>= \case Nothing -> fail ("File not found: " ++ show path) Just contents -> pure contents, writeFileFS = \path contents -> modify (insert path contents) } interpretDirectIO :: (IOE :> es, EffectDirect f) => f IO -> Eff (Direct f : es) a -> Eff es a interpretDirectIO = interpretDirect . fmapEffect liftIO interpretDirect :: (EffectDirect f) => f (Eff es) -> Eff (Direct f : es) a -> Eff es a interpretDirect p = interpret \(Direct f) -> withFromEff (\k -> f (fmapEffect k p)) reinterpretDirect :: (EffectDirect f) => f (Eff (e' : es)) -> Eff (Direct f : es) a -> Eff (e' : es) a reinterpretDirect p = reinterpret \(Direct f) -> withFromEff (\k -> f (fmapEffect k p))