Changes to Getting To Know Lean

book/FPLean/GettingToKnow/DatatypesPatterns.lean

@@ -44,9 +44,11 @@ inductive Bool where
 
 This definition has two main parts.
 The first line provides the name of the new type ({anchorName Bool}`Bool`), while the remaining lines each describe a constructor.
-As with constructors of structures, constructors of inductive datatypes are mere inert receivers of and containers for other data, rather than places to insert arbitrary initialization and validation code.
-Unlike structures, inductive datatypes may have multiple constructors.
-Here, there are two constructors, {anchorName Bool}`true` and {anchorName Bool}`false`, and neither takes any arguments.
+Inductive datatypes have multiple constructors, unlike structures that contain only one, for their creation.
+Constructors for Inductive datatypes are mere inert receivers of and containers for other data.
+Here, there are two constructors, {anchorName Bool}`true` and {anchorName Bool}`false`, and neither takes any arguments, neither hold any data.
+The two constructors have their type explicitly declared for clarity but this is facultative here, as they must construct the Type under which they are defined.
+
 Just as a structure declaration places its names in a namespace named after the declared type, an inductive datatype places the names of its constructors in a namespace.
 In the Lean standard library, {anchorName BoolNames}`true` and {anchorName BoolNames}`false` are re-exported from this namespace so that they can be written alone, rather than as {anchorName BoolNames}`Bool.true` and {anchorName BoolNames}`Bool.false`, respectively.
 :::
@@ -81,6 +83,7 @@ The names {anchorName NatNames}`zero` and {anchorName NatNames}`succ` are in a n
 Argument names, such as {anchorName Nat}`n`, may occur in Lean's error messages and in feedback provided when writing mathematical proofs.
 Lean also has an optional syntax for providing arguments by name.
 Generally, however, the choice of argument name is less important than the choice of a structure field name, as it does not form as large a part of the API.
+having {anchorName newNat}`succ : Nat -> Nat` would be faily similar, since {anchorName newNat}`succ` don't use the variable itself.
 
 In C# or Java, {CSharp}`Nat` could be defined as follows:
 ```CSharp
@@ -112,6 +115,8 @@ type Nat = Zero | Succ;
 ```
 Just like C# and Java, this encoding ends up with more types than in Lean, because {typescript}`Zero` and {typescript}`Succ` are each a type on their own.
 It also illustrates that Lean constructors correspond to objects in JavaScript or TypeScript that include a tag that identifies the contents.
+This identification is crucial, {anchorName Bool}`true` and {anchorName Bool}`false` are not _equal_ to {anchorName Bool}`Bool`, they are _of type_ {anchorName Bool}`Bool`.
+Pattern matching check for exhaustiveness, matching against a value of type {anchorName Bool}`Bool` means branching all the possible ways that value could have been constructed
 
 # Pattern Matching
 
@@ -412,3 +417,5 @@ h✝ : ¬n < k
 This message means that {anchorName div}`div` requires a manual proof of termination.
 This topic is explored in {ref "division-as-iterated-subtraction"}[the final chapter].
 :::
