Live data from Hacker News

Diminishing returns of static typing

blog.merovius.de

581–590 of 632 posts

Re: Diminishing returns of static typing

#581

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

I agree that the third point is important, but it's not clear that it's static typing that is important, and not type annotations. One reason why I can still fairly easily read and understand Eiffel code that I wrote decades ago is Design by Contract. And there's normally nothing static about DbC, it's about assertions that are checked at runtime and that by convention are part of a class's interface. What both type…

I think one disadvantage of runtime type checking and DbC is that the compiler can't aid you in refactoring.

For example, if you add a case to a variant or sum type, or change the parameter or return type of some function, in a static type system, the compiler can tell you all the locations you need to change. In a runtime system, you have to find them yourself, or wait till you see an error at runtime.

Now, this is still better than the alternative of having the error propagate until it crashes 10 functions down, but the compiler finding all the places that need to be changed is something I've found to be really useful, especially in early development when there's a lot of refactoring happening. Presumably, this is probably useful in later stages as well, when the system is large enough that you can't expect to find all the uses of a function or type manually.

Re: Diminishing returns of static typing

#582
post #568
post #563

Earlier quoted context omitted.

Java is a static language. While there are dynamic languages on the JVM like Jython, JRuby, Groovy, they don't get anywhere near the performance of the static languages.

Oh, sure it's statically typed language with all things being constantly cast to and from Object. (Have you ever used collections? Have you ever heard of "type erasure" term?)

That it doesn't have reified generics like C# does not make it a dynamic language. Go doesn't have generics at all, but it's still a static language.

Re: Diminishing returns of static typing

#583
post #568
post #563

Earlier quoted context omitted.

Java is a static language. While there are dynamic languages on the JVM like Jython, JRuby, Groovy, they don't get anywhere near the performance of the static languages.

Oh, sure it's statically typed language with all things being constantly cast to and from Object. (Have you ever used collections? Have you ever heard of "type erasure" term?)

There is code that doesn't `constantly cast ti and from Object`, most code won't need to, anyway. Generic information is kept during type-checking and then is discarded, this can be considered an optimization. There are some warts that appear because of erasure, but I believe you're wrong in implying that most developers care (most java developers, maybe scala peole have more issues because of erasure).

Re: Diminishing returns of static typing

#584

Earlier quoted context omitted.

Fair point about 'sequence'. There are probably a bunch of these I use regularly in Scala without realizing it. Though as a counterpoint, 'Future.sequence' wouldn't really lose _that_ much if it didn't return a collection of the same type. And I haven't yet felt the need for a generic `sequence`, which I'm sure scalaz has. I don't buy your point about not needing to unpack side-effectless code, however. There are _al…

It's a pretty typical symptom I've seen a lot of hardcore FP developers exhibit: they forget how much time it took them to reach their level of mastery. It's like spending ten years learning to speak Russian and then criticizing anyone who says that learning Russian is difficult. Puzzling out scalaz code is difficult and requires an enormous investment in hours and practice, investment that a lot of people prefer to…

Yea, puzzling out some scalaz code takes investment. On the other hand, the library is used for web apps, network servers, database based applications, streaming libraries etc.

It's incredibly multipurpose, more so than even Spring or Guava or LINQ, and these are things that developers regularly have to invest serious time in.

The argument is just that FP libraries (like Scalaz) have a bigger payoff in the investment.

At Verizon Labs were have 20+ microservices that I have touched/looked at. Some use Akka, some use Play, some use Jetty, some use Http4s but everyone makes use of Scalaz somehow.

Re: Diminishing returns of static typing

#585
post #409

Earlier quoted context omitted.

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. You can prove a program does what the types say it should do but that is not what "correctness" means. >Now a big part of the problem is expressing with sufficient accuracy what the properties of t…

No, I’m pretty sure there’s a pretty large body of academic and industrial research on proving program correctness that you can’t just hand wave away with sophistic “but what if your type signature is wrong” nonsense. And there’s a huge difference between a test and a proof - a test can only tell you a program doesn’t do what you think it should for a particular case, a proof tells you that your program does exactly…

Defining "correctness" in terms of types is the CS equivalent of defining "risk" in terms of volatility - it replaces a real and fundamentally unsolvable problem with a problem that, while it has the advantage of being tractable, isn't actually all that important to solve. Great for publishing papers, dangerous when people start confusing the fake problem and the real problem.

Re: Diminishing returns of static typing

#586
post #409

Earlier quoted context omitted.

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. You can prove a program does what the types say it should do but that is not what "correctness" means. >Now a big part of the problem is expressing with sufficient accuracy what the properties of t…

