4 ms·
Hmmm, I think this is an interesting discussion. There's many sides I need to respond here, maybe I will not be able to cover everything but here I go. See, I
by nipah 2y ago
Hmmm, I think this is an interesting discussion. There's many sides I need to respond here, maybe I will not be able to cover everything but here I go.
See, I fundamentally disagree that those languages are "unusable beyond very narrow tasks", because I never stated that only a complete and absolutely proven type system can provide those proofs. In fact, even a relatively mid-tier (a little bit above average) type-system like C#'s can already provide enormous benefits in this regard. See, when you test for something like raw JavaScript, you end up testing things that are even about the shape of your objects, in C# you don't have to do this (because the type system dictates the shape). You also have to be very careful around possibly null objects and values, which in a language with "proper" nullable types (and support from it in the type system and static checkers) like C# can be lowered vastly (if you use the resource, naturally). C# is also a language that "brings the types into runtime" through reflection, so it will even bring you things that you don't need to test in your code (only when developing the library) like reflection for example (you will not see things that are meant to assert shapes, like 'zod' or 'pydantic' in C# or other mid-tier typed languages for example). C#'s type system also proves many things about the safety of your code, for example you basically never need to test your usage of Spans, the type system and static analysis will already rule out most problematic usages of those things. You also never need to test if your int is actually a float because some random place in your code it was set to be so (like in JS), you also never need to test against many other basic assumptions even an extremely basic type system would give you (even Go's one).
This is to say that, basically, this don't hold true for relatively simple type systems. I'm also yet to see this holding true for more advanced ones, for example: Rust is a relatively well used language for a lot of low-level projects. I never saw someone testing (well bounded safe) rust code for basic shapes of types, nor for the conclusions the type system provides when writing on it. For example, testing if the type system was really able to catch that ownership transference happening here, of it is really safe to assume that there's only one mutable reference to that object after you called that method, or if the destructor of the object is really running in the end of the scope of the function, or even if the overly complex associated type result was actually what you meant it to be (in fact, if you would ever use those complicated types, it would be precisely to have very strong compile-time guarantees that both a test would not be able to cover for -- entirely, and that you would not write unit tests specifically for in the first place). So I don't think it is true that you need a powerful type system to see the reduction in tests that you would need to write in a completely dynamically typed language, nor I think it is true when you start having really powerful type constructs, that you will come to this conclusion """start to notice that your tests end up covering all the same cases as your advanced types""". I also don't think that you need to go to the extreme of this spectrum to see those benefits, they appear gradually and increase gradually as you move towards the end (when you end up with more extremely uncommon things like dependent typing, refinement types or effect systems).
I also certainly don't agree that it does matter that "most people" think or don't think about powerful type systems and the languages using them, it matters more that the right people are using them, people that want to be benefitted from this, than the everyday masses (this is another overly complex disccussion tho).
And while I can understand the feelings you have towards the "low end of half-assery type systems", and even agree to a certain reasonable degree (naturally, with my own considerations), I don't think glorifying mediocre type systems is the way to go (like many people usually do, for some terrifying reason). It is enough to recognize that a half-assery type-system usually gets the job done and that's it, completely fine and okay, it may even be faster to write, instead of trying to justify that we should "pursue primitive type systems" because of the fact that we can do things well on them. Maybe I'm digressing to much, it's hard to respond to this comment in a satisfactory manner.
>> I don't think the "industry" is a person
> Nobody does.
Yeah, this was not a very productive point of mine, sorry.
- 9rx 2y ago> I fundamentally disagree that those languages are "unusable beyond very narrow tasks" Then why do you think nobody uses them (outside of certain narrow tasks)? It is hard to deny the results. The reality is that they are intractable. For the vast majority of programming problems, testing is good enough and far, far more practical. There is a very good reason why the languages people normally use (yes, including C# and Rust) prefer testing over types. > See, when you test for something like raw JavaScript, you end up testing things that are even about the shape of your objects Incidentally, but not explicitly. You also end up incidentally testing things like the shape even in languages that provide strict guarantees in the type system. That's the nature of testing. I do agree that testing is not well understood by a lot of developers. There are for sure developers who think that explicitly testing for, say, the shape of data is a test that needs to be written. A lot of developers straight up don't know what makes for a useful test. We'd do well to help them better understand testing, but I'm not sure "don't even think about it, you've got a half-assed type system to lean on!" get us there. Quite the opposite. > it matters more that the right people are using them Well, they're not. And they are not going to without some fundamental breakthrough that changes the tractability of using languages with an advanced (on the full spectrum, not relative to Go) type system. The tradeoffs just aren't worth it in nearly every case. So we're stuck with half-assed type systems and relying on testing, for better or worse. Yes, that includes C# and Rust. > I don't think glorifying mediocre type systems is the way to go (like many people usually do, for some terrifying reason). Does it matter? Engineers don't make decisions based on some random emotional plea on HN. A keyboard cowboy might be swayed in the wrong direction by such, but then this boils down to being effectively equivalent to "If we don't talk about sex maybe teenage pregnancy will cease." Is that really the angle you want to go with?
- nipah 2y ago> Then why do you think nobody uses them (outside of certain narrow tasks)? It is hard to deny the results. > The reality is that they are intractable. For the vast majority of programming problems, testing is good enough and far, far more practical. There is a very good reason why the languages people normally use (yes, including C# and Rust) prefer testing over types. Deny what results? Do you have some kind of formal demonstration that they are impossible to use outside of those "certain narrow tasks" (unknown)? Or do you have proof that NOBODY use them for more than those "certain narrow tasks"? Otherwise this is more "I feel like it" than something I would even need to justify deeply. Also, with Rust this is certainly false, most people that I've saw using it (and myself) don't overly test everything in it besides more complex behavior (which types hardly can prove it is correct), but it eliminates the need for a whole suit of smaller tests that would be necessary in less powerful languages (it is literally regarded as one of the languages where "if it compiles, it works" -- or "generally works" for a reason). > Incidentally, but not explicitly. You also end up incidentally testing things like the shape even in languages that provide strict guarantees in the type system. That's the nature of testing. Now I want some proof to it. Make an example test that "incidentally tests things like the shape" in C#, please. I've seen a good bunch of codebases in C# and I'm pretty sure I never saw something even remotely like this. > I do agree that testing is not well understood by a lot of developers. There are for sure developers who think that explicitly testing for, say, the shape of data is a test that needs to be written. A lot of developers straight up don't know what makes for a useful test. We'd do well to help them better understand testing, but I'm not sure "don't even think about it, you've got a half-assed type system to lean on!" get us there. Quite the opposite. Now this point is getting lost, you changed from: > At some point you start to notice that your tests end up covering all the same cases as your advanced types, and you begin question why you are putting in so much work repeating yourself, which ultimately sees you want to look for better. To "I know better than a lot of developers how to test", which don't make any sense to me. You either has the same baseline testing knowledge of this "lot of developers", and hence reach similar conclusions in regards to testing (what I quoted), or you have a better understanding of it than them (and your conclusions are merely based on your own perception of testing). I don't think those points are free to take, you would need to justify this a little bit more, and I'm sure """don't even think about it, you've got a half-assed type system to lean on!""" was not the core of my point, nor a faithful representation of what I said. > Well, they're not. And they are not going to without some fundamental breakthrough that changes the tractability of using languages with an advanced (on the full spectrum, not relative to Go) type system. The tradeoffs just aren't worth it in nearly every case. So we're stuck with half-assed type systems and relying on testing, for better or worse. Yes, that includes C# and Rust. I would not call Rust's type system 'half-assed' tho, it is very compatible with a bunch of ML languages, it is really a very sophisticated type system with HM type inference, generic associated types, traits and more powerful things. Comparing it to C# would be unreasonable. I may also be a little bit mean to C#, it has a "mid-tier, but sufficiently good type system" for many purposes, my main problems with it are regarding to the type inference (and the lack of some basic features), but it has generics since early versions, it has interfaces, classes, subtyping, recursive type constraints, extension methods, deterministic destructors, scoped local definitions and a bunch of small useful resources. It is surely mid-tier in many aspects, but not something trivial and I don't think you can put them all in the same basket. Either way, I also don't think that you got my point: I said it matters more that the right people are using them, precisely because those are the people that would make good use of those type systems. As a very simple example (and I consider Rust type system a very powerful one in this context) it was interesting to see that someone like Asahi Lina said the Rust language and it's features were useful for making a GPU driver, that she experienced less problems common in C (a language with a way smaller and simpler type system) and that it was having some positive effects on it. Surely, most software is not written in Rust, but the ones that are, and this is what matters, are being developed by the right people that would use them right. This is another point, as I stated earlier, but you responded to it so I'm giving a better exploration on the surroundings of what I meant here. > Does it matter? Engineers don't make decisions based on some random emotional plea on HN. A keyboard cowboy might be swayed in the wrong direction by such, but then this boils down to being effectively equivalent to "If we don't talk about sex maybe teenage pregnancy will cease." Is that really the angle you want to go with? It absolutely does matter. And I do believe we should talk less about mundane things and that glorifying bad ways of living can have a terrible influence in teenage brains (and even in adults in many cases), but this is also another discussion. My point is that people don't argue emotionally like they were arguing emotionally, they argue emotionally like they were right. They are (generally) not saying "well, see, I really love Go and its simplicity, so because of my personal preferences I'm saying that other languages are bad", they are saying "see, as we obviously values simplicity, and Go is simpler than that X language, Go is better than X language" (which is the shape of arguments I usually see, not ipsis literis, but in implications and the style of pointing things), and this is much more dangerous than any "purely emotional plea" (and also, most software engineers are not masters of argumentation that can dissect something like this and find all the intricate problems and possible fallacies behind it, they will believe what is most believable at the moment for them and that's generally it).