Earlier quoted context omitted.
Indeed. To expand on your point: yep, it's incorrect. An untyped language is a language in which there is no concept of type. Assembly languages tend to be untyped. Forth is untyped. The Ruby and Python languages do have the concept of type, it's just that they're dynamically typed, not statically typed. They check types at runtime.
But when you have things like "duck typing", don't you think "they check types at runtime" becomes less meaningful? The majority of functions written in Python, even the ones that have type annotations, do not effectively have "assert isinstance(...)" in the program text below their signature, which is what I'd expect after reading "check types at runtime". Also, Python now has (in its stdlib!) things like typing.Pro…
It's true that types aren't checked in the act of passing a value as an argument, but at bottom, Python still has a concept of types, and they are still checked at runtime. Try the following and you'll see Python check your types and determine that there's an error:
"Hello" + 42
> Python now has (in its stdlib!) things like typing.Protocol, which is almost exclusively checked at type checking time
Yes, Python is now adding optional static typing, and of course, JavaScript has TypeScript. I'm afraid I don't know a lot about these new systems but presumably the end result is that type errors can occur either at compile-time (or static type-checking time, or whatever we call it) or at runtime. This isn't exactly anything new, it's always been possible in Java for instance, which has always permitted downcasts, and has always had covariant array types, checking both at runtime. [0] This is despite being a statically typed language where all variables must have a fixed type, the type they are declared with. (Remember that a variable's type is distinct from the precise class of a pointed-to object.)
We can draw a distinction between statically typed languages like Java where there's still a need for runtime type checks, and statically typed languages like Haskell where there's no need for runtime type checks. Type theorists use the term soundness for this property: in a language with a sound type system, a program that is successfully validated by the static type system can never have a type-related error at runtime. In engineering terms then, a sound type system means you don't need to check types at runtime, as 100% of type errors are caught by the static type system and there's no way for type errors to ever arise at runtime.
I used Haskell as an example, rather than C, because although C doesn't give us runtime type-checks, C programs can still go haywire if you make a mistake in your program (termed undefined behaviour). C has an unsound type system, and it lacks runtime checks. This is one reason C is so famously 'unsafe'.
So anyway, we have the situation where Python code can encounter type errors at compile time or at runtime, and Java can encounter type errors at compile time or at runtime, but we call Python dynamically typed and we call Java statically typed. The difference is that in Java, a variable must be declared with a fixed type, unlike in Python.
Things can get messy in the middle-ground: in C#, the dynamic keyword allows for true dynamic typing, where a variable's type is determined at runtime. [1] So you could write a C# program in traditional Python style, where there's very little compile-time type-checking. And you could write a modern Python3 program using lots of static type assertions, minimising the opportunity for runtime type errors. We'll still call the C# language 'statically typed' as it's typically true of C# code, and we'll probably still call Python 'dynamically typed', as that will probably remain typically true of Python code.
Disclaimer: I'm not a type theorist or a programming language researcher, corrections welcome if I've got anything wrong.
[0] https://news.ycombinator.com/item?id=13050491
[1] https://docs.microsoft.com/en-us/dotnet/csharp/programming-g...