Edit Chapter 1

- Edit out use of first person singular
- Clean up phrasing to make things flow better
- Update text to reflect the chapter being broken up into subchapters
- Introduce more structured formatting to some section
- Clean up links to pages on the Idris2 github wiki that no longer exist
- Add link to pack-db to the getting help section

Author: nmccarty

conversion-todo.org

@@ -1,32 +1,37 @@
-* DONE Get CI up and running
-* DONE Fix that whole extra line breaks bug
-* DONE Rewrite README
-** DONE Link to SUMMARY.md
-** DONE Document building mdbook
-** DONE Move some of the existing prose to a preface chapter
-* DONE Build docker container locally instead of using one from my personal forgejo
-* DONE Add links from github to mdbook and from mdbook to github
+* Conversion tasks and initial editing
+** DONE Get CI up and running
+** DONE Fix that whole extra line breaks bug
+** DONE Rewrite README
+*** DONE Link to SUMMARY.md
+*** DONE Document building mdbook
+*** DONE Move some of the existing prose to a preface chapter
+** DONE Build docker container locally instead of using one from my personal forgejo
+** DONE Add links from github to mdbook and from mdbook to github
 This one's best done after migrating to the community project so we can have the correct url
-* DONE Organize ipkg modules in chapter order
-* DONE Break Chapters into sub-chapters as appropriate
-* DONE Configure mdformat
-* DONE Audit links
-* DONE Figure out exercise solutions situation
+** DONE Organize ipkg modules in chapter order
+** DONE Break Chapters into sub-chapters as appropriate
+** DONE Configure mdformat
+** DONE Audit links
+** DONE Figure out exercise solutions situation
 Will probably want to either convert the solutions files to markdown with katla or manually, and add them in a an appendex. Will need to go back and insert links/references.
-* STRT Rewrite prose to remove use of first person
-As this is becoming a community maintained tutorial, the prose should reflect the collective ownership and avoid the use of first person pronouns.
-* TODO Cleanup Imports and Exports
-* TODO Clean up fixity declarations
-* TODO Consistent on summary vs conclusion
-* TODO Place modules and visibility primer upfront
-* TODO Cleanup references to outdated sources
+** DONE Consistent on summary vs conclusion
+** STRT Clean Up Prose
+Need to:
++ Remove use of first person singular, to reflect the collective ownership
++ Update prose to reflect the new sub-chapter structure
++ Update links and clean up broken ones
++ Other minor editing changes to make the text flow better
+** TODO Cleanup Imports and Exports
+** TODO Clean up fixity declarations
+** TODO Place modules and visibility primer upfront
+** TODO Cleanup references to outdated sources
 Like the wiki library page
-* TODO Clean up exercise titling
+** TODO Clean up exercise titling
 Make sure section names match up with headers in solutions
-* TODO Inject highlighted repl output
-** TODO Actual test injection
+** TODO Inject highlighted repl output
+*** TODO Actual test injection
 Thread local IDEMode?
-** TODO Golden Tests
+*** TODO Golden Tests
 Should golden test the repl outputs to detect breakage
 
 These should also be compared in a whitespace insensitive way, im thinking, like:
@@ -40,10 +45,12 @@ These should also be compared in a whitespace insensitive way, im thinking, like
 #+end_src
 
 This keeps it readable as a raw markdown document, but provides easy processing for extraction and injection of the /actual/ repl output complete with highlighting.
-** TODO Special Handling for exec
-* TODO Selenized custom themes
+*** TODO Special Handling for exec
+** TODO Selenized custom themes
 Because I love myself
-* IDEA Standard library types
+** IDEA Standard library types
 When a subchapter reimplements a standard library type, we should maybe call this out and use the standard library type in future subchapters to decrease cross dependencies
-* IDEA Rename Modules To Chapter/Subchapter number?
+** IDEA Rename Modules To Chapter/Subchapter number?
 Could also potentially insert automatic linking?
+* New sections
+** TODO Property based testing

src/SUMMARY.md

@@ -10,7 +10,7 @@
   - [A First Idris Program](./Tutorial/Intro/FirstIdrisProgram.md)
   - [The Shape of an Idris Definition](./Tutorial/Intro/ShapeOfADef.md)
   - [Where to Get Help](./Tutorial/Intro/WhereToGetHelp.md)
-  - [Summary](./Tutorial/Intro/Summary.md)
+  - [Conclusion](./Tutorial/Intro/Conclusion.md)
 - [Functions Part 1](./Tutorial/Functions1.md)
   - [Functions With More Than One Argument](./Tutorial/Functions1/FunctionsWithMultipleArguments.md)
   - [Function Composition](./Tutorial/Functions1/FunctionComposition.md)

src/Tutorial/Intro/AboutTheLanguage.md

@@ -1,44 +1,50 @@
 # About the Idris Programming Language
 
