Unfortunately, monads are a bad way of encapsulating and controlling effects. Effects are the most important -- and most bug prone -- of any interesting software aside from compilers, and monads take this central element and make it un-composable. This is why I don't like the current advanced type systems: they help most where they're least needed (the relatively bug-free portions of the code, namely data transformations), and don't help -- interfere, even -- where they're most needed. Effect systems -- if we can get them right and easy to use -- will be a great help. In the meantime, some of the most production-ready effect systems (though they're not general, but have to be built ad-hoc for a specific use) can be found in Java 8's pluggable type systems provided by the Checker framework[1]. It's got a rudimentary lock-use effect system and a GUI effect system (plus some other cool type systems, like physical units, immutability, security and even a linear type system for aliasing).
> Effects are the most important -- and most bug prone -- of any interesting software aside from compilers, and monads take this central element and make it un-composable.
Can you elaborate on this? Because, AFAICT, the big selling point for monads for dealing with effects is precisely composability.
I think the point is that there is no good effect-union type; this has to be pieced together with monad transformers where you might have that types "Atransformer (Btransformer C)" is not equal to "Btransformer (Atransformer C)".
This is, for example, why Haskell has one monolithic "IO" monad instead of one for hitting the filesystem, one for HTTP requests, one for IORefs, etc. Haskell does not, for example, represent the difference between program nondeterminism (reading a file and doing stuff differently based on its contents) and permanent side-effects on the file system (writing a file); and I'd say the reason that it doesn't do that is because NondeterministicT (FilesystemAlteredT Identity) x would be different from FilesystemAlteredT (NondeterministicT Identity) x.
In some ways the granularity is nice because those two types are not isomorphic; but you might want to "erase" the granularity, which is not possible in Haskell. In terms of the "unioning" that you want, it's something like a dual of the unions that appear in typed exceptions: once you trace through some code you find out that it might fail via `FileNotFound` or `HTTP404`; this means that the relevant effects are `FileSystem :+: HTTP` in some sense.
I know there are a lot of solutions to this, but I've personally found the `mtl` mechanism in Haskell to be completely sufficient. I describe whatever effect languages I want my application bits to be able to operate over as separate type classes and then build one or more interpreters of these classes to run.
The problem with this mechanism is not felt by the application writer but instead the library writer. It forces you to instantiate (n x m) combinations of effects for your (concrete instantiators) x (effectful languages). For the core classes mtl bears this well, but it might explain why this technique is not as well represented in written libraries.
That said, as an application writer the number of concrete instantiators is often between 1 and 3 so the pain is very reasonable.
(Edit: I should add that there is another downside in the mtl method in that authors of these finally-tagless code fragments cannot choose priority order of effects---the interpreter is free to decide this on their own. There's nothing wrong with this as long as you, as interpreter writer, consider the burden of correctness. You should be anyway, though, so... It ends up being a minor pain point, imo.)
I'm kind of interested in knowing why you don't think that there isn't an isomorphism along the ordering of the monad transformers. Wouldn't it just be a question of rebuilding combinators so that they're targetting the right depth? Or am I missing something
I'll demonstrate the lack of an isomorphism via a counterexample.
Consider MaybeT and WriterT (and the basic Identity monad for the bottom of our stack)
newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }
newtype WriterT w m a = WriterT { runWriterT :: m (a, w) }
newtype Identity a = Identity { runIdentity :: a }
I'm going to claim that MaybeT (WriterT w Identity) is not isomorphic to WriterT w (MaybeT Identity). If we expand the first
MaybeT (WriterT w Identity) a
==
WriterT w Identity (Maybe a)
==
Identity (Maybe a, w)
==
(Maybe a, w)
And if we expand the second
WriterT w (MaybeT Identity) a
==
MaybeT Identity (a, w)
==
Identity (Maybe (a, w))
==
Maybe (a, w)
So we can see that the Maybe is wrapped around something different in each stack. So now to the claim that there's no isomorphism should be obvious---any witnesses to the isomorphism f and g would have to have that for all w, f (g (Nothing, w)) = (Nothing, w), but since g :: (Maybe a, w) -> Maybe (a, w) cannot fabricate an `a`, it must be such that g (Nothing, w) = Nothing which means that f :: Maybe (a, w) -> (Maybe a, w) cannot determine the right `w` to return.
Monads themselves are composable via bind, but the values encapsulated by the monad are not. Consider there is no real converse to the return operator: once something has been wrapped by a monad, then it is forever stuck in that monadic world. That can be rather annoying, because in languages such as OCaml (not sure about Haskell &c), monad-like interfaces are a convenient abstraction, yet using them leads to highly idiosyncratic code. Rather similar to the sync/async, red/blue distinction in the original article.
Sure the values are. Any function `a -> b -> c` can be lifted into a function `m a -> m b -> m c` for any Monad. That's (part of) the exact thing that bind buys you.
"Escaping" from a monad is an artifact of a bad intuition. There's no reason for a monad (m a) to "contain" values a and thus no reason to believe that they can be removed.
Even Maybe is a sufficient model of this. I can make a whole big compositional pipeline with all kinds of compositions at the value level, but if my inputs are Nothing then there won't be anything to "pull out" at the end.
Ultimately, "monadic worlds" is a good intuition. Just realize that your monadic world may be a strange one when you pull it back into "your" world---the interpretation may not be obvious, it may demand something of you, and it may not look very much like the "values" you felt like you were playing around with.
Let's take a simple, quotidian example: logging and errors. I write functions that produce logs and may generate errors. If I were using monads, I'd have a log monad and an error monad. For logs, my functions would produce a value and a list of log messages. The monad would combine the list of messages. For errors, my functions return an OK and a value, or an error, and the monad short-circuits errors. Now I write functions that might produce both logs and errors. How do the two monads compose?
Of course there are two ways. The problem is that there is not enough information in the mere product of the two algebras to indicate what proper behavior is.
If you don't mind deferring the definition of "correct" to the interpreter writer then that intentional choice is captured by
(MonadWriter Log m, MonadExcept m) => m a
If you want more controls then we need to start specifying laws. For instance, the following law distinguishes between the two instances
throwError e >> m == throwError e
and this now clearly indicates that EitherT e (WriterT Log) is wrong while WriterT Log (Either e) is fine.
So how do we specify what additional laws are needed to cut down the free product of the effectful languages? Dunno, that's a hard one. You could clearly do it using dependent types, but that's still today very expensive.
But given that we literally lack proper information to make a choice it's very important that all of those choices are allowable. It's my position that there is no meaningful default. It's also my position that the `mtl` style free products are perfectly acceptable.
But in general, effects are not "the values encapsulated by the monad", so the fact that the values are "stuck" within the monad doesn't have any bearing on whether using monads to manage effects makes effects non-composable.
To be fair, I like pluggable type systems a lot. I don't think that privileged type systems are the end-all-be-all.
I disagree a lot that the current effect systems don't prevent errors, however. You're right that linear types are difficult to encode in Haskell at least, but you can get away with a lot of bang for relatively little buck even without them.
The right choice (or choices) in design space here is a big challenge. It'll be exciting to see new research as it develops. I'm especially excited to see what comes of Pfenning's Pi calculus linear types [0].
[0] To be clear, I don't know if they're "his" excepting that he appears to be doing a lot of modern research there and that's where I learned about them.
[1]: http://types.cs.washington.edu/checker-framework/current/che...