Comment by catnaroek | Hacker News Reader

Comment by catnaroek | Hacker News Reader

Parent Full thread

> 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