In my opinion, you've got the order wrong: types are the abstraction, and untyped-ness is the concrete implementation (just look at almost all assembly languages).

> Do you want to invest your time worrying about types or actually programming?

Another order reversal: type systems allow you to focus on programming, instead of hunting around for bugs because somebody 50 levels up the call stack passed you a value that doesn't support the interface it needs to support.

This is an endless debate of course, just wanted to throw in a typed pl fan's opinion in the mix.

>Another order reversal: type systems allow you to focus on programming, instead of hunting around for bugs

Except that is false. Bug prevalence is empirically orthogonal to type system.

See Xmonad

But this is in deployment software, i.e. I interpret your assertion as meaning "bug prevalence in software after it has been debugged is the same regardless of type system." My argument is that, at least for me, code becomes bug-free faster with static types than with dynamic, not that it ends up more bug-free in the end.

Are you saying that Xmonad is buggy? I never realized that, but I'm quite new to it. I'd think I've seen other window managers crash with similar amount of use, though.

Or are you saying that Xmonad is not buggy? But then I don't understand how it relates to empirical orthogonality at all.

Window managers crash often? I can't think of the last time I saw one do so.

I presume when you exclaim "type-theoretic monstrosities" I presumes you have some specific language in mind?

For example, in F# types maintain program correctness but get out of the way. They're not about obstinate bureaucracy but a way for the compiler to remind me "dude, this is not doing what you earlier specified it should do" and then I observe that yes, I've forgotten some corner case, do a small modification to the type definition and the whole damn thing works.

If types are getting in the way then the language is not very good (by my definition C++ is not very good and I mostly earn my living writing it).

Worrying about type is programming.

When the type is right, the implementation is trivial.

Type-theoretic monstrosities point towards incomprehension of the problem.

Tackling two problems is a triviality, an engineer worries about more.

A modern language does not hide the machine code, but abstracts it.

A type cannot be abstracted, a type is the abstraction.

Types are not for efficiency of programmer or machine, they're for correctness. They're a form of test that can be run statically on the program. And unlike tests, they potentially offer a proof that some kinds of error cannot occur.

Without types you end up with a different sort of monstrosity - the corner cases that you get when comparing ints to strings in Javascript, for example.

That's a bad example, as it has really nothing to do with types, but instead the semantics of the coercion-implicit equality operator (==) vs the strict equality operator (===). Javascript has types, they are just dynamic, tied to values, not variables.

I don't think it's such a bad example. In a strongly typed language, it would be relatively difficult to 'type' the '==' operator which would be reflected by its horrific signature. The '===' operator, especially in language supporting type classes, would instead be relatively easy to define. The type indicates whether a concept, which might seem simple, is complex.

However, where static languages are lacking is in supplying proof of the rules associated with these operators. In the case of equality, that would be associativity, reflexivity and transitivity.

I think fiddling around with types is attractive to academic researchers because types are relatively easy to reason about mathematically. It's a lot easier to convince others (and possibly yourself) that you're "doing science" if your paper is full of math or math-like constructs.

The factors that make Python, Ruby, Javascript, etc. popular aren't nearly as amenable to formal mathematical analysis.

Worrying about types means thinking about issues that matter to the success of your program, whether or not your language makes you do it.

If you're struggling with your language's type system instead of leaning on it and using it as a tool to help you express when you write, you're doing it wrong. Or maybe your language has sh#tty type system.

On the other hand, do you want your code to have to deal with any object or type from anywhere in the world or actually programming?

Programming is inherently the art of making something specific to a use. Types help that in that you limit what the code operates on, which makes the code you write simpler, because you have less ambiguity.