[dllthomas]

Yes they do.

Ignoring trivial cases and dependent types, types tell you one of two things: "this might be correct" or "this is incorrect". Again ignoring trivial cases where exhaustive checking is possible, that's the same thing that tests tell you - and it's a hugely useful thing to be told!

[hueving]

No they don't. They only tell you that you are matching function signatures correctly. This is valuable but it's not a substitution for unit tests.

[dllthomas]

"it's not a substitution for unit tests"

It is a substitute for those unit tests that are essentially checking type invariants. It is not a substitute for all unit tests, but I don't think anyone made (much less intended to make) that claim anywhere in this thread.

"They only tell you that you are matching function signatures correctly."

All of computation can be expressed as application of functions, so for sufficiently expressive function signatures that's not much of a limitation. Of course, if you want to guarantee that your compiles terminate, you need to apply some limits to the expressiveness of your function signatures... but there are powerful guarantees you can get out of even so simplistic a type system as C's, if you work with it rather than against it.

[curryhoward]

Type signatures can completely encode specifications in systems with dependent types. Of course no mainstream programming language supports dependent types, but it's worth pointing out that in principle a type can encode any property checked by a unit test. Actually, dependent types are strictly more powerful, since you can prove undecidable properties which can't be checked by unit tests (e.g., that a function does the right thing for all possible inputs).