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

211–220 of 306 posts

Re: Why static languages suffer from complexity

#211

Post by lmm »

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…

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

Which is exactly what a type error is!

> The Rust borrow checker is an invariant enforcer. It explicitly does automatic global analysis, and reports explicitly that what's going on at point B is inconsistent with what point A needs. This is real progress in programming language design, and is Rust's main contribution.

> That's the direction to go.

The borrow checker is an ad-hoc informally specified implementation of half of an affine type system. Having to switch programming languages every time you want to add a new invariant is a poor paradigm. What we need is a generic framework that allows you to express invariants that are relevant to your program - but again, that's exactly what a type system is.

Rust has done a great thing in showing that this is possible, but linear Haskell or Idris - where borrow checking is not an ad-hoc language feature that works by gnarly compiler internals, but just a normal part of the everyday type system that you can use and customize like any other library feature - are the approach that represents a viable future for software engineering.

Re: Why static languages suffer from complexity

#212

Post by ImprobableTruth »

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…

>your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one.

Yes, just like you have to evolve your specification/documentation. Similarly, in the exploratory phase you'll stick to very 'rough' typing and next to no proofs and as the program gets clearer and solidifies, you can continuously refine your types (with the amount of refinement depending on how much certainty one wants). A mature program with a rigid spec is going to be harder to change, but that's just how it is anyway.

>Moreover proofs are non-compositional: you make a tiny change somewhere and you might have to change all proofs.

People on HN keep repeating this, but it's trivial because it's actually just a statement about the nature of properties. Proven invariants provide an interface to be used by the rest of the program. If the changes you make don't break your invariants but only the proofs, then you just have local adjustments to make. If your change cascades through the entire program, then it's because all the invariants get invalidated and your 'tiny' change actually changes a good deal about the semantics (and thus the spec) of the program.

The exact same thing applies to unit tests, but you don't see people constantly bemoan the non-compositional nature of unit tests even though a 'tiny' change could break all your unit tests.

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

Not only are specifications declarative, they're generally magnitudes smaller. If you're as confident in your spec as in your code, something is very, very wrong with your spec. Well, or your code is your spec, but in that case you get what you pay for.

Re: Why static languages suffer from complexity

#213

Post by Jensson »

throw10920 wrote: post #122
armchairhacker wrote: post #54

"Why not add X feature? If people don't want to use X, they just don't, and there are basically 0 downsides." In theory this is true. If the compiler is decent, compile times and analysis shouldn't really be affected. Maybe libraries will use X but otherwise they would use a manual implementation of X anyways. But in practice developers misuse features, so adding a feature actually leads to worse code. It also create…

> But in practice developers misuse features, so adding a feature actually leads to worse code. Is that really a problem on the language's side, though? Devs are capable of mis-using any feature, even extremely basic ones that almost every language has (variable names, for instance (although I'm laughing in FORTH)). Code standards and code reviews are necessary tools in the first place because it doesn't matter what…

> Is that really a problem on the language's side, though?

Yes, for a language to be good in practice you need to look at what developers actually do and not how a perfectly rational developer would use the language.

Re: Why static languages suffer from complexity

#214

Post by lmm »

Jtsummers wrote: post #176
yakshaving_jgt wrote: post #154

Earlier quoted context omitted.

Is there any reason you didn't address the second link that I shared?

Mostly because, per my reading (as an admitted Haskell dabbler and not fluent), it looks like a variation on a theme rather than a totally different thing. It seems to be a more consistent and refined (har har) way of doing the same thing as the first link, and still has a dynamic check (at least in one form, refine vs refineTH ) just like the smart constructors. But also because we got derailed from my initial point…

