Monads ====== The [[tradition in the functional programming literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to introduce monads using a metaphor: monads are spacesuits, monads are monsters, monads are burritos. We're part of the backlash that prefers to say that monads are monads. The closest we will come to metaphorical talk is to suggest that monadic types place objects inside of *boxes*, and that monads wrap and unwrap boxes to expose or enclose the objects inside of them. In any case, the emphasis will be on starting with the abstract structure of monads, followed by instances of monads from the philosophical and linguistics literature. ### Boxes: type expressions with one free type variable Recall that we've been using lower-case Greek letters α, β, γ, ... to represent types. We'll use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a type schema is a type expression that may or may not contain unbound type variables. For instance, we might have P ≡ Int P ≡ α -> α P ≡ ∀α. α -> α P ≡ ∀α. α -> β etc. A box type will be a type expression that contains exactly one free type variable. Some examples (using OCaml's type conventions): α Maybe α List (α, P) Tree (assuming P contains no free type variables) (α, α) Tree The idea is that whatever type the free type variable α might be, the boxed type will be a box that "contains" an object of type α. For instance, if `α List` is our box type, and α is the basic type Int, then in this context, `Int List` is the type of a boxed integer. We'll often write box types as a box containing the value of the free type variable. So if our box type is `α List`, and `α == Int`, we would write Int for the type of a boxed Int. At the most general level, we'll talk about *Kleisli arrows*: P -> Q A Kleisli arrow is the type of a function from objects of type P to objects of type box Q, for some choice of type expressions P and Q. For instance, the following are arrows: Int -> Bool Int List -> Int List Note that the left-hand schema can itself be a boxed type. That is, if `α List` is our box type, we can write the second arrow as Int -> Int We'll need a number of schematic functions to help us maneuver in the presence of box types. We will want to define a different instance of each of these for whichever box type we're dealing with: mid (/εmaidεnt@tI/ aka unit, return, pure): P -> P map (/maep/): (P -> Q) -> P -> Q map2 (/maep/): (P -> Q -> R) -> P -> Q -> R mapply (/εm@plai/): P -> Q -> P -> Q mcompose (aka <=<): (Q -> R) -> (P -> Q) -> (P -> R) mbind (aka >>=): ( Q) -> (Q -> R) -> ( R) mflipcompose (aka >=>): (P -> Q) -> (Q -> R) -> (P -> R) mflipbind (aka =<<) ( Q) -> (Q -> R) -> ( R) mjoin: P -> P Note that `mcompose` and `mbind` are interdefinable: u >=> k ≡ \a. (ja >>= k). In most cases of interest, the specific instances of these types will provide certain useful guarantees. * ***Mappable*** ("functors") At the most general level, some box types are *Mappable* if there is a `map` function defined for that boxt type with the type given above. * ***MapNable*** ("applicatives") A Mappable box type is *MapNable* if there are in addition `map2`, `mid`, and `mapply`. * ***Monad*** ("composable") A MapNable box type is a *Monad* if there is in addition a `mcompose` and `join`. In addition, in order to qualify as a monad, `mid` must be a left and right identity for mcompose, and mcompose must be associative. That is, the following "laws" must hold: mcompose mid k = k mcompose k mid = k mcompose (mcompose j k) l = mcompose j (mcompose k l) To take a trivial example (but still useful, as we will see), consider the identity box type Id: `α -> α`. In terms of the box analogy, the Identity box type is an invisible box. With the following definitions mid ≡ \p.p mcompose ≡ \f\g\x.f(gx) Id is a monad. Here is a demonstration that the laws hold: mcompose mid k == (\f\g\x.f(gx)) (\p.p) k ~~> \x.(\p.p)(kx) ~~> \x.kx ~~> k mcompose k mid == (\f\g\x.f(gx)) k (\p.p) ~~> \x.k((\p.p)x) ~~> \x.kx ~~> k mcompose (mcompose j k) l == mcompose ((\f\g\x.f(gx)) j k) l ~~> mcompose (\x.j(kx)) l == (\f\g\x.f(gx)) (\x.j(kx)) l ~~> \x.(\x.j(kx))(lx) ~~> \x.j(k(lx)) mcompose j (mcompose k l) == mcompose j ((\f\g\x.f(gx)) k l) ~~> mcompose j (\x.k(lx)) == (\f\g\x.f(gx)) j (\x.k(lx)) ~~> \x.j((\x.k(lx)) x) ~~> \x.j(k(lx)) Id is the favorite monad of mimes everywhere. To take a slightly less trivial example, consider the box type `α List`, with the following operations: mcompose f g p = [r | q <- g p, r <- f q] In words, if g maps a P to a list of Qs, and f maps a Q to a list of Rs, then mcompose f g maps a P to a list of Rs by first feeding the P to g, then feeding each of the Qs delivered by g to f. For example, let f q = [q, q+1] in let g p = [p*p, p+p] in mcompose f g 7 = [49, 50, 14, 15] It is easy to see that these definitions obey the monad laws (see exercises).