Changes to Getting To Know Lean

book/FPLean/GettingToKnow/Polymorphism.lean

@@ -479,15 +479,15 @@ tag := "prod"
 %%%
 
 The {anchorName Prod}`Prod` structure, short for “Product”, is a generic way of joining two values together.
-For instance, a {anchorTerm fragments}`Prod Nat String` contains a {anchorName fragments}`Nat` and a {anchorName fragments}`String`.
-In other words, {anchorTerm natPoint}`PPoint Nat` could be replaced by {anchorTerm fragments}`Prod Nat Nat`.
+For instance, a {anchorTerm fragments}`Prod Nat String` contains a {anchorName fragments}`Nat` and a {anchorName fragments}`String` in a {anchorName Prod}`Prod` structure.
+Using {anchorTerm fragments}`Prod Nat Nat` would computally be the same as using our {anchorTerm natPoint}`PPoint Nat`.
+However, many applications are best served by defining their own structures, even for simple cases like {anchorName Point}`Point`, because using domain terminology can make it easier to read the code.
+Additionally, defining structure types helps catch more errors by assigning different types to different domain concepts, even if they are of a similar body, preventing them from being mixed up.
 {anchorName fragments}`Prod` is very much like C#'s tuples, the {Kotlin}`Pair` and {Kotlin}`Triple` types in Kotlin, and {cpp}`tuple` in C++.
-Many applications are best served by defining their own structures, even for simple cases like {anchorName Point}`Point`, because using domain terminology can make it easier to read the code.
-Additionally, defining structure types helps catch more errors by assigning different types to different domain concepts, preventing them from being mixed up.
 
 On the other hand, there are some cases where it is not worth the overhead of defining a new type.
-Additionally, some libraries are sufficiently generic that there is no more specific concept than “pair”.
-Finally, the standard library contains a variety of convenience functions that make it easier to work with the built-in pair type.
+Additionally, a standard library can contains a variety of convenience functions that make it easier to work with the built-in pair type of the language.
+Finally, some libraries are sufficiently generic that there is no more specific concept than “pair”.
 
 :::paragraph
 The structure {anchorName Prod}`Prod` is defined with two type arguments:
@@ -501,11 +501,12 @@ structure Prod (α : Type) (β : Type) : Type where
 :::
 
 :::paragraph
-Lists are used so frequently that there is special syntax to make them more readable.
+These names are abbreviations for "first" and "second".
+Lists are used so frequently that there is special syntax to make them more readable ({lit}`[a, b, c]`, {lit}`::`, etc).
 For the same reason, both the product type and its constructor have special syntax.
