Yes, you're right. I'm not very familiar with Haskell, but I was thinking about it when I called the title "An alternative.."
I think of Haskell as being to tests what up-front design is to Agile. It's great if you're trying to carve out right and wrong behaviors along the dimensions it's been designed to help with (and my vague sense is that linear types and other such advances are trying to expand that set of dimensions). But how would you ensure that your program meets its performance guarantees? Or is guaranteed not to block between these two memory barriers? Tests are less rigorous and more work, but if you're willing to put in the elbow grease they'll work for anything you throw at them.
That sounds about right. Static types can only guarantee a certain subset of behavior. Unit tests work for a huge amount of behavior, because they run at run-time. They are very versatile. But there are still some things that unit tests cannot test.
In particular, unit tests cannot guarantee the absence of behavior. As an example, Haskell can use its static type system to say, "this function (and any functions it uses) is guaranteed to be pure". Or you can say, "this function (and any functions it uses) is guaranteed to only use certain side effects, but other side effects do not happen".
Languages like Idris go even further and can guarantee that a function terminates (never goes into an infinite loop)!
As another example, Haskell has Software Transactional Memory, and it uses the static type system to guarantee that arbitrary I/O cannot occur, which is important because the transaction might be retried multiple times.
I don't remember which language it was in, but I remember reading about a language that used static types to guarantee that exceptions are always handled. In other words, you will never have an uncaught exception.
Nulan uses its static type system to make a distinction between blocking impure functions and non-blocking impure functions. In JavaScript, there's a big difference between blocking and non-blocking, both in terms of behavior and performance. By using the static type system, it's possible to say "this function (and any functions it uses) is always blocking, and never non-blocking".
As you are aware, Rust uses its static type system to guarantee that pointers are always used correctly, and that data races cannot occur, even with concurrency.
But the biggest reason I like static types is because they make refactoring easier. Let's say you have a type that represents a person. So you have a name property, age property, etc.
Now let's say you want to add in a new property. Some of the existing functions will need to change to accommodate this new property. Without static types, you need to carefully go through your entire code base and find the functions which use the type, and then change their behavior to work with the new property.
Unit tests won't help you with that, because the unit tests are all testing the old properties, not the new property. So in the end, you have no choice but to just bite the bullet and spend a significant amount of time searching through the code and making the changes.
But with static types, it's as simple as adding the new property, compiling, fixing any type errors, compiling, fixing any type errors, etc.
Each type error tells you the file and line where the error occurs, making it easy to fix. You don't need to search through your code to find the places which need fixing: the type system does that for you. And after all the type errors are fixed, it's basically guaranteed that your code is correct.
Another example: a function used to always return a result, but now you need to change it so that it can potentially fail. So anybody that uses that function now has to account for the possibility of failure. With a static type system, you simply make the change and fix the type errors.
With unit tests, you better hope that you have 100% code coverage, because you're going to need it to find all of the functions which need to be changed. And don't forget that the unit tests need to be updated, and you probably need to add in new tests as well. That takes time, in addition to the time spent fixing the code.
So the end result is that it's faster and easier to refactor with a static type system, and it's more likely to be correct as well.
So I think static types and unit tests complement each other: they can both do things that the other cannot. Static types can make guarantees that unit tests cannot, and static types also remove some of the burden from unit tests, which speeds up development without sacrificing correctness.
On the other hand, unit tests can make certain guarantees that static types cannot. So in the end, I think you need both.
P.S. Static typing also helps tremendously with things like smart IDEs. I think Unison is a really cool example of that:
Typeclasses are amazing. They're similar to multimethods, but more powerful, and they have the same performance as regular functions.
You can use them to solve the expression problem, giving you a huge amount of flexibility, power, and conciseness. Or you can use them to create dynamically scoped variables which actually work correctly (unlike dynamic variables in most languages).
The thing is, typeclasses are only possible with static types. They're the main reason I changed Nulan to be statically typed.
----
By the way, I would like to point out that the static type systems in languages like Haskell is very different from the static type systems in other languages like C, C++, or Java. So even if you like/dislike one of them, you might end up liking the other. I used to lump all of the static type systems together, but I think that's a mistake.
There are bugs which are not caught by C, C++, or Java, but which are caught by Haskell. And there are programs which do not type check in C, C++, or Java, but which do type check in Haskell.
Yes, I wanted to say something similar in response to your phrasing that "type systems (including dynamic and static type systems) are another way to carve out the territory". When you say "dynamic type systems", in particular, I think Python and Ruby, and the modularity guarantees there seem much inferior to tests. But Haskell and the more advanced type systems might well disprove my thesis.
You're right: dynamic type systems tend to provide very weak guarantees. But I'll still take those guarantees over silent failures.
In my opinion, static guarantees (including static types) are the best, followed by unit tests, followed by dynamic guarantees (including dynamic types).
Yes, that's exactly the trade-off I've been thinking of. When I program I like to start out writing tests at the start when I don't yet know what properties I should try to enforce. Over time I start finding places where tests aren't good enough, and start feeling the need for more rigorous checking. But by then I've painted myself into a corner with my choice of language, and it's too hard to switch to a more rigorous platform.
In Mu my plan to break this dichotomy between coverage and soundness is to allow arbitrary metadata to be attached to instruction operands. As a result you aren't stuck with the type annotations and checking that I build into the system. You can have arbitrary metadata and will be able to write programs that can deduce and check this metadata to enforce all sorts of properties. Arbitrary checkers feels to me like a generalization of Lisp macros.
Arbitrary metadata is cool. Clojure has arbitrary metadata, which the compiler uses to optimize function performance, but you can use it for other purposes as well:
