Constructors are red.

Types are blue.

Your code always works

Because Idris loves you.

In How Functional Programming Mattered, Zhenjiang Hu, John Hughes, and Meng Wang argue that (pure) functional programming has changed the way we think about programs. An important part of the reason why is equational reasoning and referential transparency.

As an example, Hu, Hughes, and Wang use a function to reverse a list to show how functional languages such as Haskell allow us to write properties of programs as programs, and to prove such properties by hand, just like in mathematics. But functional languages such as Agda and Idris go a step further. They have dependent types, which means we can write proofs of properties of programs as programs.

In this blog post, we'll use Haskell (GHC 7.10.2 and QuickCheck 2.8.1) to test that a function to reverse a list satisfies the property that such a function is its own inverse, and Idris (0.9.19) to prove that it does.

Let's begin by creating a file `reverse-reverse.hs`

for the Haskell
code. We're not going to use the standard `++`

and `reverse`

functions, so let's hide them:

```
import Prelude hiding ((++), reverse)
```

We can now add the definition of the `++`

function to append lists.
This is not necessary because it corresponds to the standard `++`

function, but it can be useful to include it for reference:

```
infixr 5 ++
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : xs ++ ys
```

Now, let's define a `reverse`

function to reverse lists:

```
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
```

Given a definition like the one above, we can express as a function
the property that `reverse`

should be its own inverse:

```
reverseReverse :: [Integer] -> Bool
reverseReverse xs = reverse (reverse xs) == xs
```

This function returns `True`

if applying `reverse`

twice to a list
yields the same list, and `False`

otherwise:

```
ghci> reverseReverse [1,2,3,4,5]
True
```

We can test this property using QuickCheck, which will generate 100 lists of integers and check that the property holds for all of them:

```
ghci> import Test.QuickCheck
ghci> quickCheck reverseReverse
+++ OK, passed 100 tests.
```

We've just tested that our definition of `reverse`

satisfies the
`reverseReverse`

property. Equational reasoning, however, gives us the
power to reason about definitions. Thus, we can actually prove that
the property holds for all finite lists. We can do it by induction on
the given list, as follows:

- In the case of an empty list:

`reverse (reverse [])`

`==`

(by definition of `reverse`

)

`reverse []`

`==`

(by definition of `reverse`

)

`[]`

- And, in the case of a list
`x:xs`

:

`reverse (reverse (x:xs))`

`==`

(by definition of `reverse`

)

`reverse (reverse xs ++ [x])`

`==`

(see below)

`reverse [x] ++ reverse (reverse xs)`

`==`

(by inductive hypothesis)

`reverse [x] ++ xs`

`==`

(by definition of `reverse`

)

`(reverse [] ++ [x]) ++ xs`

`==`

(by definitions of `reverse`

and `++`

)

`x:xs`

In order to prove that `reverse`

is its own inverse, we need to prove
that `reverse`

and `++`

commute for all finite lists:

```
reverse (xs ++ ys) == reverse ys ++ reverse xs
```

We won't prove this property here. Instead, we'll assume that it holds (and it does, we could prove it by induction too).

The above proof is one of the most basic examples of correctness proofs, but we did it by hand. Functional languages with dependent types make it possible to write such proofs as programs, which is even more impressive.

Let's create a file `reverse-reverse.idr`

for the Idris code. We're
not going to use the standard `reverse`

function, so let's hide it:

```
%hide reverse
```

Next, we can write the type of the `reverse`

function:

```
reverse : List a -> List a
```

Functional languages like Idris are great for type-driven and incremental development, and the Idris mode for editors such as Emacs and Vim take full advantage of that.

If we place the cursor on top of `reverse`

(the name of the function),
we can make a new definition with `C-c C-s`

for Emacs (or `\d`

for
Vim):

```
reverse : List a -> List a
reverse xs = ?reverse_rhs
```

This adds a line for the definition of `reverse`

and a hole
(`?reverse_rsh`

) to fill with the actual definition. We can place the
cursor on `xs`

and split cases with `C-c C-c`

(or `\c`

):

```
reverse : List a -> List a
reverse [] = ?reverse_rhs_1
reverse (x :: xs) = ?reverse_rhs_2
```