-Idris is a *pure*, *dependently typed*, *total* *functional* programming language. I'll quickly explain each of these adjectives in this section.
+Idris is a *pure*, *dependently typed*, *total* *functional* programming language.
+
+Lets break that down and explore what each of those terms means on their own.
 
 ## Functional Programming
 
-In functional programming languages, functions are first-class constructs, meaning that they can be assigned to variables, passed as arguments to other functions, and returned as results from functions. Unlike for instance in object-oriented programming languages, in functional programming, functions are the main form of abstraction. This means that whenever we find a common pattern or (almost) identical code in several parts of a project, we try to abstract over this in order to have to write the corresponding code only once. We do this by introducing one or more new functions implementing this behavior. Doing so, we often try to be as general as possible to make our functions as versatile to use as possible.
+In functional programming languages, functions are *first-class constructs*, meaning that they can be assigned to variables, passed as arguments to other functions, and returned as results from functions, just like any other value in the language. Unlike in, for instance, object-oriented languages, functions are the main form of abstraction in functional programming.
+
+Whenever we find a common pattern or (almost) identical code in several parts of a project, we try to implement an abstraction over it to avoid write the same code multiple times. In functional programming, we do this by introducing one or more new functions implementing the required behavior, often trying to be as general as possible to maximize the versatility and re-usability of our functions.
 
-Functional programming languages are concerned with the evaluation of functions, unlike classical imperative languages, which are concerned with the execution of statements.
+Functional programming languages are concerned with the evaluation of functions, unlike imperative languages, which are concerned with the execution of statements.
 
 ## Pure Functional Programming
 
-Pure functional programming languages come with an additional important guarantee: Functions don't have side effects like writing to a file or mutating global state. They can only compute a result from their arguments possibly by invoking other pure functions, *and nothing else*. As a consequence, given the same input, they will *always* generate the same output. This property is known as [referential transparency](https://en.wikipedia.org/wiki/Referential_transparency).
+*Pure* functional programming languages come with an additional important guarantee:
+
+Functions don't have side effects, like writing to a file or mutating global state. They can only compute a result from their arguments possibly by invoking other pure functions, *and nothing else*. Given the same input, a pure function will *always* generate the same output, this property is known as [referential transparency](https://en.wikipedia.org/wiki/Referential_transparency).
 
 Pure functions have several advantages:
 
-- They can easily be tested by specifying (possibly randomly generated) sets of input arguments together with the expected results.
+- They are easy to test by specifying (possibly randomly generated) sets of input arguments alongside the expected results.
 
-- They are thread-safe, since they don't mutate global state, and as such can be freely used in several computations running in parallel.
+- They are thread-safe. Since they don't mutate global state, they be used in several computations running in parallel without interfering with each other.
 
 There are, of course, also some disadvantages:
 
-- Some algorithms are hard to implement efficiently using only pure functions.
+- Some algorithms are hard to implement efficiently with only pure functions.
 
-- Writing programs that actually *do* something (have some observable effect) is a bit trickier but certainly possible.
+- Writing programs that actually *do* something (have some observable effect) is a bit tricky, but certainly possible.
 
 ## Dependent Types
 
-Idris is a strongly, statically typed programming language. This means that every Idris expression is given a *type* (for instance: integer, list of strings, boolean, function from integer to boolean, etc.) and types are verified at compile time to rule out certain common programming errors.
+Idris is a strongly, statically typed programming language. Every expression is given a *type* (for instance: integer, list of strings, boolean, function from integer to boolean, etc.), and types are verified at compile time to rule out certain common programming errors.
 
-For instance, if a function expects an argument of type `String` (a sequence of unicode characters, such as `"Hello123"`), it is a *type error* to invoke this function with an argument of type `Integer`, and the Idris compiler will refuse to generate an executable from such an ill-typed program.
+For instance, if a function expects an argument of type `String` (a sequence of unicode characters, such as `"Hello123"`), it is a *type error* to invoke this function with an argument of type `Integer`, and Idris will refuse to compile such an ill-typed program.
 
-Being *statically typed* means that the Idris compiler will catch type errors at *compile time*, that is, before it generates an executable program that can be run. The opposite to this are *dynamically typed* languages such as Python, which check for type errors at *runtime*, that is, when a program is being executed. It is the philosophy of statically typed languages to catch as many type errors as possible before there even is a program that can be run.
+Being *statically typed* means that Idris will catch type errors at *compile time*, before it generates an executable program that can be run. This stands in contrast with *dynamically typed* languages such as Python, which check for type errors at *runtime*, while a program is already being executed. It is the goal of statically typed languages to catch as many type errors as possible before there even is a program that can be run.
 
-Even more, Idris is *dependently typed*, which is one of its most characteristic properties in the landscape of programming languages. In Idris, types are *first class*: Types can be passed as arguments to functions, and functions can return types as their results. Even more, types can *depend* on other *values*. What this means, and why this is incredibly useful, we'll explore in due time.
+Furthermore, Idris is *dependently typed*, which is one of its most characteristic properties in comparison to other programming languages. In Idris, types are *first class*: Types can be passed as arguments to functions, and functions can return types as their results. Types can also *depend* on other *values*, as one example, the return type of a function can depend on the value of one of its arguments. This is a quite abstract statement that may be difficult to grasp at first, but we will be exploring its meaning and the profound impact it has on programming through example as we move through this book.
 
 ## Total Functions
 
