Taking advantage of type synonyms in monad-control
December 26, 2014
Bas van Dijk has recently released monad-control-220.127.116.11, the main purpose of which is to replace associated data types with associated type synonyms. The change caused minor breakages here and there, so people might wonder whether and why it was worth it. Let me show you a simple example that demonstrates the difference.
Let’s say we are writing a web application. wai defines an application as
type Application = Request -> (Response -> IO ResponseReceived) -> IO ResponseReceived
Our web app will need a database connection, which we’ll pass using the
type ApplicationM m = Request -> (Response -> m ResponseReceived) -> m ResponseReceived myApp :: ApplicationM (ReaderT DbConnection IO)
However, warp can only run an
run :: Port -> Application -> IO ()
Can we build
runM :: Port -> ApplicationM m -> m () on top of the simple
run function? Solving the problems like this one is exactly the purpose of monad-control.
Here’s how such a function might look like:
runM :: (MonadBaseControl IO m) => Port -> ApplicationM m -> m () runM port app = do liftBaseWith $ \runInIO -> run port $ \req ack -> runInIO $ app req (liftBase . ack)
What’s going on here?
liftBase, allows to run a primitive monadic action in a complex monad stack. The difference is that it also gives us a function, here named
runInIO, which lets to “lower” complex actions to primitive ones. Here we use
runInIO to translate the return value of our app,
m (), into a basic
IO () value that the
run function can digest.
All is well, except…
Could not deduce (StM m ResponseReceived ~ ResponseReceived) Expected type: IO ResponseReceived Actual type: IO (StM m ResponseReceived) Relevant bindings include runInIO :: RunInBase m IO In the expression: runInIO $ app req (liftBase . ack)
The type of
forall a . m a -> IO (StM m a) (a.k.a.
RunInBase m IO), while we would like a simple
forall a . m a -> IO a. The purpose of
StM is to encompass any “output effects”, such as state or error.
In our case, we don’t have any “output effects” (nor would we be allowed to), so
StM (ReaderT DbConnection IO) ResponseReceived is really isomorphic to
In monad-control 0.x,
StM used to be an associated data family, and its constructors for the standard monad transformers were hidden. Even though we knew that the above two types were isomorphic, we still couldn’t resolve the error nicely.
Not anymore! Since in monad-control 1.0
StM is an associated type synonym,
StM (ReaderT DbConnection IO) ResponseReceived and
ResponseReceived are not just hypothetically isomorphic; they are literally the same type. After we add the corresponding equality constraint to
runM :: (MonadBaseControl IO m, StM m ResponseReceived ~ ResponseReceived) => Port -> ApplicationM m -> m ()
our app compiles!
This example is not just an isolated case. The general problem with monad-control is that it is all too easy to discard the output effects as Edward Yang shows.
Monads for which
StM m a ~ a provide a “safe subset” of monad-control. Previously, it was hard to tell apart safe and unsafe uses, because the output effects or absence thereof hid behind the opaque StM data family.
Now not only is it transparent when the output effects are absent, but we can actually encode that fact right in the type system! As an example, Mitsutoshi Aoe and I are experimenting with a safe lifted async module.
One may wonder if this subset is too boring, since it only includes monads that are isomorphic to a reader transformer over the base monad. While that is technically true, there are a lot of things you can do with a reader. The
CustomWriterT transformers that I described in another article, as well as the
Proxied transformer they’re based upon, are reader-like and thus safe to use with monad-control.