From 1cf93986ef5e7a09e84cf8ba02d671bd5da7b0ab Mon Sep 17 00:00:00 2001 From: jim Date: Sun, 22 Mar 2015 10:10:51 -0400 Subject: [PATCH] add addl reading section --- topics/week7_introducing_monads.mdwn | 53 ++++++++++++++++++++++++++++++------ 1 file changed, 44 insertions(+), 9 deletions(-) diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn index b5f1d48a..6204b8a7 100644 --- a/topics/week7_introducing_monads.mdwn +++ b/topics/week7_introducing_monads.mdwn @@ -1,8 +1,6 @@ -Introducing Monads -================== The [[tradition in the functional programming literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to @@ -22,11 +20,10 @@ any case, our emphasis will be on starting with the abstract structure of monads, followed in coming weeks by instances of monads from the philosophical and linguistics literature. -> After you've read this once and are coming back to re-read it to try to digest the details further, the "endofunctors" that slogan is talking about are a combination of our boxes and their associated maps. Their "monoidal" character is captured in the Monad Laws, where a "monoid"---don't confuse with a mon*ad*---is a simpler algebraic notion, meaning a universe with some associative operation that has an identity. For advanced study, here are some further links on the relation between monads as we're working with them and monads as they appear in Category Theory: -[1](http://en.wikipedia.org/wiki/Outline_of_category_theory) -[2](http://lambda1.jimpryor.net/advanced_topics/monads_in_category_theory/) -[3](http://en.wikibooks.org/wiki/Haskell/Category_theory) -[4](https://wiki.haskell.org/Category_theory), where you should follow the further links discussing Functors, Natural Transformations, and Monads. +> After you've read this once and are coming back to re-read it to try to digest the details further, the "endofunctors" that slogan is talking about are a combination of our boxes and their associated `map`s. Their "monoidal" character is captured in the Monad Laws, for which see below. + +[[!toc levels=2]] + ## Box types: type expressions with one free type variable ## @@ -234,7 +231,8 @@ has to obey the following Map Laws: > The first of these says that if you have a triply-boxed type, and you first merge the inner two boxes (with `map join`), and then merge the resulting box with the outermost box, that's the same as if you had first merged the outer two boxes, and then merged the resulting box with the innermost box. The second law says that if you take a box type and wrap a second box around it (with `mid`) and then merge them, that's the same as if you had done nothing, or if you had instead wrapped a second box around each element of the original (with `map mid`, leaving the original box on the outside), and then merged them.

> The Category Theorist would state these Laws like this, where `M` is the endofunctor that takes us from type `α` to type α: > 

μ ○ M(μ) == μ ○ μ
μ ○ η == id == μ ○ M(η)
- > A word of advice: if you're doing any work in this conceptual neighborhood and need a Greek letter, don't use μ. In addition to the preceding usage, there's also a use in recursion theory (for the minimization operator), in type theory (as a fixed point operator for types), and in the λμ-calculus, which is a formal system that deals with _continuations_, which we will focus on later in the course. So μ already exhibits more ambiguity than it can handle. + > A word of advice: if you're doing any work in this conceptual neighborhood and need a Greek letter, don't use μ. In addition to the preceding usage, there's also a use in recursion theory (for the minimization operator), in type theory (as a fixed point operator for types), and in the λμ-calculus, which is a formal system that deals with _continuations_, which we will focus on later in the course. So μ already exhibits more ambiguity than it can handle. + > We link to further reading about the Category Theory origins of Monads below. There isn't any single `mid` function, or single `mbind` function, and so on. For each new box type, this has to be worked out in a useful way. And as we hinted, in many cases the choice of box *type* still leaves some latitude about how they should be defined. We commonly talk about "the List Monad" to mean a combination of the choice of `α list` for the box type and particular definitions for the various functions listed above. There's also "the ZipList MapNable/Applicative" which combines that same box type with other choices for (some of) the functions. Many of these packages also define special-purpose operations that only make sense for that system, but not for other Monads or Mappables. @@ -289,7 +287,7 @@ Here are some other monadic notion that you may sometimes encounter: * Haskell has a notion `>>` definable as `\u v. map (const id) u m$ v`, or as `\u v. u >>= const v`. This is often useful, and `u >> v` won't in general be identical to just `v`. For example, using the box type `List α`, `[1,2,3] >> [4,5] == [4,5,4,5,4,5]`. But in the special case of `mzero`, it is a consequence of what we said above that `anything >> mzero == mzero`. Haskell also calls `>>` `Control.Applicative.*>`. -* Haskell has a correlative notion `Control.Applicative.<*`, definable as `\u v. map const u m$ v`. For example, `[1,2,3] <* [4,5] == [1,1,2,2,3,3]`. You might expect Haskell to call `<*` `<<`, but they don't. They used to use `<<` for `flip (>>)` instead, but now they seem not to use `<<` anymore. +* Haskell has a correlative notion `Control.Applicative.<*`, definable as `\u v. map const u m$ v`. For example, `[1,2,3] <* [4,5] == [1,1,2,2,3,3]`. * mapconst is definable as `map ○ const`. For example `mapconst 4 [1,2,3] == [4,4,4]`. Haskell calls `mapconst` `<$` in `Data.Functor` and `Control.Applicative`. They also use `$>` for `flip mapconst`, and `Control.Monad.void` for `mapconst ()`. @@ -383,3 +381,40 @@ But for some types neither of these will be the case. For function types, as we For the third failure, that is examples of MapNables that aren't Monads, we'll just state that lists where the `map2` operation is taken to be zipping rather than taking the Cartesian product (what in Haskell are called `ZipList`s), these are claimed to exemplify that failure. But we aren't now in a position to demonstrate that to you. + +## Further Reading ## + +As we mentioned above, the notions of Monads have their origin in Category Theory, where they are mostly specified in terms of (what we call) `mid` and `join`. For advanced study, here are some further links on the relation between monads as we're working with them and monads as they appear in Category Theory: +[1](http://en.wikipedia.org/wiki/Outline_of_category_theory) +[2](http://lambda1.jimpryor.net/advanced_topics/monads_in_category_theory/) +[3](http://en.wikibooks.org/wiki/Haskell/Category_theory) +[4](https://wiki.haskell.org/Category_theory), where you should follow the further links discussing Functors, Natural Transformations, and Monads. + +Here are some papers that introduced Monads into functional programming: + +* Eugenio Moggi, Notions of Computation and Monads: Information and Computation 93 (1) 1991. This paper is available online, but would be very difficult reading for members of this seminar, so we won't link to it. However, the next two papers should be accessible. + +* [Philip Wadler. The essence of functional programming](http://homepages.inf.ed.ac.uk/wadler/papers/essence/essence.ps): +invited talk, *19'th Symposium on Principles of Programming Languages*, ACM Press, Albuquerque, January 1992. + + +* [Philip Wadler. Monads for Functional Programming](http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf): +in M. Broy, editor, *Marktoberdorf Summer School on Program Design +Calculi*, Springer Verlag, NATO ASI Series F: Computer and systems +sciences, Volume 118, August 1992. Also in J. Jeuring and E. Meijer, +editors, *Advanced Functional Programming*, Springer Verlag, +LNCS 925, 1995. Some errata fixed August 2001. + + +Here is some other reading: + +* [Haskell wikibook on Monad Laws](http://www.haskell.org/haskellwiki/Monad_Laws). +* [Yet Another Haskell Tutorial on Monad Laws](http://en.wikibooks.org/wiki/Haskell/YAHT/Monads#Definition) +* [Haskell wikibook on Understanding Monads](http://en.wikibooks.org/wiki/Haskell/Understanding_monads) +* [Haskell wikibook on Advanced Monads](http://en.wikibooks.org/wiki/Haskell/Advanced_monads) +* [Haskell wikibook on do-notation](http://en.wikibooks.org/wiki/Haskell/do_Notation) +* [Yet Another Haskell Tutorial on do-notation](http://en.wikibooks.org/wiki/Haskell/YAHT/Monads#Do_Notation) + +There's a long list of monad tutorials linked at the [[Haskell wiki|https://wiki.haskell.org/Monad_tutorials_timeline]] (we linked to this at the top of the page), and on our own [[Offsite Reading]] page. (Skimming the titles is somewhat amusing.) If you are confused by monads, make use of these resources. Read around until you find a tutorial pitched at a level that's helpful for you. -- 2.11.0