> there is no type system (that I'm aware of, not even Idris as far as I know) which can prove in its static type system every piece of logic about a program.

Many static type systems can prove anything that can be proven. Notionally one might write a program that relies on something unproven like the Collatz conjecture, though I'm not sure that would happen in practice (e.g. it's easy to write a program that relies on the Collantz conjecture for numbers below 2^64, but that's quite provable). Whether it's actually worth writing out the proof is another question though.

> This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.

This is true but makes surprisingly little difference, because you still want to keep track of which values have or haven't had that runtime check applied. So you almost always want your postconditions expressed as types (even if they're just "marker" types that indicate that a given runtime check was passed). Put another way, any metadata you would want to be able to track about a function's argument values or return value, you almost always want to be able to carry that metadata around with that value before it's passed in or after it's returned - but at that point that metadata is a type, and it's easiest to represent it as one.

Re: Why static languages suffer from complexity

#215

Post by lmm »

tomp wrote: post #114
HideousKojima wrote: post #23

Earlier quoted context omitted.

In C# I can just parse it to a Dictionary , and I can do that without destroying the usability of the rest of the language.

What if the JSON represents a list, or an int? Also, how do you then access nested objects, like data['key'][0]['attr'] in Python?

> What if the JSON represents a list, or an int?

Then you write one short operator (and I agree that some static languages make this more cumbersome than it should be) to say so, and either handle the case where it isn't, or explicitly declare yourself partial and not handling it.

> Also, how do you then access nested objects, like data['key'][0]['attr'] in Python?

With lenses, something like:

    data ^? (key "key") >>> (nth 0) >>> (key "attr")
If you do several unsafe operations in a row then this is cumbersome by design - you want to be clear which parts of your program are safe and which are unsafe, so that readers can understand and know where to review. But a good language should let you compose together several unsafe operations in a lightweight way and then execute them as a single unsafe operation, for cases like this where you want to work in the unsafe part of the language for a bit.

Re: Why static languages suffer from complexity

#216

Post by chubot »

Nice article! Highly related discussions:

https://github.com/fsharp/fslang-suggestions/issues/243#issu...

https://old.reddit.com/r/ProgrammingLanguages/comments/placo...

F# designer Don Syme is making the "biformity" argument, e.g. needing a debugger for compile time as well as runtime.

and

Syme & Matsakis: F# in the Static v. Dynamic divide https://old.reddit.com/r/ProgrammingLanguages/comments/rpcm6...

I still think something an application language with something like Zig's comptime would fill a big niche. (As opposed to a systems language.)

Re: Why static languages suffer from complexity

#217

Post by mananaysiempre »

jayd16 wrote: post #16
gumby wrote: post #12

Earlier quoted context omitted.

> > I cannot imagine a single language without the if operator… Production languages (like prolog or make) don’t need an if statement or operator as selection is implicit when a production matches.

Shader languages are also hellbent on avoiding branches too so if is frowned upon and often not used. I could easily imagine not having it in a shader language.

The old assembly-like languages (ARB_fragment_program, NV_fragment_program*, et al.) did indeed not have branches, only selection and conditional termination, because that was the extent of the capabilities of the underlying hardware. (I understand the execution on modern fragment processors can’t actually diverge within a single batch, either, so they execute both branches and select afterwards, but they are at least capable enough not to do that if the branch went the same way everywhere. But it’s been a long time since I’ve had a state-of-the-art GPU to play with.)

Re: Why static languages suffer from complexity

#219

Post by chrisaycock »

AndyKelley wrote: post #198

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?

Debating language design with people who don't actually know the language (or understand the features) is extremely frustrating.

But anyway, thanks for your work on Zig. Your metaprogramming concepts were heavily influential for some of the ideas in my own language, Empirical.

Re: Why static languages suffer from complexity

#220

Post by earleybird »

BalinKing wrote: post #159
spc476 wrote: post #158

Earlier quoted context omitted.

> You can write your programs and use the same language to prove theorems about them. Didn't Kurt Gödel and Alan Turing do some work on proving statements within a system?

AFAIK languages like Idris, Agda, and Coq are not Turing-complete (specifically, they disallow general recursion) for just this reason.

General recursion, yes however often the fixed point operator is added (and its associated judgements) to have interesting programs/proofs.

Hmm, that fixed point operator, rings a bell, can't quite put my finger on it . . . :-)

Post reply on HN