0

I understand that there are major technical differences between how a strongly typed language is compiled and how a type annotated language is compiled/transpiled.

But as a developer writing in a strongly typed language and a weakly typed language with type annotations feels pretty similar to me. I can't really articulate any differences.

What are the differences between working in a strongly typed language and a weakly typed language with type annotations from the developer's point of view?

I am primarily thinking about the examples C++ and JavaScript with TypeScript annotations.

1

Strong and weak typing have no universally agreed upon definition. So let's invent our own!

  • A stronger type system provides an automatic proof of (partial) correctness. Stronger type systems can prove more aspects of correctness. I can encode some aspects of correctness into the type system.

  • A weaker type system can detect some errors. This is just a kind of linting.

For example, let's consider a function declared with a type (string) -> int. What does this type declaration do or guarantee?

  • A weaker type system may be able to alert us when we call that function with a wrong type. However, there may be ways to circumvent this check, for example if we can locally disable the type checker, or if the function can be called from untyped code (like calling TypeScript from plain JavaScript). So the type system cannot guarantee that the argument will always be a string. If we need to ensure that, we will have to use runtime type checks as well.

  • A stronger type system guarantees that the function cannot be called with wrong types, so runtime checks are unnecessary.

No practical type system is clearly weak or strong. For example, C++ makes it possible to reinterpret values as a different type, which essentially allows you to circumvent any type checks. But as long as we don't do that, the language provides a very strong type system that can prove a huge amount of correctness properties at compile time, for example around object lifetimes.

But strong type systems are not always desirable: in order to prove certain properties, code that makes these proofs impossible must be ruled out. This limits how expressive the language can be. The classic example would be Pascal, which had a type system that could not deal with variable-length strings. As a more recent example, C++'s template system does not make it possible to express something like Java's generic interface methods without resorting to unsafe casts. A similar problem is in the current version of Go, which has a type system that makes it impossible to express generic higher-order functions like map() or filter().

Such scenarios happen frequently when a type system is bolted on to a dynamic language. E.g. Python's new type system currently cannot describe the type of callbacks with keyword arguments, and cannot describe Go-style interfaces – despite such semantics being common in untyped Python code.

Note that the choice of type system has little to do with whether a language is compiled or transpiled or interpreted. As long as there is some kind of static type system, there will be some kind of check that happens before running the code. This type check may not be necessary to run the code. For example, early C compilers (before structs worked like they do now) would not have needed any type checks.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.