# 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

`runStateT :: StateT Int IO Char -> Int -> IO (Char, Int)`

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:

```
> :kind! StM (StateT Int IO) Char
StM (StateT Int IO) Char :: *
= (Char, Int)
```

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

```
> :kind! StM (ExceptT Text IO) Char
StM (ExceptT Text IO) Char :: *
= Either Text Char
```

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:

```
> :kind! StM (ReaderT Int IO) Bool
StM (ReaderT Int IO) Bool :: *
= Bool
```

**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

`StM m ResponseReceived ~ ResponseReceived`

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`

:

`allocate :: MonadResource m => IO a -> (a -> IO ()) -> m (ReleaseKey, a)`

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 $ allocate
(\runInIO
(runInIO acquire). release)) (runInIO
```

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

`type StatelessAt m a = StM m a ~ a`

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:

```
class StM m a ~ a => StatelessAt m a
instance StM m a ~ a => StatelessAt m a
```

Now `StatelessAt`

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

:

`type Stateless m = Forall (StatelessAt m)`

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
= action \\ (inst :: Stateless m :- StatelessAt m a) assertStateless action
```

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

`assertStateless :: forall m a r . Stateless m => (StM m a ~ a => r) -> r`

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 @a $
assertStateless @() $
assertStateless @(ReleaseKey, a) $
assertStateless
liftBaseWith-> runInIO $ allocate
(\runInIO
(runInIO acquire). release)) (runInIO
```

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`

:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
= do ... foo
```

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

:

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

And somewhere in there we need to allocate something:

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

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 ()
= do
foo <- getThing
thing flip runReaderT thing $ do
<- lift $
resource -- 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

`statelessT :: forall t m . (StatelessT t, Stateless m) :- Stateless (t m)`

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:

```
= Sub $ forall prf
statelessT where
prf :: forall a . (StatelessT t, Stateless m) => Dict (StatelessAt (t m) a)
= Dict \\ (instV :: StatelessT t :- StatelessTAt t m a)
prf 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
= action \\ statelessT @t @m liftStatelessT action
```

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

:

```
foo :: (MonadBaseControl IO m, MonadResource m, Stateless m) => m ()
= do
foo flip runReaderT () $ liftStatelessT $ do
<- allocateM (return ()) (const $ return ())
resource 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 @a $
assertStateless @() $
assertStateless @(ReleaseKey, a) $
assertStateless
liftBaseWith-> runInIO $ allocate
(\runInIO
(runInIO acquire). release)) (runInIO
```

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

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 ()
= do
foo flip runReaderT () $ liftStatelessT $ do
<- allocateM acq rel
resource return ()
where
acq :: ReaderT () m ()
= return ()
acq rel :: () -> ReaderT () m ()
= return () rel _
```

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

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

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

`bar :: (MonadBaseUnlift IO m, MonadReader () m) => m ()`

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`

:

`foo :: MonadBaseUnlift IO m => m ()`

We can’t call `bar`

directly because the
`MonadReader`

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

layer to satisfy it,

```
foo :: MonadBaseUnlift IO m => m ()
= runReaderT bar () foo
```

… 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 ()
= return ()
bar
foo :: (Monad m, Stateless m) => m ()
= runReaderT (liftStatelessT bar) () foo
```

## 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
= action \\ (inst :: Stateless m :- StatelessAt m a)
assertStateless action
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)
= Sub $ forall prf
statelessT where
prf :: forall a . (StatelessT t, Stateless m) => Dict (StatelessAt (t m) a)
= Dict \\ (instV :: StatelessT t :- StatelessTAt t m a)
prf 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
= action \\ statelessT @t @m liftStatelessT action
```