Live data from Hacker News

Diminishing returns of static typing

blog.merovius.de

171–180 of 632 posts

Re: Diminishing returns of static typing

#171

Earlier quoted context omitted.

I agree that static typing helps reading comprehension and that IDEs like pycharm help getting into big code bases, that said, at the end of the day, when you know the code both the IDE and static typing are getting in the way. Actually, I never saw anybody as quick as people using simple editors like emacs and vim. GUI is getting in the way of the programmers intent. Static typing is a hindrance in front of refactor…

You're kinda damning it with faint praise when you say that you can use dynamically typed languages on small projects that fit in your head (and are also probably written by a single developer). You can pretty much use any language in that scenario. But the chickens come to roost around day 30+ or so.

A large project is a poorly decoupled set of small projects.

Re: Diminishing returns of static typing

#172
post #127

Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Relatively little behavior can be encoded in inexpressive type systems, so there's a lot of room for bugs that have nothing to do with types. A lot more behavior (e.g. the sorts of invariants mentioned in agentultra's top level comment) can be encoded in a more expressiv…

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that…

The article was not trying to discuss how to make programmers smarter. No language is going to help with that so there is no point in talking about it. As far as the scope of the article is concerned, it's fair to say that statically verified code equals bug-free code.

Re: Diminishing returns of static typing

#173
I think talking about a sweet spot is correct

I've been thinking about the trajectory of C++ language development recently and the emphasis has definitely been on making generics more and powerful. You watch CppCon talks and see all this super expressive template spaghetti and see that while it's definitely a better way to write code - the syntax is just horrifying and hard to "get over"

Just like when "auto" took off and people starting thinking about having "const by default" - I'm starting to think that generic by default is the way to go. The composability of generic code is incredible powerful and needs to be more accessible

However the other end of the spectrum: dynamic code leaves a lot of performance on the table and leads to runtime errors

Re: Diminishing returns of static typing

#174
post #3

The benefit of static typing isn't just reliability. Tooling is another major argument. Won't appeal to certain hardcore programmers who think that even notepad has too many features. But it is great for refactoring, finding all references to a function or a property or navigating through the code at design time. Basically all the features visual studio excels at for .net languages. And I disagree with the barrier to…

This is really true. I was a complete Java newbie and knew some Python when I joined Google. Yet I found working in an unfamiliar Java code base much, much easier here.

Large Python code bases are really hard to understand and work in (here).

Re: Diminishing returns of static typing

#175

Earlier quoted context omitted.

> The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. There are languages that enforce termination. They only accept programs that can be shown to terminate through syntactic reasoning (e.g., when processing lists, you only recurse on the tail), or where you can prove termination by other means. Coq is like this, as is Isabelle, as is F* , as are others. They…

I'm aware of strongly normalizing systems and the escape hatch of coinductive programming. But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. How else do we judge the merit of a type system except by seeing how it fits into the overall space of computable processes? There are two ways to see type systems. In the first way you construct terms along with their…

> But when we're talking about the space of all programs, the fundamental limit of incompleteness is important.

I agree with this. But I think that usually we are not really talking about all programs. We are talking about useful programs, and those are usually terminating. In theory, not always, see first-order theorem provers; but in practice, we always call a prover with a time limit because nontermination isn't useful.

> Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity.

That's an interesting point, and I agree in many respects. I think when programming in a dynamically typed language, I approach things in one style, and in statically typed languages in another style. But specifically for termination, I don't think so. I never want to write a nonterminating program; the termination property for my programs exists (as a requirement) before the program does.

Re: Diminishing returns of static typing

#176
post #3

The benefit of static typing isn't just reliability. Tooling is another major argument. Won't appeal to certain hardcore programmers who think that even notepad has too many features. But it is great for refactoring, finding all references to a function or a property or navigating through the code at design time. Basically all the features visual studio excels at for .net languages. And I disagree with the barrier to…

I'm so happy to see the pendulum swing the other way, because when JavaScript was becoming popular, and Ruby and Python had a popularity renaissance (around mid to late 2000s), I had a lot of online arguments about the value of static typing. People were complaining about static typing for the dumbest reasons (it's too 'wordy'). It started as a backlash against old-school enterprise Java development (which was fair,…

The type systems of Java and C/C++ are the most commonly encountered ones and by far the most widespread in industry programming (as opposed to academia/research) and they are actually awful and really add a lot of friction and inertia to developing. Being free of that kind of type system when using a language like Python really does feel like a big upgrade.

There is a different problem with the more powerful and useful type systems in more modern statically typed languages though: learning curve. Haskell is dysfunctionally hard to learn and other languages do a little bit better but there's still friction in the learning curve that gets in the way of widespread adoption in projects that want to be able to hire rapidly.

Re: Diminishing returns of static typing

#177

Earlier quoted context omitted.

>>There are a class of bugs you just never need to worry about when the compiler does some compile-time checks for you ... like worrying that you passed the wrong type into a function, or the wrong number of arguments. People always say this and it baffles me. Bugs like that should be caught immediately by your test cases. You shouldn't rely on the compiler to catch them for you.

Why would I write test-cases for something the compiler can catch for me? Yes, I need to write tests for all the correctly-typed cases, but there are a whole class of bugs that I don't need to test for any more because I can't even write the failing case.

you're already writing the test cases to ensure correct behavior with typical input, and predictable exceptional input. putting in one more assert for predictable exceptional input (wrong type) doesn't really add a noticeable amount of overhead to writing the tests you were already writing.

Re: Diminishing returns of static typing

#178

Earlier quoted context omitted.

My main progamming language at the time is Java, and the amount of assistance my IDE provides is astonishing (to the surprise of no one, it's IntelliJ). The confidence strong automatic refactors provide is of great help when managing large codebases.

I agree that static typing helps reading comprehension and that IDEs like pycharm help getting into big code bases, that said, at the end of the day, when you know the code both the IDE and static typing are getting in the way. Actually, I never saw anybody as quick as people using simple editors like emacs and vim. GUI is getting in the way of the programmers intent. Static typing is a hindrance in front of refactor…

> Unit tests is the only truth that matters, static typing or not.

Well that's provably false, because there exist properties that you can type check that literally can't be verified via unit tests, even in principle. For instance, race and deadlock freedom.

Re: Diminishing returns of static typing

#179
post #114

Earlier quoted context omitted.

>Not just, "who the hell uses this", but "where the hell is this defined" as well. On Common Lisp, a dynamic language, I can also get this answered instantly. I just press a key combination on a method call and i jump to the definition. So this isn't exclusive to statically typed languages.

But if the compiler doesn't enforce that types are statically determinable, there will be cases where the tool will have to show you more potential definitions for function definitions than would be shown for a statically typed language. Maybe good tools are able to perform some static analysis and rule out some of the methods with the same name but impossible types, but the language doesn't rule out situations where…

there will be cases where the tool will have to show you more potential definitions for function definitions than would be shown for a statically typed language.

And even in a statically-typed language there will be cases where the tooling can only determine fairly generic things statically.

I don't see anyone advocating for abandoning static typing over that occasional limitation. Yet I do see people proposing similarly-infrequent issues as cause to abandon dynamic typing.

Re: Diminishing returns of static typing

#180
post #127

Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Relatively little behavior can be encoded in inexpressive type systems, so there's a lot of room for bugs that have nothing to do with types. A lot more behavior (e.g. the sorts of invariants mentioned in agentultra's top level comment) can be encoded in a more expressiv…

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that…

Or as Knuth pithily put it, "Beware of bugs in the above code; I have only proved it correct, not tried it."
Post reply on HN