+
+You may be interested in reading about how numbers [are treated at runtime](https://lean-lang.org/doc/reference/latest//Basic-Types/Natural-Numbers/#nat-runtime) for efficiency.

book/FPLean/GettingToKnow/FunctionsDefinitions.lean

@@ -109,19 +109,30 @@ if 13 < 14 then 14 else 13
 
 Expressions that evaluate to natural numbers, integers, and strings have types that say this ({anchorName Nat}`Nat`, {anchorName Positivity}`Int`, and {anchorName Book}`String`, respectively).
 This is also true of functions.
-A function that accepts a {anchorName Nat}`Nat` and returns a {anchorName Bool}`Bool` has type {anchorTerm evenFancy}`Nat → Bool`, and a function that accepts two {anchorName Nat}`Nat`s and returns a {anchorName Nat}`Nat` has type {anchorTerm currying}`Nat → Nat → Nat`.
+A function that accepts a {anchorName Nat}`Nat` and returns a {anchorName Bool}`Bool` has type {anchorTerm evenFancy}`Nat → Bool`, as it transform a {lit}`Nat` into a {lit}`Bool`.
+A function that accepts two {anchorName Nat}`Nat`s and returns a {anchorName Nat}`Nat` has type {anchorTerm currying}`Nat → Nat → Nat`, because :
+
+behind the scenes, all functions actually expect precisely one argument.
+Functions like {anchorName maximum3Type}`maximum` that appear to take more than one argument are in fact functions that take one argument and then return a new function.
+This new function takes the next argument, and the process continues until no more arguments are expected.
+This can be seen by providing one argument to a multiple-argument function: {anchorTerm maximum3Type}`#check maximum 3` yields {anchorInfo maximum3Type}`maximum 3 : Nat → Nat`, giving it another Nat yields {anchorInfo maximum3Type}`maximum 3 4 : Nat`. {anchorTerm stringAppendHelloType}`#check spaceBetween "Hello "` yields {anchorInfo stringAppendHelloType}`spaceBetween "Hello" : String → String`, giving it another String yields {anchorInfo stringAppendHelloType}`spaceBetween "Hello" "world" : String`.
+Using a function that returns a function to implement multiple-argument functions is called _currying_ after the mathematician Haskell Curry, and Lean use currying by default as a core design choice related to its type system, a concept that will be explained later (Is it ?)
+You can read Nat -> Nat -> Nat incorrectly as "takes two Nats and returns a Nat", but what it's really saying is "takes a Nat and returns something of the type Nat -> Nat", that is, it returns a function that takes a Nat and returns a Nat. {margin}[Adapted from [Haskell's wiki](https://wiki.haskell.org/Currying)]
+Function arrows associate to the right, which means that {anchorTerm currying}`Nat → Nat → Nat` should be parenthesized {anchorTerm currying}`Nat → (Nat → Nat)`.
 
 As a special case, Lean returns a function's signature when its name is used directly with {kw}`#check`.
 Entering {anchorTerm add1sig}`#check add1` yields {anchorInfo add1sig}`add1 (n : Nat) : Nat`.
 However, Lean can be “tricked” into showing the function's type by writing the function's name in parentheses, which causes the function to be treated as an ordinary expression, so {anchorTerm add1type}`#check (add1)` yields {anchorInfo add1type}`add1 : Nat → Nat` and {anchorTerm maximumType}`#check (maximum)` yields {anchorInfo maximumType}`maximum : Nat → Nat → Nat`.
-This arrow can also be written with an ASCII alternative arrow {anchorTerm add1typeASCII}`->`, so the preceding function types can be written {anchorTerm add1typeASCII}`example : Nat -> Nat := add1` and {anchorTerm maximumTypeASCII}`example : Nat -> Nat -> Nat := maximum`, respectively.
-
-Behind the scenes, all functions actually expect precisely one argument.
-Functions like {anchorName maximum3Type}`maximum` that seem to take more than one argument are in fact functions that take one argument and then return a new function.
-This new function takes the next argument, and the process continues until no more arguments are expected.
-This can be seen by providing one argument to a multiple-argument function: {anchorTerm maximum3Type}`#check maximum 3` yields {anchorInfo maximum3Type}`maximum 3 : Nat → Nat` and {anchorTerm stringAppendHelloType}`#check spaceBetween "Hello "` yields {anchorInfo stringAppendHelloType}`spaceBetween "Hello " : String → String`.
-Using a function that returns a function to implement multiple-argument functions is called _currying_ after the mathematician Haskell Curry.
-Function arrows associate to the right, which means that {anchorTerm currying}`Nat → Nat → Nat` should be parenthesized {anchorTerm currying}`Nat → (Nat → Nat)`.
+This arrow can also be written with an ASCII alternative arrow {anchorTerm add1typeASCII}`->` directly when writing a type signature.
+Moving arguments into the signature just as how lean does when putting a function in parentheses, means that the values passed are not bound to a local variable for use in the function.
+Rather, the function should return a function whose type match its type signature as it can't treat by itself its argument as it is having none :
+```anchor myAppend
+def originalAppend : String -> String -> String := String.append
+def myAppend (a : String) (b : String) : String  := a++b
+#check (originalAppend)
+#check (myAppend)
+```
+Both functions have the same type signature, but only {anchorTerm myAppend}`String.append` and {anchorTerm myAppend}`myAppend` are equipped to deal with the values passed to them.
 
 ## Exercises