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.
SF opens up with an example explaining sum types in terms of days of the week. In Idris, the main data type looks like:
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 takes a day of the week and returns the weekday that follows it. A few things are notable:
total: this means that if a case is missing, make it a compile-time error
totalcan 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:
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:
Tuesday did not equal
Tuesday, our test would fail at compile-time because it failed to satisfy reflexivity over equality.
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.