-A *total* function is a pure function, that is guaranteed to return a value of the expected return type for every possible input in a finite number of computational steps. A total function will never fail with an exception or loop infinitely, although it can still take arbitrarily long to compute its result
+A *total* function is a pure function which is guaranteed to return a value of its return type for every possible set of inputs in a finite number of computational steps. A total function will never fail with an exception or loop infinitely, although it can still take arbitrarily long to compute its result.
 
-Idris comes with a totality checker built-in, which enables us to verify the functions we write to be provably total. Totality in Idris is opt-in, as in general, checking the totality of an arbitrary computer program is undecidable (see also the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)). However, if we annotate a function with the `total` keyword, Idris will fail with a type error, if its totality checker cannot verify that the function in question is indeed total.
+Idris comes with a totality checker built-in, which allows us to verify that the functions we write are provably total. Totality in Idris is opt-in, as checking the totality of an arbitrary computer program is undecidable in the general case (a dilemma you may recognize as the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)). However, if we annotate a function with the `total` keyword, and the totality checker is unable to verify that the function is, indeed, total, Idris will fail with a type error. Notably, failing to determine a function is total is not the same as judging the function to be non-total.
 
 <!-- vi: filetype=idris2:syntax=markdown
 -->

src/Tutorial/Intro/Summary.md src/Tutorial/Intro/Conclusion.mdsrc/Tutorial/Intro/Summary.md renamed to src/Tutorial/Intro/Conclusion.md

@@ -1,4 +1,4 @@
-# Summary
+# Conclusion
 
 In this introduction we learned about the most basic features of the Idris programming language. We used the REPL to tinker with our ideas and inspect the types of things in our code, and we used the Idris compiler to compile an Idris source file to an executable.
 

src/Tutorial/Intro/FirstIdrisProgram.md

@@ -4,40 +4,42 @@
 module Tutorial.Intro.FirstIdrisProgram
 ```
 
-We will often start up a REPL for tinkering with small parts of the Idris language, for reading some documentation, or for inspecting the content of an Idris module, but now we will write a minimal Idris program to get started with the language. Here comes the mandatory *Hello World*:
+While we will often start with the REPL for tinkering with small parts of the Idris language, for reading some documentation, or for inspecting the content of an Idris module, lets go ahead and will write a minimal Idris program to get started with the language.
+
+Here comes the mandatory *Hello World*:
 
 ```idris
 main : IO ()
 main = putStrLn "Hello World!"
 ```
 
-We will inspect the code above in some detail in a moment, but first we'd like to compile and run it. From this project's root directory, run the following:
+We will inspect the code above in some detail in a moment, but first we'd like to compile and run it. If you have checked out this books source code, you can run the following from the root directory:
 
 ```sh
-pack -o hello exec src/Tutorial/Intro.md
+pack -o hello exec src/Tutorial/Intro/FirstIdrisProgram.md
 ```
 
-This will create executable `hello` in directory `build/exec`, which can be invoked from the command-line like so (without the dollar prefix; this is used here to distinguish the terminal command from its output):
+This will create an executable called `hello` in the `build/exec` directory, which can be invoked from the command-line like so (without the dollar prefix; this is used here to distinguish the terminal command from its output):
 
 ```sh
 $ build/exec/hello
 Hello World!
 ```
 
-The pack program requires an `.ipkg` to be in scope (in the current directory or one of its parent directories) from which it will get other settings like the source directory to use (`src` in our case). The optional `-o` option gives the name of the executable to be generated. Pack comes up with a name of its own it this is missing. Type `pack help` for a list of available command-line options and commands, and `pack help <cmd>` for getting help for a specific command.
+The pack program requires an `.ipkg` to be in scope (in the current directory or one of its parent directories), which provides other settings like the source directory to use (`src` in our case). The optional `-o` option provides a name to use for the executable to be generated. Pack comes up with a name of its own it this is not provided. Type `pack help` for a list of available command-line options and commands, and `pack help <cmd>` for help with a specific command.
 
-As an alternative, you can also load this source file in a REPL session and invoke function `main` from there:
+You can also load this source file in a REPL session and invoke function `main` from there:
 
 ```sh
-pack repl src/Tutorial/Intro.md
+pack repl src/Tutorial/Intro/FirstIdrisProgram.md
 ```
 
 ```repl
 Tutorial.Intro> :exec main
 Hello World!
 ```
 
-Go ahead and try both ways of building and running function `main` on your system!
+Go ahead and try both ways of building and running `main` on your system!
 
 <!-- vi: filetype=idris2:syntax=markdown
 -->