4 Naturals

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

My commentary on PLFA is keyed to its section titles, with the addition of my own short preludes and postscripts. You can read PLFA and these notes in parallel, and watch the embedded asciicasts here, which use the "starter" local versions of PLFA code files. The end results are available in the "completed" local versions, which are the starting point for assignment submissions. Some exercises from PLFA are marked to be done for credit in this course, while others are optional. I have also added some exercises of my own, and modified some of the PLFA exercises.

4.1 Prelude

The natural numbers, developed here as in the Agda standard library, are an excellent introduction to working in Agda. The construction presented here is fundamental in formal logic and dates back to the 19th Century.

4.2 Unpacking the inference rules

PLFA introduces inference rules in the definition of natural numbers. As pointed out there, the hypotheses are above the horizontal line and the conclusion is below. This is a standard way of presenting "if/then" rules in a concise (though two-dimensional) format. In this case, the naturals are built from constructors zero and suc, but we can’t use them arbitrarily; the inference rules give restrictions on how they can be used.

PLFA then moves from the inference rules to the datatype definition. In this case, the datatype definition is simple enough that we probably don’t need the inference rules presentation. But the idea of moving from inference rules to datatype definition will be useful later on when the inference rules are talking about more complicated judgments.

Unicode symbols are starting to show up here, and it’s not obvious how to type them in Emacs. Fortunately, when editing an Agda file, a special input method is set up (if you have properly configured your Emacs to use Agda mode). Backslash (\) is the escape key that starts to build a special character. If you really want a backslash, just type it twice. But otherwise what you type next determines the special character. Typing \to gives the small right arrow →. Each PLFA chapter has a list of new Unicode characters and their shortcuts, and I have done this in my local versions as well. Note that these shortcuts don’t work outside of Agda mode (without further configuration of Emacs).

4.3 Operations on naturals

Here is an asciicast showing the interactive development of the addition function. Note that the type system does not ensure correctness. We could have just written x + y = zero as the single line of the definition. This may seem obvious now, but in proving theorems, any valid proof (that is, any value with the correct type) will suffice, and after a while it is easy to forget that sometimes it does not suffice.

The Emacs keystroke commands needed are covered in the PLFA section "Writing definitions interactively", further down in this PLFA chapter. You can read that section at any point during work on this chapter, and replay the asciicast paying attention to the command log on the right, or try recreating the development with whatever variations you want to try.

The type signature for the addition function is ℕ → ℕ → ℕ. The two arrows are important: it’s not ℕ ℕ → ℕ or (ℕ,ℕ) → ℕ or anything that might group the two parameters together. In fact, every function in Agda has exactly one parameter. The → type constructor is right-associative, so the type signature ℕ → ℕ → ℕ is read as ℕ → (ℕ → ℕ). That is, addition consumes one natural number and produces a function that consumes another natural number and produces the sum of the two. Since function application is left-associative, we can write _+_ 3 4 and it means (_+_ 3) 4, or we can write 3 + 4 to mean the same thing. This is a common decision among statically-typed functional programming languages, and has a number of advantages, but if you’re more used to conventional imperative languages, this may take some adjustment.

Pattern matching is available in most functional programming languages, but Agda’s pattern matching is particularly sophisticated, as it needs to deal with dependent types in a way that helps the user. We will use it a lot, and gradually learn about the pattern language. Patterns are matched against values. For now, note that a pattern like m means "match anything, and call the result m", and a pattern using a constructor, like suc m, means "match anything whose outer constructor is suc, and let m be the thing that suc is applied to."

In a conventional static type system, a file is completed by the user without using the compiler. The compiler then typechecks the code without running it. Finally, it creates an executable version which can then be run. There is consequently a clean separation between terms (expressions in the language) and types. In fact, one goal for a compiler is to erase types after checking, so they incur no run-time overhead.

