Python: `foo = '1' + 1` gives `TypeError: Can't convert 'int' object to str implicitly`
C: `char bar[] = "1"; char* foo = bar + 1;` gives literally no error.
Good errors occur because of strong/weak typing, not because of static/dynamic typing.
A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO, and a type system that gathers little type information is a weakly-typed language. Static languages can be strongly typed (Haskell, ML) or weakly typed (C) and dynamic languages can be strong(ish)ly typed (Python) or weakly typed (JavaScript).
There are two sources of such information: the static context (e.g., in Scheme, which variables are in scope) and the dynamic environment (e.g., again in Scheme, the type of an object, and, in Python, pretty much everything). The static context grows whenever you bind variables in the program text (e.g., when you define a procedure). The dynamic environment grows when the control flow reaches such binders (e.g., when it enters a called procedure).
> I posit that there's nothing stopping you from gathering that information at runtime; it just typically isn't done to the same extent in dynamic languages as in ML-family languages.
A fundamental limitation of dynamic analysis (that applies to any dynamic language, already invented or to be invented in the future) is its inability to “peek into the future”. For example, if you create an empty mutable list object, dynamic analysis can't tell you what its element type is supposed to be, until you actually start inserting elements into it. Static analysis, on the other hand, can determine what the element type is solely from inspection of the program text, e.g., if you make a procedure that inserts strings into the list, the list's element type must be a supertype of string, whether you actually call the procedure or not.
Here's an example of a type error that Python couldn't possibly diagnose: http://ideone.com/0KUVVb
> A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO
This isn't true. C++'s type system gathers a lot of type information, yet C++ isn't “strongly typed” (assuming that term means anything at all) by any stretch of the term.
Rather than “strongly-typed”, a more useful term is “sound”. A type system is sound when it actually protects the language's basic abstractions. For example, Standard ML has a sound type system, and there's a formal proof of this fact. Java's type system is actually unsound, but it makes up for this deficiency by inserting runtime checks to turn wrong operations (e.g., invalid downcasts) into runtime exceptions (just like in Python!). C++'s type system is also unsound, and performing wrong operations is simply undefined behavior.
Heh, I intended that as a rhetorical question, but I admit that wasn't clear from my post, and this is a very thorough answer. :)
> For example, if you create an empty mutable list object, dynamic analysis can't tell you what its element type is supposed to be, until you actually start inserting elements into it.
That's a limitation of most implementations of mutable list objects in dynamically typed languages, but there's nothing preventing a dynamic language from having a mutable list that enforces a single type in a list at runtime starting from the construction of the list. In Python it would not be difficult to implement an `IntegerList` class which enforces that all its elements are integers, for example.
Yes, we can't determine at compile time that the following is a type error:
a = IntegerList()
a.append('Hello, world')
Further, one can imagine a hypothetical dynamic language where we parameterize types, too:
a = List<Integer>()
a.append('Hello, world')
> > A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO
> This isn't true. C++'s type system gathers a lot of type information, yet C++ isn't “strongly typed” (assuming that term means anything at all) by any stretch of the term.
You're right, I can't imagine what brain fart caused me to say what I said there. /shrug
> Rather than “strongly-typed”, a more useful term is “sound”. A type system is sound when it actually protects the language's basic abstractions. For example, Standard ML has a sound type system, and there's a formal proof of this fact. Java's type system is actually unsound, but it makes up for this deficiency by inserting runtime checks to turn wrong operations (e.g., invalid downcasts) into runtime exceptions (just like in Python!). C++'s type system is also unsound, and performing wrong operations is simply undefined behavior.
"Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't). "Strength" is a different concept which admittedly isn't an objective measure. But I think we can agree on it as a subjective measure for comparing some things. For example, I do think there's a real phenomenon described that we can agree on when I say that Python is more strongly-typed than JavaScript, and Java is more strongly-typed than C, and I think you'd agree with me on these comparisons, even though none of these languages are soundly typed. Sound typing corresponds to a very strong type system. :)
> Further, one can imagine a hypothetical dynamic language where we parameterize types, too: (snippet)
If you're going to take the trouble to specify that it's an integer list, might as well use a statically typed language, right? When you use a dynamically typed language, presumably the point is to not have to worry about static types.
> The reason, I think, that this isn't done is that once you get to the point where you're putting type parameters like this, you've lost most of the benefits of a dynamic type system, and would gain more from seeing your errors at compile time.
Yep, exactly. The optimal tradeoff is that you don't anotate anything, yet static types are still there. What you described achieves the exact opposite.
> "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't).
That's precisely why it's better!
> For example, I do think there's a real phenomenon described that we can agree on when I say that Python is more strongly-typed than JavaScript,
Out of the box, Python certainly catches more errors than JavaScript, and does so earlier.
> and Java is more strongly-typed than C
I'm not so sure about this one. Although Java is certainly safer than C, because it replaces undefined behavior with a battery of runtime checks (just like a dynamic language), I feel it's about equally difficult in Java and C to translate my thoughts into types. Ironically, C++, despite being unsafe and unfixably so, does a much better job of helping me arrange things so that my errors are caught statically.
Yes, I said that. :)
> > "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't).
> That's precisely why it's better!
Well... it's better for some purposes, but it doesn't allow us to talk about most languages effectively. None of the top 10 most commonly-used languages in industry today are soundly typed. If memory serves me, in fact, the only language I know of with a mature implementation that's soundly typed is ML. So it's a useful concept in a very specific context, but not that useful for talking about most languages.
> I'm not so sure about this one. Although Java is certainly safer than C, because it replaces undefined behavior with a battery of runtime checks (just like a dynamic language), I feel it's about equally difficult in Java and C to translate my thoughts into types.
Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it.
C does no real checking i.e. around `void` pointers, adding integers to pointers, tagging unions, etc., at compile time or at runtime, which is why I claim it's a very weakly-typed language (and also why I tend to avoid some of those features).
For me, the real payoff of using a static type system is enforcing the invariants I care about. In other words, a type system is a tool that partially relieves me of my proof obligation as a programmer. A “type system” that doesn't do this is just annoying ceremony. So, if we insist on calling type systems “strong” and “weak”, this is still a binary question: a type system is either capable (“strong”) or incapable (“weak”) of expressing what I want to express in a crisp, elegant, crystal clear way. From this point of view, Java is just as unacceptable as C, perhaps even more so, because C at least has the decency not to pretend it has much of a type system.
OTOH, it seems that, to you, and perhaps most programmers, a type system is merely a tool for preventing catastrophic errors. If that's your only goal, then turning catastrophic errors (say, memory corruption) into less catastrophic ones (say, raising exceptions everywhere) is a perfectly valid approach, and of course Java is “more strongly typed” than C. This can be useful or harmful, depending on what kind of program you're writing, but I refuse to call it a type system.
ML family is particularly nice -- with Hindley-Milner type inference, you get a lot of static guarantees with none of the verbosity of languages like Java.
(0) Parametricity: Type variables are never case-analyzed. As a result, types convey useful information about what functions may or may not do. Haskellers call this “free theorems”. Java's `instanceof`, C++'s `sizeof` and template specialization, and GHC's `TypeFamilies` are blatant violations of parametricity that make types less informative.
(1) A clear distinction between data (sums of products) and operations (functions). In a general-purpose language, operations will always be somewhat ill-behaved: they may raise exceptions, fail to terminate, etc. Data tends to be better behaved, and algebraic laws can be stated about it, which hold even in the presence of effectful and/or non-terminating functions. This makes ML superior to Haskell, not to mention object-oriented languages.
(2) A module system that enforces abstraction boundaries between subsystems of a larger system. ML's opaque signature ascription (which has no counterpart in Haskell or object-oriented languages) ensures that the internal representation of abstract types is only visible in the module where they're implemented. In a well architected ML program, trying to violate another module's internal invariants is a type error!
That's a rather generous interpretation, given that hacker_9 said nothing about strong types, and instead made a claim about static vs. dynamic languages.
I do agree with your assertion, though; learning Haskell and OCaml prepared me for writing Python in ways that many of my peers in the Python community are unprepared. One big example is the difference between str and bytes in Python 3: a lot of Pythonistas find this distinction an annoyance, but I find it extremely useful, largely because I learned how to leverage such type differences to reduce errors from ML family languages.
For example, the char pointer increment compiles to:
4004fb: 48 83 c0 01 add $0x1,%rax
40050c: 48 83 c0 04 add $0x4,%rax