# Universally stateless monads

Published on ; updated on

## Background: monad-control and stateless monads

The monad-control package allows to lift IO functions such as

```
forkIO :: IO () -> IO ThreadId
catch :: Exception e => IO a -> (e -> IO a) -> IO a
allocate :: MonadResource m => IO a -> (a -> IO ()) -> m (ReleaseKey, a)
```

to IO-based monad stacks such as `StateT Int (ReaderT Bool IO)`

.

The core idea of the package is the associated type `StM`

, which, for a given monad `m`

and result type `a`

, calculates the “state” of `m`

at `a`

.

The “state” of a monad is whatever the “run” function for this monad returns.

For instance, for `StateT Int IO Char`

, we have

The result type of this function (minus the outer monad constructor, `IO`

, which is always there) is `(Char, Int)`

, and that is what `StM (StateT Int IO) Char`

should expand to:

In this case, `StM m a`

is not the same as `a`

; it contains `a`

plus some extra information.

In other cases, `StM m a`

may not contain an `a`

at all; for instance

and we cannot always extract a `Char`

from `Either Text Char`

.

For some monads, though, `StM m a`

reduces precisely to `a`

. I call such monads “stateless”. A notable example is the reader monad:

**Definition.** A monad `m`

is stateless at type `a`

iff `StM m a ~ a`

.

Note that a monad like `ReaderT (IORef Int) IO`

is also stateless, even though one can use it to implement stateful programs.

The important feature of stateless monads is that we can fork them without duplicating the state and terminate them without losing the state. The monad-control package works best with stateless monads: it is less tricky to understand, and you can do some things with stateless monads that are hard or impossible to do with arbitrary `MonadBaseControl`

monads.

## Universally stateless monads

When both the monad `m`

and the result type `a`

are known, the compiler can expand the associated synonym `StM m a`

and decide whether `StM m a ~ a`

.

However, there are good reasons to keep the monad `m`

polymorphic and instead impose the constraints (e.g. `MonadReader Int m`

) that `m`

must satisfy.

In this case, the compiler cannot know *a priori* that `m`

is stateless, and we need to explicitly state that in the function signature. In Taking advantage of type synonyms in monad-control, I showed one such example: running a web application with access to the database. In order to convince the compiler that `m`

is stateless, I needed to add the constraint

to the type signature.

As you can see, this doesn’t quite say “monad `m`

is stateless”; instead it says “monad `m`

is stateless at type `a`

” (where `a`

is `ResponseReceived`

in the above example).

This is fine if we only use monad-control at one result type. But if we use monad-control functions at many different types, the number of constraints required quickly gets out of hand.

As an example, consider the `allocate`

function from resourcet’s `Control.Monad.Trans.Resource`

:

As the module’s documentation says,

One point to note: all register cleanup actions live in the IO monad, not the main monad. This allows both more efficient code, and for monads to be transformed.

In practice, it is often useful for the register and cleanup actions to live in the main monad. monad-control lets us lift the `allocate`

function:

```
{-# LANGUAGE FlexibleContexts, TypeFamilies, ScopedTypeVariables #-}
import Control.Monad.Trans.Control
import Control.Monad.Trans.Resource
allocateM
:: forall m a . (MonadBaseControl IO m, MonadResource m,
StM m a ~ a, StM m () ~ (), StM m (ReleaseKey, a) ~ (ReleaseKey, a))
=> m a -> (a -> m ()) -> m (ReleaseKey, a)
allocateM acquire release =
liftBaseWith
(\runInIO -> runInIO $ allocate
(runInIO acquire)
(runInIO . release))
```

This small function requires three different stateless constraints — constraints of the form `StM m x ~ x`

— and two additional stateless constraints per each additional type `a`

at which we use it.

These constraints are artefacts of the way type synonyms work in Haskell; `StM m a`

is not really supposed to depend on `a`

. If a monad is stateless, it is (pretty much always) stateless at every result type.

**Definition.** A monad `m`

is universally stateless iff for all `a`

, `StM m a ~ a`

.

In order to capture this universal statelessness in a single constraint, we can use `Forall`

from the constraints package.

First, we need to transform the constraint `StM m a ~ a`

to a form in which it can be partially applied, as we want to abstract over `a`

. Simply saying

won’t do because type synonyms need to be fully applied: `StatelessAt m`

is not a valid type.

We need to use a trick to create a class synonym:

Now `StatelessAt`

is a legitimate class constraint (not a type synonym), and so we can abstract over its second argument with `Forall`

:

Now we only need to include the `Stateless m`

constraint, and every time we need to prove that `StM m a ~ a`

for some result type `a`

, we wrap the monadic computation in `assertStateless @a (...)`

, where `assertStateless`

is defined as follows:

```
assertStateless :: forall a m b . Stateless m => (StM m a ~ a => m b) -> m b
assertStateless action = action \\ (inst :: Stateless m :- StatelessAt m a)
```

The type signature of `assertStateless`

is crafted in such a way that we only need to specify `a`

, and `m`

is inferred to be the “current” monad. We could have given `assertStateless`

a more general type