But in a type system supporting dependent types, this clean separation breaks down. We want to be able to prove things about our code, which means that expressions involving it (applications of functions, etc.) are going to appear in our types. If we want to prove "my-function 1 = 3" by means of typechecking, then there has to be some evaluation of "my-function 1" at typechecking time.

There are points in Agda’s typechecking where, internally, it must check whether two types are equal. This is obvious in the case above, but there are other points as well. What it does is this: it evaluates each of the types as much as it can, and then it checks equality. To make this clearer, we need to distinguish several kinds of equality.

Structural equality is when exactly the same constructors are used in exactly the same ways to create the two types. For example, suc (suc zero) and suc (suc zero) are structurally equal. The kind of equality I talked about in the previous paragraph is definitional equality. For example, 1 + 3 and 4 are definitionally equal, because 1 + 3 can be evaluated to 4. (I am using shorthand here; 1 really means suc zero, and so on.) Finally, propositional equality is a way of talking about definitional equality in Agda itself. For example, I could say "1 + 3 ≡ 4". But I could also say "1 + 3 ≡ 5". The former has a proof, while the latter does not.

The main takeaway from this discussion is that Agda needs to do some evaluation during typechecking. And PLFA tries to show how this would work for our definition of +. Each step is an application of one of the equational rules used to define +. More specifically, one step consists of matching an expression which is a function application against the patterns on the left-hand side of the definitional equations for that function. When a match is found, the expression is rewritten. PLFA displays these steps using syntax imported from the standard library to display equational reasoning.

But it’s important to understand the limitations of such a display. It isn’t really checking that the next expression follows from the previous one by "one step of computation". This is evident by moving the terms around, or removing some; the result will still typecheck. All the syntax accomplishes is to take expressions \(e_1, e_2, \dots e_n\), where \(e_1 = e_2\), \(e_2 = e_3\), and so on, and let us chain them into the equivalent of \(e_1 = e_2 = e_3 \dots = e_n\). We do this all the time in mathematics, but the rules of Agda are somewhat more rigid, and once we define ≡ as relating two expressions, we cannot then use it to link more than two expressions into one. Hence the additional syntax.

It is possible to create an executable from Agda code and run it, but we will not do so in this course. That may seem strange, to not even compile our programs to native code, let alone run them. But, as explained above and made clear in this chapter, evaluation is taking place, and we can test our functions as part of typechecking. You understand programming from your previous exposure to computation. The goal of this course is to improve your understanding of proof in a computational setting. For that, typechecking suffices.

4.4 Multiplication

There is a PLFA/747 exercise on defining exponentiation.

4.5 Monus

We see from the example functions in this chapter that a function definition is a series of definitional equations, with patterns on the left-hand sides. Those patterns have to cover all cases, or the compiler will not accept the definition. This is one of the ways that Agda ensures that all functions are total. Two cases may overlap, in the sense that there is a value that matches both left-hand-side patterns. This is permitted, but Agda mode will slightly highlight the second equation as a warning. For a value falling into the overlap, the second equation will not be used, and this could cause problems during interaction when we are trying to get types to match up. The moral of the story is that sometimes it is better to write a bit more code to avoid overlap. If you use C-c C-c (case split) to develop patterns as done in the asciicast, this will come naturally.

As mentioned in the Demo chapter, propositional equality (≡) and its proof refl are not built-in. Both are defined in library code, using a generalization of the same mechanism as we used to build ℕ. refl is the single constructor of the datatype for _≡_. It may seem odd that refl can construct a value in the two different types 3 ≡ 3 and 4 ≡ 4. But we will see that refl has a hidden argument. Further details show up in the Equality chapter.

When I first taught from PLFA, the binary representation exercise at the end of this chapter used the default prefix operators, which resulted in the most significant bit being at the far right (that is, numbers looked "backwards"). Following an idea of David Darais, I changed the representation in the 747 file to use postfix operators. PLFA has since adopted the same idea, but with different operator names. There are followup exercises in subsequent chapters which I have also adapted.