5 ms·

They're so right about that. As a frontend dev, I don't care about that extra 1-2% of bugs that, say, ownership types could catch if it kills my productivity by

They're so right about that. As a frontend dev, I don't care about that extra 1-2% of bugs that, say, ownership types could catch if it kills my productivity by having to annotate everything. However, if I can figure out what a method actually returns and click through to it in the IDE, that's the real gain from types for me. Type analysis has to be fast to be able to do that. My impression of research in academia is that it's disproportionately focused on even stronger types that are even harder to compute. Not everyone builds spaceships.

mpweiher 9y ago
The "documentation for humans" effect is also the only effect that has had at least some empirical validation[1]. Interestingly, it is not necessary to have the type names/annotations actually statically checked. [1] https://sites.google.com/site/stefanhanenberg/ https://sites.google.com/site/stefanhanenberg/ [EDIT] Clarified which effect
- rhaps0dy 9y ago
  > That's also the only effect that has had at least some validation scientifically Which effect, sorry? I can't identify the referent of "That".
  - mpweiher 9y ago
    Sorry, fixed. They also studied "time to completion" and "correctness" for a new task, and for those the dynamic languages did better.
    - rhaps0dy 9y ago
      Thanks. After commenting I read the first paper in the page you linked. The one about trying to give an advantage to dynamic languages (Groovy vs Java), and measuring time-to-completion, for 4 tasks. Turns out a static language has a time advantage when using an API, but a dynamic one has an advantage when writing code (that nobody will reuse).
mafribe 9y ago
research in academia is that it's disproportionately focused on even stronger types that are even harder to compute. Type inference for simple types in sequential computation is a solved problem, Milner and Damas showed how to do it in [1] in 1982. However, most extensions of Damas/Milner cross from decidable type inference to undecidability, so some annotation is often necessary, e.g. Scala, Rust, Haskell (kinding). Most work on expressive typing systems (e.g. dependent types) has a different aim, namely using types for the verification of arbitrary program properties. This is undecidable, but we want (and need) as much automation as possible to lower the cost of verification, whence a lot of research is about partially automated type inference for very expressive typing systems. For most standard front-end dev, verification is not an issue since - the field has fairly low correctness requirements that can easily achieved with testing - typically you don't have strong specifications to verify against. No formal spec, no verification. [1] L. Damas, R. Milner: Principal type-schemes for functional programs, http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_typ...
hacker_9 9y ago
Just going to point out here that you are conflating Javascript problems with dynamic language problems. Try Clojure, a well designed dynamic language, and you'll find you are a lot more productive with it than any statically typed language. Indeed over the weekend I was able to design and build a GUI DSL, layout system, model-view databinding, command event system, and serialisation/deserialisation logic for a side project of mine. This sort of stuff would have taken weeks of effort in a static language.
- wtetzner 9y ago
  Clojure is a fine language, and I wrote it professionally for a few years. However, I don't see why this would be true: > This sort of stuff would have taken weeks of effort in a static language. I've also written plenty of things in typed languages, and in many ways they can be faster to develop in than dynamic languages. Of course, you do need to change the way you program a bit to really take advantage of types. I think the main advantage Clojure has over most typed languages is macros, but there is work being done to rectify even that.
  - hacker_9 9y ago
    I used to think this, until I used Clojure. I'm surprised you used it professionally and have that mindset, I write far less code in Clojure and get far more done. The productivity gains are amazing, especially when I can just upload new code on the fly as the program is running.
    - nickpsecurity 9y ago
      It's because it's a LISP with good ecosystem. LISP is already strongly, but dynamically, typed from what I'm told. So, you get quite a bit of benefit. You could probably do the same in a statically- or gradually-typed LISP. Main difference is you'll catch a few more interface errors without tests. Also, if using specs or types, one can do automated generation of testing, enabled better static analysis, and/or improve optimization in compilers. Basically, the tools know a bit more about what you're trying to do.

mpweiher 9y ago

The "documentation for humans" effect is also the only effect that has had at least some empirical validation[1]. Interestingly, it is not necessary to have the type names/annotations actually statically checked. [1] https://sites.google.com/site/stefanhanenberg/ https://sites.google.com/site/stefanhanenberg/ [EDIT] Clarified which effect

rhaps0dy 9y ago
> That's also the only effect that has had at least some validation scientifically Which effect, sorry? I can't identify the referent of "That".
- mpweiher 9y ago
  Sorry, fixed. They also studied "time to completion" and "correctness" for a new task, and for those the dynamic languages did better.
  - rhaps0dy 9y ago
    Thanks. After commenting I read the first paper in the page you linked. The one about trying to give an advantage to dynamic languages (Groovy vs Java), and measuring time-to-completion, for 4 tasks. Turns out a static language has a time advantage when using an API, but a dynamic one has an advantage when writing code (that nobody will reuse).

mafribe 9y ago

research in academia is that it's disproportionately focused on even stronger types that are even harder to compute. Type inference for simple types in sequential computation is a solved problem, Milner and Damas showed how to do it in [1] in 1982. However, most extensions of Damas/Milner cross from decidable type inference to undecidability, so some annotation is often necessary, e.g. Scala, Rust, Haskell (kinding). Most work on expressive typing systems (e.g. dependent types) has a different aim, namely using types for the verification of arbitrary program properties. This is undecidable, but we want (and need) as much automation as possible to lower the cost of verification, whence a lot of research is about partially automated type inference for very expressive typing systems. For most standard front-end dev, verification is not an issue since - the field has fairly low correctness requirements that can easily achieved with testing - typically you don't have strong specifications to verify against. No formal spec, no verification. [1] L. Damas, R. Milner: Principal type-schemes for functional programs, http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_typ...

hacker_9 9y ago

Just going to point out here that you are conflating Javascript problems with dynamic language problems. Try Clojure, a well designed dynamic language, and you'll find you are a lot more productive with it than any statically typed language. Indeed over the weekend I was able to design and build a GUI DSL, layout system, model-view databinding, command event system, and serialisation/deserialisation logic for a side project of mine. This sort of stuff would have taken weeks of effort in a static language.

wtetzner 9y ago
Clojure is a fine language, and I wrote it professionally for a few years. However, I don't see why this would be true: > This sort of stuff would have taken weeks of effort in a static language. I've also written plenty of things in typed languages, and in many ways they can be faster to develop in than dynamic languages. Of course, you do need to change the way you program a bit to really take advantage of types. I think the main advantage Clojure has over most typed languages is macros, but there is work being done to rectify even that.
- hacker_9 9y ago
  I used to think this, until I used Clojure. I'm surprised you used it professionally and have that mindset, I write far less code in Clojure and get far more done. The productivity gains are amazing, especially when I can just upload new code on the fly as the program is running.
  - nickpsecurity 9y ago
    It's because it's a LISP with good ecosystem. LISP is already strongly, but dynamically, typed from what I'm told. So, you get quite a bit of benefit. You could probably do the same in a statically- or gradually-typed LISP. Main difference is you'll catch a few more interface errors without tests. Also, if using specs or types, one can do automated generation of testing, enabled better static analysis, and/or improve optimization in compilers. Basically, the tools know a bit more about what you're trying to do.