More work on documentation

docs/conf.py

@@ -32,7 +32,13 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = ['sphinx.ext.mathjax']
+extensions = [
+    'sphinx.ext.mathjax',
+    'sphinx.ext.autosectionlabel',
+]
+
+# Make sure the target is unique
+autosectionlabel_prefix_document = True
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']

docs/introduction/algebraic.rst

@@ -0,0 +1,8 @@
+Algebraic data types
+====================
+
+.. admonition:: To be written
+
+   - Sum types
+   - Type definitions
+   - Recursive types (lists, trees)

docs/introduction/arithmetic.rst

@@ -8,14 +8,16 @@ deeper into the arithmetic operations supported by Disco.
 Addition and multiplication
 ---------------------------
 
-The most basic arithmetic operations Disco supports are addition and
-multiplication.
+The most basic arithmetic operations Disco supports are :doc:`addition
+</reference/addition>` and :doc:`multiplication
+</reference/multiplication>`.
 
 - Addition is written using ``+``, for example, ``3 + 5 + 2/3``.
 - Multiplication is written using ``*``, for example, ``(-2) * 6 *
   (1/3)``.
-- The multiplication sign can also sometimes be omitted, just like in
-  standard mathematical notation.  For example:
+- The multiplication sign can also :doc:`sometimes
+  </reference/multiplication>` be omitted, just like in standard
+  mathematical notation.  For example:
 
   ::
 
@@ -30,7 +32,7 @@ multiplication.
      Disco> (1 + 3)(5 - 2)  -- means the same as above
      12
 