We now have two equations for the definition of `reverse`

and two
holes to fill with appropriate definitions. After loading the file
with `C-c C-l`

(or `\r`

), we can place the cursor on the
`?reverse_rhs_1`

hole and ask for its type with `C-c C-t`

(or `\t`

):

```
a : Type
--------------------------------------
Main.reverse_rhs_1 : List a
```

The only thing we know is that `a`

is a `Type`

and we need to provide
a value of type `List a`

. The only option we have is to fill the hole
with an empty list:

```
reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = ?reverse_rhs_2
```

We can now put the cursor over the `?reverse_rhs_2`

hole and ask for
its type:

```
a : Type
x : a
xs : List a
--------------------------------------
Main.reverse_rhs_2 : List a
```

In this case, we have that `a`

is a `Type`

, `x`

is a value of type
`a`

, `xs`

is a list of elements of type `a`

, and we need to provide a
value of type `List a`

. There's more than one way to build such a
list, but we already know the answer for reversing a list:

```
reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]
```

Since we have dependent types, we can define a new function for the
proof that `reverse`

is its own inverse:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
```

Given a value `xs`

of type `List a`

, `reverseReverse xs`

is a proof of
the property that `reverse (reverse xs) = xs`

. This is similar to what
we did with Haskell, but at the type level -- the `=`

here is an
actual data type representing equality.

Let's make a new definition for `reverseReverse`

:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse xs = ?reverseReverse_rhs
```

And split cases for `xs`

:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = ?reverseReverse_rhs_1
reverseReverse (x :: xs) = ?reverseReverse_rhs_2
```

In the case of an empty list, this is the type of the hole:

```
a : Type
--------------------------------------
Main.reverseReverse_rhs_1 : [] = []
```

We can prove that `[] = []`

by reflexivity. Actually, we can place the
cursor on the hole and tell Idris to search for a proof with `C-c C-a`

(or `\o`

). Idris will fill the hole with a `Refl`

, which is the only
constructor for the `=`

type:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) = ?reverseReverse_rhs_2
```

Let's check the type of the second hole:

```
a : Type
x : xs
xs : List a
--------------------------------------
Main.reverseReverse_rhs_2 : reverse (reverse xs ++ [x]) = x :: xs
```

We know that we need a proof of the property that `reverse`

and `++`

commute. This time, we can't simply assume that it holds -- we have to
either prove it or postulate it if we want to use it. We should prove
it, but let's postulate it and focus on `reverseReverse`

:

```
postulate
reverseAppend : (xs : List a) -> (ys : List a) ->
reverse (xs ++ ys) = reverse ys ++ reverse xs
```

We can `rewrite`

the left-hand side of the goal using the
`reverseAppend`

property for `reverse xs`

and `[x]`

:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in ?reverseReverse_rhs_2
```

Let's ask for the type of the new hole:

```
a : Type
x : xs
xs : List a
_rewrite_rule : x :: reverse (reverse xs) = reverse (reverse xs ++ [x])
--------------------------------------
Main.reverseReverse_rhs_2 : x :: reverse (reverse xs) = x :: xs
```

The type now includes a rewrite rule that explicitly tells us what was
replaced in the previous step. The left-hand side of the new goal can
be rewritten using the inductive hypothesis (that is, `reverseReverse xs`

):

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in
rewrite reverseReverse xs in ?reverseReverse_rhs_2
```

Let's ask for the type of the new hole:

```
a : Type
x : xs
xs : List a
_rewrite_rule : x :: reverse (reverse xs) = reverse (reverse xs ++ [x])
_rewrite_rule1 : xs = reverse (reverse xs)
--------------------------------------
Main.reverseReverse_rhs_2 : x :: xs = x :: xs
```

The only thing remaining is to prove that `x :: xs = x :: xs`

, which
is true by reflexivity:

```
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in
rewrite reverseReverse xs in Refl
```

"It type checks! Ship it!"

Many thanks to Eric Jones for the idea for this blog post.

For more information about Idris and complete tutorials, see Idris and the Idris documentation.

All the quotes in this blog post were taken from the Idris mode for Emacs.