Add script

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 <u>is</u>.
+
+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 <u>all possible</u> 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 <u>properly</u> 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
+<u>program</u> 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.

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