-The type {anchorTerm ProdSugar}`Prod α β` is typically written {anchorTerm ProdSugar}`α × β`, mirroring the usual notation for a Cartesian product of sets.
-Similarly, the usual mathematical notation for pairs is available for {anchorName ProdSugar}`Prod`.
-In other words, instead of writing:
+The type {anchorTerm ProdSugar}`Prod α β` is typically written {anchorTerm ProdSugar}`α × β`, mirroring the usual notation for a [Cartesian product](https://en.wikipedia.org/wiki/Cartesian_product) of sets.
+Similarly, the usual [mathematical notation](https://en.wikipedia.org/wiki/Ordered_pair) for pairs is available for {anchorName ProdSugar}`Prod`.
+Meaning, instead of writing:
 
 ```anchor fivesStruct
 def fives : String × Int := { fst := "five", snd := 5 }
@@ -592,6 +593,7 @@ def howManyDogs (pets : List PetName) : Nat :=
 
 Function calls are evaluated before infix operators, so {anchorTerm howManyDogsAdd}`howManyDogs morePets + 1` is the same as {anchorTerm howManyDogsAdd}`(howManyDogs morePets) + 1`.
 As expected, {anchor dogCount}`#eval howManyDogs animals` yields {anchorInfo dogCount}`3`.
+Infix operators and precedences values will be explained in {ref "Refer to modad -> Infix Operators"}[Infix operator]
 :::
 
 ## {anchorName Unit}`Unit`
@@ -621,17 +623,26 @@ inductive ArithExpr (ann : Type) : Type where
   | times : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
 ```
 
-The type argument {anchorName ArithExpr}`ann` stands for annotations, and each constructor is annotated.
-Expressions coming from a parser might be annotated with source locations, so a return type of {anchorTerm ArithExprEx}`ArithExpr SourcePos` ensures that the parser put a {anchorName ArithExprEx}`SourcePos` at each subexpression.
-Expressions that don't come from the parser, however, will not have source locations, so their type can be {anchorTerm ArithExprEx}`ArithExpr Unit`.
+The type argument {anchorName ArithExpr}`ann` stands for annotations, and each constructor having it is therefore _annotated_.
+An anotation can be anything useful, expressions coming from a parser might be annotated with source locations (a line and column number from a source code file), so a return type of {anchorTerm ArithExprEx}`ArithExpr SourcePos` ensures that the parser put a {anchorName ArithExprEx}`SourcePos` at each subexpression, allowing access to the location of each in a hypothetical source code for different reasons.
+
+Expressions that don't come from the parser, however, may not have source locations, so their type can be {anchorTerm ArithExprEx}`ArithExpr Unit`:
+
+```anchor ArithExprVal
+def toEval := (ArithExpr.times () (ArithExpr.int () 2) (ArithExpr.int () 3))
+#check toEval
+```
+```anchorInfo ArithExprVal
+toEval : ArithExpr Unit
+```
+Unit's constructor can be written as empty parentheses: {anchorTerm unitParens}`() : Unit`.
 
 :::
 
 Additionally, because all Lean functions have arguments, zero-argument functions in other languages can be represented as functions that take a {anchorName ArithExprEx}`Unit` argument.
 In a return position, the {anchorName ArithExprEx}`Unit` type is similar to {CSharp}`void` in languages derived from C.
 In the C family, a function that returns {CSharp}`void` will return control to its caller, but it will not return any interesting value.
 By being an intentionally uninteresting value, {anchorName ArithExprEx}`Unit` allows this to be expressed without requiring a special-purpose {CSharp}`void` feature in the type system.
-Unit's constructor can be written as empty parentheses: {anchorTerm unitParens}`() : Unit`.
 
 ## {lit}`Empty`
 
@@ -652,7 +663,20 @@ These terms are related to sums and products used in ordinary arithmetic.
 The relationship is easiest to see when the types involved contain a finite number of values.
 If {anchorName SumProd}`α` and {anchorName SumProd}`β` are types that contain $`n` and $`k` distinct values, respectively, then {anchorTerm SumProd}`α ⊕ β` contains $`n + k` distinct values and {anchorTerm SumProd}`α × β` contains $`n \times k` distinct values.
 For instance, {anchorName fragments}`Bool` has two values: {anchorName BoolNames}`true` and {anchorName BoolNames}`false`, and {anchorName Unit}`Unit` has one value: {anchorName BooloUnit}`Unit.unit`.
-The product {anchorTerm fragments}`Bool × Unit` has the two values {anchorTerm BoolxUnit}`(true, Unit.unit)` and {anchorTerm BoolxUnit}`(false, Unit.unit)`, and the sum {anchorTerm fragments}`Bool ⊕ Unit` has the three values {anchorTerm BooloUnit}`Sum.inl true`, {anchorTerm BooloUnit}`Sum.inl false`, and {anchorTerm BooloUnit}`Sum.inr Unit.unit`.
+The product {anchorTerm fragments}`Bool × Unit` can have the two values {anchorTerm BoolxUnit}`(true, Unit.unit)` and {anchorTerm BoolxUnit}`(false, Unit.unit)`, and the sum {anchorTerm fragments}`Bool ⊕ Unit` can have the three values {anchorTerm BooloUnit}`Sum.inl true`, {anchorTerm BooloUnit}`Sum.inl false`, and {anchorTerm BooloUnit}`Sum.inr Unit.unit`:
+
+```anchor SumType
+def SumType := Bool ⊕ Unit
+def one : SumType := Sum.inr Unit.unit
+def two : SumType := Sum.inl true
+def three: SumType:= Sum.inl false
+```
+
+```anchor ProdType
+def ProdType := Bool × Unit
+def one : ProdType:= (false, Unit.unit)
+def two : ProdType:= (true, Unit.unit)
+```
 Similarly, $`2 \times 1 = 2`, and $`2 + 1 = 3`.
 
 # Messages You May Meet