-All the number types (:doc:`natural numbers </reference/natural>`
+All the numeric types (:doc:`natural numbers </reference/natural>`
 ``N``, :doc:`integers </reference/integer>` ``Z``, :doc:`fractional
 numbers </reference/fraction>` ``F``, and :doc:`rational numbers
 </reference/rational>` ``Q``) support both addition and
@@ -79,8 +81,8 @@ Of course, Disco has many more operators than we have seen so far
 (almost 30 in total), but you do not need to memorize the precedence
 (*i.e.* order of operations) for all the operators!  You can use the
 ``:doc`` command to see information about an operator, including its
-precedence level.  For example, let's check out the documentation for
-``+``:
+precedence level.  For example, let's check out the
+:doc:`documentation </reference/docs>` for ``+``:
 
 ::
 
@@ -97,7 +99,7 @@ precedence level.  For example, let's check out the documentation for
    https://disco-lang.readthedocs.io/en/latest/reference/addition.html
 
 There is a lot of information here, so let's go through it slowly.
-The first few lines tell us some of the :doc:`type <types>`
+The first few lines tell us some of the :doc:`types`
 the addition operator can have.  Don't worry for now about what the various
 symbols like ``~``, ``×``, and ``→`` mean; essentially this is telling
 us that ``+`` takes a pair of natural numbers and returns a natural
@@ -130,8 +132,8 @@ has a *higher* precedence (8) than addition:
 The higher precedence level of ``*`` is how Disco knows that it should
 come before (*i.e.* have parentheses put around it before) addition.
 
-Exercises
----------
+Precedence exercises
+--------------------
 
 * What is the precedence level of subtraction, and how does it compare
   to the precedence levels of addition and multiplication?  Does this
@@ -175,21 +177,88 @@ and rational numbers into fractional numbers.  For example:
 Division
 --------
 
-Division is written using ``/``.  Only fractional numbers (``F``) and
-rational numbers (``Q``) support division.
+Division can be performed in Disco, using the ``/`` operator.  As you
+learned in the section on :doc:`types`, only fractional numbers
+(``F``) and rational numbers (``Q``) support division; however,
+natural numbers or integers can be converted to those types as
+necessary.
 
-Integer division
-----------------
+::
+
+   Disco> :type 3
+   3 : ℕ
+   Disco> :type (-5)
+   -5 : ℤ
+   Disco> :type 3/(-5)
+   3 / (-5) : ℚ
+   Disco> 3/(-5)
+   -3/5
 
-Division on N, Z that rounds down.
+Division in Disco always gives an exact answer; it never rounds down
+or gives an approximate result.
 
 Floor and ceiling
 -----------------
 
-``floor(x)``, ``ceiling(x)``.  Definitions.  Cool Unicode notation.
-Turns Q into Z, F into N.
+In many cases, we might want to round some number to an integer.
+Disco provides the ``floor`` and ``ceiling`` functions for this
+purpose.
+
+* ``floor(x)`` rounds ``x`` *down* to the nearest integer.  In other
+  words, ``floor(x)`` is the largest integer which is less than or
+  equal to ``x``.  As an alternative, Disco also supports the standard
+  mathematical notation ``⌊x⌋`` instead of ``floor(x)``.
+* Likewise, ``ceiling(x)`` rounds *up* to the nearest integer, that
+  is, it results in the smallest integer greater than or equal to
+  ``x``.  As an alternative, Disco also supports the standard
+  mathematical notation ``⌈x⌉`` instead of ``ceiling(x)``.
+* Disco does not provide a built-in ``round`` function for rounding to
+  the *nearest* integer; however, you can use ``floor(x + 1/2)`` for
+  this purpose.
+
+Note that ``floor`` and ``ceiling`` turn rational numbers into
+integers, and fractional numbers into natural numbers.  In other
+words, they have types like:
 
-Note that ``x // y`` is really just shorthand for ``floor(x / y)``.
+::
+
+   floor : 𝔽 → ℕ
+   floor : ℚ → ℤ
+
+Integer division
+----------------
+
+One common application for ``floor`` is *integer division*, that is,
+dividing two integers and rounding the result down to the nearest
+integer.  Integer division can therefore be written ``floor(x / y)``.
+However, this is such a common operation that Disco provides a
+built-in integer division operator ``//``, so ``x // y`` is shorthand
+for ``floor(x / y)``.
 
 Exponentiation
 --------------
+
+Exponentiation in Disco can be written using the ``^`` operator, just
+like most calculators.  For example:
+
+::
+
+   Disco> 2 ^ 4
+   16
+   Disco> 5 ^ 1
+   5
+   Disco> 3 ^ 0
+   1
+   Disco> 2 ^ (-3)
+   1/8
+   Disco> 2 ^ 500
+   3273390607896141870013189696827599152216642046043064789483291368096133796404674554883270092325904157150886684127560071009217256545885393053328527589376
+
+Note that exponentiation can handle exponents which are zero or negative.
+
+The type of exponentiation is somewhat complex, but it is not
+too important to understand at the moment.
+
+.. admonition:: To be written
+
+   * Exercises

docs/introduction/booleans.rst

@@ -0,0 +1,13 @@
+
+Booleans and Logic
+==================
+
+.. admonition:: To be written
+
+   - Introduce type `Bool`, values `T` and `F`
+   - Introduce logic operators (and, or, not, implies, iff)
+   - Mention `:table` command
+   - Introduce basic comparison operators
+   - Introduce basic tests
+   - Exercises:
+     - xor

docs/introduction/functions.rst

@@ -0,0 +1,92 @@
+Functions
+=========
+
+*Functions* are central to Disco.  We've already seen a few special
+built-in functions: ``floor``, ``abs``, and even the arithmetic
+operations like addition, which are really functions with special
+notation.  In this section, you'll learn more about functions, their
+types, and how to define your own.
+
+Functions as machines
+---------------------
+
+What is a *function*?  As a concrete metaphor, think of a function as
+a box, with some kind of machinery inside and a slot on each end.  If
+you put some kind of *input* into the slot on one end, the machinery
+whirrs away and an *output* spits out of the slot on the other end.
+
+More formally, a function is some kind of *rule* or *procedure* that
+turns each *input* value (taken from some collection of possible
+inputs, called the *domain*) into an associated *output* value (from a
+collection of possible outputs, called the *codomain*).  For example,
+:math:`\mathit{double}(n) = 2n` defines a function called
+:math:`\mathit{double}` which associates each input value :math:`n`
+with the output value :math:`2n`.
+
+Function types and definitions
+------------------------------
+
+By now you know that :doc:`everything in Disco has a type <types>`, so
+functions must have types as well.  The :doc:`type of a function
+</reference/function-types>` which takes values of type ``A`` as input
+and produces values of type ``B`` as output is written ``A -> B``.
+For example, the type of a function which takes natural numbers as
+input and produces rational numbers as output would be written ``N ->
+Q`` (or ``Natural -> Rational``, or ``ℕ → ℚ``, *etc.*).
+
+Let's see how to define the :math:`\mathit{double}` function in Disco.
+It follows the :doc:`same pattern we saw before for defining variables
+<variables>`: we first declare the type of the function by writing its
+name, a colon, and its type, then we give a definition of the function
+on another line.  The only difference is that instead of writing
+``double = ...`` we write ``double(n) = ...`` to show that ``double``
+is a function taking an input we call ``n``.
+
+::
+
+   double : N -> N
+   double(n) = 2n
+
+Note that the name of the input does not matter; there is nothing
+magical about naming the input ``n`` (or any other particular name).
+If we wanted we could also call the input ``x``, or ``flerb``, or any
+other :doc:`valid name <variables>`, and it would still define exactly
+the same function:
+
+::
+
+   double : N -> N
+   double(flerb) = 2 * flerb
+
+(Here we also used an explicit :ref:`multiplication
+<introduction/arithmetic:addition and multiplication>`
+operator ``*``, but writing ``2flerb`` or ``2 flerb`` would work too.)
+
+Function application
+--------------------
+
+Once a function has been defined, we can use it in any expression by
+*applying* it to an input, writing the input in parentheses after the
+name of the function.
+
+::
+
+   Disco> 3 + double(5)
+   13
+   Disco> double(7) + double(2) + double(double(1))
+   22
+
+We can also use it as part of the definition of other functions. For
+example:
+
+::
+
+   quadruplePlusOne : N -> N
+   quadruplePlusOne(n) = double(double(n)) + 1
+
+.. admonition:: To be written
+
+   * Applying functions to inputs of the wrong type.
+   * Loading functions from a file.
+   * Example: factorial function.
+   * Exercises.

docs/introduction/getting-started.rst

@@ -32,7 +32,8 @@ Exercises
 ---------
 
 Disco can be used as a basic calculator.  Enter each of the following
-expressions at the Disco prompt and report the results.
+:doc:`arithmetic expressions </reference/arithmetic>` at the Disco
+:doc:`prompt </reference/REPL>` and report the results.
 
 - ``2 + 3``
 - ``5 - 8``

docs/introduction/index.rst

@@ -8,7 +8,7 @@ through a series of short lessons with exercises, introducing the
 
 .. _`Disco language`: https://github.com/disco-lang/disco/#readme
 
-**The Gentle Introduction is currently (Spring 2024) under construction,
+**The Gentle Introduction is currently (Spring 2025) under construction,
 check back later for more!**
 
 Note that the gentle introduction contains many links to the
@@ -23,3 +23,11 @@ more detail on some particular topic.
    types
    variables
    arithmetic
+   functions
+   booleans
+   number-theory
+   pairs
+   sets
+   lists
+   polymorphism
+   algebraic

docs/introduction/lists.rst

@@ -0,0 +1,8 @@
+Lists
+=====
+
+.. admonition:: To be written
+
+   - Literal lists, ellipsis notation
+   - List comprehensions
+   - Basic recursion patterns (motivate polymorphism)

docs/introduction/number-theory.rst

@@ -0,0 +1,14 @@
+Number Theory
+=============
+
+.. admonition:: To be written
+
+   - Integer division
+   - Mod
+   - Divisibility
+   - Quantified tests
+       - Tests can start with `forall` or `exists`
+       - Explain syntax.
+       - `Prop` vs `Bool`.
+           - `holds`
+   - Exercises

docs/introduction/pairs.rst

@@ -0,0 +1,7 @@
+Pairs and pattern matching
+==========================
+
+.. admonition:: To be written
+
+   - Pairs, product type
+   - Basic pattern matching

docs/introduction/polymorphism.rst

@@ -0,0 +1,6 @@
+Polymorphism
+============
+
+.. admonition:: To be written
+
+   Polymorphic list functions

docs/introduction/sets.rst

@@ -0,0 +1,9 @@
+Sets
+====
+
+.. admonition:: To be written
+
+   - Basic literal sets
+   - Ellipsis notation
+   - Set operations (union, intersection, difference, size, cartesian product, power set)
+   - Set comprehensions