Solution (source code)

= Solution

Thread the explicit <program state> through the computation, using the base <computational monad> to sequence its effects:
$$
\boxed{\begin{aligned}
\operatorname{result}(x)\,s&=r_m(x,s),\\
(p\triangleright f)\,s&=(p\,s)\triangleright_m\bigl(\lambda(x,s').\,f(x)\,s'\bigr).
\end{aligned}}
$$
In <Haskell> notation, with `resultM` and `bindM` standing for the base operations:

``
result :: Monad m => a -> MemT m a
result x s = resultM (x,s)

bind :: Monad m => MemT m a -> (a -> MemT m b) -> MemT m b
bind p f s = bindM (p s) (\(x,s') -> f x s')
``

This is the <state monad transformer>. The first computation's final <program state>, rather than its initial <program state>, becomes the second computation's input. The base <computational monad> decides whether that pair is available at all.