Types and tests have one thing in common, they prevent bugs in software.
What are the tests? This is the application you write to make sure that your actual software doesn't have some class of bugs and to make sure no such bugs will be introduced in the future.
What are type systems? Static type checker is an application that checks that your actual software doesn't have some class of bugs and to make sure no such bugs will be introduced in the future.
Side note: dynamic type systems combined with error tracking software also helps to discover bugs, but generally doesn't prevent an introduction of bugs in the future. Dynamic type system rather helps to catch the error, where it actually happens instead of down the stack. Have you ever seen on the webpage "NaN something" or "Blah-blah undefined" showed to the end user? Welp this is because nothing stopped error to propagate down the stack.
How types and tests bug prevention compares?
With tests, you can check almost* any type of errors, but the issue here is that you check one thing at once. So tests poking universe of all possible error here and there.
On the other hand, the type system can check that the whole class of some errors are absent, but it is limited in what class of errors it can check. Depending on the power of the type system and how it is used it can check more or fewer classes of errors.
Simplified schema showed below:
A way to improve type system effectiveness and other error prevention methodologies
There are ways to improve type systems effectiveness, for example:
- Making impossible state impossible
- An exhaustive check of pattern matching
- Opaque types
- IO validation
- Type-checked side effects
- Dependent type systems, like Agda and Idris
- And, probably, other things about which I forgot or don't know
There are other methods to prevent software errors, like:
- Garbage collection solves issues with unsafe memory operations
- The finite state machine makes sure there are no illegal states or no illegal transitions, this is like the first step to formal verification of state logic
- With borrow checker in Rust you can go for fearless concurrency
- Thanks to reference capabilities in Pony language it can do non-stop garbage collection, zero-copy messages in the actor model. It is kind of borrow checker on the steroids.
- Immutability prevents race conditions
- QuickCheck - a library for random testing of program properties
- Unidirectional data flow
But all the above is nothing compared to formal verification, like TLA+, Dafny, F star and others.
Conclusions:
- Types don't replace tests - you still need to write tests, even if you use type checker
- Types are more effective at eliminating some classes of errors
- Error prevention not limited by type checking and tests, there are other ways to make sure there are no errors in your application
Speed of adoption of tests vs types
Tests are easy to write for libraries (where the scope is limited) or for projects with established conventions, like Ruby on Rails. Tests are harder to write for the fresh code when you just started and doing some prototyping.
Types are easy to start with unless you have to deal with unreadable error messages and missing type signatures (Flow).
If you have experience with types, types should be much easier to adopt than tests, but keep in mind you still need to write tests for your code unless you are using something advanced as formal verification.
PS
TDD means Test Driven Development, but also can mean Type Driven Development.
This post is part of the series. Follow me on twitter and github.
Latest comments (0)