Diminishing returns of static typing • Hacker News Board

Re: Diminishing returns of static typing

#341

Post by hinkley » Mon, Oct 02, 2017, 9:33 PM UTC

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.

I work with an in-house framework written in Javascript.

You would think by looking at the code that the creators had a 30 word vocabulary, because 80% of the code uses the same six nouns and four verbs to pass data around and what you use those for depends on the context of who is calling it.

Oh, but the entire thing is written using promises, so most of your function calls have no context. It's hell, and I'm starting to worry that Node has dug itself a reputation hole it will never get out of.

Re: Diminishing returns of static typing

#342

Post by Merovius » Mon, Oct 02, 2017, 9:37 PM UTC

pdonis wrote: post #127

catpolice wrote: post #106

Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Relatively little behavior can be encoded in inexpressive type systems, so there's a lot of room for bugs that have nothing to do with types. A lot more behavior (e.g. the sorts of invariants mentioned in agentultra's top level comment) can be encoded in a more expressiv…

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that…

> The author of the article implicitly equates "statically verified code" with "bug-free code".

Not at all. First, the statements as put here are discrete (boolean even) while I present both "statically verified code" and "bug-freedom" as living on a continuum. Secondly, I don't equate them. If anything, I assume a monotonic, positive relationship between them (strictly speaking not even that. I make pretty clear that the curves could also have whatever shape. But I yield that I am very suggestive in this because I do strongly believe it to be the case). In fact, one of the main points of the argument is that the two are not equal - otherwise, the blue curves I drew would all be straight lines from (0,0) to (1,1). And lastly, none of this is done implicitly. I mention all of this pretty explicitly :)

Re: Diminishing returns of static typing

#343

Post by Merovius » Mon, Oct 02, 2017, 9:43 PM UTC

zbobet2012 wrote: post #281

pdonis wrote: post #127

Earlier quoted context omitted.

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that…

It depends on your type system. In new languages like Idris or F* you can encode in the type the correctness of an algorithm and it will not compile if the compiler can not prove that correctness. For example I can prove my my string reverse works in Idris ( https://www.stackbuilders.com/news/reverse-reverse-theorem-p... ). Or I could prove that my function squares all elements in a list. Etc. Now a big part of the p…

> For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-p...).

This article basically demonstrates GP point, though. It proves that `reverse` is self-inverse, but there are lots and lots of functions that are self-inverse (for example, `x -> x` is self-inverse. As would be the function that swaps any odd-index element with the one following it).

The claim was a difficulty of how to encode the actual correctness into your type-system. That this article doesn't actually encode correctness of reverse, seems like pretty good for that difficulty.

Re: Diminishing returns of static typing

#344

Post by UncleMeat » Mon, Oct 02, 2017, 9:43 PM UTC

crdoconnor wrote: post #294

rbobrowicz wrote: post #203

Earlier quoted context omitted.

Personal anecdote: I worked on a small Python project some years ago and we had a type error in production despite having tests. We traced it back to a call to a third party library. It was supposed to return a list of results, and all of the test cases around it worked and always got a list back. In production however we encountered an error because if there was only one value to return, the library would not return…

>or the author of the library for bad design That's the one. That's a damned stupid decision.

Yeah and a static type system refuses to let you make such a stupid decision. When interoperating with code I didn't write, knowing that the code is guaranteed to conform to some specification is valuable.

Re: Diminishing returns of static typing

#345

Post by hinkley » Mon, Oct 02, 2017, 9:44 PM UTC

Ace17 wrote: post #150

Eridrus wrote: post #35

Earlier quoted context omitted.

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.

Actually, refactoring browsers were pioneered by Smalltalk people.

And smalltalk had to leave trampolines in place to deal with renames that it couldn't finish deterministically. No thank you.

Nobody ever talks about that little horror when they bring up how Smalltalk could to refactoring JUST FINE without static types. It wasn't just fine, turns out.

Re: Diminishing returns of static typing

#346

Post by flavio81 » Mon, Oct 02, 2017, 9:44 PM UTC

Tade0 wrote: post #305

bad_user wrote: post #204

Earlier quoted context omitted.

The other possibility is that the industry suffers from anti-intellectualism, so we keep reinventing the same 2 languages.

Do you believe that this is plausible?

I think this has happened for a long time. First (70s), features from Algol-68, like structured programming or better flexibility for data types, were ported to other languages. Then (80s-present), the features from Smalltalk and Lisp started slowly to be ported to other languages, many times in an incomplete or unelegant way.

We're still doing this, for example the last production spec of the Java language finally incorporated a mechanism to pass functions as input parameter on a method. And the next version of Java (9) will attempt to have some interactivity, with a kind of REPL. This, coupled with the powerful facilities of good Java IDEs, will give Java developers of 2017 the level of Interactivity and easiness of development that Smalltalk and Lisp users have enjoyed since the late 70s. Sad but true.

Julia -an interesting language, by the way- borrows multiple dispatch from the Common Lisp Object System (CLOS), among other features. CLOS itself was a further evolution of the OOP brought to the table by Smalltalk, invented by a true genius: Alan Kay.

Rust is basically a "fixed C++", that is, a more usable, less annoying C++.

So it's difficult to say there are truly new things in programming language. But it's not everything limited to Smalltalk and Lisp -- Prolog, ML (and OCaml, F# and Haskell) do bring new concepts to the table, and are worth checking out.

Re: Diminishing returns of static typing

#347

Post by seanwilson » Mon, Oct 02, 2017, 9:47 PM UTC

ridiculous_fish wrote: post #42

drblast wrote: post #31

Earlier quoted context omitted.

Definitely. Static typing lets you turn the compiler into a hard-working friend that helps you refactor large projects without going insane. There are no diminishing returns. Defining types is easy and enhances code readability.

If you believe there are no diminishing returns, I'm interested to hear your reply to the author's question about why we don't all use Agda or Idris.

Have you used them? Switching to a language like Agda or Idris is entering the realm of formal verification because the types are so expressive. It's completely different to what most programmers are used to.

Essentially the types being used as so complex the type checker cannot automate the decision about two types being compatible so you have to write maths proofs to help. The types used in mainstream languages are simple enough that the type checker never needs help like that.

The cost of formal verification right now is immense but the benefit is close to bug free code. Mainstream strong statically languages require nowhere near the same amount of effort and give clear benefits over dynamic types.

Re: Diminishing returns of static typing

#348

Post by Merovius » Mon, Oct 02, 2017, 9:51 PM UTC

simon_o wrote: post #12

The biggest issue with claims like "there are only diminishing results when using a type system better than the one provided in my blub language" is that it assumes people keep writing the same style of code, regardless of the assurances a better type system gives you. "I don't see the benefit of typed languages if I keep writing code as if it was PHP/JavaScript/Go" ... OF COURSE YOU DON'T! This is missing most of th…

The article makes two main points: a) static typing has a cost and b) thus, any benefit it brings should be examined against that cost.

I am sorry, but I don't really see how you stating more benefits of static typing really counters either of them.

I recommend reading the article again. But this time, try not to read it as defending a specific language (I only mentioned my blub language so that it's a more specific and extensive reference in the cases where I use it - if you are not using my blub language, you should really just ignore everything I write about it specifically) and more as trying to talk on a meta-level about how we discuss these things. Because your comment is an excellent example of how not to do it and the kind of argument that prompted me to this writeup in the first place.

Re: Diminishing returns of static typing

#349

Post by nv-vn » Mon, Oct 02, 2017, 9:51 PM UTC

yellowapple wrote: post #185

fulafel wrote: post #111

Earlier quoted context omitted.

There have been references to Clojure, Elixir, Smalltalk, Common Lisp in the comments here, what makes you think just Javascript & Python?

It's worth noting that Elixir (by descent from Erlang) can emulate at least a basic static typing system pretty easily through pattern matching. You miss out on some features common in more traditionally-object-oriented languages (namely: subtypes), but tagged tuples and structs do provide a lot of the same safety benefits in runtime (and tools like Dialyzer can - last I check - use such pattern matching as a basis f…

Elixir and Erlang still lack the ability to typecheck any process behaviors because messages can take any type anywhere.

Re: Diminishing returns of static typing

#350

Post by bitwalker » Mon, Oct 02, 2017, 9:52 PM UTC

Sir_Cmpwn wrote: post #284

muricula wrote: post #278

Earlier quoted context omitted.

void * is part of it, but you can also implicitly cast from between integer types, and also between integers and enums. Think of passing an enum or an int into a function which takes a long as an argument.

I mean... I don't really think that's a strong case for calling C's type system weak.

I suspect most people which state that C has a weak type system are really talking about the fact that C has a weakly _enforced_ type system. You can break the type system's rules rather easily (or perhaps it's more accurate to say, the type system is too permissive), either way it doesn't provide you the same guarantees a stronger type system provides). At least that's my take on it.