Software Foundations in Idris; Chapter 1 - Weekdays

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.

Days of the Week

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.

Proofs in Action

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.

Closing Thoughts

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.