And there are a ton of other type errors that you cannot catch. For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. A method that wants an integer in a range. An array of maximum N elements. And we can go on forever.
So what you do? I find code that uses excessive type checks too verbose, you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen (e.g. a variable that can be null but given a particular condition you know that it cannot be because it was initialized earlier, but the compiler is not smart enough to know).
So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript).
> For example take a method that wants a string in a particular format, you pass a string in another format and it breaks.
This sentence betrays a confusion about what types are, and how to use them. In particular, you seem to be mixing up two possible scenarios.
In the first scenario, we have a method which "wants a string" (i.e. its input type is 'String'), and we can "pass a string" (i.e. call it with an argument of type 'String'). This code passes the type-checker, since it implements the specification we gave: accept 'String'. Perhaps there are higher-level concepts like "formats" involved, and the resulting application doesn't work as intended; but that's not the fault of the types. More specifically: typecheckers verify that code implements its specification; but they do not validate that our specification captures the behaviour we want.
In the second scenario, we have a method which "wants a string in a particular format" (i.e. its input type is 'Format[A]'), and we "pass a string in another format" (i.e. call it with an argument of type 'Format[B]'). That is a type error, and the typechecker will spot that for us; perhaps pointing us to the exact source of the problem, with a helpful message about what's wrong and possible solutions. We do not get a runnable executable, since there is no meaningful way to interpret the inconsistent statements we have written.
tl;dr if you want a typechecker to spot problems, don't tell it that everything's fine!
If you want the safety and machine-assistance of such 'Format' types, but also want the convenience of writing them as strings, there are several ways to do it, e.g.
> A method that wants an integer in a range. An array of maximum N elements. And we can go on forever.
You're making the same mix-up with all of these. Fundamentatlly: does your method accept a 'Foo' argument (in which case, why complain that it accepts 'Foo' arguments??!) or does it accept a 'FooWithRestriction[R]' argument (in which case, use that type; what's the problem?)
Again, there are multiple ways to actually write these sorts of types, depending on preferences and other constraints (e.g. the language we're using). Some examples:
Your "integer in a range" is usually called 'Fin n', an array with exactly N elements is usually called 'Vector n t', etc. I don't think there's an "array of maximum N elements" type in any stdlib I've come across, but it would be trivial enough to define, e.g.
data ArrayOfAtMost Nat (t: Type) where
Nil : {n: Nat} -> ArrayOfAtMost n t
Cons : {n: Nat} -> (x: t) -> (a: ArrayOfAtMost n t) -> ArrayOfAtMost (S n) t
This is exactly the same as the usual 'Vector' definition (which is a classic "hello world" example for dependent types), except a Nil vector has size zero, whilst a Nil 'ArrayOfAtMost' can have any 'maximum size' we like (specified by its argument 'n'; the {braces} tell the compiler to infer its value from the result type). We use 'Cons' to prepend elements as usual, e.g. to represent an array of maximum size 8, containing 5 elements [a,b,c,d,e] of type 'Foo', we could write:
myArray: ArrayOfAtMost 8 Foo
myArray = Cons a (Cons b (Cons c (Cons d (Cons e (Nil 3)))))
Note that (a) we can write helper functions which make this nicer to write, and (b) just because the code looks like a linked-list, that doesn't actually dictate how we represent it in memory (we could use an array; or we could optimise it away completely https://en.wikipedia.org/wiki/Deforestation_(computer_scienc... )
Also note that we don't actually need to write such constraints directly, since we can often read them in from some external specification instead (known as a "type provider"), e.g. a database schema https://studylib.net/doc/18619182
> you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen
You might know it, but the compiler doesn't; you can either prove it to the compiler, which is what types are for; or you can just tell the compiler to assume it, via an "escape hatch". For example, in any language which allows non-termination (including Idris, which lets us turn off the termination checker on a case-by-case basis), we can write an infinite loop which has a completely polymorphic type, e.g.
-- Haskell version
anything: a
anything = anything
-- Dependent type version
anything: (t: Type) -> t
anything t = anything t
We can use this to write a value of any type the compiler might require. Even Coq, which forbids infinite loops (except for co-induction, which is a whole other topic ;) ) we can tell the compiler to assume anything we like by adding it as an axiom.
> So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript).
Static types certainly give a compiler more information to work with; although whether the resulting language is faster or not is largely orthogonal (e.g. V8 is a very fast JS interpreter; Typed Racket not so much).
As for merely using a type system for linting, that's ignoring most of the benefits. No wonder your code is full of inappropriate types like "string" and "int"! I highly recommend you expand your assumptions about what's possible, and take a look at something like Type Driven Development (e.g. https://www.idris-lang.org )
So what you do? I find code that uses excessive type checks too verbose, you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen (e.g. a variable that can be null but given a particular condition you know that it cannot be because it was initialized earlier, but the compiler is not smart enough to know).
So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript).