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]
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))
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
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
One concrete example would be this rewrite of
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.