Typeclasses
"Key ideas include the following: (1) we will define a safe version of foldr that wil works for any monoid; we’ll see how to associate monoid data (a binary operation, identity element, property proofs) with types, whose values are taken as monoid elements; (4) how to tell Lean to automaticall (implicitly) find and pass monoid data structures to functions depending on the types of other arguments; (5) and ways to use this approach in useful ways."
Should be something like: "Key ideas include the following: (1) we will define a safe version of foldr that will work for any monoid; (2) we’ll see how to associate monoid data (a binary operation, identity element, property proofs) with types, whose values are taken as monoid elements; (3) how to tell Lean to automatically (implicitly) find and pass monoid data structures to functions depending on the types of other arguments; (4) and ways to use this approach in useful ways."
5.1.1. Algebraic Structures
"This chapter will explain how to formalize such structures in Lean, settings patterns for more abstract mathematics as well as for important generalized programming abstractions, as well. For example, we ‘ll see that applicative functor objects extend function application to multiple arguments, and that monads extend function composition to add useful behaviors to it, in turn enabling apparently imperative styles of programming in pure functional languages."
Should be something like: "This chapter will explain how to formalize such structures in Lean, setting patterns for more abstract mathematics as well as for important generalized programming abstractions, as well. For example, we‘ll see that applicative functor objects extend function application to multiple arguments, and that monads extend function composition to add useful behaviors to it, in turn enabling apparently imperative styles of programming in pure functional languages."
I think "settings patterns" is supposed to be "setting patterns", but not 100% sure.
5.1.2. Monoids so far
"Here are examples using these constructs. .First we apply foldr to a monoid α and a list α."
Should be "Here are examples using these constructs. First, we apply foldr to a monoid α and a list α."
5.2. Associating values with types
"We can then use the + and notations to denote whathever operators are recorded in the op field of any given monoid object."
Should be "We can then use the + and * notations to denote whatever operators are recorded in the op field of any given monoid object."
"For this to work (and for some other reasons) we’’ define separate additive and multiplicative monoid types."
Should be: "For this to work (and for some other reasons) we’ll define separate additive and multiplicative monoid types."
5.2.1. Foldr over any monoid
"Finally, given these constraints, we note an real opportunity. "
Should be: "Finally, given these constraints, we note a real opportunity. "
Should be something like: "Key ideas include the following: (1) we will define a safe version of foldr that will work for any monoid; (2) we’ll see how to associate monoid data (a binary operation, identity element, property proofs) with types, whose values are taken as monoid elements; (3) how to tell Lean to automatically (implicitly) find and pass monoid data structures to functions depending on the types of other arguments; (4) and ways to use this approach in useful ways."
5.1.1. Algebraic Structures "This chapter will explain how to formalize such structures in Lean, settings patterns for more abstract mathematics as well as for important generalized programming abstractions, as well. For example, we ‘ll see that applicative functor objects extend function application to multiple arguments, and that monads extend function composition to add useful behaviors to it, in turn enabling apparently imperative styles of programming in pure functional languages."
Should be something like: "This chapter will explain how to formalize such structures in Lean, setting patterns for more abstract mathematics as well as for important generalized programming abstractions, as well. For example, we‘ll see that applicative functor objects extend function application to multiple arguments, and that monads extend function composition to add useful behaviors to it, in turn enabling apparently imperative styles of programming in pure functional languages." I think "settings patterns" is supposed to be "setting patterns", but not 100% sure.
5.1.2. Monoids so far "Here are examples using these constructs. .First we apply foldr to a monoid α and a list α."
Should be "Here are examples using these constructs. First, we apply foldr to a monoid α and a list α."
5.2. Associating values with types "We can then use the + and notations to denote whathever operators are recorded in the op field of any given monoid object."
Should be "We can then use the + and * notations to denote whatever operators are recorded in the op field of any given monoid object."
"For this to work (and for some other reasons) we’’ define separate additive and multiplicative monoid types."
Should be: "For this to work (and for some other reasons) we’ll define separate additive and multiplicative monoid types."
5.2.1. Foldr over any monoid "Finally, given these constraints, we note an real opportunity. "
Should be: "Finally, given these constraints, we note a real opportunity. "