PL research is not necessarily for "contributing to programmer productivity." Formalization of various programming language concepts into a type system[0] allows researchers to apply analysis and verification techniques. The simplest example I can think of is the Maybe type. Instead of having null pointers and, if you forget to check for NULL, getting a runtime error (segfault, NullPointerException, whatever), instead you would fail to compile since the "null-like" pointer would be a Maybe type, not the concrete value. You can't use it without unwrapping it. Concretely, the code:
int foo(int *p) {
return *p + 17; //well, probably something more complicated.
}
if p is NULL, this code doesn't work. In a language with a more expressive type system, we would write:
foo :: Maybe Int -> Maybe Int
foo p = case p of
Just x -> Just (x + 17)
Nothing -> Nothing
(Note: there are more succinct ways to write this example in Haskell, but I'm trying to illustrate the code.)
In this case, we have demonstrably covered every case. That's what an expressive type system gets you: you can completely preclude certain classes of bugs like null pointer dereferences by having a sufficiently expressive type system. It's the same in more relevant PL research: people are attempting to formalize systems so that whole classes of bugs can be removed at compile time. It's not about user case studies or anything like that: those can come later, when features look like they'd be useful to integrate into languages.
It looks like the featured article gives a case study about a pretty bad type system. A sufficiently expressive type system doesn't get in the way--it aids the programmer, not hinders her. Heck, in Haskell and ML, you don't even have write down types--the compiler will infer them for you. (It is Haskell practice to type-annotate toplevel functions anyway).
[0] When I say type system, I mean a static type system. For the purposes of this discussion, dynamically typed programs are statically typed, just with not-very-useful types.
You say: "when features look like they'd be useful to integrate into languages". How do you know a feature would be "useful" without compelling evidence that this is really a problem for programmers? Now you're back to the original problem of figuring out what the most significant problems are for programmers. Wouldn't it be better to figure this out BEFORE PL people plunge into a particular topic?
Remember all the research done on typestates? The motivation section of those papers was usually a few paragraphs of total BS. AFAIK, there was no real data nor experiment that demonstrated this was a real problem for professional programmers.
FYI: I like static type systems and used Haskell et. al. But no one has demonstrated that it is better than even Visual Basic!
Not really. The research, again, isn't in programmer usability. It's in formal logic and analysis of the semantics of computer programs. Benefits for programmers are just a side-benefit. The goal is advancing humanity's understanding of computer science, not in helping programmers, although sometimes the two goals are somewhat linked and deeper understanding occasionally yields industry benefits. In my example, and in many instances of expressive type systems, research has yielded tangible benefits for industry.
In this case, we have demonstrably covered every case. That's what an expressive type system gets you: you can completely preclude certain classes of bugs like null pointer dereferences by having a sufficiently expressive type system. It's the same in more relevant PL research: people are attempting to formalize systems so that whole classes of bugs can be removed at compile time. It's not about user case studies or anything like that: those can come later, when features look like they'd be useful to integrate into languages.
It looks like the featured article gives a case study about a pretty bad type system. A sufficiently expressive type system doesn't get in the way--it aids the programmer, not hinders her. Heck, in Haskell and ML, you don't even have write down types--the compiler will infer them for you. (It is Haskell practice to type-annotate toplevel functions anyway).
[0] When I say type system, I mean a static type system. For the purposes of this discussion, dynamically typed programs are statically typed, just with not-very-useful types.