I must admit I was very surprised so see what started as a static-types rant ending up extolling the merits of Idris.
Why static languages suffer from complexity
201–210 of 306 posts
Re: Why static languages suffer from complexity
#202Earlier quoted context omitted.
> Fascination with type systems does not seem to be all that useful in practice. > ... > The Rust borrow checker is an invariant enforcer. [...] This is real progress in programming language design, and is Rust's main contribution. I'm so confused by your stance here. You essentially say "type systems are not useful" and then "oh but this most recent advance in type systems — that one is useful." Do you find type sys…
I think the key is the following: > It explicitly does automatic global analysis They appear to think that the borrow checker isn't achieved with type theory, but with some other technique ("global analysis"). Although, to be fair, my understanding of making a practical affine type checker is that things get kind of wonky if you do it purely logically. So practically you do some data flow analysis. Which is, I believ…
>They appear to think that the borrow checker isn't achieved with type theory, but with some other technique ("global analysis").
No, I think they appear to think that the borrow checker is not about the programmer stuffing the program with type theory annotations for this purpose, but the borrow checker handles the analysis automatically across the program.
Of course it doesn't handle it perfectly, so there's some "fighting the borrow checker" and lifetime annotations sometimes needed - but it's not like designing the whole of your program based on type theory - the same way you're somewhat free from thinking about freeing memory in a gc language.
Re: Why static languages suffer from complexity
#203Earlier 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.
That's exactly what I did, because I felt that I was just too sure that typed language were just superior to non typed languages without actually having proper experience.
I learnt Clojure, to the point that it's now my favourite language and the one I use for many things. Nevertheless, I still think that typed languages have two advantages that make them a more practical option for most situations:
- It's easier to evolve your code. This includes refactor but also normal program evolution through aggregation.
- It allows to express abstractions in pure code, rather than in documents or comments.
The first advantage requires little explanation. The second I think is more difficult to appreciate without enough experience with typed systems and an interface oriented programming style.
How these two things are important for a given person is difficult to say. I have come to the conclusion that it relates a lot to how your brain works. Unfortunately, mine can only track 3 or 4 things at the same time, so I need to abstract away anything else than the little piece of code I'm working on and get the compiler to worry about how things glue together.
I need the comfort of getting the compiler to help me change my hats and be able not to think about anything else that the concrete piece of code I'm working on and the interfaces of the other parts it uses. When I don't have this possibility, I miss it even more than the comfort of programming using inmutable data structures that Clojure spoilt me with. I think need to seriously try Scala 3 at some point, since it seems to combine inmutable data structures by default with an advance type system (although the lenses libraries I've seen look like an abomination in comparison with Clojure's update-in and company, not to mention the absolute elegance and triviality of the implementation of the latter: https://github.com/clojure/clojure/blob/clojure-1.10.1/src/c...).
So I would second your recommendation and encourage people trapped in dynamic language echo chambers to try for a year something like Typescript or Kotlin to appreciate other ways of doing things in languages with practical type systems. Perhaps some of them will discover that it suits them better or help them better understand why they prefer the dynamic style.
Re: Why static languages suffer from complexity
#204Earlier 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 was a mild advocate of static type systems. Then I spent about two years working on dynamic languages, mostly Python, on two jobs with otherwise very different code bases. I am now fully converted: after that experience, I strongly, strongly, strongly advocate static typing, so much that I will leave any job that requires me to use languages that lack them. I don't know if I was just unlucky, but I found that experience to be dreadful. Aside from the million small friction points, I remember things like needing to allocate a full week for a refactor that would have taken less than one hour (and that's a pessimistic estimate) with the standard tools of a static language's IDE.
I really don't see the advantages of dynamic languages. Supposedly you develop faster, but in my experience that's absolutely not true.
Re: Why static languages suffer from complexity
#205Fascination 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…
> and is able to do much of Google's internal server side work.
You mean, one of the companies with the largest number of developers on the world, paying one of the highest average salaries for them is able to use the language?
That means absolutely nothing.
Re: Why static languages suffer from complexity
#206Earlier quoted context omitted.
Oh yeah the easiest code in the world to read is some contorted type system and function signatures that look like hieroglyphics that you need a PHd in CS to comprehend. Python is easy to grok, and if you have programmers writing code like bar(foo,baz) then the problem is not Python. You can write crap in any language. Unit tests do much of what typing checks anyway ... and here's the thing ... you NEED unit tests no…
> Python is easy to grok It’s what you’re used to. I personally find Python horrible to read because I used to a whole different class of programming languages. But I’m sure some of my code might be hard to read by others who aren’t used to that particular programming language too. > Unit tests do much of what typing checks anyway ... and here's the thing ... you NEED unit tests no matter what. Some, not all. Strictl…
I'm glad to see someone else that finds Python unreadable. I keep seeing people saying that it's one of the most readable languages out there, and each time I feel like I'm from another planet.
Re: Why static languages suffer from complexity
#207Almost all software running the world is written in statically typed languages. This is not by accident or because developers don’t know better. Every few months on HN somebody will make some new claim about why dynamically typed languages are somehow better. But the truth is that statically typed languages have won in the market place for real world software. And I don’t see anything changing that.
Re: Why static languages suffer from complexity
#208Earlier quoted context omitted.
> Fascination with type systems does not seem to be all that useful in practice. > ... > The Rust borrow checker is an invariant enforcer. [...] This is real progress in programming language design, and is Rust's main contribution. I'm so confused by your stance here. You essentially say "type systems are not useful" and then "oh but this most recent advance in type systems — that one is useful." Do you find type sys…
I think the key is the following: > It explicitly does automatic global analysis They appear to think that the borrow checker isn't achieved with type theory, but with some other technique ("global analysis"). Although, to be fair, my understanding of making a practical affine type checker is that things get kind of wonky if you do it purely logically. So practically you do some data flow analysis. Which is, I believ…
Also, the borrow checker doesn't do global analysis. Not doing so is an important design decision in Rust, and is part of the reason why we don't infer type signatures, including lifetimes generally. You want to keep things easy to compute.
That said, you're right that the current borrow checker ("non-lexial lifetimes") is built off of a control flow analysis, absolutely. But it still operates only within bodies, not globally.
Re: Why static languages suffer from complexity
#209Almost all software running the world is written in statically typed languages. This is not by accident or because developers don’t know better. Every few months on HN somebody will make some new claim about why dynamically typed languages are somehow better. But the truth is that statically typed languages have won in the market place for real world software. And I don’t see anything changing that.
The article is about attempting to escape this static vs dynamic dichotomy, not about declaring dynamic languages superior to static ones.
Re: Why static languages suffer from complexity
#210Earlier quoted context omitted.
No - (a) is not what I'm suggesting. And (b) while disappointing, just doesn't slow one's work down very frequently in daily practice. Look, I just don't buy the suggestion that static typing magically solves a huge set of problems (or that it does so without imposing negative tradeoffs of its own -- the very topic of the original article). Or that dynamic languages are plainly crippled, and that one has to be a kind…
> just doesn't slow one's work down very frequently in daily practice. Well, maybe you don't feel it slows you down, but it is manual work you must do to get a reliable product only because of dynamic typing. Not only that, but you have to then refer to these docs to check you're not creating a type calamity at some nebulous point down the run time road. Static languages just won't let you mess that up, and often hav…
I think I've said about 3 times in this thread that I'm firmly in the "pro" camp as regards the net positives of static typing, and for precisely the reasons you've detailed. I just don't see its absence (or instances where it less than algebraically perfect) as the crippling dealbreakers that others seem to regard it as.
What I was referring to as "not slowing one's work down very frequently" was the corner case situation that someone brought up 4 comments above yours, which (in their view) renders the general type checking capabilities of Python >= 3.5 moot. I don't buy that logic, but that was their argument, not yours.
But to shift gears: if there are languages besides JS that you feel get their type system "just right", I'd be curious as to what they are, for the benefit of that future moment when I have the luxury of time to think about these things more.