From 24cbeb01fbcc6f3f98f4728cc60beadccd13a8ec Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 30 Jun 2023 17:52:06 -0400 Subject: [PATCH] Add script --- README.md | 385 +++++++++++++++++++++++++++++++++++++++++++++++ src/Naturals.idr | 18 +++ 2 files changed, 403 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..c5c234a --- /dev/null +++ b/README.md @@ -0,0 +1,385 @@ +--- +author: Nathan McCarty +title: "Idris 2: Natural Numbers" +--- + +# Script + +This video is going to be a trial run of a format that I want to use for +a longer running series teaching the [Idris +2](id:584e89dc-61f7-4c57-a6a4-72c5470c3280) programming language and the +basics of programming with dependent types. + +We'll kick things off by examining a core concept that crops up +everywhere in programming, and breaking down how the formalism of it +works. + +## What is a "number" + +This may seem like a bit of a crazy question, everyone knows what +numbers are, numbers are these values that we can do addition, +subtraction, etc, on and get more numbers back out, right? + +However, to be able to make mathematical guarantees about our programs, +we need to break the concept of number down to its basic parts and +formalize what we mean by "addition" and "multiplication" + +To make things a bit simpler, for now we'll restrict our discussion of +numbers to the natural numbers: zero and the positive whole numbers. +We'll be using a common formalism known as Peano Arithmetic + +## Peano Axioms + +We'll go through the relevant peano axioms, one by one, implementing +them as we go. Don't be scared by the term "axiom", it's just +mathematical jargon for "basic assumption". + +The historical peano axioms are: + +1. Zero is a natural number +2. For all x, x = x equality is reflexive +3. For all x and y, if x = y, then y = x equality is symmetric +4. For all x, y, and z, if x = y and y = z, then x = z equality is + transitive +5. for all a and b, if a is a natural number, and a = b, then b is a + natural number The naturals are closed under equality +6. For every natural number, S(n) is a natural number The naturals are + closed under S +7. For all natural numbers m and in, if S(m) = S(n), then m = n S is an + injection +8. For every natural number, S(n) = 0 is false + +Idris provides, in a way, a more powerful logic than the one peano +arithmetic was originally conceived in, so we will be proving some of +these statements rather than assuming them as axioms, and many of theses +proofs will turn out to be "freebes". + +We'll start out by defining a `Natural` data type. + +### Building the data type + +1. Zero is a natural number + + We can assert that zero is a natural number by simply creating a + constructor representing zero, giving us axiom 1. + +2. For every natural n, S(n) is a natural number + + `S(n)` is the successor function, it's equivalent to taking a + natural number and adding one to it. We'll implement this by taking + a constructor `S` which takes a natural number as an argument, and + returns the natural number `S(n)` + + Now that we have these two constructors, we can start to define + representations of some common numbers that we might want to use + + The type signature of the constructor provides us with axiom 6 + +3. For every natural number n, n = n + + The first thing we want to be able to say about natural numbers is + that every natural is equal to itself. + + To say this, we'll need a notion of equality, we can do this by + defining another type that starts to invoke some dependent magic, + we'll call it `Equality`. This type will take two natural numbers as + value arguments, so we can say, for example, the type of a value is + `Equality n m` where n and m are natural numbers. + + The equality type provides one constructor, `Reflexive`, + traditionally this is shortened to `Refl`, but we'll keep it long + hand for teaching purposes. This constructor states that equality + over the naturals is reflexive, meaning that every natural number is + equal to itself, giving us axiom 2. + + This constructor enforces equality by only taking one natural as an + implicit argument, and then using it for both "slots" in the type. + So long as this is the only constructor of the type, if we are + holding a value of type `Equality m n`, then we know that `m` and + `n` must be the same number, as that's the only way to construct + such a value. + + The definition of the constructor for the equality type, + `Reflexive`, provides us with axiom 2, and the "kind", or + type-of-the-type, provides us with axiom 5 + +### Writing some proofs + +Now we'll transition into writing some proofs, this requires a bit of a +detour into what a proof is. + +1. Proving positives + + The logic we use in Idris is what is known as constructive, to prove + a statement, you must construct an example of it. For example, to + prove that the number "two" exists, we construct the value "two" and + return it, and to prove that two numbers m and n are equal, we + construct an instance of type `Equality m n` and return it + +2. A detour into totality + + There is one caveat with using functions returning values as proofs, + in order for the resulting logic to be sound, all the functions + involved must be "total". + + We say that a function is "total" when it returns a value in finite + time, without crashing, for all possible inputs. A non-total + function can be used to prove nonsense statements by either never + returning or by being undefined for a particular input. + + Idris helpfully includes a totality checker, we'll go ahead and use + a compiler directive to ask idris to signal an error if any of our + functions are non-total. + + Some of you may be screaming at your screen about the halting + problem right now, and don't worry, we'll get into detail about how + the totality checker works later, but for now we'll just say that + it's not a complete solution, it doesn't work automatically for + every program, and both can and will result in false negatives for + programs that aren't structured in such a way that proving totality + is more or less trivial, requiring either manual proving or + restructuring the program. + + Now that we have `%default total`, we can go ahead and prove an + example equality + +3. Proving a negative + + In constructive logic, the way you establish a negative, a "not X" + statement, is to show that the statement results in a contradiction. + + In idris, this looks like a function which is total and returns a + value of an empty type. Since the return type has no possible + values, and the function is total, and thus must return in finite + time for all possible inputs, the impossibility of returning + speaks to the impossibility of at least one of the inputs. + + We'll demonstrate this by proving that zero is not equal to one, by + writing out a function that takes an `Equality 0 1` as it's input + and returns void. As a value of the type `Equality 0 1` is + structurally impossible, idris lets us use the `impossible` keyword + to signify that this function is impossible to call in a well-typed + program. + +4. For all x and y, if x = y then y = z (symmetric) + + This property, formally stating that equality over the naturals is + symmetric, takes the form of a function with two naturals, x and y, + as arguments, as well as an `Equality x y`, turning that into an + `Equality y x`. Totality here provides us an assurance that this + works for all possible inputs + + This turns out to be nearly trivial to prove in Idris's logic, by + simply writing out the function, and pattern matching the + `Equality x y` argument to it's `Reflexive` constructor, idris + realizes that the two naturals must be the same value and "rewrites" + y into x, changing our output type to `Equality x x`, which we can + return simply with the `Reflexive` constructor, making use of the + 'indiscernability of identicals' principle, and giving us axiom 3. + +5. For all x, y, and z, if x = y and y = z, then x = z + + We'll state this one as a function taking naturals x, y, and z, an + `Equality x y`, and a an `Equality y x`, and returning an + `Equality x z` + + Much like the previous example, Idris also gives us this one "for + free", we can simply pattern match both `Equality` arguments down to + their `Reflexive` constructors, "rewriting" the output type into + `Equality x x`, which can again be created simply with the + `Reflexive` constructor, giving us axiom 4 + +6. For all x and y, if S(x) = S(y), then x = y + + We'll state this one as function taking naturals x and y, and an + `Equality S(x) S(y)`, returning an `Equality x y`. + + Much like the previous two, this is another freebe from idris, + pattern matching on the equality argument "rewrites" the output type + to `Equality x x`, giving us axiom 7 with another simple invocation + of the `Reflexive` constructor + +7. For every n, S(n) != 0 + + This one is a little more interesting, we'll phrase it as a function + taking a natural n, an `Equality (S n) Zero`, and returning Void. + + This still ends up being a bit of a freebe, however, since a value + of the type `Equality (S n) Zero` is structurally impossible, idris + lets us use the impossible keyword, giving us axiom 8 + +## Implementing Operations + +Now that we have our natural numbers defined, and have proven that they +obey the peano axioms, we can start to implement some operations over +them. For the sake of keeping this video reasonable in length, we'll +only be implementing addition, but the other familiar operations, like +subtraction, multiplication, and division can also be implemented over +peano numbers. + +### Defining Addition + +Addition over the natural numbers is a function of two arguments with +the following properties: + +- Zero is the identity (x + 0 = x) Both left and right +- Commutative (x + y = y + x) +- Associative (x + (y + z) = (x + y) + z) + +We'll go ahead and write these out as types before we implement +anything, then we'll go ahead and implement the definition of addition +over the peano numerals. + +This is a pretty simple recursive definition, if the right argument is +zero, return the left argument, but if the right argument is a +successor, return the successor of the right argument plus the number +the right argument is the successor of. + +This can be seen as a structural replacement of the `Zero` at the bottom +of the right argument's "stack" with the value of the left argument +(draw example) + +### Proving identity + +The proof that zero is the identity is trival for the case when the zero +is on the right, as we are just "replacing" the zero with the other +value. + +The case where the Zero is on the left is a little bit more complex. +Pattern matching the argument, the branch where the argument is Zero is +trivial. In the other branch, we recurse on the value our argument is a +successor of. + +We now need a way to turn `Equality x y` into `Equality (S x) (S y)`, so +we define a new `eqSucc` utility, and have the compiler implement it for +us. + +Now that we have our eqSucc utility, we can call it on the equality we +generated via recursion and call our function complete. + +This isn't the only way we could have implemented this function, we +could have applied the symmetry axiom as a "rewriting rule" to transform +the statement being proved into the left-handed version, and while the +standard library provides the mechanics for this, they are based on the +built in equality type, not our bespoke one, and those mechanics are out +of scope for this video + +### Proving the commutative property + +We'll start off by pattern matching our right argument, to match the +structure of `plus`. The zero case is pretty simple, It's actually just +our `zeroIdentityLeft` statement + +Pattern matching the left argument, we can see that our new zero case is +just our `zeroIdentityLeft` with a successor slapped on each side, so we +pull out `eqSucc` and get that branch done + +We then recursively call commutative to get a lemma, using the inner, +decreased, value of m, but the full value of n. This still gives us +totality because the m argument is decreasing towards the base case, but +gives us back something that's almost our output type, minus an +applicaton of `eqSucc`. We notice that the resulting equality has an `S` +in the wrong place on the right hand side, so we'll sketch out a helper +function to do that rearrangement for us. + +This helper function is a true statement, rest assured, but it is rather +annoying to prove without rewriting rules, so we'll leave this one +unimplemented for now, and touch on it again in a later episode + +We have now proven, assuming that for all n and m `(S (plus m n))` is +equivalent to `(plus (S m) n)`, addition commutes. + +### Proving the associative property + +The associative property is somewhat easy to prove with access to +rewriting rules, but complicated without them, so we'll again leave this +for a future video where we investigate the standard library types. + +## Correspondence with the integers + +The peano arithmetic implementation of natural numbers has some pros, it +has almost no moving parts, it's easy to reason about, and naturally +lends itself to recursive inductive proofs, but it also has some major +downsides. As peano numerals are basically just linked lists where the +length of the list is the number we are encoding, they are horribly +space inefficient and operations are much slower than they really need +to be. + +It would be great if we could keep the ease of reasoning, but still +represent peano numeral as space and time efficient machine integers. + +### Idris already does part of this for us + +It turns out that, as reasoning about numbers is such a fundamental part +of theorem proving and working with dependent types, idris has an +optimization that does this shifting of representation for us. + +Any time idris sees a data structure that looks enough like the peano +definition of natural numbers, it will automatically optimize it's +runtime representation to an `Integer`, and we can enforce this with the +`%builtin Natural` pragma + +### Creating conversion functions + +Idris's natural optimization very helpfully also applies to functions +that convert between naturals and integers, but we must be careful in +how we write them. + +We'll start by writing out the type signature for the `natToInteger` +function from Naturals to Integers and explain the conditions as we go: + +1. Exactly one argument must be pattern matched on This applies in our + case because there is exactly one argument +2. The right hand side of the `Zero` case must be 0 +3. The right hand side of the successor case must be + `1 + natToInteger k` + +With all these criteria met, idris will helpfully optimize our +`natToInteger` function to a constant time operation + +Going the other direction is a little bit more complicated, for +`integerToNat` we will be using the `%builtin IntegerToNatural` pragma, +which will give us an error if the optimization does not apply. + +The first thing we need to do is check if the integer is negative, and +short circuit to 0 if it is. In the case that the integer is positive, +we branch on its value, returning `Zero` for the zero case, and +recursing in the non-zero case + +This complains about totality, so we'll assert that `i - 1` is +structurally smaller than `i`, which is valid here as `i` will strictly +decrease down to 0, which is our base case. We'll go into more detail in +a future episode about how to properly make the compiler happy +here. + +We now apply our builtin pragma to make sure the function works as +expected, and we now have our constant-time casting operations +implemented. + +### Replacing our operations at runtime with operations over integers + +Idris provides us with a helpful pragma, `%transform`, which tells idris +that we want it to rewrite an expression into another in the runtime +environment. + +We can use this on our natural number operations to make them constant +time as well, such as plus The idris standard library makes heavy use of +`%transform` for it's natural number operations, making natural numbers +much more efficient to work with than you might expect + +## Conclusion + +This video was, first and foremost, intended to be a test of the format, +and give me a chance to get my recording and editing workflow setup +before diving into it more seriously, so I've left a lot unsaid and this +probably feels terribly unmotivated. + +While I hope I've managed to provide a taste of what theorem proving and +dependent typing has to offer in this little adventure through +re-implementing natural numbers from first principals, the next video in +this series, the first proper entry, will consist of a lot more down to +earth programming. We'll start off without anything in the way of proofs +or dependent types, and get a feel for what idris is like to +program in, building back up from there, giving proper context, +more insight, and more detailed explanations to the concepts we covered +here as we go along. diff --git a/src/Naturals.idr b/src/Naturals.idr index 5b86564..b5f5b65 100644 --- a/src/Naturals.idr +++ b/src/Naturals.idr @@ -8,6 +8,22 @@ data Natural : Type where ||| The successor of a natural n is a natural S : Natural -> Natural +%builtin Natural Natural + +natToInteger : Natural -> Integer +natToInteger Zero = 0 +natToInteger (S x) = 1 + (natToInteger x) + +integerToNat : Integer -> Natural +integerToNat i = + if i < 0 + then Zero + else case i of + 0 => Zero + _ => S (integerToNat (assert_smaller i (i - 1))) + +%builtin IntegerToNatural Naturals.integerToNat + one : Natural one = S Zero @@ -40,6 +56,8 @@ plus : (n, m : Natural) -> Natural plus n Zero = n plus n (S x) = S (n `plus` x) +%transform "plus" Naturals.plus n m = Naturals.integerToNat (Naturals.natToInteger n + Naturals.natToInteger m) + zeroIdentityRight : (n : Natural) -> Equality n (n `plus` Zero) zeroIdentityRight n = Reflexive