Monad Transformer

definition theorem example program

Monads do not compose in general, but adjunctions do. Given an “inner” monad $T=R^{\prime }{L}^{\prime }$ and an “outer” adjunction $L⊣R$, the composite $R\circ T\circ L$ is again a monad (Monads from Adjunctions) — the monad transformer of the outer adjunction applied to $T$. Its unit and multiplication, drawn as string diagrams, are

$${\eta }_a=R({\eta }_{La}^i)\circ {\eta }_a^o,{\mu }_c=R({\mu }_{Lc}^i)\circ (RT)({\epsilon }_{(TL)c}^o).$$

Sources: DaoFP §15.4 (“Monad Transformers”, “State monad transformer”); the Monad Transformer Library (MTL).

State transformer. With the currying adjunction $L_{s}a=a\times s$, $R_{s}c=c^s$: newtype StateT s m a = StateT (s -> m (a, s)), return x = StateT (\s -> return (x, s)) (outer unit followed by the inner return post-composed via $R$), and

join mma = StateT (join . fmap (uncurry runStateT) . runStateT mma)

(outer counit = uncurry runStateT lifted by $RT$ = post-composition and fmap, then the inner join). Then MaybeState s a = StateT s Maybe a is s -> Maybe (a, s), combining state with failure — matching the hand-written instance whose laws one would otherwise have to check by hand — and State s = StateT s Identity.

JuliaLeanHaskell

Docs: plain Julia — Catlab has no dedicated API for this; related: Catlab v0.16 docs · GATlab standard library

# StateT over Maybe: s -> Union{Some{(a, s)}, Nothing}
retST(a) = s -> Some((a, s))
bindST(st, k) = s -> (r = st(s); r === nothing ? nothing : ((a, s′) = something(r); k(a)(s′)))
popST = s -> isempty(s) ? nothing : Some((s[1], s[2:end]))          # fails on empty stack
prog = bindST(popST, x -> bindST(popST, y -> retST(x + y)))
prog([3, 4, 5])                     # Some((7, [5]))
prog([3])                           # nothing

import Mathlib
#check @StateT               -- StateT σ m α := σ → m (α × σ)
#check @OptionT
#check @ReaderT
example : StateT (List ℕ) Option ℕ := do
  let s ← get
  match s with
  | x :: rest => set rest; pure x
  | [] => failure

newtype StateT s m a = StateT (s -> m (a, s))
runStateT :: StateT s m a -> s -> m (a, s)
runStateT (StateT h) = h
instance Functor m => Functor (StateT s m) where
  fmap f (StateT h) = StateT (fmap (\(a, s) -> (f a, s)) . h)
instance Monad m => Applicative (StateT s m) where
  pure x = StateT (\s -> return (x, s))
  mf <*> ma = mf >>= \f -> fmap f ma
instance Monad m => Monad (StateT s m) where
  mma >>= k = StateT (\s -> runStateT mma s >>= \(a, s') -> runStateT (k a) s')
type MaybeState s a = StateT s Maybe a