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

Why static languages suffer from complexity

hirrolot.github.io

Post reply on HN
Print view View original

191–200 of 306 posts

Re: Why static languages suffer from complexity

#191

Post by sidlls »

dmitriid wrote: post #164
agentultra wrote: post #145

Earlier quoted context omitted.

> Fascination with type systems does not seem to be all that useful in practice. And yet type theory is an excellent way to express all kinds of invariants. The more rich the type system the more you can express. If you get to dependent types you essentially have all of mathematics at your disposal. This is the basis of some of the most advance proof automation available. What is super cool is that proofs are program…

> The more rich the type system the more you can express. If you get to Ah yes. And then you end up writing entire prgrams in types. So the next logical setep would be to start unit- and integration tests for these types, and then invent types for those types to more easily check them... > you essentially have all of mathematics at your disposal. Most of the stuff we do has nothing to do with mathematics.

One of the major selling points of a robust (not "strong", necessarily, but at least...not weak?) type system is that an entire class of unit tests are no longer necessary (e.g., those that validate/exercise handling of cases where data of an invalid type are passed as a parameter to the function). Integration tests are necessary independently of the implementation language--they don't test the correctness of units of code, but of communication between APIs.

Re: Why static languages suffer from complexity

#192

Post by Verdex »

amelius wrote: post #178
mountainriver wrote: post #167

Earlier quoted context omitted.

Try working in a big system without them =P I think they are invaluable

They are especially useful when refactoring, or as a documentation tool. However, without a type checker, choosing your names wisely will get you a long way. I think anyone advocating type systems should spend a year working in a dynamic language, to get out of their echo chamber and form a more objective opinion.

What you appear to be saying is that people who like type systems must be ignorant because with experience you suspect they would think differently.

This seems to me to be extremely uncharitable point of view.

But let's roll with it.

I advocate type systems.

I've also worked in several non-trivial projects in lua. Several non-trivial projects in python. Several trivial projects in common lisp. Several trivial projects in erlang.

Additional I've worked in a non trivial project in ruby for several months. And one non trivial project in node for a year. Both of these in a professional 8 hours a day capacity.

I still advocate type systems. More so after working in dynamic languages.

Re: Why static languages suffer from complexity

#193

Post by preseinger »

mountainriver wrote: post #167
preseinger wrote: post #152

Earlier quoted context omitted.

Type systems are useful, but not nearly as useful as many people believe they are.

Try working in a big system without them =P I think they are invaluable

Oh, I'll never program in a dynamically typed language again. I'm sold on that. What I'm speaking to is the notion that types are the best model for solving most/all problems in software engineering.

Re: Why static languages suffer from complexity

#194

Post by [deleted] »

morelisp wrote: post #185
amelius wrote: post #178

Earlier quoted context omitted.

They are especially useful when refactoring, or as a documentation tool. However, without a type checker, choosing your names wisely will get you a long way. I think anyone advocating type systems should spend a year working in a dynamic language, to get out of their echo chamber and form a more objective opinion.

The average user of Haskell, Rust, or ML today has certainly spent sufficient time in the Python/JS/Tcl/what have you mines. The opposite is much less likely to be true; at best they may have done a project or two in Java or started migrating to TypeScript. (Please also keep in mind: The average ML user probably reads, or intentionally avoids, HN. The average JS user doesn’t know it exists.)

[deleted]

Re: Why static languages suffer from complexity

#195

Post by agentultra »

YorkshireSeason wrote: post #187
agentultra wrote: post #145

Earlier quoted context omitted.

> Fascination with type systems does not seem to be all that useful in practice. And yet type theory is an excellent way to express all kinds of invariants. The more rich the type system the more you can express. If you get to dependent types you essentially have all of mathematics at your disposal. This is the basis of some of the most advance proof automation available. What is super cool is that proofs are program…

> The more rich the type system the more you can express Why is this interesting? You pay an extremely heavy price in terms of language complexity. In practise, you almost never have the invarants at all or correct when you begin programming, and your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one. Moreover proofs are non-composit…

> Why is this interesting? You pay an extremely heavy price in terms of language complexity.

As you say, there is no free lunch. Not having a useful type system introduces its own complexity. It depends on what abstractions you find most useful.

The present limitations of dependently typed languages will not be limitations tomorrow. Evolution in the field of proof engineering is providing new frameworks for making proofs more compositional and being able to extract programs from the proofs. It's not amazing and super useful today but it's a lot better than it was even five years ago and I suspect will continue to improve.

> After all, your specification is just as likely to be buggy as your implementation code

