Exploring Idris: Reflexivity Tactics one up Unit Tests

Idris the Dragon, inspiration for the language

Idris is a programming language with parametric polymorphism (think generics), dependent types (types as first class members of the language), a totality checker (think halting problem) and a syntax similar to Haskell. My first observations of the language are with another feature — the proof syntax.

Most engineers are familiar with Unit Tests, independently written and automated tests of very small bits (units) of code. These are typically functions. They are written and executed in between the compilation and execution at both the engineers desktop (prior to check-in) and in the CI pipeline if there is one (it’s nearly 2020 you should have one). Unit tests help assure that changes to a unit of code don’t have unintended consequences down the line — that the code performs to its specification.

As I start my journey into Idris (it has only been two days) I find a strange comfort between their proof syntax and the role of unit tests. There are some subtle differences and I am sure intricacies I don’t yet comprehend , but my fascination is piqued.

Let’s consider a small bit of code:

namespace Booleans     data Bool = True | False     not : Booleans.Bool -> Booleans.Bool
not True = False
not False = True

You don’t have to be an astute developer to read this tiny bit of syntax. It defines a boolean type Bool and a not function. Bool has two (empty) constructors for the True and False.

The Haskell syntax takes is different than curly-brace type syntaxes and takes some getting used to. However it is not that complex: the first line represents the type signature, where the type after the last arrow indicates the return type of the function. In this case not takes a Bool and returns a Bool. The next two lines implement the function. If the input is True (not True) it returns False. The opposite is encoded on the last line.

Once we have a function coded we can write the proof (or test). It is a pretty simple expression (with some unfamiliar syntax):

proofNotTrue : (not True) = False
proofNotTrue = Refl
proofNotFalse : (not False) = True
proofNotFalse = Refl

Each of these two proofs has the same form. The name of the proof and a test of equality separated by a colon. The second line is the implementation of the test — in this case we ask Idris to invoke the reflexivity tactic via Refl. The reflexivity tactic is used to prove that something is equal to itself. There is more to the tactics implementation within Idris, but it is short of what a language like COQ supports.

The proof statement has a decided advantage over unit tests in that you encode the proof beside your function definitions in your code base. The compiler requires both the syntax to pass and all proofs to evaluate positive prior to compiling the code.

It is pretty cool that the language prevents you from compiling and executing a program that is wrong (provided your proofs are accurate).

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store