Comment by catnaroek | Hacker News Reader

Comment by catnaroek | Hacker News Reader

Parent Full thread

> Okay, but how do you gather enough information to craft said messages?

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.

> 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).

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')

But we can report on that at runtime (remember, I'm talking about the quality of type errors, not when they occur).

Further, one can imagine a hypothetical dynamic language where we parameterize types, too:

    a = List<Integer>()
    a.append('Hello, world')

Of course this could be implemented statically, but it could be implemented dynamically, the difference being that the type error would be reported at runtime instead of compile time. 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.

> > 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. :)

> Yes, we can't determine at compile time that the following is a type error: (snippet)

> 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.

> 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.

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).

> 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.

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.

Reply on news.ycombinator.com