From: Chris Date: Mon, 16 Mar 2015 18:21:16 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=471e06ab9fd5bd6beaf7a9ccd17830b54969a5c7;hp=62abed25f0f396cd548b833805f4219cbdf79533 edits --- diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn index da0b0080..61d50094 100644 --- a/topics/_week7_monads.mdwn +++ b/topics/_week7_monads.mdwn @@ -1,4 +1,5 @@ + Monads ====== @@ -68,3 +69,92 @@ 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). +