Exploring Idris: Reflexivity Tactics one up Unit Tests
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 = ReflproofNotFalse : (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).