Diminishing returns of static typing • Hacker News Board

Re: Diminishing returns of static typing

#491

Post by Merovius » Tue, Oct 03, 2017, 5:31 AM UTC

zbobet2012 wrote: post #377

Merovius wrote: post #343

Earlier quoted context omitted.

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

This is precisely what I said in the next paragraph and even mentioned away to correctly encode that "correctness". Where a _correct_ implementation of reverse has the property `strHead' s = strTail' (reverse s)` recursively. It's important to understand that type systems can encode correctness to the level you can specify it. So the program is therefore bug-free to the accuracy of your requirements on it. Most peopl…

Sorry, you are right, of course. I fell victim to one of the internet's classic blunders: Skimming a long comment thread and not carefully read what I reply to in the end :)

Re: Diminishing returns of static typing

#492

Post by yawaramin » Tue, Oct 03, 2017, 5:41 AM UTC

iamleppert wrote: post #251

It's far more useful to implement validation and type checking via introspection and interrogation of type, quantity, structure, size, or some other property at runtime in a dynamic programming language than to pedantically have to type all your variables. Most interesting types are far from the basics of different size numbers, string and objects anyway. It's better to trade a fast and quick runtime type error than…

> It's far more useful to implement validation and type checking via ... runtime in a dynamic programming language than to pedantically have to type all your variables.

How is that? I'm not seeing the increased utility.

> It's better to trade a fast and quick runtime type error....

What if the runtime type error crashes your app in production and loses your company money? What if it's something that slipped through your end-to-end integration testing because certain unlikely conditions never got covered, but they happened in production?

> ... than a lengthy compile-time type checking process,...

There are several modern compilers which are quite fast: D, OCaml, Java.

> ... because less code needs to be evaluated at run-time to expose the type error.

With static type checking, no code needs to be evaluated at runtime to expose a type error. Does dynamic typechecking offer a reduction over that?

> Wouldn't it be great if we can use the computer to figure out what the types should be by a runtime evaluation of the code and save precious human time for things only humans can do?

Wouldn't it be great if the computer would figure out the types at compile time and save us from having to manually input them? Well, the computer can do that, thanks to type inference. Several popular languages offer full, powerful type inference.

Re: Diminishing returns of static typing

#493

Post by flukus » Tue, Oct 03, 2017, 5:45 AM UTC

irrational wrote: post #468

alkonaut wrote: post #265

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

10-20 years?! Holy Cow! Other than huge software projects (like Word or Mac OS - and even then...) is there really software that still has that kind of maintenance window? I've worked for a Fortune 150 company for nearly 2 decades. There is not a single piece of software at the company that has not been rewritten from scratch (usually due to business changes) at least once every 10 years. I can't even imagine somethi…

IME most software will last that long, if it's remotely successful then it will at least make it to the 10 year mark. Business rarely changes drastically enough for a rewrite to make financial sense.

About best you can hope for is a new "epoch" that forces a rewrite. In the MS world we went from classic VB and VC++ to .net, a lot of companies went through rewrites to keep up with that and some of that software is now nearing 20 years old. There has been a few other epoch like changes, terminal -> GUI, c++ -> java, desktop -> web, except for maybe the last one it's been quite a while since a new epoch has begun.

Re: Diminishing returns of static typing

#494

Post by yawaramin » Tue, Oct 03, 2017, 5:48 AM UTC

sordina wrote: post #402

solatic wrote: post #122

OP draws a false one-dimensional relationship between types vs tests in terms of code quality. Writing expressive types instead of tests does much more than affect a quality curve - it changes the way you approach the problem you are trying to solve. The classic Haskell example is understanding how IO being a monad allows you to push impurity to the edge of your system. Start-ups decide not to write MVPs in languages…

Sorry to contradict you, but we wrote an mvp in rails even though we have 3.5 experienced Haskell programmers on staff. We did this because we knew we could build some web stack apps with all the trimmings much faster in ror. So there is at least one counter example.

I don't think it's really a contradiction. In a startup you still have to choose the quickest path that you think will lead to success. It just depends on what your definition of success is. RoR can be a safe choice even for Haskell devs if they just want to build an off-the-shelf webapp with all the trimmings. But if your definition of success is that you want to create a formally-verified smart contract platform and cryptocurrency, you're going to use something like Haskell or OCaml: https://github.com/tezos/tezos

Re: Diminishing returns of static typing

#495

Post by yawaramin » Tue, Oct 03, 2017, 5:53 AM UTC

hellofunk wrote: post #195

There is one aspect to this debate that is worth pointing out. What about generative testing, which is possible in static or dynamically typed languages? The article mentions that testing is perhaps more important in a dynamically typed language since there is less compiler support. But for example, Clojure rolled out the very clever Clojure.spec library that allows you to precisely specify all details relating to fu…

