The Unreasonable Effectiveness of Dynamic Typing for Practical Programs [video]

He admits that the papers he cites are too few to make large decisions and that the analysis he does by looking at how many issues on GitHub are actually caused by type system errors (1-5%) but he's trying to steer away from dogmatism in favor of empirical evidence.

It's an interesting theory. On the other hand, the amount of time and money lost to null pointer bugs over the years suggests that we still aren't careful enough.

You could use that reasoning to argue we should be writing in assembly. I want all the automated checks I can get to get as close to bug free as possible. If you have to be careful about everything, you're going to exhaust yourself and miss even more bugs. It's much better when bugs are limited to smaller areas and you know where to be extra careful.

Having to be careful because there's no type system checking your work is a useful skill to learn in some contexts, but I think the current state of the software industry is a pretty good argument that human programmers will never be careful enough. So, we should do what we can to accommodate human fallibility and use machines to check our work early and often.

However, funding the development is sometimes harder than funding the maintenance: You need the system to operate in the first place in order to get the benefits/money/revenue/etc.

Once the system is in place and brings benefits, it is easier to fund further investment on the system, be it maintenance, extension,etc.

From my personal experience, the completeness and quality of the tests has much more impact on maintainability than the static-ness of your language. But to be fair, I haven't seen a study proving this either.

[0] http://haskell.cs.yale.edu/wp-content/uploads/2011/03/Haskel...

My own experiences learning Haskell after working Python for more than 10 years suggests this is quite plausible.

Do you identify that problem in this specific video?

"Strong typing" is itself loaded. There is a definition of "strong typing" which means "no conversions occur between types without programmer requests". For instance, under this notion, a language in which we cannot use an integer expression in a floating-point context without putting in an integer-to-float coercion is more strongly typed than one in which the conversion is inferred and takes place implicitly.

"Strong typing" has been used in reference to the facility, as in the Pascal family, for declaring type alias names for identical types (such as integers) such that the aliases are considered distinct types. The C typedef mechanism is weakly typed because a mode_t and pid_t, both perhaps just aliases for int, are considered to be indistiguishable from int and compatible. C++ has more strongly typed enum types than C, because a location of some enum type in C++ cannot be assigned a value of an integer type, or of a different enum type, without a cast.

Sometimes "strong typing" means that there are no holes in the type system: no datum is being misused if there are no diagnostics about type. (This is related to the other senses of "strong typing" because if an implicit conversion is allowed in a program which is free of type diagnostics, that conversion could be unsafe and hide a software defect. The type system knows very well that here there is an expression of real type and the context requires a integer value and silently generates the conversion; but what if it is out of range? In, C, the behavior of an out of range floating to integer conversion, and vice versa, is undefined.)

> Static typing requests you to explicitly declare types.

