docs(category/monad,bitraversable): add module docstrings #1260 (#1286)

* docs(category/monad,bitraversable): add module docstrings

* more docs

* still more doc

* doc about traversable

Author: cipher1024

src/category/bitraversable/basic.lean

@@ -2,15 +2,39 @@
 Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
-
-Functors with two arguments
 -/
 
 import category.functor
        category.bifunctor
        category.traversable.basic
        tactic.basic
 
+/-!
+# Bitraversable type class
+
+Type class for traversing bifunctors. The concepts and laws are taken from
+https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html
+
+Simple examples of `bitraversable` are `prod` and `sum`. A more elaborate example is
+to define an a-list as:
+
+```
+def alist (key val : Type) := list (key × val)
+```
+
+Then we can use `f : key → io key'` and `g : val → io val'` to manipulate the `alist`'s key
+and value respectively with `bitraverse f g : alist key val → io (alist key' val')`
+
+## Main definitions
+  * bitraversable - exposes the `bitraverse` function
+  * is_lawful_bitraversable - laws similar to is_lawful_traversable
+
+## Tags
+
+traversable bitraversable iterator functor bifunctor applicative
+
+-/
+
 universes u
 
 class bitraversable (t : Type u → Type u → Type u)

src/category/bitraversable/instances.lean

@@ -1,8 +1,36 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
 import category.bitraversable.basic
        category.bitraversable.lemmas
        category.traversable.lemmas
        tactic.solve_by_elim
 
+/-!
+# bitraversable instances
+
+## Instances
+
+ * prod
+ * sum
+ * const
+ * flip
+ * bicompl
+ * bicompr
+
+## References
+
+ * Hackage: https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html
+
+## Tags
+
+traversable bitraversable functor bifunctor applicative
+
+-/
+
 universes u v w
 
 variables {t : Type u → Type u → Type u} [bitraversable t]

src/category/bitraversable/lemmas.lean

@@ -1,5 +1,38 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
 import category.bitraversable.basic
 
+/-!
+# Bitraversable Lemmas
+
+## Main definitions
+  * tfst - traverse on first functor argument
+  * tsnd - traverse on second functor argument
+
+## Lemmas
+
+Combination of
+  * bitraverse
+  * tfst
+  * tsnd
+
+with the applicatives `id` and `comp`
+
+## References
+
+ * Hackage: https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html
+
+## Tags
+
+traversable bitraversable functor bifunctor applicative
+
+
+-/
+
 universes u
 
 variables {t : Type u → Type u → Type u} [bitraversable t]
@@ -10,12 +43,12 @@ open functor is_lawful_applicative
 variables {F G : Type u → Type u}
           [applicative F] [applicative G]
 
-@[reducible]
-def tfst {α α'} (f : α → F α') : t α β → F (t α' β) :=
+/-- traverse on the first functor argument -/
+@[reducible] def tfst {α α'} (f : α → F α') : t α β → F (t α' β) :=
 bitraverse f pure
 
-@[reducible]
-def tsnd {α α'} (f : α → F α') : t β α → F (t β α') :=
+/-- traverse on the second functor argument -/
+@[reducible] def tsnd {α α'} (f : α → F α') : t β α → F (t β α') :=
 bitraverse pure f
 
 variables [is_lawful_bitraversable t]

src/category/monad/basic.lean

@@ -1,9 +1,47 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
 
 import tactic.basic
 
+/-!
+# Monad
+
+## Attributes
+
+ * extensionality
+ * functor_norm
+ * monad_norm
+
+## Implementation Details
+
+Set of rewrite rules and automation for monads in general and
+`reader_t`, `state_t`, `except_t` and `option_t` in particular.
+
+The rewrite rules for monads are carefully chosen so that `simp with
+functor_norm` will not introduce monadic vocabulary in a context where
+applicatives would do just fine but will handle monadic notation
+already present in an expression.
+
+In a context where monadic reasoning is desired `simp with monad_norm`
+will translate functor and applicative notation into monad notation
+and use regular `functor_norm` rules as well.
+
+## Tags
+
+functor, applicative, monad, simp
+
+-/
+
+run_cmd mk_simp_attr `monad_norm [`functor_norm]
+
 attribute [extensionality] reader_t.ext state_t.ext except_t.ext option_t.ext
 attribute [functor_norm]   bind_assoc pure_bind bind_pure
+attribute [monad_norm] seq_eq_bind_map
 universes u v
 
+@[monad_norm]
 lemma map_eq_bind_pure_comp (m : Type u → Type v) [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (x : m α) :
   f <$> x = x >>= pure ∘ f := by rw bind_pure_comp_eq_map

src/category/traversable/basic.lean

@@ -2,14 +2,53 @@
 Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
-
-Type classes for traversing collections. The concepts and laws are taken from
-http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Traversable.html
 -/
 
 import tactic.cache
 import category.applicative
 
+/-!
+# Traversable type class
+
+Type classes for traversing collections. The concepts and laws are taken from
+http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Traversable.html
+
+Traversable collections are a generalization of functors. Whereas
+functors (such as `list`) allow us to apply a function to every
+element, it does not allow functions which external effects encoded in
+a monad. Consider for instance a functor `invite : email -> io response`
+that takes an email address, sends an email and wait for a
+response. If we have a list `guests : list email`, using calling
+`invite` using `map` gives us the following: `map invite guests : list
+(io response)`.  It is not what we need. We need something of type `io
+(list response)`. Instead of using `map`, we can use `traverse` to
+send all the invites: `traverse invite guests : io (list response)`.
+`traverse` applies `invite` to every element of `guests` and combines
+all the resulting effects. In the example, the effect is encoded in the
+monad `io` but any applicative functor is accepted by `traverse`.
+
+For more on how to use traversable, consider the Haskell tutorial:
+https://en.wikibooks.org/wiki/Haskell/Traversable
+
+## Main definitions
+  * `traversable` type class - exposes the `traverse` function
+  * `sequence` - based on `traverse`, turns a collection of effects into an effect returning a collection
+  * is_lawful_traversable - laws
+
+## Tags
+
+traversable iterator functor applicative
+
+## References
+
+ * "Applicative Programming with Effects", by Conor McBride and Ross Paterson, Journal of Functional Programming 18:1 (2008) 1-13, online at http://www.soi.city.ac.uk/~ross/papers/Applicative.html.
+ * "The Essence of the Iterator Pattern", by Jeremy Gibbons and Bruno Oliveira, in Mathematically-Structured Functional Programming, 2006, online at http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/#iterator.
+ * "An Investigation of the Laws of Traversals", by Mauro Jaskelioff and Ondrej Rypacek, in Mathematically-Structured Functional Programming, 2012, online at http://arxiv.org/pdf/1202.2919.
+Synopsis
+
+
+-/
+
 open function (hiding comp)
 
 universes u v w