I have heard discussions about why static typing is superior to testing (and vice versa) as the way to lower the number of bugs in systems, and I think such discussions are futile as they are comparing apples and oranges.
Consider the following program fragment (in Python with type hints).
def foo(i: int, j: int) -> bool:
return i < j
def bar(i: int, j: int) -> bool:
return i == j
If we consider only the type signatures of these functions, then we have the following.
foo: (int, int) -> bool
bar: (int, int) -> bool
Using only type signatures, we can flag the following invocations as faulty.
foo("1", 3) # first argument is not of int type
bar(3, [1,3]) # second argument is not of int type
However, type signatures are not sufficient to flag the following invocations as faulty.
if foo(3, 3):
print("val1 is equal to val2")
if bar(3, 5):
print("val1 is less than val2")
Now, we might think that these faults would not have occurred if the functions were named as equals
and less_than
. By renaming, observe that we are not relying on static typing to avoid the faults :)
Nevertheless, letβs go ahead and rename the functions.
def equals(i: int, j: int) -> bool:
return i < j
def less_than(i: int, j: int) -> bool:
return i == j
if equals(3, 3):
print("val1 is equal to val2")
if less_than(3, 5):
print("val1 is less than val2")
Even now, the code fragment is faulty.
The issue is there are (at least) two kinds of types and we have only specified only one kind of type. For the other kind of type, we are relying on the association between function names and expected function behaviors.
To understand the issue, consider the description of equals
function:
- Accepts two integer values i and j and returns a boolean value.
- Returns true if the inputs are equal; false otherwise.
The first part of the description constrains the values that are valid as input to and output from the function. This description is the value (domain) type of the function, which we specified using type hints (e.g., : int).
The second part of the description constrains the behavior of the function. This kind of description is the behavioral type of the function (one that can be realized in different ways). In the example above, we did not specify this kind of type information.
Static typing as available in most programming languages today are geared towards only specifying value types (and not behavioral types).
If you are still not convinced about behavioral types, then consider relying on just the function signature (List[int]) -> List[int]
and picking a function that sorts a given list of integers in ascending order.
What about testing?
Unlike static typing (as it is generally available today), testing is not about value types.
Testing is about specifying and checking behavioral types.
Specifically, a test case captures a specific behavior of a function (e.g., equals(3,3)
should evaluate to true, equals(3,5)
should evaluate to false), a test suite captures the behavioral type (i.e., a collection of expected behaviors) of a function, and testing checks if an implementation of a function is behaviorally type correct (i.e., function exhibits the expected behaviors).
To draw parallels with static typing, test suites are similar to type hints and testing is similar to type checking.
While testing may seem better than static typing, it is not the case. Unlike static typing, tests are neither succinct nor exhaustive in specifying the possible behaviors of a function under test (in general). This is true even with enhanced testing techniques such as property-based testing. Further, using testing as a way to ensure value type correctness is prohibitive in general.
So, where does this leave us?
Until the day we have static type systems that allow us to easily and succinctly specify both value and behavioral types and use them to check for type correctness, we will need both static typing and testing to lower the number of bugs in systems.
In short, static typing and testing are complementary. And, for now, we need to be able to specify and reason with types and create and execute tests.
Top comments (11)
Where have people been advocating that you don't need tests if you have a type system? As your article demonstrates very well, a type system only prevents you from having to write tests that ensure the function only works with the correct inputs types and returns the correct type. Or said perhaps said slightly more eloquently:
Tests should be testing for logic errors. The benefit of the type system is that you no longer have to write tests to validate function inputs and outputs. You still need tests for logic.
I have been privy to such discussions on social media involving knowledgeable folks taking extreme positions on both sides.
Yes, as of today, each have their strengths and weaknesses. This may change in the future. Until then, it is best to embrace them both :)
Do you have any links to someone taking an extreme on either side? I'd like to see their arguments.
These were remarks/threads I have seen on Twitter. So, unfortunately, nothing recorded :(
Here's a Twitter thread comparing static typing and testing -- twitter.com/Hillelogram/status/102....
By the way if you read his blog you'll also find interesting stuff on this subject and others (like formal proofs)
I am not saying Hillel or any static typing proponents are wrong. Having worked on program analysis/verification and formal methods, I am saying we need to have a broader and more permissive perspective. Instead of saying "static typing is the end all", it may be better to understand why we operate the way we do and be pragmatic about what it takes to get from where we are to where we want to be.
I definitely agree with the overall thesis, however generic types would help further constrain your equals and less than methods. Both should take the same generic type
T
which would ideally be bounded by someOrdered
orComparable
types.I doubt Python type hints support generics yet.
Anyways, you are right that generics would help. In this sense, richer static typing (e.g., linear types, ownership types, dependent types) might help checking properties/constraints via testing. However, I think we have long ways to go until static typing can tackle the kind of issues tackled by testing.
They do: mypy.readthedocs.io/en/stable/gene...
True dat.
Good to know Python type hints supports generics :)