> A little type system goes a long way, and there's such a thing as too much in my opinion.
Agreed.
The purpose of "types" is to make the program easier to understand, because the invariants expressed as type-declarations hold at all times of the program execution. That makes it EASIER to reason about the program, in other words makes it easier to understand your program and what it is doing, by understanding what it cannot be doing, meaning violating its type-constraints.
But now IF the type-declarations-language becomes highly advanced and thus complex and difficult to understand, that potentially makes your program more DIFFICULT to understand.
So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.
Of course if the program is small, it is typically easy to understand and may be even easier to understand without them.
> So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.
I don't agree with this. Part of the benefit of static types is to make it easier for programmers to reason about programs. But part is also to make it easier for compilers to reason about programs. By encoding more invariants in the type system it is possible to turn a larger class of bugs into compiler errors.
I would even go as far as arguing that in languages with manual memory management like C, types are primarily a means to tell the compiler how to treat & manipulate a given piece of memory. Type safety and making it easier for us to reason about code can be a side effect of that but it's not a given.
You have to distinguish between "understanding" and "reasoning". Understanding means "understanding what ... does", where as reasoning (in "functional" jargon) means (more like) "proving what ... does".
While it's quite easy to understand what e.g. `c = a + b;` in C does, reasoning about it is comparably hard, as there can be UB (overflow of a signed integer type) involved.
In the extreme, when you have an actual proof (in a dependently typed language), you only have to understand it, but no need to reason about it as the proof is already there ;)
[insert some dependently typed vector example here :D]
Agreed.
The purpose of "types" is to make the program easier to understand, because the invariants expressed as type-declarations hold at all times of the program execution. That makes it EASIER to reason about the program, in other words makes it easier to understand your program and what it is doing, by understanding what it cannot be doing, meaning violating its type-constraints.
But now IF the type-declarations-language becomes highly advanced and thus complex and difficult to understand, that potentially makes your program more DIFFICULT to understand.
So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.
Of course if the program is small, it is typically easy to understand and may be even easier to understand without them.