I've been reading through Plucking Constraints being sent there by the effet library because I keep wondering about one subject and I hoped seeing how this library was implemented would enlighten me.

When is (Reader (State a)) not (State (Reader a))?

This is some code in Unison demonstrating the composability of effects:

program : Unit -> {Store Int, Ask Int} Int
program = do
  x = Store.get
  y = ask
  Store.put (x Int.+ y)

lcall : Unit
lcall = Store.withInitialValue +2 (do Ask.provide +1 program)

And this is the same code showing composability in Haskell.

program
    :: ( MonadReader Int m
       , MonadState Int m
       )
    => m ()
program = do
  y <- get
  x <- ask
  put (x + y)

type Ret = ((), Int)

lcall :: (Monad a) => a Ret
lcall = runReaderT (runStateT program 1) 2

rcall :: (Monad a) => a Ret
rcall = runStateT (runReaderT program 4) 3

I've long thought this to be impossible.

And indeed with State _ (Reader _ ()) this is not possible¹. So how do these things work? How come the code runs for any ordering of layers of effects the same way Unison does?

I want to find out and I'll take you on this journey with me.

The first way to achieve this is how "mtl" does it a sort of recursive chain of resposibility where if my monad doesn't handle it another will, so we can just pass the given action through. This is done via a trivial "I am instance if I contain instance" declaration:

instance (MonadState s m) => MonadState s (ReaderT r m)

With the eventual basecase of:

instance (Monad m) => MonadReader r (ReaderT r m)

Which means that if I am a ReaderT and I contain something of MonadState, I am also of MonadState.

Why this works?

Implementing a trivial effect which just returns a value is trivial in typeclasses, in many cases it is what typeclasses do. The signature (MyEffect m) => Int -> m () is translated into a function of a signature "MyEffect.VTable" -> Int -> m () where one of the arguments is just a link to some specific implemenation, and if all I need is to call those functions then that's fine.

The next question is how to get this function to interact with the monad inside.

So when we run program it substitutes the m () for IO I think, let us test that.

iocall :: IO Ret
iocall = lcall

It works with any monad on top:

ghci> lcall :: [Ret]
[((),3)]

ghci> lcall :: IO Ret
((),3)

ghci> lcall :: Maybe Ret
Just ((),3)

ghci> runIdentity lcall
((),3)

Seems that the actual physical instance of the monad is arbitrary, does it actually make it's way down though? Let's directly change program's type to :: IO ():

No instance for ‘MonadReader Int IO’ arising from a use of ‘ask’

Oh, wait type holes are a thing!!!, if I ask what program stands for in the lcall function I find:

• Found hole: _ :: StateT Int (ReaderT Integer a) ()

Okay, this means that actually different monads are built-up and IO got substituted in by accident on top because we had no basecase. Then this should work as well:

lcall = runIdentity (runReaderT (runStateT program 1) 2)

Which it does and successfully just returns the basic type not wrapped in anything, nice.

In any case:

Why does (StateT Int (ReaderT Int a) ()) allow mixing of calls?

Because they cheat that's why (src):

instance MonadReader r m => MonadReader r (Strict.StateT s m) where
    ask   = lift ask
    local = Strict.mapStateT . local
    reader = lift . reader

Where lift is a MonadTrans typeclass function found in the transformer itself which sort of just ignores the call and passes it on. It is described as having the type lift :: Monad m => m a -> t m a which helps to explain it's purpose, it is stated that to be a MonadTrans and a monad m then t m should also be a monad. So in concrete terms it is something that could take a function on Maybe a and transform it into a function on Either (Maybe a) in some defined way.

The issue here is that for every monad MonadReader is useable with I require explicit instances for every single one. This is what "effet" and "polysemy" call the "n² instances problem" and claim to sidestep somehow.

Sidenote: GHC verifies the property of MonadTrans using the constraint forall m. Monad m => Monad (t m) (Quantified constraints)

How do we sidestep the "n² instances problem"?

For one we can use the obvious option of having a list of Monads. Haskell allows an incredibly cool way of proving that that list will contain a given handler, using DataKinds and TypeFamilies. It is too difficult for me to include here, but DataKinds allow you to use value constructors in types. Not in the sense that a list would be a true list of integers, but that the type itself is a list for example. TypeFamilies sort of act as typeclasses for these kinds I think? Anyways it allows type-level trickery to just search a type list for our desired type to verify it is in there, recurse in a handler while consing onto that type, etc.

I'm gonna go read this through I guess, see you later.

---

Further reading:

• Monads do not compose
• Polysemy is fun!
• ReasonablyPolymorphic
  • Freer Interpretations of Higher-Order Effects
  • The Effect-Interpreter Effect