doc: fix typos and do some polish on wording (#1568)

doc/monads/applicatives.lean

@@ -8,7 +8,7 @@ Let's see how they work!
 
 ## What is an Applicative Functor?
 
-An applicative functor is an defines a default or "base" construction for an object and allows
+An applicative functor defines a default or "base" construction for an object and allows
 function application to be chained across multiple instances of the structure. All applicative
 functors are functors, meaning they must also support the "map" operation.
 
@@ -29,24 +29,30 @@ simply from outside the structure, as was the case with `Functor.map`.
 
 Applicative in Lean is built on some helper type classes, `Functor`, `Pure` and `Seq`:
 
-```lean,ignore
+-/
+namespace hidden -- hidden
 class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
-```
-
+  map      := fun x y => Seq.seq (pure x) fun _ => y
+  seqLeft  := fun a b => Seq.seq (Functor.map (Function.const _) a) b
+  seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b
+end hidden -- hidden
+/-!
 Notice that as with `Functor` it is also a type transformer `(f : Type u → Type v)` and notice the
-`extends Functor f` is ensuring the base Functor also performs that same type transformation.
+`extends Functor f` is ensuring the base `Functor` also performs that same type transformation.
 
 As stated above, all applicatives are then functors. This means you can assume that `map` already
 exists for all these types.
 
 The `Pure` base type class is a very simple type class that supplies the `pure` function.
 
-```lean,ignore
+-/
+namespace hidden -- hidden
 class Pure (f : Type u → Type v) where
    pure {α : Type u} : α → f α
-```
+end hidden -- hidden
+/-!
 
-You can think of it as lifing the result of a pure value to some monadic type. The simplest example
+You can think of it as lifting the result of a pure value to some monadic type. The simplest example
 of `pure` is the `Option` type:
 
 -/
@@ -65,10 +71,12 @@ instance : Monad Option where
 The `Seq` type class is also a simple type class that provides the `seq` operator which can
 also be written using the special syntax `<*>`.
 
-```lean,ignore
+-/
+namespace hidden -- hidden
 class Seq (f : Type u → Type v) : Type (max (u+1) v) where
   seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
-```
+end hidden -- hidden
+/-!
 
 
 ## Basic Applicative Examples
@@ -248,7 +256,7 @@ Applicative functor.
 
 You may remember seeing the `SeqLeft` and `SeqRight` base types on `class Applicative` earlier.
 These provide the `seqLeft` and `seqRight` operations which also have some handy notation
-shorthands `<*` and `*>` repsectively. Where: `x <* y` evaluates `x`, then `y`, and returns the
+shorthands `<*` and `*>` respectively. Where: `x <* y` evaluates `x`, then `y`, and returns the
 result of `x` and `x *> y` evaluates `x`, then `y`,  and returns the result of `y`.
 
 To make it easier to remember, notice that it returns that value that the `<*` or `*>` notation is
@@ -284,7 +292,7 @@ using `Seq.seq` you will see somthing interesting:
 #eval Seq.seq ((.*.) <$> some 4) (fun (_ : Unit) => some 5) -- some 20
 /-!
 
-This may look a bit combersome, specifically, why did we need to invent this funny looking function
+This may look a bit cumbersome, specifically, why did we need to invent this funny looking function
 `fun (_ : Unit) => (some 5)`?
 
 Well if you take a close look at the type class definition:

doc/monads/except.lean

@@ -48,6 +48,7 @@ And now you can run this test and get the expected exception:
 #eval test      -- Except.error "can't divide by zero"
 /-!
 
+
 ## Chaining
 
 Now as before you can build a chain of monadic actions that can be composed together using `bind (>>=)`:
@@ -70,7 +71,17 @@ def chainUsingDoNotation := do
 
 /-!
 Notice in the second `divide 6 0` the exception from that division was nicely propagated along
-to the final result and the square function was pretty much ignored in that case.
+to the final result and the square function was ignored in that case.  You can see why the
+`square` function was ignored if you look at the implementation of `Except.bind`:
+-/
+def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
+  match ma with
+  | Except.error err => Except.error err
+  | Except.ok v      => f v
+/-!
+
+Specifically notice that it only calls the next function `f v` in the `Except.ok`, and
+in the error case it simply passes the same error along.
 
 Remember also that you can chain the actions with implicit binding by using the `do` notation
 as you see in the `chainUsingDoNotation` function above.
@@ -78,7 +89,7 @@ as you see in the `chainUsingDoNotation` function above.
 ## Try/Catch
 
 Now with all good exception handling you also want to be able to catch exceptions so your program
-can try continue on or do some error recovery task, which you can do like this:
+can continue on or do some error recovery task, which you can do like this:
 -/
 def testCatch :=
   try
@@ -128,7 +139,8 @@ def testUnwrap : String := Id.run do
 
 The `Id.run` function is a helper function that executes the `do` block and returns the result where
 `Id` is the _identity monad_.  So `Id.run do` is a pattern you can use to execute monads in a
-function that is not itself monadic.
+function that is not itself monadic.  This works for all monads except `IO` which, as stated earlier,
+you cannot invent out of thin air, you must use the `IO` monad given to your `main` function.
 
 ## Monadic functions
 
@@ -161,6 +173,6 @@ def forM [Monad m] (as : List α) (f : α → m PUnit) : m PUnit :=
 Now that you know all these different monad constructs, you might be wondering how you can combine
 them. What if there was some part of your state that you wanted to be able to modify (using the
 State monad), but you also needed exception handling. How can you get multiple monadic capabilities
-in the same fuunction. To learn the answer, head to [Monad Transformers](transformers.lean.md).
+in the same function. To learn the answer, head to [Monad Transformers](transformers.lean.md).
 
 -/

doc/monads/functors.lean

@@ -172,7 +172,7 @@ and now bringing it all together you can use the simple function `squareFeetToMe
 
 Lean also defines custom infix operator `<$>` for `Functor.map` which allows you to write this:
 -/
-#eval (fun s => s.length) <$> ["elephant", "tiger", "giraffe"]
+#eval (fun s => s.length) <$> ["elephant", "tiger", "giraffe"] -- [8, 5, 7]
 #eval (fun x => x + 1) <$> (some 5) -- some 6
 /-!
 
@@ -213,7 +213,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
 Note that `mapConst` has a default implementation, namely:
 `mapConst : {α β : Type u} → α → f β → f α := Function.comp map (Function.const _)` in the `Functor`
 type class.  So you can use this default implementation and you only need to replace it if
-your Functors has a more specialized variant than this which is more performant.
+your functor has a more specialized variant than this (usually the custom version is more performant).
 
 In general then, a functor is a function on types `F : Type u → Type v` equipped with an operator
 called `map` such that if you have a function `f` of type `α → β` then `map f` will convert your

doc/monads/intro.md

@@ -29,7 +29,7 @@ still be summed up in a couple simple functions.  Here you will learn how to cre
 
 ## [Monads Tutorial](monads.lean.md)
 Now that you have an intuition for how abstract structures work, you'll examine some of the problems
-that functors and applicative functors don't help you solve. Then you'll lean the specifics of how
+that functors and applicative functors don't help you solve. Then you'll learn the specifics of how
 to actually use monads with some examples using the `Option` monad and the all important `IO` monad.
 
 ## [Reader Monads](readers.lean.md)
@@ -45,19 +45,19 @@ of the things a function programming language supposedly "can't" do.
 ## [Except Monad](except.lean.md)
 
 Similar to the `Option` monad the `Except` monad allows you to change the signature of a function so
-that it can return an `ok` value or an `error` and it makes available the classic exception handling
+that it can return an `ok` value or an `error` and it provides the classic exception handling
 operations `throw/try/catch` so that your programs can do monad-based exception handling.
 
 ## [Monad Transformers](transformers.lean.md)
 
-Now that you are familiar with all the above monads it is time to answer the question of how you can
-make them work together. After all, there are definitely times when you need multiple kinds of
+Now that you are familiar with all the above monads it is time to answer the question - how you can
+make them work together? After all, there are definitely times when you need multiple kinds of
 monadic behavior. This section introduces the concept of monad transformers, which allow you to
 combine multiple monads into one.
 
 ## [Monad Laws](laws.lean.md)
-This section examines what makes a monad a monad. After all, can't you just implement these type
-classes any way you want and write a "monad" instance? Starting back with functors and applicative
-functors, you'll learn that all these structures have "laws" that they are expected to obey with
-respect to their behavior. You can make instances that don't follow these laws. But you do so at
-your peril, as other programmers will be very confused when they try to use them.
+This section examines what makes a monad a legal monad. You could just implement your monadic type
+classes any way you want and write "monad" instances, but starting back with functors and
+applicative functors, you'll learn that all these structures have "laws" that they are expected to
+obey with respect to their behavior. You can make instances that don't follow these laws. But you do
+so at your peril, as other programmers will be very confused when they try to use them.

doc/monads/laws.lean

@@ -46,7 +46,7 @@ as you will see below.
 
 Functors have two laws: the _identity_ law, and the _composition_ law. These laws express behaviors that
 your functor instances should follow. If they don't, other programmers will be very confused at the
-effect your instances have on their program. Many structures have similar laws, including monads.
+effect your instances have on their program.
 
 The identity law says that if you "map" the identity function (`id`) over your functor, the
 resulting functor should be the same. A succinct way of showing this on a `List` functor is:
@@ -65,7 +65,7 @@ def p1 : Point Nat := (Point.mk 1 2)
 #eval id <$> p1 == p1 -- false
 
 /-!
-Oh, and look while the List is behaving well, the `Point` functor fails this identity test.
+Oh, and look while the `List` is behaving well, the `Point` functor fails this identity test.
 
 The _composition_ law says that if you "map" two functions in succession over a functor, this
 should be the same as "composing" the functions and simply mapping that one super-function over the
@@ -149,9 +149,9 @@ example [Applicative m] [LawfulApplicative m] (v : m α) :
 
 `pure f <*> pure x = pure (f x)`
 
-Suppose you wrap a function and an object in pure. You can then apply the wrapped function over the
+Suppose you wrap a function and an object in `pure`. You can then apply the wrapped function over the
 wrapped object. Of course, you could also apply the normal function over the normal object, and then
-wrap it in pure. The homomorphism law states these results should be the same.
+wrap it in `pure`. The homomorphism law states these results should be the same.
 
 For example:
 
@@ -238,8 +238,12 @@ instance : Monad List  where
   pure := List.pure
   bind := List.bind
 
-#eval ["apple", "orange"] >>= pure  -- ["apple", "orange"]
-#eval [1,2,3] >>= pure              -- [1,2,3]
+def a := ["apple", "orange"]
+
+#eval a >>= pure      -- ["apple", "orange"]
+
+#eval a >>= pure = a  -- true
+
 /-!
 
 ### Right Identity
@@ -252,7 +256,7 @@ def z := 5
 #eval pure z >>= h                  -- some 6
 #eval h z                           -- some 6
 
-#eval pure z >>= h = h x            -- true
+#eval pure z >>= h = h z            -- true
 /-!
 
 So in this example, with this specific `z` and `h`, you see that the rule holds true.
@@ -312,7 +316,7 @@ There are two main ideas from all the laws:
 1. It should not matter what order you group operations in.  Another way to state this is function
    composition should hold across your structures.
 
-Following these laws will ensure other programmers are not confused by the bahavior of your
+Following these laws will ensure other programmers are not confused by the behavior of your
 new functors, applicatives and monads.
 
 -/

doc/monads/monads.lean

@@ -62,8 +62,8 @@ some kind.  Let's examine those function types:
 So `map` is a pure function, `seq` is a pure function wrapped in the structure, and `bind` takes a
 pure input but produces an output wrapped in the structure.
 
-Note: we are ignoring the `(Unit → f α)` function also used by `seq` in this comparison, since that
-was explained in [Applicatives Lazy Evaluation](applicatives.lean.md#lazy-evaluation).
+Note: we are ignoring the `(Unit → f α)` function used by `seq` here since that has a special
+purpose explained in [Applicatives Lazy Evaluation](applicatives.lean.md#lazy-evaluation).
 
 ## Basic Monad Example
 

doc/monads/readers.lean

@@ -3,13 +3,13 @@
 
 In the [previous section](monads.lean.md) you learned about the conceptual idea of monads. You learned
 what they are, and saw how some common types like `IO` and `Option` work as monads. Now in this
-part, you will be looking at some other useful monads. In particular, the `ReaderM` monad.
+section, you will be looking at some other useful monads. In particular, the `ReaderM` monad.
 
 ## How to do Global Variables in Lean?
 
 In Lean, your code is generally "pure", meaning functions can only interact with the arguments
 passed to them. This effectively means you cannot have global variables. You can have global
-definitions, but these are fixed at compile time. If some user behavior might change them, you have
+definitions, but these are fixed at compile time. If some user behavior might change them, you would have
 to wrap them in the `IO` monad, which means they can't be used from pure code.
 
 Consider this example. Here, you want to have an `Environment` containing different parameters as a
@@ -93,7 +93,7 @@ def main2 : IO Unit := do
 #eval main2 -- Result: 7538
 /-!
 The `ReaderM` monad provides a `run` method and it is the `ReaderM` run method that takes the initial
-`Environment` context.  So here you see `main2` loads the environment as before, and estabilishes
+`Environment` context.  So here you see `main2` loads the environment as before, and establishes
 the `ReaderM` context by passing `env` to the `run` method.
 
 > **Side note 1**: The `return` statement used above also needs some explanation.  The `return`
@@ -111,7 +111,7 @@ the monadic container type.
 
 > **Side note 2**: If the function `readerFunc3` also took some explicit arguments then you would have
 to write `(readerFunc3 args).run env` and this is a bit ugly, so Lean provides an infix operator
-`|>` that eliminiates those parens so you can write `readerFunc3 args |>.run env` and then you can
+`|>` that eliminates those parentheses so you can write `readerFunc3 args |>.run env` and then you can
 chain multiple monadic actions like this `m1 args1 |>.run args2 |>.run args3` and this is the
 recommended style.  You will see this patten used heavily in Lean code.
 
@@ -122,8 +122,7 @@ become available only when you are in the context of that monad.
 Here the `readerFunc2` function uses the `bind` operator `>>=` just to show you that there are bind
 operations happening here.  The `readerFunc3` function uses the `do` notation you learned about in
 [Monads](monads.lean.md) which hides that bind operation and can make the code look cleaner.
-
-The `do` notation with `let x ← readerFunc2` is also calling the `bind` function under the covers,
+So the expression `let x ← readerFunc2` is also calling the `bind` function under the covers,
 so that you can access the unwrapped value `x` needed for the `toString x` conversion.
 
 The important difference here to the earlier code is that `readerFunc3` and `readerFunc2` no longer
@@ -149,7 +148,7 @@ Now, remember in Lean that a function that takes an argument of type `Nat` and r
 like `def f (a : Nat) : String` is the same as this function `def f : Nat → String`.  These are
 exactly equal as types.  Well this is being used by the `ReaderM` Monad to add an input argument to
 all the functions that use the `ReaderM` monad and this is why `main` is able to start things off by
-simply passing that new input argument in `readerFunc3 env`. So now that you know the implementation
+simply passing that new input argument in `readerFunc3.run env`. So now that you know the implementation
 details of the `ReaderM` monad you can see that what it is doing looks very much like the original
 code we wrote at the beginning of this section, only it's taking a lot of the tedious work off your
 plate and it is creating a nice clean separation between what your pure functions are doing, and the
@@ -158,7 +157,7 @@ global context idea that the `ReaderM` adds.
 ## withReader
 
 One `ReaderM` function can call another with a modified version of the `ReaderM` context. You can
-use the `withReader` function from the `MonadWithReader` typeclass to do this:
+use the `withReader` function from the `MonadWithReader` type class to do this:
 
 -/
 def readerFunc3WithReader : ReaderM Environment String := do
@@ -166,8 +165,8 @@ def readerFunc3WithReader : ReaderM Environment String := do
   return "Result: " ++ toString x
 
 /-!
-Here we changed the `user` in the `Environment` context to "new user" and then we
-passed that modified context to `readerFunc2`.
+Here we changed the `user` in the `Environment` context to "new user" and then we passed that
+modified context to `readerFunc2`.
 
 So `withReader f m` executes monad `m` in the `ReaderM` context modified by `f`.
 
@@ -189,6 +188,12 @@ find that in larger code bases, with many different types of monads all composed
 greatly cleans up the code. Monads provide a beautiful functional way of managing cross-cutting
 concerns that would otherwise make your code very messy.
 
+Having this control over the inherited `ReaderM` context via `withReader` is actually very useful
+and something that is quite messy if you try and do this sort of thing with global variables, saving
+the old value, setting the new one, calling the function, then restoring the old value, making sure
+you do that in a try/finally block and so on. The `ReaderM` design pattern avoids that mess
+entirely.
+
 Now it's time to move on to [StateM Monad](states.lean.md) which is like a `ReaderM` that is
 also updatable.
 -/

doc/monads/states.lean

@@ -9,7 +9,7 @@ part, you will explore the `StateM` monad, which is like a `ReaderM` only the st
 
 ## Motivating example: Tic Tac Toe
 
-For this part, let's build a simple model for a Tic Tace Toe game. The main object is the `GameState`
+For this section, let's build a simple model for a Tic Tace Toe game. The main object is the `GameState`
 data type containing several important pieces of information. First and foremost, it has the
 "board", a map from 2D tile indices to the "Tile State" (X, O or empty). Then it also knows the
 current player, and it has a random generator.
@@ -59,7 +59,7 @@ provide an initial state, in addition to the computation to run. `StateM` then p
 the result of the computation combined with the final updated state.
 
 If you wish to discard the final state and just get the computation's result, you can use
-`run'` method instead.  Yes in Lean, the apostraphe can be part of a name, you read this "run
+`run'` method instead.  Yes in Lean, the apostrophe can be part of a name, you read this "run
 prime", and the general naming convention is that the prime method discards something.
 
 So for your Tic Tac Toe game, many of your functions will have a signature like `State GameState a`.
@@ -115,12 +115,16 @@ So finally, you can combine these functions together with `do` notation, and it
 clean! You don't need to worry about the side effects. The different monadic functions handle them.
 Here's a sample of what your function might look like to play one turn of the game. At the end, it
 returns a boolean determining if all the spaces have been filled.
+
+Notice in `isGameDone` and `nextTurn` we have stopped providing the full return type
+`StateM GameState Unit`.  This is because Lean is able to infer the correct monadic return type
+from the context and as a result the code is now looking really clean.
 -/
 
-def isGameDone : StateM GameState Bool := do
+def isGameDone := do
   return (← findOpen).isEmpty
 
-def nextTurn : StateM GameState Bool := do
+def nextTurn := do
   let i ← chooseRandomMove
   applyMove i
   isGameDone
@@ -149,7 +153,7 @@ def printBoard (board : Board) : IO Unit := do
       IO.println row
       row := []
 
-def playGame : StateM GameState Unit := do
+def playGame := do
   while true do
     let finished ← nextTurn
     if finished then return
@@ -186,10 +190,8 @@ at the reduced Type for `nextTurn`:
 So a function like `nextTurn` that might have just returned a `Bool` has been modified by the
 `StateM` monad such that the initial `GameState` is passed in as a new input argument, and the output
 value has been changed to the pair `Bool × GameState` so that it can return the pure `Bool` and the
-updated `GameState`.  This is why the call to `nextTurn` looks like this: `let (_, g) := nextTurn gs`.
-This expression `(_, g)` conveniently breaks the pair up into 2 values, it doesn't care what the first
-value is (hence the underscore `_`), but it does need the updated state `g` which you can then assign
-back to the mutable `gs` variable to use next time around this loop.
+updated `GameState`.  So `playGame` then is automatically saving that updated game state so that each
+time around the `while` loop it is acting on the new state, otherwise that would be an infinite loop!
 
 It is also interesting to see how much work the `do` and `←` notation are doing for you.  To
 implement the `nextTurn` function without these you would have to write this, manually plumbing
@@ -204,6 +206,12 @@ def nextTurnManually : StateM GameState Bool
 
 /-!
 
+This expression `let (i, gs)` conveniently breaks a returned pair up into 2 variables.
+In the expression `let (_, gs')` we didn't care what the first value was so we used underscore.
+Notice that nextTurn is capturing the updated game state from `chooseRandomMove` in the variable
+`gs`, which it is then passing to `applyMove` which returns `gs'` which is passed to `isGameDone`
+and that function returns `gs''` which we then return from `nextTurnManually`.  Phew, what a lot
+of work you don't have to do when you use `do` notation!
 
 ## StateM vs ReaderM
 
@@ -220,6 +228,11 @@ In this function `chooseRandomMove` is modifying the state that `applyMove` is g
 and `chooseRandomMove` knows nothing about `applyMove`.  So `StateM` functions can have this
 kind of downstream effect outside their own scope, whereas, `withReader` cannot do that.
 
+So there is no equivalent to `withReader` for `StateM`, besides you can always use the `StateM`
+`set` function to modify the state before calling the next function anyway.  You could however,
+manually call a `StateM` function like you see in `nextTurnManually` and completely override
+the state at any point that way.
+
 ## State, IO and other languages
 
 When thinking about Lean, it is often seen as a restriction that you can't have global variables or
@@ -242,7 +255,7 @@ your code cannot communicate with the outside world, you can be far more certain
 The `StateM` monad is also a more disciplined way of managing side effects. Top level code could
 call a `StateM` function multiple times with different independent initial states, even doing that
 across multiple tasks in parallel and each of these cannot clobber the state belonging to other
-tasks. Monadic code is more reusable than code that uses global variables.
+tasks. Monadic code is more predictable and reusable than code that uses global variables.
 
 ## Summary
 

doc/monads/transformers.lean

@@ -117,7 +117,7 @@ lifting.  You already used lifting in the above code, because you were able to c
 `parseArguments` which has a bigger type `StateT Config (ReaderT Arguments (Except String))`.
 This "just worked" because Lean did some magic with monad lifting.
 
-To give you a simpler example of this, suppose you have the following funciton:
+To give you a simpler example of this, suppose you have the following function:
 -/
 def divide (x : Float ) (y : Float): ExceptT String Id Float :=
   if y == 0 then
@@ -193,9 +193,9 @@ If you have an instance `MonadLift m n` that means there is a way to turn a comp
 inside of `m` into one that happens inside of `n` and (this is the key part) usually *without* the
 instance itself creating any additional data that feeds into the computation. This means you can in
 principle declare lifting instances from any monad to any other monad, it does not, however, mean
-that you should do this in all cases.  You can get a report from Lean of how all this was done by
-add the line `set_option trace.Meta.synthInstance true in` before main and moving the
-cursor to the end of the first line after `do` and you will see a nice detailed report.
+that you should do this in all cases.  You can get a very nice report on how all this was done by
+adding the line `set_option trace.Meta.synthInstance true in` before `divideCounter` and moving you
+cursor to the end of the first line after `do`.
 
 This was a lot of detail, but it is very important to understand how monad lifting works because it
 is used heavily in Lean programs.
@@ -225,7 +225,7 @@ instance  : MonadLift m (ReaderT ρ m) where
 This lift operation creates a function that defines the required `ReaderT` input
 argument, but the inner monad doesn't know or care about `ReaderT` so the
 monadLift function throws it away with the `_` then calls the inner monad action `x`.
-This is a perfectly legal and trivial way to implement a `ReaderM` monad.
+This is a perfectly legal implementation of the `ReaderM` monad.
 
 ## Add your own Custom MonadLift
 
@@ -270,10 +270,10 @@ def main3 : IO Unit := do
 #eval main3 -- (2.500000, 1)
 /-!
 
-It turns out that the `IO` monad you see in your `main` function is based on a `Result` type
+It turns out that the `IO` monad you see in your `main` function is based on the `EStateM.Result` type
 which is similar to the `Except` type but it has an additional return value. The `liftIO` function
 converts any `Except String α` into `IO α` by simply mapping the ok case of the `Except` to the
-`Result.ok` and the error case to the Result.error.
+`Result.ok` and the error case to the `Result.error`.
 
 ## Lifting ExceptT