I’ve been playing with Idris lately. It’s a very well-designed, dependently typed programming language. I’ve been impressed time and time again by the kinds of things I can express at the type level.

Towards this end, I decided to start working through Software Foundations(SF). Rather than using Coq, the language used to express ideas in SF, I’ve been translating examples to Idris.

SF opens up with an example explaining sum types in terms of days of the week. In Idris, the main data type looks like:

```
Day : Type -- the type of a type is `Type`!
-- this becomes important when dealing with higher-kinds
data Day
= Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday
```

As with Haskell (and other ML-inspired languages), the branches of this type are distinct from every other type and are enforced by the compiler.

Let’s look at a function definition, `nextWeekday`

:

```
total nextWeekday : Day -> Day -- type signature
nextWeekday d = case d of
Monday => Tuesday
Tuesday => Wednesday
Wednesday => Thursday
Thursday => Friday
Friday => Monday
Saturday => Monday
Sunday => Monday
```

`nextWeekday`

takes a day of the week and returns the weekday that follows it. A few things are notable:

- The implementation is guided by the types - we consider each case in turn
`total`

: this means that if a case is missing, make it a compile-time error- It’s one way of saying - require that my proofs be complete
- This is stronger than Haskell’s warning on inexhaustive pattern matches
`total`

can be left off, and the compiler won’t enforce totality

Now, let’s test this! Rather than put together a run-time test, let’s leverage the type system to lay out some properties. That I could do this was pleasantly surprising for me. Let’s test that `nextWeekday`

behaves as we expect for a few cases:

```
proofMonTue : Tuesday = nextWeekday Monday -- types as tests
proofMonTue = Refl
proofFriMon : Monday = nextWeekday Friday
proofFriMon = Refl
proofSatNN : Tuesday = nextWeekday $ nextWeekday Saturday
proofSatNN = Refl
```

We’ve covered only a few cases to test the waters. Notice that we’re using the function and type definitions we’ve written so far at the **type level**.

The definition of each of these functions is `Refl`

. What does that mean? `Refl`

goes back to the algebraic reflexive property. Here, we’re invoking the reflexive relation over equality. We’re saying: “ensure that LHS = RHS”. Expanding below to illustrate:

```
proofSatNN : Tuesday = nextWeekday $ nextWeekday Saturday
proofSatNN : Tuesday = nextWeekday Monday
proofSatNN : Tuesday = Tuesday
```

If `Tuesday`

did not equal `Tuesday`

, our test would fail at compile-time because it failed to satisfy reflexivity over equality.

I’m using the emacs editor with the idris-mode module in order to work through these examples. It *really* makes the compilation/proof-checking property a joy to work with.

Here’s the examples I’ve shown so far prior to compilation:

Here’s the example after I’ve triggered type-checking (Ctrl-c Ctrl-e):

Due to my particular color scheme, it’s **intensely green**.

The proof/type-checking step is fast, too. It takes more time to type the keys ‘ctrl-c’ ‘ctrl-e’ than it does for the type-check to complete.

Software Foundations is a great book for picking up these concepts. It’s also freely available.

It’s a lot of fun to work in Idris. It really highlights how much power we have available to us at the horizons of language design. If we ever refactored `nextWeekday`

in such a way that our type-level proofs were broken, we’d know at compile time, rather than having to wait to build and run our test suites.

Next time, I’ll cover the implementation of a simple Boolean algebra from SF using Idris.