> There's no such thing as "proving correctness". Given the caveats you mention, is there such thing as proving anything?

There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world, like programs (of course, a program also exists both as an abstraction about which things can be proved, but when you're talking about programs which are actually doing things in the real world, you can't treat them as being pure logic).

The second sense is the scientific "gather enough supporting evidence that your are reasonably sure". In this sense, you can prove a lot of things.

Re: Diminishing returns of static typing

#587
post #419

Earlier quoted context omitted.

> For any code base that isn't a throwaway like a one-off script or similar, say 10 or 20 years maintenance I think one of our problems is that people have downgraded the importance of this. Much code nowadays (rightly or wrongly) is considered "disposable" - people think that the likelihood of any given piece of code they are writing as surviving more than a few years is negligible. It is a natural assumption when y…

> I observe this in myself: my favorite language to code in is Groovy - a dynamic, scripting language with all kinds of fancy tricks. But my favorite language to decode is Java. Because it is so simple, boring, there is almost nothing clever it can do. Every type declared, exception thrown, etc. is completely visible in front of me. one of my favorite things about groovy is that it's easy to start strongly typing thi…

Static typing was grafted onto Apache Groovy in 2012, but no-one really uses it. I'm not sure about its reliability -- its use never took off on the Android platform, and none of the Groovy codebase itself has ever been rewritten in static Groovy.

Groovy's still great for scripting on the JVM though, for stuff like those 10-liner build scripts for Gradle, glue code, and mock testing. Just don't use Groovy for building systems -- use a language based on static typing from the ground up, like Java, Scala, or Kotlin.

Re: Diminishing returns of static typing

#588
post #485

Earlier quoted context omitted.

15 commits 4 years ago, 121 commits 8 months ago If these things are so good why does no one use them? EVERYONE using Erlang is using the same hotswapping facility. This sort of dynamism is just fighting against the language in an environment like Haskell.

Why would you need to? GHCi supports dynamic code reloading which most people do during development. During runtime there’s not so much of a use case though for most people.

Replying to myself. There are some use cases though, and in fact my comment points to one of them. Xmonad configurations are themselves Haskell code, and Xmonad does dynamic code reloading to make configuration changes without having to logout. Xmonad rolled their own solution, but "dyre" is a reusable generalization inspired by what Xmonad does. Using Haskell DSL's for configuration of Haskell programs has some significant advantages and dynamic code reloading is essential if the program itself is long-lived or can tolerate no downtime. I don't meant to imply there are no uses ... but outside of configuration or development environments (or real-time routing algorithms in Erlang's case, something I wouldn't advise doing in Haskell) I really don't know what general use cases there are for it. If someone does though, I'd love to learn something new.

Re: Diminishing returns of static typing

#589
post #296
post #283

Earlier quoted context omitted.

> Macros are quite orthogonal to this. You ain't gonna to find any sane way to combine macros with a powerful type system in a way the doesn't make a 140+ IQ a requirement for any programmer touching the code using these features in a real world project... Problem with programming language design is that the ideal/Nirvana solutions lie at the edge, or beyond, the limits of human intellect. If you want something that…

There is a programming language property called Restrictability - it means that you only need to know a subset of the features the language provides to become productive. The best languages have high restrictability without compromising on the high level features like powerful macros. The point of having macros is that they allow you to solve problems that cannot be solved elegantly in any other way. But 95% of progr…

> it means that you only need to know a subset of the features the language provides to become productive.

That only works when you work by yourself (or in a small team to whom you can dictate the language subset), and without any third party code.

> But 95% of programmers don't need to solve such problems and can do very well without using macros.

Languages that have great macro systems use them to bootstrap themselves. So when you use the standard, documented features, you're using macros.

E.g. if you're writing in Lisp and your file begins with (defun ..., you've just used a macro.

Re: Diminishing returns of static typing

#590
post #585

Earlier quoted context omitted.

No, I’m pretty sure there’s a pretty large body of academic and industrial research on proving program correctness that you can’t just hand wave away with sophistic “but what if your type signature is wrong” nonsense. And there’s a huge difference between a test and a proof - a test can only tell you a program doesn’t do what you think it should for a particular case, a proof tells you that your program does exactly…

Defining "correctness" in terms of types is the CS equivalent of defining "risk" in terms of volatility - it replaces a real and fundamentally unsolvable problem with a problem that, while it has the advantage of being tractable, isn't actually all that important to solve. Great for publishing papers, dangerous when people start confusing the fake problem and the real problem.

And you’re just doubling down on sophistry. Why should anyone take you seriously in this conversation?
Post reply on HN