# Programming Idris 1

The promise of strong, static typing as it's used in programming languages
like Haskell is that "if it compiles it's correct". While Haskell
e.g. fulfills that promise to a greater degree than other languages, it's
still hard to encode many invariants into the types of a program. What I'd
like to do more often is to have an actual *proof* that my code has
certain properties. A programming language that fulfills the promise of "if it
compiles it's correct" to a greater degree
is Idris.

### Idris basics

To developers that are familiar with Haskell the syntax of Idris is immediately familiar, consider e.g. the following function:

```
mySum : List Nat -> Nat
mySum [] = 0
mySum (x :: xs) = x + mySum xs
```

The only really notable difference here is that the colon `:`

is
used for beginning a type-signature while the double-colon is used to prepend
elements to a list.

Data type definitions should also look familiar. Consider for example the way
natural numbers are encoded
as peano numbers in the
ubiquitous `Nat`

type:

```
data Nat =
Z |
S Nat
```

Another frequently used data structure in Idris are length-indexed vectors, i.e. vectors that carry their length in their types:

```
data Vect : (len : Nat) -> (a : Type) -> Type where
Nil : Vect Z a
(::) : (x : a) -> (xs : Vect len a) -> Vect (S len) a
```

This is an ADT with two variants:

- A variant for an empty vector, with length zero
- A cons operator that prepends an element and increases the length by one

Using the definitions we have so far we can define a reversal function such as:

```
mySnoc : Vect n a -> a -> Vect (S n) a
mySnoc [] x = [x]
mySnoc (y :: ys) x = y :: (mySnoc ys x)
myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse (x :: xs) = mySnoc (myReverse xs) x
```

In contrast to functions in similar languages this gives us an additional
guarantee that our `myReverse`

function does not change the length
of the input list. However this guarantee still doesn't tell us a lot about
the behavior of this function in the rest of this post I'll explore ways to
encode more interesting guarantees.

### Writing proofs

In this section we'll prove that two properties hold for
our `myReverse`

function:

- In a first step we will prove that prepending an element to the reverse of a vector is the same as first appending the element and then reversing. The following figure will illustrate what we want to prove:
- Using the helper proof from step 1 we'll prove that reversing a vector and reversing the result yields the original vector.

#### Helper proof: append then reverse == reverse then prepend

Proofs in Idris are formulated as types so let's start with that:```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x xs = ?rhs
```

There are some things that are notable about this code snippet:

- The proof is formulated as a function that will give us a proof value that we can use at runtime for any given element and vector
- Since we don't know how the implementation will look like yet we'll leave
it as a
*hole*. Holes are much more important in Idris editing than in Haskell. More on that later. - The
`=`

in the result of the function is not magic but rather a vanilla type called`=`

with one constructor which is`Refl`

.

What happens if we try to load this code in the REPL? We'll get something like

```
- + Blog.rhs [P]
`-- 0 n : Nat
0 a : Type
x : a
xs : Vect n a
--------------------------------------------------------
Blog.rhs : myReverse (mySnoc xs x) = x :: myReverse xs
```

This is a listing of all holes in our program with their name, expected type and
the local variables that are in scope.
The way we'll go about our proof is by induction. The idea of inductive proofs is to prove two things:

- given a property holds for something of size
`n`

then it will also hold for "one more item", i.e. size`n+1`

. The hypothesis that the property holds for something of size`n`

that this step works with is called*induction hypothesis* - we also need a base-case so that the first proof will cover everything after that base case

Applying this to our case means we'll do a case split on `xs`

. The
interactive editing support that Idris offers us actually helps us with
this. In emacs there is a function called `idris2-case-split`

that
we'll trigger when hovering over xs which will expand the definition of our
proof to this:

```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x [] = ?rhs_1
appendReverseEqReversePrepend x (y :: xs) = ?rhs_
```

Let's deal with our base case first. Fortunately Idris is not completely dumb
so it can automatically figure out that `myReverse (mySnoc [] x)`

is in fact the same as `x :: myReverse []`

So all we have to do is
to replace the first hole with `Refl`

and we're done:

```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x [] = Refl
appendReverseEqReversePrepend x (y :: xs) = ?rhs_
```

When we load this in the repl we now get a changed hole description

```
- + Blog.rhs_ [P]
`-- 0 a : Type
x : a
y : a
xs : Vect len a
0 n : Nat
-------------------------------------------------------------------------------
Blog.rhs_ : mySnoc (myReverse (mySnoc xs x)) y = x :: mySnoc (myReverse xs) y
```

The next step in completing our proof is to do the inductive step. Since we're
going for a proof by induction the first thing we should do is to formulate
our induction hypothesis. In our case the induction hypothesis is that
our `appendReverseEqReversePrepend`

proof also holds if the vector
we're proving for is one element shorter. If we formulate the induction
hypothesis we get code that looks like this:

```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x [] = Refl
appendReverseEqReversePrepend x (y :: xs) =
let inductionHypothesis = appendReverseEqReversePrepend x xs
in ?rhs_
```

The next thing we should do is look at our hole again:

```
- + Blog.rhs_ [P]
`-- 0 a : Type
x : a
y : a
xs : Vect len a
0 n : Nat
inductionHypothesis : myReverse (mySnoc xs x) = x :: myReverse xs
-------------------------------------------------------------------------------
Blog.rhs_ : mySnoc (myReverse (mySnoc xs x)) y = x :: mySnoc (myReverse xs) y
```

What we have gained with the `inductionHypothesis`

value is proof
that we can use to `rewrite`

the actual result we're going to
return. The `rewrite`

construct in Idris essentially allows to
replace an `A`

that occurs in an expression with
some `B`

if we have a proof of `A = B`

. Doing this
results in the following code:

```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x [] = Refl
appendReverseEqReversePrepend x (y :: xs) =
let inductionHypothesis = appendReverseEqReversePrepend x xs
in rewrite inductionHypothesis in ?rhs_
```

Looking at our hole once more reveals we've made progress:

```
- + Blog.rhs_ [P]
`-- 0 a : Type
x : a
y : a
xs : Vect len a
0 n : Nat
inductionHypothesis : myReverse (mySnoc xs x) = x :: myReverse xs
-------------------------------------------------------------------------
Blog.rhs_ : x :: mySnoc (myReverse xs) y = x :: mySnoc (myReverse xs) y
```

What you'll see now is that the left hand side of our equality-proof is the
same as the right hand side. Such proofs are expressed with the single
constructor of the `=`

type which is `Refl`

. So let's do
that and we're done:

```
appendReverseEqReversePrepend : (x : a)
-> (xs : Vect n a)
-> myReverse (mySnoc xs x) = x :: myReverse xs
appendReverseEqReversePrepend x [] = Refl
appendReverseEqReversePrepend x (y :: xs) =
let inductionHypothesis = appendReverseEqReversePrepend x xs
in rewrite inductionHypothesis in Refl
```

#### Proving that reverse (reverse xs) == xs

As in the helper proof we'll do this one by induction as well. Let's start out by formulating our type signature again:

```
reverseTwiceIsId : (xs : Vect n a) -> myReverse (myReverse xs) = xs
reverseTwiceIsId xs = ?rhs
```

Let's first case split on `xs`

. The empty vector case is again
trivial, I'll also add our induction hypothesis immediately for the sake of brevity:

```
reverseTwiceIsId : (xs : Vect n a) -> myReverse (myReverse xs) = xs
reverseTwiceIsId [] = Refl
reverseTwiceIsId (x :: xs) =
let inductionHypothesis = reverseTwiceIsId xs
in ?rhs
```

Let's look at our hole again:

```
- + Blog.rhs [P]
`-- 0 a : Type
x : a
xs : Vect len a
0 n : Nat
inductionHypothesis : myReverse (myReverse xs) = xs
----------------------------------------------------------
Blog.rhs : myReverse (mySnoc (myReverse xs) x) = x :: xs
```

The current equality we have to prove looks a bit awkward. What we're going
for is to use our helper proof to extract the `x ::`

part from the
left hand side. If you look closely at our proof obligation `rhs`

you'll see that we can use our helper proof on the ```
mySnoc (myReverse xs)
x
```

part. If we do that our updated proof looks like this:

```
reverseTwiceIsId : (xs : Vect n a) -> myReverse (myReverse xs) = xs
reverseTwiceIsId [] = Refl
reverseTwiceIsId (x :: xs) =
let inductionHypothesis = reverseTwiceIsId xs
in rewrite appendReverseEqReversePrepend x (myReverse xs) in ?rhs
```

```
- + Blog.rhs [P]
`-- 0 a : Type
x : a
xs : Vect len a
0 n : Nat
inductionHypothesis : myReverse (myReverse xs) = xs
-------------------------------------------------------
Blog.rhs : x :: myReverse (myReverse xs) = x :: xs
```

At this point it should be obvious that we're pretty much done once we use our induction hypothesis. To do this we'll make use of two helper functions:

`sym : x = y -> y = x`

is a function that basically expresses the property that equivalence is symmetric.`(f : (t -> u)) -> a = b -> f a = f b`

This helps us to deal with rewriting things that are equal except for a modifier that is the same in both sides

```
reverseTwiceIsId : (xs : Vect n a) -> myReverse (myReverse xs) = xs
reverseTwiceIsId [] = Refl
reverseTwiceIsId (x :: xs) =
let inductionHypothesis = reverseTwiceIsId xs
in rewrite sym $ cong (x::) inductionHypothesis in
rewrite appendReverseEqReversePrepend x (myReverse xs) in Refl
```

### Conclusion

In this post we walked through some of the basics of Idris and how
equivalences in Idris can be proven. It should be emphasized how amazing what
we did here is: *we don't have to write any more unit tests for the
properties we've proven and we're guaranteed that they'll hold.*

The downside is that writing these proofs is cumbersome, especially if you're not familiar with writing them. It does get easier though, once one gets used to it.

The equality proved in this post is fairly basic but using the techniques shown here I'll do a follow-up post in which we'll write a sort-function that is proven to output a vector that is both guaranteed to be sorted and guaranteed to have the same elements as the original vector.