[rbehrends]

No, there's more to it. There's been some research in recent years on the actual benefits of types and the results are less straightforward than some people think.

An important aspect of type annotations, for example, seems to be that they help document the API of a module, regardless of whether they're statically checked. This is especially relevant with respect to maintenance tasks.

Conversely, the benefits of static type checking to get correct code initially seem to be a lot murkier. There seems to be a cost associated with static types and that is that it takes longer to write code; time that can be spent in a dynamically typed language on other validation work (remember that types do not even remotely capture all software defects).

This means that it is definitely worth exploring the benefits of optional/gradual/soft typing vs. static typing and/or runtime type checking vs. compile-time type checking.

Conversely, the assumption that static types are an unalloyed good is not currently borne out by the evidence (in part, of course, that is because the evidence is inconclusive).

[adrianratnapala]

There seems to be a cost associated with static types and that is that it takes longer to write code;

But this is not the only cost that matters, indeed might not even be a cost.

I've gone from being neutral about static vs. dynamic types to being pro-static types -- and the change happened when maintenance became a bigger part of my job.

Writing new code is now far less important to me than looking at a small part of a large system and trying to understand what is and is a not possible at that point. Static typing does not make this easy, but dynamic typing makes it far more difficult.

[rbehrends]

> But this is not the only cost that matters, indeed might not even be a cost.

I'm not saying otherwise. My point is that there's no objective way to proclaim one better than the other. This depends on application domain, economic constraints, engineering constraints, what you're doing, and so forth.

Writing Ada software that controls a pacemaker has totally different requirements than exploratory programming in Jupyter that mostly deals with integers, floats, and arrays and matrices thereof, for example.

[adrianratnapala]

> I'm not saying otherwise. My point is that there's no objective way to proclaim one better than the other.

Very true. But any analysis that emphasizes writing code over maintaining it will systematically bias itself in favor of dynamic typing.

Interestingly I have had the converse debate with some of my colleagues, who have learned to hate Python because they keep having to debug existing systems. I try to tell them that it is an excellent language for the kind of one-off data-analysis that I did when I was a scientist.

They don't believe me, because here among software engineers, seemingly innocent 400 line scripts keep growing into giant, decade old, 100kloc typeless monstrosities.

[rbehrends]

> Very true. But any analysis that emphasizes writing code over maintaining it will systematically bias itself in favor of dynamic typing.

This is not what the studies do. There is no emphasis on anything. They look at how people do on a number of different tasks with different typing options and report the results.

Also, it's not just dynamic vs. static typing. Gradual and soft typing is also of interest, because it allows you to turn dynamically typed code into statically typed code without a complete rewrite.

[mathw]

Type annotations are brilliant for documentation, and it does matter if they're checked or not, because otherwise they're just comments, and we all know comments become wrong over time. If the compiler doesn't enforce your type annotations you can't trust them.

The sweet spot for me at the moment is a language which is fundamentally static but has good type inference so that you don't actually have to mention types all the time.

Haskell's pretty good at this, although because it's possible to write many Haskell programs without actually mentioning a single type anywhere it can be a pain to read the results. Rust deliberately constrained type inference so that you have to have type annotations on functions, which makes sure your interfaces don't get too murky when reading the code.

I'll go with the idea in another reply that static typing really starts to show its benefit in long-lived code bases under maintenance.

Certainly a static type checker makes refactoring a lot easier, in my experience.

[rbehrends]

> Type annotations are brilliant for documentation, and it does matter if they're checked or not, because otherwise they're just comments, and we all know comments become wrong over time. If the compiler doesn't enforce your type annotations you can't trust them.

Note that I wrote statically checked. You can also check them at runtime (basically as a form of Design by Contract), which is what Dart does at the moment.

[mathw]

You could, but why should you spend the cycles on that at runtime when you could've done it just once in the compile phase and errored out at a useful time instead of six weeks later when you hit the one branch you neglected to write unit tests for?

[rbehrends]

Because designing a type system that is sound and expressive and simple is bloody hard. Haskell frequently has a number of `{-# LANGUAGE ... #-}` directives at the top of source files, OCaml has acquired no less than six different ways of doing runtime polymorphism: as an extreme case, the module system has morphed into a fully functional OO system in addition to the one OCaml already has.

Runtime type checks allow you to greatly simplify the difficult parts of the type system or make it more expressive.

People often forget how many expressiveness shortcuts we take so that our type systems keep working out. We have integers (which are in actually practice often just elements of a finite ring), but introduce natural numbers and suddenly a lot of static type checks stop working out. How about interactions between the natural numbers with and without zero? Integers modulo your wordsize vs. infinite precision integers? Can you statically check overflow or underflow? Dart has both `num`, `int`, and `double` types, and `int` and `double` are subtypes of `num`, but `int` is not a subtype of `double`; readAsBytesSync() returns an `Uint8List` that conforms to `List<int>`. From a mathematician's perspective, computer science type systems are usually painfully simplistic. They usually capture something about the representation of the data, not its actual mathematical properties. Their role is often is to prevent undefined behavior, not to capture the actual semantics. Computer science typing often tends to be opportunistic rather than semantically oriented, based on what's easily possible rather than what one wants to express (see the entire family of covariance issues).

As an extreme example, consider GAP's [1] type system. We're dealing with computer algebra here, and some of the types simply cannot be captured at compile-time. Any type annotations would have to be checked at runtime, other than the trivial ones (and even integers are basically a subtype of the rationals or any polynomial ring with integer coefficients).

If I want to do effective implementations of matrices and vectors over finite fields, I pack several finite field elements into a machine word and extract them; no static type system in existence has even remotely the power to statically typecheck these operations for me, unless layered over a ton of unsafe code, and then only for some languages.

From the computer science side of things (I have a background in formal methods), type systems are underpowered specification languages that just pick a small subset of a formal spec that happens to be convenient to prove. They can express only a subset of program behavior (compare what types in even (say) Haskell do to a full-blown formal specification in Z) and often not even the interesting ones. As a result, I don't particularly stress out over whether checks only occur at compile time. Runtime type checking is simply a different tradeoff in that you move from the set of types that you can build a sound type system around to predicates that can be expressed at runtime. It's simply a different set of tradeoffs.

[1] http://www.gap-system.org/

[tome]

> There seems to be a cost associated with static types and that is that it takes longer to write code

Perhaps. As someone who has used Python and Haskell for roughly equal amounts of time in my professional career I definitely find Haskell faster to write in.

[baq]

mypy is getting good (from haskell's perspective that would be 'barely passable', still a great improvement from what it used to be), been using it actively for the last year and advocating it for 6 months and seeing nice ROI even considering it's warts.