Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Diminishing returns of static typing

blog.merovius.de

Post reply on HN
Print view View original

131–140 of 632 posts

Re: Diminishing returns of static typing

#131

Post by danharaj »

tom_mellior wrote: post #66
danharaj wrote: post #18

Just a technical point that hints at a significant philosophical idea: The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. The x-axis should go off to infinity. Also, it's not a smooth progression. There are huge jumps in expressivity involved here. Going from Java-style types to Hindley-Milner to full System F are all massive jumps in expressivity. There are…

> 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 types, this is called Church style. In the second way, the terms exist before their types and you use types to describe their behavior, this is called Curry style. In particular take System F. In Church style the terms of System F come with their types. In Curry style we see System F types as a way to describe the behavior of untyped lambda terms.

I used to think Church style was more important but lately I've been more partial to Curry style. 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.

Re: Diminishing returns of static typing

#132

Post by noncoml »

I think there are two kind of static typing languages. The ones that static typing is for helping the compiler(eg C) and the ones that it’s for helping the user(eg Typescript).

I think Go with its lack of algebraic type is more of the first, helping the compiler, so I wouldn’t use it as a good example of static typing.

Haskell, OCaml and Rust would make excellent case studies, but we have nothing to compare against.

So IMHO the best way to compare static typing vs dynamic typing is by comparing Typescript against JS. And in my experience the difference when writing code is huge. It completely eliminates the code-try-fix cycle during development.

Re: Diminishing returns of static typing

#133

Post by matharmin »

19873287234 wrote: post #39
cm2187 wrote: 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…

>Tooling is another major argument. vscode seems to figure out the types in javascript without any static typing. >But it is great for refactoring Searching for strings isn't that much worse. Also, when it comes to web development, you cross into the client-side and suddenly you can't refactor. So you can only refactor the server-side and end up with a mismatch. >finding all references to a function or a property or…

> vscode seems to figure out the types in javascript without any static typing.

It is actually using TypeScript's engine for this. It uses TypeScript's type definitions where it is available (e.g. most popular libraries and built-ins), and some inference rules where it has to work with plain JavaScript.

While this does give you decent auto-complete in a lot of cases (and still getting better), it's not quite as good as using TypeScript directly.

> Searching for strings isn't that much worse.

I'm busy with a large refactoring project, and TypeScript has been amazing for this. After restructuring code, you can just keep on fixing things until there's no more red. This is not just about reducing bugs - it removes almost any thinking/mental overhead required for the refactoring process.

> Also, when it comes to web development, you cross into the client-side and suddenly you can't refactor. So you can only refactor the server-side and end up with a mismatch.

TypeScript also works very well for client-side. Of course, if you change the API between the client and server, that's a different story.

Re: Diminishing returns of static typing

#134

Post by grumpyprole »

fulafel wrote: post #123
willtim wrote: post #101

Our industry has not yet even scratched the surface of what types can offer: Types for enforcing architectures and controlling effects, types for checking correct use/free of scarce resources, types for verifying protocol implementations etc etc. Currently, half the industry is using schema-less json and dynamic languages; so really it is far too early to generally talk about any diminishing returns.

For data, schemas ala clojure.spec are a competing idea - it makes the "type system" much easier to metaprogram and apply selectively.

I'd argue that any schema is a type system of sorts.

Re: Diminishing returns of static typing

#135

Post by bjz_ »

gwbas1c wrote: post #113
cm2187 wrote: 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…

Isn't static typing a requirement when writing an algorithm and data structures for "every bit and clock cycle counts" situations? How can a 0-compute overhead for dynamic typing exist in a dynamic typed environment? I always thought dynamic typing is a feature for situations where the code needs an extreme amount of flexibility to adapt to a wide variety of data; even at the expense of performance.

A good static type system will give you the ability to be able to control the level of dynamism in various parts of you code. For example you could create tagged unions to create mini dynamic type systems within parts of your codebase.

Re: Diminishing returns of static typing

#136

Post by dwaltrip »

ruskimalooski wrote: post #22
gipp wrote: post #19

Earlier quoted context omitted.

They're just sketches. That's part of the point, and the article says that directly. The point isn't the exact shape or slope of the curves, but just their asymptotic behavior and the relationship of "correct features/day" to the other two. I.e. As long as the two curves have that general shape, then the "sweet spot" exists somewhere between 0-100%, the exact location of which depends on language, developer experienc…

But even the asymptotes are an assumption derived from pure thought experiment.

More realistically, it's an educated guess based off the author's personal experience as well as their understanding of the experiences of other developers operating under different constraints.

The author makes it clear that the analysis is not perfectly rigorous. There is a very wide landscape between perfectly rigorous and completely useless.

Do you think the article fails to hint at any of the fundamental dynamics of how type systems affect software development? How so?

Re: Diminishing returns of static typing

#137

Post by [deleted] »

Eridrus wrote: post #35
cm2187 wrote: 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 think dynamic typing proponents get hung up on the auto-complete aspect. The real benefit is when you find someone writing a property with a common-ish name to a data structure and you want to know "who the hell uses this", you can answer that question pretty easy in statically typed languages. In dynamically typed languages you kind of just grep and hope the name is not too common.

[deleted]

Re: Diminishing returns of static typing

#138

Post by grumpyprole »

hwayne wrote: post #130
grumpyprole wrote: post #125

Earlier quoted context omitted.

Yes it's true that retrofitting better type systems into existing languages may not be low-hanging fruit. But developers have shown a willingness to adopt new languages when they see clear benefits.

> Yes it's true that retrofitting better type systems into existing languages may not be low-hanging fruit. Disagree here, actually! Javascript (Typescript) and Python (mypy) are both seeing pretty big benefits from adding gradual typing.

Glad to hear it!

Re: Diminishing returns of static typing

#139

Post by FranOntanaya »

It bothers me that types as representation of hardware constraints are mixed up with types as a machine readable subset of validation.

It makes the higher level types seem more transcendental than they are, and also seems to put actual validation on a second rate level. End of the day if an argument is the right scalar or interface you'll get the same result on runtime whether you hinted it -- for one's quality of life improvements -- or checked it with some boilerplate validation. Worst case scenario people will forgo encoding known stricter constraints after generally hinting the expected type.

Re: Diminishing returns of static typing

#140

Post by caseymarquis »

flavio81 wrote: post #49
Eire_Banshee wrote: post #41

Earlier quoted context omitted.

This. Not just, "who the hell uses this", but "where the hell is this defined" as well.

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

I had to do a decent amount of setup and wrote a quick script to run the tools which generate ctags to make this happen in CL using slimv. With top tier ides for static languages, this is built in from day 1 with no effort. You can't not have it. That said, a top tier repl for development is missing in languages like C#. I'd love to see that gap bridged.
Post reply on HN