The static typing makes even less sense at finer code scopes, like I don't need to keep asserting that a for-loop counter is an int.
As for your comment on `any`, the reason why one doesn't want to fall back on such is that you throw out most of the gains of using static types with such a construct when your function likely doesn't work with `any` type (I've never seen a function that works on absolutely anything other than `id :: a -> a` and I argue there isn't one even with RTTI).
Instead you want to declare the subset of types valid for your function using some kind of discriminated union (in rust this is `enum`, zig `union(enum)`, haskell ADTs/GADTs, etc etc) where you set a static bound on the number of things it can be. You use the type system to model your actual problem instead of fighting against it or "lying" (by saying `any`) to the compiler.
The same applies to services, APIs, protocols, and similar. The more work the compiler can help you with staying on spec the less work you have to do later when you've shipped a P1-Critical bug by mistake and none of your tests caught it.
Indeed "any" breaks type checking all around it, but it can be contained more easily in a helper func with a simple return type. Most common case is your helper does a SQL query, and it's tedious and redundant to specify the type of rows returned when the SQL is already doing that.
This is true, but the difference is you don't have to write a compiler, it's already written for you. The testing, you have to write, and do so correctly.
A lot of the woes of statically typed languages can be mitigated with tooling. Don't want to repetitively create types from an OpenAPI spec? Generate the code. Don't want to create types from SQL records? Generate the code. Don't want to write types everywhere? Deduce them.
You get all the benefits of static typing, but none of the work. It's so advanced these days that lots of statically-typed languages look dynamically-typed when you see the code. But they're not, everything has a type if you hover over them. The type deduction is just that good.
For example `foo :: Semigroup a, Traversable t => t a -> a` I already know that whatever is passed to this function can be traversed and have it's sum computed. It's impossible to pass something which doesn't satisfy both of those constraints as this is a specification given at the type level which is checked at compile-time. The things that cannot be captured as part of a type (bounded by the effort of specification) are then left to be captured by tests which only need to handle the subset of things which the above doesn't capture (e.g `Semigroup` specifies that you can compute the sum but it doesn't prevent `n + n = n` from being the implementation of `+`, that must be captured by property tests).
Another example, suppose you're working with time:
tick :: Monad m => m Clock.Present
zero :: Clock.Duration
seconds :: Uint -> Clock.Duration
minutes :: Uint -> Clock.Duration
hours :: Uint -> Clock.Duration
add :: Clock.Duration -> Clock.Present -> Clock.Future
sub :: Clock.Duration -> Clock.Present -> Clock.Past
is :: Clock.Duration -> Clock.Duration -> Bool
until :: Clock.Future -> Clock.Present -> Clock.Duration
since :: Clock.Past -> Clock.Present -> Clock.Duration
timestamp :: Clock.Present -> Clock.Past
compare :: Clock.Present -> Clock.Foreign.Present -> Order
data Order = Ahead Clock.Duration | Equal | Behind Clock.Duration
In short, types are specifications, programs are proofs that the specification has a possible implementation, and tests ensure it behaves correctly for that the specification cannot constrain (or it would be too much effort to constrain it with types).
As for SQL, I'd rather say the issue is that the SQL schema is not encoded within your type system and thus when you perform a query the compiler cannot help you with inferring the type from the query. It's possible (in zig [1] at least) to derive the type of a prepared SQL query at compile-time so you write SQL as normal and zig checks that all types line up. It's not that types cannot do this, your tool just isn't expressive enough. F# [2] is capable of this through type providers where the database schema is imported making the type system aware of your SQL table layouts solving the "redundant specification" problem completely./
So with all of that, I assume (and do correct me if I'm wrong) that your view on what types can do is heavily influenced by typescript itself and you've yet to explore more expressive type systems (if so I do recommend trying Elm to see how you can work in an environment where `any` doesn't even exist). What you describe of types is not the way I experience them and it feels as if you're trying to fight against a tool that's there to help you.
[1]: https://rischmann.fr/blog/how-i-built-zig-sqlite [2]: https://github.com/fsprojects/SQLProvider
Statically-types languages are a form of automatically-verified documentation, and an opportunity to name semantic properties different modules have in common. Both of those are great, but it is awkward that it is usually treated as an all-or-nothing matter.
Almost no language offers what I actually want: duck typing plus the ability to specify named interfaces for function inputs. Probably the closest I've found is Ruby with a linter to enforce RDoc comments on any public methods.
Javascript has to check on each iteration that the item is an int and for arrays that the length of those arrays hasn't changed underneath along with a bunch of other things as the language doesn't guarantee that it can't change. Even the JIT compiler in use has to check "is this path still that I expect" as at any point the type of the variable used in the loop can change to something else which invalidates the specialization the JIT compiler emitted for the case of it being an int. When you don't use languages with static types you push all of this work on runtime which makes the program slower for every check it needs to do while offering none of the advantages you have with static types.
Thus with a for loop in say C you don't assert that it is an int each time you statically constrain it to be an int as the loop condition can well be based on something else even if int is the more common to use. For example in zig `for` only takes slices and integer ranges with any other type being a compile-error:
var example: [1 << 8]usize = @splat(0);
for (&example, 0..) |*num, int| num.* = int;