@samth Re: https://twitter.com/samth/status/1196846044555988992, I’m happy to explain if you want, but doing it on twitter is hard… so maybe I should reply here and satisfy both of your desires. :)

Really I’m still unconvinced about tracking effects in the type system, but I know that’s not what you mean

So, I should start by saying that monads are absolutely enough to express all the things I want. Basically the semantics I’ve arrived at is just delimited control… and it’s well-known that you can express delimited control with monads. The problem is twofold: programming with them is awkward, and it’s hard to compile them efficiently. The former is basically just syntactic, and though there’s a reasonable conversation to be had about it, it’s not what I’m talking about, so I’ll just focus on the latter.

I also think that a monadic interface isn’t actually fundamentally the problem. That’s good, because as I mentioned here https://twitter.com/lexi_lambda/status/1196845975173763072, you can’t get away from them in a lazy language (or at least we don’t currently know a better way). You can, of course, argue that laziness isn’t worth it, but that’s a totally separate conversation as well. :)

The thing I’m actually complaining about is the situation that Haskell has: you implement monads in userland code, except for one “blessed” monad, IO, which can do all the real side-effects. The main problem with this is that if you’re doing real side-effects, then at some point, you have to do it in IO. So this leaves you two choices: (1) build a data structure in pure code and interpret it in IO (e.g. free monads), or (2) build a monad that is a wrapped version of IO (e.g. monad transformers).

We don’t know how to efficiently compile the former, so it’s disqualified immediately. Maybe someday we’ll figure out supercompilation or whatever, but we’re not there yet. That leaves the latter. But that approach has two big problems: one is about correctness, and one is about performance.

The correctness one is probably more interesting/compelling, so I’ll start with that. I’m going to use Haskell’s IO exceptions as a concrete example of what can go wrong, but even if you don’t like exceptions, it comes up in other forms, too.

If you want to catch an exception in Haskell, you use a catch operation with the following type: catch :: Exception e => IO a -> (e -> IO a) -> IO a That generally seems reasonable… but it actually has a massive, fundamental problem once you start layering things on top. If you want to implement effects using monads, you need to generalize that type to this one: catch :: (MonadCatch m, Exception e) => m a -> (e -> m a) -> m a Here’s the problem: in general, you can’t.

The issue is that catch only allows actions of type IO a, since it needs control of their entire continuation in order to install the relevant exception handler. For some monads, this is okay. Consider, for example, the traditional ReaderT monad transformer, which essentially has the following definition: type ReaderT r m a = r -> m a This is just the function monad lifted to a monad transformer, and it basically adds the idea of a binding with dynamic extent to Haskell. If you have ReaderT r IO a, that’s just r -> IO a, so you can always get an IO a out of it by applying the function to r. You can therefore implement catch on ReaderT by applying the functions to get IO values from ReaderT r IO values before passing them to catch.

But this only works because ReaderT is such a simple monad. Imagine you have StateT instead: type StateT s m a = s -> m (s, a) This is very similar, but instead of a single global value, >>= uses the result of the previous action as the state of the next one. Now if we have StateT s IO a, we can’t get an IO a, just an IO (s, a). We can pass that to catch by instantiating a in catch’s type signature to (s, a), but there’s a problem: if the exception handler is called, all the state changes that happened in the first argument get discarded.

This behavior is sometimes defended because it is, indeed, sometimes sort of useful—you basically get “transactional” state semantics, where raising an exception “rewinds” the state. But it breaks down completely for more complex effects. For example, imagine you have ContT r m a = (a -> m r) -> m r, the continuation monad transformer. You simply cannot get an IO a from ContT r IO a, no matter how hard you try.

So the problem is basically that the interface of IO is too restrictive, and it makes it impossible to actually use any of the fancy delimited control stuff you can implement with monads as soon as your program needs to do any actual side-effects (at least without incurring some really weird/broken semantics).

…I could also go into the performance problem, but that’s probably enough text, and it gets the point across well enough.

This is shaping up to be much more interesting than “monads probably aren’t worth it.”

It sounds like you’re talking about making a new catch-all monad that adds delimited control to IO. You’re talking as though you want to use this new monad directly to write code, but it sounds like this would be a more expressive base monad for building monad transformer stacks on top of.

Meanwhile, the attention you’re paying to the catch effect is interesting because (as you well know) it’s one of the ways people can use the IO monad for sequencing Haskell’s non-monadic effects, effects like throw and killThread that happen during the execution of a so-called “pure” expression.

So overall you seem to be pursuing a design that would synthesize the multiple notions of side effects in Haskell. It’s set to cater to both the “side effects = whatever it is monads can do” and “side effects = whatever it is that can happen during execution” worlds and get them to play more nicely together.