Proper Treatment 正當作法/ blog/ posts/ Monad transformers
標籤 Tags:
2020-05-14 14:47

In denotational semantics and functional programming, the terms monad morphism, monad layering, monad constructor, and monad transformer have by now accumulated 20 years of twisted history. The exchange between Eric Kidd and sigfpe about the probability monad prompted me to investigate this history.

Chapter 4 of Eugenio Moggi’s ”An Abstract View of Programming Languages” (Edinburgh LFCS technical report ECS-LFCS-90-113, 1990) defines a monad morphism as you’d expect in the category of monads: a natural transformation between two monads as functors that commutes with the two monads’ unit (return) and bind (>>=) operations. The two monads don’t even need to be over the same category of types, but Haskell has only one category of types (pace type classes), so Moggi focuses on the simplified case, where the functor U is an identity. Further, Moggi cares only about strong monads, which Haskell programmers like Wadler call a monad for short. Roughly, a strong monad respects the Cartesian structure (in particular of environments) of the category of types. Moggi thus defines a simplified strong monad morphism, which relates two strong monads over the same category of types. For short, Haskell programmers (like me henceforth) call it a monad morphism, of type forall a. m a -> n a where m and n are the two (strong) monads being related.

Moggi continues with “some examples of monad constructions” (emphasis mine). He defines “several endofunctors on Obj(Mon(C))”, where Obj(Mon(C)) is a category with monads for objects but only trivial (identity) morphisms. In other words, he defines several maps from monads to monads, including what Haskell calls ErrorT, StateT, ReaderT, WriterT, and ContT.

Endofunctors on Obj(Mon(C)) have very little structure. One of them exchanges the Identity monad with the State Int monad while leaving all other monads alone. You can’t even define this exchange as a Haskell type constructor of kind (*->*)->(*->*). Moggi thus considers several ways to add structure to a given endofunctor F on Obj(Mon(C)).

  1. ”Can F be extended to an endofunctor F over Mon(C)?” That is, does every monad morphism MN yield a monad morphism FMFN such that blah commutes? For the Haskell monad maps listed above, the answer is yes except for ContT.

  2. ”Is there a natural transformation from IdMon(C) to F?” That is, does every monad M yield a monad morphism MFM such that blah commutes? For the Haskell monad maps listed above, the answer is all yes.

  3. Can we lift the operations (such as changing the state or producing output) of each monad M into FM? That is, as F adds new operations to a monad, can it preserve the old operations of the monad?

The last question is crucial for Moggi’s goal, to make denotational semantics modular. Steele, Espinosa, and Liang, Hudak, and Jones turn Moggi’s goal into a puzzle in functional programming, that of building a modular interpreter. Liang et al. define a monad transformer as a monad-to-monad map that satisfies item 2 above, in other words, a natural transformation from IdMon(C) to an endofunctor on Obj(Mon(C)). The monad morphism MFM in their definition is known as lift in Haskell’s MonadTrans class.

Of items 1 and 3 above, the latter has received by far more attention in the literature. After all, monads are useful only to the extent that they provide useful operations. Filinski defines a layering of a monad N over another monad M as a function family M(NA) → NA (for each type A) such that blah commutes. In Haskell notation, a layering defines a polymorphic function

layer :: forall a. m (n a) -> n a

where m and n are the two monads. Filinski explains that monad morphisms and monad layerings are equivalent:

lift = layer . liftM return
layer = join . lift

Filinski then encodes layered monads in terms of delimited control. Lüth and Ghani propose another approach to combining monads and their operations using coproducts.

So, that’s what I know of the story of monad morphisms, layerings, constructors, and transformers in the literature.

Three asides. First, Cartwright and Felleisen pursue modular denotational semantics with side effects but not (directly) monads. Second, monads generalize to endofunctor-enriched categories or parameterized monads, a more general notion of computation.

Finally, although the probability monad factors into the list monad and the writer monad transformer (the latter for the monoid of probabilities with multiplication as the binary operation), we need to distinguish the list monad from the set monad: the distribution “True 0.2, True 0.2, False 0.6” is equivalent not to “True 0.2, False 0.6” but to “True 0.4, False 0.6”. This equivalence arises only from the probability monad as a whole. As long as we only apply the monad to types with equality, we can reduce distributions using such equivalences to compute more efficiently. Then the monad generalizes from probabilities to any semiring (with a multiplicative identity), while remaining an instance of MonadWriter and (assuming the semiring also has an additive identity) MonadPlus. This generalization is used in speech recognition and other applications in natural-language processing.