Clojure.spec is very clever, but it can be exactly duplicated in a statically-typed language by unit or property testing. It doesn't bring anything to the table that is totally a superset of static typing.

> In such a case, the line between these two type environments narrows.

Not really. Static types still offer you total proofs of the properties you encode as types, not just experimental results of tests.

Re: Diminishing returns of static typing

#496

Post by tluyben2 » Tue, Oct 03, 2017, 5:56 AM UTC

irrational wrote: post #468

alkonaut wrote: post #265

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

10-20 years?! Holy Cow! Other than huge software projects (like Word or Mac OS - and even then...) is there really software that still has that kind of maintenance window? I've worked for a Fortune 150 company for nearly 2 decades. There is not a single piece of software at the company that has not been rewritten from scratch (usually due to business changes) at least once every 10 years. I can't even imagine somethi…

I have started companies 15+ years ago that I sold which still use (a lot of) the same code. You think (I thought) that would never happen but I think this idea that every company rewrites everything is not all that common. Banks don't, but the small startups I work with don't either. Frontends get redone, there is refactoring and library updates but most (unless trivial tiny systems) just stays the same. You need to think that they run a business and that business is not software development usually. So if there is not a pressing reason to replace things, why would they allocate money for that?

Re: Diminishing returns of static typing

#497

Post by yawaramin » Tue, Oct 03, 2017, 5:57 AM UTC

hellofunk wrote: post #210

continuational wrote: post #97

Earlier quoted context omitted.

Static typing reduces the time you spend on debugging. Automatically reducing errors in code is not just for reducing errors in the resulting program. It also greatly reduces the time you spend on hunting bugs, especially if you have a poorly designed type systems where errors are reported far from their origin. Null, interface{}, NaN etc. propagates errors and thus gives you a stacktrace that is worthless when it fi…

In my experience, the time saved from writing in a statically typed language where the compiler catches the bugs for you is made up by having to work more closely with the compiler, typically write more code (type annotations and other things) and in general spend that same time on compile-time rather than run-time bug hunting. Dynamically typed languages typically involve a lot less code, which is time gained. That…

May I ask what your experience of statically-typed languages has been? I find that most people have had a common experience where they didn't get to work in tandem with a fast compiler and a succinct language which inferred most or all types for them, and so their perceptions are coloured by that.

Re: Diminishing returns of static typing

#498

Post by eastWestMath » Tue, Oct 03, 2017, 6:07 AM UTC

s17n wrote: post #409

zbobet2012 wrote: post #281

Earlier quoted context omitted.

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…

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. You can prove a program does what the types say it should do but that is not what "correctness" means. >Now a big part of the problem is expressing with sufficient accuracy what the properties of t…

No, I’m pretty sure there’s a pretty large body of academic and industrial research on proving program correctness that you can’t just hand wave away with sophistic “but what if your type signature is wrong” nonsense. And there’s a huge difference between a test and a proof - a test can only tell you a program doesn’t do what you think it should for a particular case, a proof tells you that your program does exactly what it is supposed to.

Re: Diminishing returns of static typing

#499

Post by nitrogen » Tue, Oct 03, 2017, 6:14 AM UTC

crimsonalucard wrote: post #467

alkonaut wrote: post #265

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

Rather than conduct experiments I believe that existing data still holds an answer. There's one metric that hasn't been looked at. Many projects over a long period of time tend to get rewritten in a different pattern or a new language/framework. I would say dynamic languages tend to have this problem in greater proportion over say a typed language like java. This is a direct long term marker for the maintainability o…

Counterpoint: Java projects tend to be maintained rather than rewritten because the verbosity of the language makes it difficult to tell boilerplate from productive code. It's less dramatic to rewrite in a dynamic language because understanding the full system before and after is easier.

Re: Diminishing returns of static typing

#500

Post by rbehrends » Tue, Oct 03, 2017, 6:16 AM UTC

alkonaut wrote: post #265

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

I agree that the third point is important, but it's not clear that it's static typing that is important, and not type annotations. One reason why I can still fairly easily read and understand Eiffel code that I wrote decades ago is Design by Contract. And there's normally nothing static about DbC, it's about assertions that are checked at runtime and that by convention are part of a class's interface.

What both type annotations and DbC are is self-enforcing documentation (of an interface) that doesn't go out of sync with the actual code. But for that, you don't necessarily need static type checks. Now, type checking of type annotations that happens exclusively at runtime is an option that hasn't been explored much (after all, if you already have type annotations, why not let the compiler make use of them?), but an option that has sometimes been used successfully is having a mixture of static and dynamic type checks. You can often greatly simplify a type system by delaying (some) type checking until runtime (examples: for covariance or to have simpler generics).