If you can't think of the right theorems or specifications I doubt you will write a correct program.

One is a lot easier to reason about than the other.

> Even type-checking can easily become undecidable when the ambient typing system is too expressive.

I'm not sure I follow. I understand how type inference can become undecidable but how does a sound type theory end up this way? The judgement and inference rules for CoC are rather small [0].

> There is no free lunch.

I don't disagree. I still enjoy programming in C. And I might even choose it for a project. And if it so happened that I had certain requirements like the system had to be real-time and could not deadlock then... I might be making a trade off to write my proofs and specifications in another language than my implementation.

We're not at a place yet where we can extract a full program from a specification and not in a place where we can write dependently-typed programs with deterministic run times either.

I would like to have my cake and eat it too but that's where we are.

[0] https://en.wikipedia.org/wiki/Calculus_of_constructions

Re: Why static languages suffer from complexity

#196

Post by benhoyt »

morelisp wrote: post #190
benhoyt wrote: post #135

Earlier quoted context omitted.

Nit: they're adding Generics in 1.18 (not 1.8). Regarding "another 5 years": I'm not so sure. Go is very conservative about language changes. The type system didn't change at all from version 1.0 through version 1.17 (a 12-year period).

Some changes to nil accesses were made in 1.3. Tags were ignored in casts since 1.8. Overlapping methods were allowed in 1.14. New array pointer casts were added in 1.17. (Arguably, also type aliases in 1.9.) None of these are as significant as generics, but things do change.

Yes, you're right. Saying that it didn't change "at all" was perhaps overstatement. But those are all very subtle changes. I've coded Go daily for 3-4 years and never been affected by them, except the tags one -- I think I used that once (post 1.8). Not sure what you're referring to about the nil changes in 1.3 -- I didn't see anything about nil in the 1.3 release notes: https://go.dev/doc/go1.3

Re: Why static languages suffer from complexity

#197

Post by gundamdoubleO »

amelius wrote: post #178
mountainriver wrote: post #167

Earlier quoted context omitted.

Try working in a big system without them =P I think they are invaluable

They are especially useful when refactoring, or as a documentation tool. However, without a type checker, choosing your names wisely will get you a long way. I think anyone advocating type systems should spend a year working in a dynamic language, to get out of their echo chamber and form a more objective opinion.

I advocate for type systems specifically because of how much I've worked with dynamic languages in big corps.

Re: Why static languages suffer from complexity

#198

Post by AndyKelley »

This article incorrectly states that Zig has "colored" `async` functions. In reality, [Zig async functions do not suffer from function coloring](https://kristoff.it/blog/zig-colorblind-async-await/).

> Yes, you can write virtually any software in Zig, but should you? My experience in maintaining high-level code in Rust and C99 says NO.

Maybe gain some experience with Zig in order to draw this conclusion about Zig?

Re: Why static languages suffer from complexity

#199

Post by quickthrower2 »

agentultra wrote: post #145
Animats wrote: post #100

Fascination with type systems does not seem to be all that useful in practice. Go has a minimal type system, and is able to do much of Google's internal server side work. Most of the problems that cause non-trivial bugs come from invariant violations. At point A, there's some assumption, and way over there at point B, that assumption is violated. That's an invariant violation. Type systems prevent some invariant viol…

> Fascination with type systems does not seem to be all that useful in practice. And yet type theory is an excellent way to express all kinds of invariants. The more rich the type system the more you can express. If you get to dependent types you essentially have all of mathematics at your disposal. This is the basis of some of the most advance proof automation available. What is super cool is that proofs are program…

This advanced types stuff sounds really useful but it needs to be made very easy to use for the mainstream Java of C# programmer to use.

A success story in this regard is the async keyword. Very quickly you can get used to it and it feels like any other imperative programming.

In C# if I can add assertions and have C# compile time check the source that the assertion will not be violated. This would be great. I know they do this for null checking.

Re: Why static languages suffer from complexity

#200

Post by betterunix2 »

preseinger wrote: post #193
mountainriver wrote: post #167

Earlier quoted context omitted.

Try working in a big system without them =P I think they are invaluable

Oh, I'll never program in a dynamically typed language again. I'm sold on that. What I'm speaking to is the notion that types are the best model for solving most/all problems in software engineering.

Do people commonly think types are a solution to most or all problems? Other than correctness I am not sure what software engineering problems a type system actually solves, and the rest of the debate is about the expressiveness of the type system (or lack thereof, which forces suboptimal engineering practices in some languages).
Post reply on HN