Any ideas why the effect system may be deprecated in favour of the state machine/indexed monads system? To me, they seem to be fulfilling two different requirements: algebraic effects let us call 'operations' in an expression by writing placeholder values, track the usage of such operations in the type, and plug in the implementation afterwards. For example, we can write "print" as a placeholder, give it a "StdOut" effect type, and provide a production implementation which writes to the program's stdout, a test implementation which produces a normal String value for us to check, a remote implementation which writes to a WebSocket, etc.
The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can't close a file unless it's open, you can't read from a file unless it's open, you can't run an expression unless it closes all of its files, etc.
There's certainly overlap, but I'm not sure whether one subsumes the other.
Extensible effects arise from combining a free monad with an open union of functors. Using an indexed free monad with indexed functors instead is a generalization that provides more expressive power.
Intuitively, I like to think of it as:
- Extensible effects describe what we permit (read from console, print to console)
- Indexed monads describe what we demand (you must auth before you can access db, you must open file before you can read it)
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?
The new States library is really a new implementation of Effects. It works in pretty much the same way, but emphasising the thing that the Effects library is best at and fixing some of its shortcomings.
There are two main differences at the moment:
- Everything has to be labelled
- There's no 'implicit' lifting of smaller sets of states
The first is annoying for things like Console IO, so I might change that. The second means that we have a much better chance of providing decent error messages, one day.
The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can't close a file unless it's open, you can't read from a file unless it's open, you can't run an expression unless it closes all of its files, etc.
There's certainly overlap, but I'm not sure whether one subsumes the other.