Not in anything that can be called state-of-the-art static typing, except at module boundaries (where the compiler cannot always infer parameter or return types since some of the information is in another module that it doesn't know about).

Types can be inferred implicitly from basic terms in the program syntax tree whose type information is known (like literal operands, standard functions and operators and such) and then from there by inference (which can also go in the other direction, like from known function parameters to unknown terms nested inside the function). https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...

A concern Smallshire spesifically addresses in the talk, pointing out the correct distinctions.

Normally it's hard to tell when somebody hasn't read before commenting, but given that a non-trivial portion of this talk is explicitly laying out the different facets of type systems and doing compare-and-contrast analysis, it's really obvious that your reply was written without watching.

https://news.ycombinator.com/item?id=15083003

As chriswarbo said:

> One reason for this is the tight coupling in developers' minds between what I'd call "types" and "representations" (these terms are very overloaded, so others may use them in different ways).

> Just because, say, a function name and a string are represented in memory the same way, that doesn't mean they are the same type; in particular there are many strings which aren't function names, and there are many operations (e.g. append) which make sense for strings but not for function names.

This is a well-known problem, called 'stringly typing': The language is enforcing the type system it knows about, but it only knows the representation of values, not the semantics, not what it is valid to do to them at a high level. Therefore, you can defeat the type system entirely by just passing everything as strings.

I brought up the idea of having layers of representation:

> Length is a type of value, whether it's expressed in inches or centimeters or light-seconds is a representation, and whether it's in ints or floats or strings is another layer to the representation. You can add inches to centimeters with the right conversion, much like you can add numerical values represented ints and strings with the right conversions. The conversions just have to be at the right layer of representation.

This, to my mind, means that autoconversion is orthogonal to strong typing, in that it preserves the type system if it's done in a way which converts between different representations of values with the same (or compatible) semantics. Of course, if your type system is focused entirely or almost entirely on representations, autoconversion defeats it totally.

Finally, the little historical note:

> Your ideas sound a lot like the original Hungarian notation, BTW: If your language-level types are representations (as in, your type system says int and float, as opposed to semantic notions like pixels-from-edge or alpha-percentage) you can encode the real type information in variable names. People mutilated this to encoding language-level type information in variable names, which is utterly pointless and potentially harmful.

You are confusing explicit typing with static typing. "Static" means "compile-time checking". "Dynamic" means "defer checks to run-time". Some language implementations can disable run-time type checking if optional type annotations are added, such as in Typed Racket.

In other words, all the following combinations are possible:

  - Implicit + dynamic + strong: Python
  - Implicit + dynamic + weak: JavaScript
  - Implicit + static + strong: Standard ML without type annotations
  - Explicit + dynamic + strong: Elixir with type annotations
  - Explicit + static + strong: Java
  - Explicit + static + weak: C

  - Implicit + static + weak
  - Explicit + dynamic + weak

Static types prove the absence of some errors.

Any type snob will tell you that even in supposedly good type systems, without dependent types, all lists are dynamic! Yet most of us that swear by static types don't use dependent types (much). There might be a limit where "more types" don't pay off their added cost relative to the thinking and typing needed and the security gained. Where that limit is depends on the application. Formally verified programs aren't used for many simple web backends - for good reason.

Also, type systems aren't equal. There are decent dynamic ones and terrible ones. Same goes for static type systems.

Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first.

On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :)

To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it.

On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.

Your fallacy is saying: there is a whole class of errors that can avoided if only we use a different type system, so there is no point in using that type system which defers (some or all) checks at runtime.

I can write code that manipulates values which represent types in the language, at runtime. If the types happen to be known or declared during compilation, fine enough, they can be optimized away. Otherwise, they will be checked later (which transparently invokes dynamic dispatch if needed), and I can even use them once they are known to compile the code myself, on a closure; there, along with other values which are then known, they can be taken into account to perform more aggressive optimizations. Why don't all language provide this?

As for bugs or errors, if you cannot lower risks (with static guarantees) then you have to improve on fault tolerance. You take other approaches to ensure the system behaves well, even if some parts can fail (e.g. Erlang).

To be honest, I really don't understand what the benefit of dynamic types are supposed to be. People say it's easier and less hassle to get something up and running because you don't need type annotations but this isn't an issue with decent type inference and all you're doing is replacing compile time checks with runtime crashes.

Do you have any data to back this up or have links to papers that try and do a better job of counting issues that statically typed languages catch?

When you're re-coding all the time, the upfront cost isn't amortized over future runs as much as it used to be. Libraries are, but the massive real-world crowd-testing (i.e. usage) catches them...

BTW I really like units of measure types, you get dimensional analysis almost for free. You can do it in e.g. java but it's verbose (i.e. it's java). Classes, with arithmetic methods (add, sub, mult etc), You need an ezplicit class for each unit combination (though you can do a little better with generics). And get compile-time type errors when you assign, compare or operate incorrectly.

Ok, so you are writing an algorithm for a fast approximation of ATANH using IEEE floating point standard.

In type: IEEE floating point number Out type: the same.

Tell me how the magical type checking of the excellent programming language you propose will ensure that my calculations are correct.