From 471e06ab9fd5bd6beaf7a9ccd17830b54969a5c7 Mon Sep 17 00:00:00 2001 From: Chris Date: Mon, 16 Mar 2015 14:21:16 -0400 Subject: [PATCH] edits --- topics/_week7_monads.mdwn | 90 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) 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). + -- 2.11.0