- Some error conditions are inexpressible in your program. You cannot write classical tests to verify these, as trying to recreate the erroneous conditions will result in type errors.
- You cannot forget to "write a type" like you can forget to write a test. A type always covers all the guarantees it makes. This is especially useful when there are no tests, as you have at least some kind of helper available to you.
- Types are a form of documentation. Again, even a poorly documented, poorly named project still has types.
- Types do not make tests obsolete, but they greatly reduce the number of them you have to write and maintain.
As a result of this, most Haskell projects have abysmal test coverage compared to what you'd expect in Python or Java. Nobody would (or could!) write tests that all "instanceof" checks are covered. When you forget to implement a branch in your program, you'll get a compilation warning. When you feed a value to a well-written function, you're guaranteed to get a non-nonsense result out of it (instead of an exception). But still, you can make core changes to programs you do not understand at all - while understanding the type system in general - and have your changes work as expected.
In a sufficiently strong type system, you can express constraints stronger than "returns a string" or "takes an integer". For instance, if you want to make sure that a particular function always returns a valid file descriptor, make a structure for file descriptors that just contains a single int, and give it a private constructor that can only be called by the low-level functions that call the actual syscalls, or maybe a public constructor that confirms that the provided integer is actually a file descriptor. Then, as long as your function typechecks, it can only possibly return a valid file descriptor, for all possible inputs.
If you take this to an extreme, you get the https://en.wikipedia.org/wiki/Curry-Howard_correspondence, that there's a direct mapping between mathematical propositions and types, and between their proofs and functions of the corresponding type. This is what all modern proof assistants build on top of, though their type systems are usually extremely complicated.
Really good type systems are incredibly powerful tools for testing and refactoring code.
Especially in the prototyping phase, I do a lot of iterating and refactoring - and I mean A LOT, because I've found that this is the best way for a good design to fall out. Sometimes like 20-30% of the code get refactored, replacing core data structures and control flow.
If I ever had to rely on unit tests for this, I'd shoot myself, mainly because it would make me 1/2 times slower (because I'd have to reimplement all unit tests every time) and this would really break my flow.
Also, relying on unit tests for refactoring means that having anything short of 100% code coverage (i.e. 70-80% isn't enough) defeats the purpose of the whole thing anyway - and I've yet to see 100% test coverage in a real-world project. I realize this isn't an argument in the context of your reply (it was either test coverage or static types), but still, something to consider.
And, again, I'm talking traditional types like in Java or C++ rather than dependent types and other esoteric stuff.
http://mit.bme.hu/~micskeiz/pages/code_based_test_generation...
Enjoy!
I would love to encode the business logic into types. But, I am always afraid I might end up in type hell!
Edit: In fact, there's this library! https://github.com/acowley/Frames
You don't need those with static types. You only need to write tests for your actual code, not things that the compiler can check for you.
Manually writing code to check things the computer can test for you is a waste of developers time.
Foo(str, str, str) strikes me as somewhat suspect. I realize this isn't always avoidable, but a lot of the time it is.
loginUser(String, String)
loginUser(Username, Password)