X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week7_monads.mdwn;h=61d50094fe6c41d2064ba29c6f504c62082ff206;hp=e8785bbdfdfd03bc78c0297d98d9f241da35a534;hb=471e06ab9fd5bd6beaf7a9ccd17830b54969a5c7;hpb=6cb98be545c373b3eb4aa5be81cb51982f2dc458;ds=sidebyside diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn index e8785bbd..61d50094 100644 --- a/topics/_week7_monads.mdwn +++ b/topics/_week7_monads.mdwn @@ -1,6 +1,5 @@ -x
- - + + Monads ====== @@ -12,10 +11,150 @@ 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 +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. -x
+### 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). +