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

Typing Is Hard

typing-is-hard.ch

Post reply on HN
Print view View original

71–80 of 83 posts

Re: Typing Is Hard

#71

Post by bitwize »

elmo2you wrote: post #65
bitwize wrote: post #48

Earlier quoted context omitted.

Static typing takes the burden of verifying certain forms of program correctness off the programmer and puts it in the compiler where it belongs, thus expanding the space of correct code the same programmer can write per unit cognitive load. The more kinds of things you check for in the type system (static lifetimes in Rust, for instance), the more benefits you get. It doesn't serve as a substitute for good taste, be…

I get you point(s) and I guess you mean well. Statically typed languages do essentially what you said. They mostly (if not only) move data validation from run time to compile time. In dynamically typed languages, this often doesn't happen in the first place, while with static typing you are pretty much forced to. I have a little over 30 years of programming experience, the majority of it in statically typed languages…

> Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them.

This is a trap many programmers fall into. You should be parsing, not validating[0]. If you are ingesting JSON data, for instance, what you need is not a generic JSON parser but a parser that only accepts JSON representations that map to a particular, static data type and throws parse errors where in a dynamic language you might find "validation errors", for example, an unknown data field or a field value of the wrong type.

Getting the types right early doesn't substantially slow you down overall, and yields a result that's much, much easier to get correct. Any such slowdown is a greater "capex" in the form of initial development, that's more than offset by much, much lower "opex" in the form of maintenance.

> In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those.

This is wrong, and it's wrong for "theory vs. reality" reasons. Take one of the languages in your background: C. What you see may be true of a hypothetical programmer who knows all the arcane rules to C and can avoid tripping one of C's many, many UB landmines the first time, every time. But most programmers in the real world are human beings who may not have had their coffee. And they are going to make mistakes and unwittingly trip UB landmines. And this is as true of great C programmers as it is of beginners. You could build some strong rules around C, such as "allocate memory as little as humanly possible" and "avoid threading unless you can justify needing the performance gains" that will help programmers stay well clear of the traps inherent to C programming. Or you can switch to Rust, and fearlessly write code that allocates memory and even threaded code, because Rust's type system guarantees memory safety and a lack of data races.

[0] https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

Re: Typing Is Hard

#72

Post by elmo2you »

bitwize wrote: post #71
elmo2you wrote: post #65

Earlier quoted context omitted.

I get you point(s) and I guess you mean well. Statically typed languages do essentially what you said. They mostly (if not only) move data validation from run time to compile time. In dynamically typed languages, this often doesn't happen in the first place, while with static typing you are pretty much forced to. I have a little over 30 years of programming experience, the majority of it in statically typed languages…

> Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them. This is a trap many programmers fall into. You should be parsing, not validating[0]. If you are ingesting JSON data, for instance, what you need is not a generic JSON parser but a parser that only accepts JSON representations that map to a particular, static data type and throws parse erro…

> This is a trap many programmers fall into. You should be parsing, not validating.

Maybe it was an unfortunate choice of words on my part. Additionally, and I only meant to indicated how it was promoted/advertised, rather than make any statement about weather it was a sound argument. Either way, at the end of the day, a parser is a validator all the same.

Sure, more (domain) specific parsers indeed make better code (duh). That's true for both compile time and run time parsing. But how often, in real life business situation, is there enough time to create a solid architecture and fully fleshed out (domain) specific (run time, or compile time) parsers?

Again, I'm not disputing that statically typed languages may have a potential for creating more structurally healthy code. However, from my experience it still takes a hell of a lot of time and effort (for which there often is no room in real life business situations). Dynamically typed languages often create seriously flawed software, no doubt about that. But I'm convinced that this is more because many programmers just don't do what they actually should be doing in any case (in any language).

Statically types language can alleviate that problem a little, by forcing programmers to think more about what they should already be thinking about in the first place. But it is not a magic bullet. I'm not even going to discuss the downsides from overly specified/specific software code.

> This is wrong, and it's wrong for "theory vs. reality" reasons.

In case you missed it: my main gripe with all of this is that I just can not find any of all these great improvements, that evangelists keep pushing, in actual real world examples (at least not within my personal experience). Yet here you try to convince me that my point it too much theory and telling me a story about how real world programming actually works. Seriously? I mentioned C to indicate from which direction in the industry I come from, nothing more. Well, maybe also to indicate that I've been doing this for some time now.

No need to tell me how programmers work (plenty of experience with that), or making excuses for how it's just human nature for them to fuck up if they aren't held by their hand. I might have bought that kind of bullshit 25 years go. There have been plenty of attempts, purporting to to give programmers better tools and assist them writing better software. Most of them with only good intentions. Nothing new about that, about as old as commercial software itself. However, I've seen a rather depressing trend how all of those hardly ever held up in reality, over time. Whether that is because the knowledge level of programmers constantly degrades, or if it is because such solutions promote laziness, that might be more of a philosophical discussion and hard to establish as fact.

I find it at least a bit ironic though, how I apparently am being schooled on how I "just don't get it right", by what to me sounds and smells a hell of a lot like theoretical evangelical drivel itself. In fact, at this point I can't help but recall an iconic argument about how plants crave Brawndo, because of the electrolytes.

