Nathan McCarty 24cbeb01fb  

src  
.gitignore  
Naturals.ipkg  
README.md 
README.md
author  title 

Nathan McCarty  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 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:
 Zero is a natural number
 For all x, x = x equality is reflexive
 For all x and y, if x = y, then y = x equality is symmetric
 For all x, y, and z, if x = y and y = z, then x = z equality is transitive
 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
 For every natural number, S(n) is a natural number The naturals are closed under S
 For all natural numbers m and in, if S(m) = S(n), then m = n S is an injection
 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

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.

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 constructorS
which takes a natural number as an argument, and returns the natural numberS(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

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 isEquality n m
where n and m are natural numbers.The equality type provides one constructor,
Reflexive
, traditionally this is shortened toRefl
, 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 thatm
andn
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 typeofthetype, 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.

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 
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 nontotal 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 nontotal.
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 
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 typeEquality 0 1
is structurally impossible, idris lets us use theimpossible
keyword to signify that this function is impossible to call in a welltyped program. 
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 anEquality y x
. Totality here provides us an assurance that this works for all possible inputsThis 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'sReflexive
constructor, idris realizes that the two naturals must be the same value and "rewrites" y into x, changing our output type toEquality x x
, which we can return simply with theReflexive
constructor, making use of the 'indiscernability of identicals' principle, and giving us axiom 3. 
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 anEquality y x
, and returning anEquality 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 theirReflexive
constructors, "rewriting" the output type intoEquality x x
, which can again be created simply with theReflexive
constructor, giving us axiom 4 
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 anEquality 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 theReflexive
constructor 
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 lefthanded 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:
 Exactly one argument must be pattern matched on This applies in our case because there is exactly one argument
 The right hand side of the
Zero
case must be 0  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 nonzero 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 constanttime 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 reimplementing 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.