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.Protocol, which is almost exclusively checked at type checking time. So if such a thing exists, and you still say "types are checked at runtime", isn't that confusing?
I don't really know what you're trying to say here.
Why would it be less meaningful to say types are checked at runtime with ducktyping? The nature of ducktyping is that the specific class of an object does not matter relative to behaviour, but a class is not entirely equivalent to a type.
If I need an object that implements method `foo`, and don't care about class, then "objects that implements foo" is in itself a type, that can potentially be inferred and checked be it at runtime or before.
> 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".
You're thinking his "checks types" too narrowly. Every time I try to call a method on an object in a strongly typed language, typing is involved. It doesn't so much "check" it as look up the method to see whether this method applies to this specific objectat this point in time and decide whether or not to throw exceptions.
But the point remains that it is a typed. And strongly so - in both Ruby and Python objects has a type associated with the object itself, unlike e.g. C or C++ which are weakly typed because it is the variables that are typed, not the values.
Quibbles with your final paragraph: that's not what strongly typed means. It refers to when a language has strict rules restricting implicit type conversions. [0] Also, C++ has RTTI.
It's not that simple. There's no uniform definition of strong. You're right strong typing is often used to refer to absence of (or restrictions to) implicit type conversions, but it has also since the beginning been used to reference languages that does not prevent obscuring the identity of the type of an object.
E.g. Liskov and Zilles [1] defined it this way for example:
"whenever an object is passed from a calling function to a called function, its type must be compatible with the type declared in the called function."
Under this definition C and C++ fails hard, since you can statically cast a pointer to an object and pass it to a function expecting a totally incompatible type.
Note that the system described relied at least partly on dynamic/runtime type checks (in case it reads as if the quote above suggests they used "strong" to refer to static typing):
"It is desirable to do compile-time type checking, since type errors are detected as early as possible. Because of the freedom with which types can be used in the language, however, it is not clear how complete the compile time type checking can be. Therefore, the design of the language is based on a runtime type checking mechanism which is augmented by as much compile-time checking as is possible. "
If C++ fails when you do casts, why doesn't Haskell fail since it allows infinite recursion to build terms of whatever type you like? You can make the same argument: "don't do that". C++ compilers can warn when you cast. Haskell compilers can warn on incomplete pattern matches.
Is the definition you use not so broad as to admit all invariants being described as types?
If a method requires a dictionary arguments with a certain key, is that a type to you? If you extend the term "type" to cover all invariants, I don't think that is the way that the term is commonly used, even though many invariants can be proven in e.g. dependently typed languages.
All these terms are so wonky because a C++ type is not equal to a Haskell type. So I feel we can't ever have solid definitions of terms like "strong", since it depends what you compare it to, and it also depends what you compare from. So while X is strong in comparison to Y, that doesn't say much about X's relation to Z.
> 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
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
This never happens in, say, Haskell (statically typed and never performs runtime type checks) or in Forth (untyped, no concept of type at all).
> 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.
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.