Your type system is sound or complete (cannot be both, if it's a Turing-complete language). If it's dynamically typed, then it's probably complete but not sound (many, but not all, dynamically typed language implementations have some basic static type checking). If it's statically typed, it can be either sound or complete. The difference between sound and complete is: Sound type systems will reject valid programs that they cannot prove are valid; Complete type systems will reject only those invalid programs they can prove are invalid.
In practice, the choice is more one of default these days:
Do you default to static typing and allow some dynamic (runtime) type checking? C++, C#, Java, etc.
Do you default to dynamic typing and allow some static (compile-ish time) type checking? Python, JS, Common Lisp, etc.
This lets both sides have what they really want. They want to be able to express all valid programs (a complete type system) but they want to reject all invalid programs (a sound type system). They can't have it. So you end up choosing a direction to approach it from. Either start conservatively and relax constraints, or start liberally and add constraints.
If you accept that, then the case for dynamic typing is that it's a choice to move from the too permissive extreme towards a stricter position. For me this works better (in general, though I also happily use statically typed languages like Ada) because I find it easier to add constraints to a relaxed system than to remove constraints from a restrictive system.
It's very simple: sometimes lower development effort matters more than correctness. Not all software has to run in a hostile production environment to be useful.
Just saying "dynamic typing is easier" doesn't do it for me without further qualification since that statement doesn't conform to my own experience.
Please excuse my pedantry: That would seem to lead to the question …
I can see how it appeared that I was using the phrase in the incorrect way! That usage bothers me too, and I am attentive to it.
No, it is correct. The value None is not with the domain of type int, a parameter that can take the value None does not in fact have type int.
> This yields no value because when you say `= None` you are saying that this is an optional argument.
When you provide any default value, you are making the argument optional, but that's an orthogonal concern to the Optional[T] type, which doesn't mean “optional argument", it is simply a more convenient way of expressing Union[T, None], though with the modern type syntax, T | U is generally more convenient than either Union[T, U] or Optional[T] for U=None.
If you declare a function parameter as `foo: int = None`... that is just an incorrect declaration. Of course a variable annotated as `int` can take a `None` value, but that is because any variable can take any type in Python. Within the Python type (annotation) system it is simply the case that an `int` and an `int | None` are two different things, as they are in other languages (eg Rust's `T` vs `Option<T>` types).
Mypy used to support the "implicit optional" feature you describe but now you must make nullable arguments explicitly optional. This is in line with Python's "explicit is better than implicit" design philosophy. In any case, how long does it take you to just type `foo: int | None = None`? Or you could re-enable the old behavior to allow implicit optionals with `--implicit-optional` or the corresponding config file option. It seems like you just need to configure mypy to match your preferences rather than fighting with its defaults.
To return to the broader point, I'm unsure what an "irrelevant type warning" is, but I suspect that has something to do with my lack of appreciation for dynamic typing. Can you give an example that isn't just a complaint about typing an extra 6 characters or about mypy being misconfigured for your preferences?
Because you can run your program to see what it does without having to appease the type checker first.
There is nothing wrong with presenting type hints or type errors as warnings. The problems arise when the compiler just flat-out refuses to run your code until you have finished handling every possible branch path.
fn main() {
let x: i32 = if true {1} else {"3"};
println!("{}", x);
}
x = 1 if True else "3"
print(x)
"Can not" and "will not" are kind of the same thing in this context. It's not like compilers have free will and just decide to give you a hard time. It's the language design that makes it (im)possible to run code that won't type-check.
This means you can only really rely on the parts of your program which are type correct, so...
Surely you can't be against putting a TODO in an unfinished part of the code?
Who are you to tell me what I want? You are making all manner of tacit assumptions about the kind of work I do and what my requirements are. I absolutely do want the compiler filling in every hole it possibly can. For me, that's the whole point of using a high-level language in the first place. For the kind of work I do, what matters most is getting things done as quickly as possible. Correctness and run-time efficiency are secondary considerations.
But for people who prioritize precision and correctness, that's what programming languages were invented for.
But yeah, if all you need to do is build a vanilla app then an LLM is probably an effective tool.
2. Dynamic typing lets you change what shape your data is without having to change type annotations everywhere.
Problem is, I think both of these are deeply flawed:
1. If you're writing something nontrivial, you probably have several layers of nested function calls, some of which may be calls to libraries that are not yours. If you're saying "anything I can do these operations on, I accept", it becomes very difficult to say what the full extent of "these operations" are. Thus it becomes hard to say whether the caller is passing in valid input. You can "just try it", but that becomes hard if you care about it working in all cases.
2. Refactoring IDEs are a thing these days. You want to change the type signature? Press the button. Even better, it will tell you everything you broke by making the change - everywhere where you're doing something that the new type can't do. Without types, sure, you can just change it without pressing the button. Now try to find all the places that you broke.
It may be possible to construct a better steelman than I have done. For myself, even trying to steelman the position, I find it incredibly unconvincing.
And with #2, you can get that with static typing too... Let's say a method accepts an instance of an object `Foobar`. I can change the definition of `Foobar` ("change what shape [my] data is") without having to change type annotations everywhere.
I agree with you, I guess, that I find the steel man position unconvincing.
https://ics.uci.edu/~lopes/teaching/inf212W12/readings/rdl04...
Do failing tests show what we broke?
Any!
Then maybe the immediate feedback of consistent types conveys a false impression.
The implication of what you're saying seems to be that if you're concerned about some kind of correctness you should be writing unit tests anyway and not being so fussed about type checking in a language like Python. I suppose if you are strictly following TDD that might work, but in all other cases type checks give you feedback much more quickly than unit tests ever can. I guess I don't understand.
No doubt we're at cross purposes.
I'm a little surprised that you haven't mentioned — "Program testing can be used to show the presence of bugs, but never to show their absence!" (or existential versus universal quantification).
Oh, you don't have that? Then do not scorn the help you can get from types.
https://news.ycombinator.com/item?id=42473314
I wonder how many were not found.
"Less than 35 bugs were found in the 17,100 changes."