Programming Idris 1

Written 2021-11-11

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:

  1. sym : x = y -> y = x is a function that basically expresses the property that equivalence is symmetric.
  2. (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
Now let's look at the finished proof:

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.