Hello, and thanks for asking.
In my Elixir experience, I don’t miss a type system for the solo purpose of checking that the types of expressions are ok.
In fact, I never feared refactoring large amounts of code, and usually I get everything ok at first, or sometimes after fixing one or two type mismatches, which in general are very easy to find and fix.
I do not recommend to write test just to check for types. I think it is a nonsense.
Instead, write tests to be sure that the code does what is supposed to do, and type-checking will come along the way.
Obviously, if your test coverage is not wide enough, then you probably are not testing a part of the code where a type mismatch is hidden … and this is where a static type system will help you avoid these hidden type mismatches. But if someone is not covering well the code with tests, then probably they don’t care for that code’s quality too, so you get as much as you put in.
What I expect of a kind of static type system that is really worth to use is that of a dependent type system. I have no experience with these, but I suspect they may help avoid writing large swathes of tests in exchange of writing proofs about what is expected from the code. For example, I think this kind of type systems can avoid peppering the code with assertions by providing proofs about what we want to assert.
The advantage of proofs is that they ensure a kind of “100% test coverage” of the code you prove. However, some say proofs are frequently (generally?) more difficult to write in comparison to tests.
Property-based testing can help you more than case-based testing, because it automatically tests on a large range of inputs, thus raising coverage, however it cannot provide full guarantees like proofs do.
I think these are all tradeoffs, and I look forward one day to experiment with such a dependent type system, to have a more complete view of this topic.
Hope this helped you.
