Recently, a friend of mine and I were going over the ages old tests vs. types debate. Specifically, if a programmer wants to have some degree of certainty that their program will function as intended, does it work better to use unit testing or static typing? However, the more I looked at the argument we were having, the less it made sense to me as a strict dichotomy. Obviously, best practices for ensuring Python code works as intended are different from ensuring Haskell code works as intended, and you'll catch some bugs with Python best practices that you won't catch with Haskell best practices and vice versa, but in a sufficiently advanced language, assertions about the code are the same as function types and vice versa.

For instance, consider the (rather trivial) example of a function that reverses lists. In python:

1 def reverse(list):
2   return list[::-1]

In Idris

1 reverse : List a -> List a
2 reverse = reverse' []
3   where
4     reverse' : List a -> List a -> List a
5     reverse' acc [] = acc
6     reverse' acc (x::xs) = reverse' (x::acc) xs

Suppose we want to show that an example list reversed twice is itself. In Python, we might try an assertion.

1 import unittest
2 
3 testVar = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
4 
5 assert testVar == reverse(reverse(testVar))

If we were doing something more complex, we could use unittest or nose or any number of other options, but for the sake of simplicity, we'll stick with with assert for now.

Now we wish to make the same assertion about our idris function.

1 testvar : List Int
2 testVar = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
3 
4 reverseTwice : testvar = reverse $ reverse testvar
5 reverseTwice = refl

Note that the assertion happens in the type of reverseTwice, not the definition like in the Python example, but the two serve the exact same purpose. This is because an assertion is a proposition about a program, and a proposition is a type, so any assertion can be written as the type of a variable, given sufficient tools to do so. The definition of the variable with that type then, is the proof of the proposition the assertion makes in the first place. Notably, this allows us to use relatively advanced tactics to make much more powerful assertions than in languages without this functionality. For instance, Jesse Hallett's category theory proofs.

One concrete example would be this rewrite of reverse by defanor, that generalizes our earlier assertion to not just testVar, but any Vect. Obviously, this is more work than a simple assert statement, but an assert statement is also more work than not testing at all, and for code that really needs to work, a proof that it always will work is often desirable.

Obviously, there are types of testing that can't be written as a type. It's unlikely that selenium can ever have a type-level equivalent, and something like quickcheck that uses stochastic methods to give a fuzzier guarantee is a fundamentally different tactic, but the vast majority of unit testing is equivalent to simple types. Not only that, but dependent types and totality checking allow us to check every possible value for a parameter against its expected output all at once using mathematical reasoning. And while there is certainly a place for assertions, dependent types make them seem as primitive as the goto when it comes to ensuring program correctness.