Keep on programming the way you do. If you are a good programmer, it shouldn't matter which language or tools you use. I wish you nothing but the best and good luck. Time will tell if Rust will survive the hype and actually deliver what it has been promising for a while. Maybe it indeed will. I'm not holding my breath though. Especially not since (nontransparent) corporate influence/control on languages and tools in becoming an ever growing factor (with all kind of problems associated with it).

Re: Typing Is Hard

#73

Post by ThreeFx »

p0llard wrote: post #47

> There exist many type inference algorithms, the best known one is the so-called Algorithm W. Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is more efficient (which was what I had been led to believe), but that Algorithm W is more suited to functional (as opposed to imperative) implementations. Edit: Actually I think I'm parsing this sentence incorrectly, "best known" means literally…

Best known is indeed meant as "most widely known" (although that may be true for only my little bubble). I think it's taught in most type theory / formal methods courses though. If anybody has facts for/against this claim I'd be happy to update the page.

Re: Typing Is Hard

#75

Post by ThreeFx »

dnautics wrote: post #55

Is the comment about zig correct about its typing? It's certainly true about its compilation , but that's not the same thing. Also, if you're going to have a turing-complete compile time, you might as well have it in something that looks like a programming language, since that will fit your debugging mental model.

Since you can pass types to compile-time functions, yes that is correct. Take the example [from the 0.6.0 documentation](https://ziglang.org/documentation/0.6.0/#comptime) for example: At compile time the compiler has to figure out whether to type the `max` function using `u32` or `f64`. Since you can make the boolean condition arbitrarily complex the _type_ of max function called is undecidable in general.

I'm not arguing for or against undecidability in type systems, the page aims to be present the information neutrally.

Re: Typing Is Hard

#76

Post by ThreeFx »

riwsky wrote: post #24

Correction: Java’s type system has been unsound since version 5; version 8 (which TFA describes as the start of the issue) just happened to be the latest version at the time it was discovered.

Thanks, fixed!

Re: Typing Is Hard

#77

Post by dnautics »

ThreeFx wrote: post #75
dnautics wrote: post #55

Is the comment about zig correct about its typing? It's certainly true about its compilation , but that's not the same thing. Also, if you're going to have a turing-complete compile time, you might as well have it in something that looks like a programming language, since that will fit your debugging mental model.

Since you can pass types to compile-time functions, yes that is correct. Take the example [from the 0.6.0 documentation]( https://ziglang.org/documentation/0.6.0/#comptime ) for example: At compile time the compiler has to figure out whether to type the `max` function using `u32` or `f64`. Since you can make the boolean condition arbitrarily complex the _type_ of max function called is undecidable in general. I'm not…

Sorry, I wasn't defensive about the decidability of the type system, just curious about the analysis, which squares with my understanding of zig now! Thanks for the clarification; it might be helpful to expand on that in the doc.

Re: Typing Is Hard

#78

Post by kevincox »

ThreeFx wrote: post #73
p0llard wrote: post #47

> There exist many type inference algorithms, the best known one is the so-called Algorithm W. Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is more efficient (which was what I had been led to believe), but that Algorithm W is more suited to functional (as opposed to imperative) implementations. Edit: Actually I think I'm parsing this sentence incorrectly, "best known" means literally…

Best known is indeed meant as "most widely known" (although that may be true for only my little bubble). I think it's taught in most type theory / formal methods courses though. If anybody has facts for/against this claim I'd be happy to update the page.

It might make sense to update to "most widely known" to avoid that source of ambiguity. You can take that sentence as ((best known) algorithm) or (best (known algorithm))

Re: Typing Is Hard

#79

Post by choeger »

remexre wrote: post #46
choeger wrote: post #43

Earlier quoted context omitted.

Julia has no (what some call "static" but that's actually the only form that matters) type system. It also has lisp-like macros.

Having no type system (e.g. Forth) is different from having dynamic checking for your types (e.g. JavaScript, Python, Julia iirc), though. Julia also has Common Lisp-like multimethods, which are pretty nice, especially for linear algebra sorts of stuff, where you might be multiplying a scalar by a tensor, or a tensor by a tensor, and don't want to have to specify different syntax for the two operations.

What you call "dynamic checking your types" is actually the same as having an algebraic uni type and inspecting its construction.

A type system is a means to prove the absence of certain errors in a program.

Think of a type system as a park pilot that sounds an alarm before you hit an obstacle. What python does is the crashing sound when you hit the obstacle. Forth is finding the dent days later and wondering where the eff that came from. Python is more conclusive then Forth, but you still have a dent.

Re: Typing Is Hard

#80

Post by TheCoelacanth »

orthoxerox wrote: post #32
kps wrote: post #7

If you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.

A Turing-incomplete macro system will always terminate, but it may terminate in 2 years.

I don't think a Turing-incomplete language implies that programs always terminate. As a counter-example, imagine an obviously Turing-incomplete language that contains only a single instruction which simply does nothing in an infinite loop.
Post reply on HN