but now we have to apply it to both `m`

and `a`

.

As an example of using `assertStateless`

, let’s rewrite the lifted `allocate`

function to include a single stateless constraint:

```
allocateM
:: forall m a . (MonadBaseControl IO m, MonadResource m, Stateless m)
=> m a -> (a -> m ()) -> m (ReleaseKey, a)
allocateM acquire release =
assertStateless @a $
assertStateless @() $
assertStateless @(ReleaseKey, a) $
liftBaseWith
(\runInIO -> runInIO $ allocate
(runInIO acquire)
(runInIO . release))
```

Here, `assertStateless`

generated all three `StM m x ~ x`

constraints for us on the fly, from the single universally-quantified constraint `Stateless m`

.

## Stateless monad transformers

Let’s say we are writing a function that works in some stateless monad, `m`

:

But locally, it adds another layer on top of `m`

:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
foo = do
thing <- getThing
flip runReaderT thing $ do
...
```

And somewhere in there we need to allocate something:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
foo = do
thing <- getThing
flip runReaderT thing $ do
resource <- allocateM acq rel
...
```

The compiler won’t accept this, though:

```
• Could not deduce: StM
m (Data.Constraint.Forall.Skolem (StatelessAt (ReaderT () m)))
~
Data.Constraint.Forall.Skolem (StatelessAt (ReaderT () m))
arising from a use of ‘allocateM’
from the context: (MonadBaseControl IO m,
MonadResource m,
Stateless m)
bound by the type signature for:
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) =>
m ()
```

In order to run `allocateM`

in the inner environment, `ReaderT Thing m`

, we need to satisfy the constraint `Stateless (ReaderT Thing)`

, which is different from the `Stateless m`

that we have in scope.

If the `acq`

and `rel`

actions do not need to access the `thing`

, we can avoid the problem by lifting the action to the outer environment:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
foo = do
thing <- getThing
flip runReaderT thing $ do
resource <- lift $
-- this happens in m
allocateM acq rel
...
```

But what if `acq`

and `rel`

do need to know the `thing`

?

In that case, we need to prove to the compiler that for all `m`

, `Stateless m`

implies `Stateless (ReaderT Thing)`

. This should follow from the fact that `ReaderT e`

is itself a “stateless transformer”, meaning that it doesn’t change the state of the monad that it transforms. As with `Stateless`

, we put this in the form of partially-applicable class and then abstract over `a`

(and `m`

):

```
class StM (t m) a ~ StM m a => StatelessTAt t (m :: * -> *) a
instance StM (t m) a ~ StM m a => StatelessTAt t m a
type StatelessT t = ForallV (StatelessTAt t)
```

Now we need to prove that `StatelessT t`

and `Stateless m`

together imply `Stateless (t m)`

. In the notation of the constraints package, this statement can be written as

How to prove it in Haskell is not completely obvious, and I recommend that you try it yourself. I also posted a simplified version of this exercise on twitter the other day.

Anyway, here is one possible answer:

```
statelessT = Sub $ forall prf
where
prf :: forall a . (StatelessT t, Stateless m) => Dict (StatelessAt (t m) a)
prf = Dict \\ (instV :: StatelessT t :- StatelessTAt t m a)
\\ (inst :: Stateless m :- StatelessAt m a)
```

Finally, here is a function analogous to `assertStateless`

that brings the `Stateless (t m)`

constraint into scope:

```
liftStatelessT
:: forall t m b . (StatelessT t, Stateless m)
=> (Stateless (t m) => (t m) b) -> (t m) b
liftStatelessT action = action \\ statelessT @t @m
```

And here is a minimal working example that demonstrates the usage of `liftStatelessT`

:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
foo = do
flip runReaderT () $ liftStatelessT $ do
resource <- allocateM (return ()) (const $ return ())
return ()
```

## monad-unlift

After this article was originally published, MitchellSalad pointed out the monad-unlift library, which Michael Snoyman announced two years earlier, and which I was not aware of.

Indeed, Stateless and monad-unlift (v0.2.0) are strikingly similar.

(“Stateless” is the name of the code and the module described in this article. You can find the contents of the module below. I have not published it on github or hackage.)

But here are some important differences.

### the interface

With Stateless, we use the normal `MonadBaseControl`

functions (like `liftBaseWith`

) and then turn `StM m a`

into `a`

with `assertStateless`

.

With monad-unlift, we call `askUnliftBase`

or `askRunBase`

*instead of* `liftBaseWith`

.

For comparison, here is `allocateM`

implemented with both approaches:

```
-- Stateless
allocateM
:: forall m a . (MonadBaseControl IO m, MonadResource m, Stateless m)
=> m a -> (a -> m ()) -> m (ReleaseKey, a)
allocateM acquire release =
assertStateless @a $
assertStateless @() $
assertStateless @(ReleaseKey, a) $
liftBaseWith
(\runInIO -> runInIO $ allocate
(runInIO acquire)
(runInIO . release))
```

