Any more papers/resources I can look at to get more context on the indexed monads vs effect systems comparison? Are they as composable as effects - ie. how do they solve the problems with monad transformers, etc?
I think the proposal people are making is better thought of as indexed monads and effects rather than indexed monads or effects.
Normal extensible effects looks like:
data Union :: [Type] -> Type -> Type where
...
data Free :: (Type -> Type) -> Type -> Type where
...
type Eff fs = Free (Union fs)
class Inject f fs where
inj :: f a -> Union fs a
data File :: Type -> Type where
Open :: FilePath -> File ()
Close :: FilePath -> File ()
send :: (Inject f fs) => f a -> Eff fs a
-- The inferred type would be more general
openClose :: Eff '[File] ()
openClose = do
send (Open "foo.txt")
send (Close "foo.txt")
You can then generalize this by also indexing everything:
data HList :: [Type] -> Type where
Nil :: HList '[]
(:>) :: a -> HList as -> HList (a ': as)
data Union :: HList fs -> HList is -> HList is -> Type -> Type where
...
data Free :: (is -> is -> Type -> Type) -> is -> is -> Type -> Type where
...
type Eff fs = Free (Union fs)
class Inject f i o fs is os where
inj :: f i o a -> Union fs is os a
data FileStatus = Open | Closed
data File :: FileStatus -> FileStatus -> Type -> Type where
Open :: FilePath -> File 'Closed 'Open ()
Close :: FilePath -> File 'Open 'Closed ()
send :: (Inject f i o fs is os) => f i o a -> Eff fs is os a
-- The inferred type would be more general
openClose :: Eff (File ':> 'Nil) ('Closed ':> 'Nil) ('Closed ':> Nil) ()
openClose = do
send (Open "foo.txt")
send (Close "foo.txt")
Yes, that helps a ton! So it's simply combining extensible effects with state transitions to help you be more specific about the legal ways to sequence effectful operations.
The proliferation of type params looks intimidating from a user perspective though - is there some way to make it easier on folks? Would it look nicer in a language with row polymorphism perhaps?