```
-- monad-unlift
allocateM
:: forall m a . (MonadBaseUnlift IO m, MonadResource m)
=> m a -> (a -> m ()) -> m (ReleaseKey, a)
allocateM acquire release = do
UnliftBase runInIO <- askUnliftBase
allocate
(runInIO acquire)
(runInIO . release)
```

The monad-lift version is simpler and more concise despite (but, in fact, thanks to) the `UnliftBase`

wrapper.

On the other hand, Stateless integrates better with the other code built on top of monad-control. If we have a third-party “lifted” library whose function returns `m (StM m a)`

, Stateless allows us to simplify that down to `m a`

. With monad-unlift, we would have to re-implement the whole function to use different primitives.

### dealing with transformers

The approach to transformers also differs between the libraries. With Stateless, we stay on the transformer level and prove that it is stateless:

```
foo :: forall m . (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
foo = do
flip runReaderT () $ liftStatelessT $ do
resource <- allocateM acq rel
return ()
where
acq :: ReaderT () m ()
acq = return ()
rel :: () -> ReaderT () m ()
rel _ = return ()
```

With monad-unlift, we bring everything down into the untransformed monad:

```
foo :: forall m . (MonadBaseUnlift IO m, MonadResource m) => m ()
foo = do
flip runReaderT () $ do
Unlift run <- askUnlift
resource <- lift $ allocateM (run acq) (run . rel)
return ()
where
acq :: ReaderT () m ()
acq = return ()
rel :: () -> ReaderT () m ()
rel _ = return ()
```

If you call `allocateM`

many times in the same function, “running” everything with monad-unlift may become tedious, but otherwise both approaches are workable.

Here is a case where `monad-unlift`

would not work, however. Consider a function

The signature seems reasonable: the function needs to run in a stateless monad so that it can do something like `allocateM`

internally; it also needs access to some configuration parameter, which I replaced with `()`

for simplicity.

We want to call `bar`

from a monad-polymorphic function `foo`

:

We can’t call `bar`

directly because the `MonadReader`

constraint will not be satisfied. But if we add a `ReaderT`

layer to satisfy it,

… then `bar`

’s `MonadBaseUnlift`

constraint is no longer satisfied.

There is just no reasonable way to do this with monad-unlift, as far as I can tell. With Stateless, this becomes trivial:

```
bar :: (Stateless m, MonadReader () m) => m ()
bar = return ()
foo :: (Monad m, Stateless m) => m ()
foo = runReaderT (liftStatelessT bar) ()
```

## unliftio

Just a couple of weeks after this article was originally published, Michael announced another library in this space: unliftio.

There are two main differences between unliftio and monad-unlift/Stateless:

- The base monad is always IO, as the package name implies.
- Instead of relying on
`monad-control`

to provide the instances for various transformers, and on libraries such as`lifted-base`

and`lifted-async`

to provide the lifted versions of the standard functions, it builds its own ecosystem.

I considered doing roughly the same when I wrote Stateless, but decided against it, as it meant writing more code. But now that Michael bit the bullet, there is no reason not to take advantage of his work.

There are plenty of reasons to prefer the specialized version: simpler and easier to understand types, better type error messages, better type inference, easier deriving (due to the absence of associated types), and no complications with monad transformers.

So, unliftio is what I would recommend today over Stateless or monad-unlift.

## Complete code for Stateless

```
-- (c) Roman Cheplyaka, 2017. License: MIT
{-# LANGUAGE GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances,
ScopedTypeVariables, RankNTypes, AllowAmbiguousTypes,
TypeApplications, TypeOperators, KindSignatures,
UndecidableInstances, UndecidableSuperClasses #-}
module Stateless where
import Data.Constraint
import Data.Constraint.Forall
import Control.Monad.Trans.Control
class StM m a ~ a => StatelessAt m a
instance StM m a ~ a => StatelessAt m a
-- | A constraint that asserts that a given monad is stateless
type Stateless m = Forall (StatelessAt m)
-- | Instantiate the stateless claim at a particular monad and type
assertStateless :: forall a m b . Stateless m => (StM m a ~ a => m b) -> m b
assertStateless action = action \\ (inst :: Stateless m :- StatelessAt m a)
class StM (t m) a ~ StM m a => StatelessTAt t (m :: * -> *) a
instance StM (t m) a ~ StM m a => StatelessTAt t m a
-- | A statement that a monad transformer doesn't alter the state type
type StatelessT t = ForallV (StatelessTAt t)
-- | A proof that if @t@ is a stateless transformer and @m@ is a stateless monad,
-- then @t m@ is a stateless monad
statelessT :: forall t m . (StatelessT t, Stateless m) :- Stateless (t m)
statelessT = Sub $ forall prf
where
prf :: forall a . (StatelessT t, Stateless m) => Dict (StatelessAt (t m) a)
prf = Dict \\ (instV :: StatelessT t :- StatelessTAt t m a)
\\ (inst :: Stateless m :- StatelessAt m a)
-- | Derive the 'Stateless' constraint for a transformed monad @t m@
liftStatelessT
:: forall t m b . (StatelessT t, Stateless m)
=> (Stateless (t m) => (t m) b) -> (t m) b
liftStatelessT action = action \\ statelessT @t @m
```