The advantages of static typing, simply stated

> And the correctness is limited only to certain properties of the program, that a given type system supports.

In case there are readers not familiar with the current state of things, you can pick solid languages today whose type systems support a LOT. It is completely fair (and good) to point out that this isn't a panacea, but it can significantly help.

You are right - in a tautalogical way - that type systems only catch type errors. However, in modern languages (including Haskell, Scala, as well as newer, more experimental languages like Idris), those type errors can be extremely powerful.

Many people assume that 'types' are simply primitives like Int and String, and that a type checker just makes sure you don't pass an Int to a function expecting String. However, it is possible to express far more powerful statements about your data using a good type system.

For example, you can express the idea of non-emptiness of a container, as mentioned in the article. Then you know that, say, taking the max element of a non-empty container is guaranteed to give you an element, whereas with a possibly-empty container you might not have any element at all, causing a null, or exception, or at least requiring an Optional type.

You can express safety properties such as a sanitized string vs. unsanitized. You can have a Sanitized type that can only be created by calling a sanitize function - which carefully escapes/handles any invalid characters - and then functions that might, say, pass a value into an SQL instruction can be typed to only take Sanitized strings. Now the representation in memory of Strings and Sanitized strings is identical, but by using different types and a certain set of allowed functions on those types, you can encode the invariant that a string cannot be inserted into an SQL query until it has been sanitized. Now your type checker can catch SQL insertion vulnerabilities for you. How's that for a type error?

I've dealt with dynamic typing vs static typing A LOT recently. In my experience static typing has a major complication that most programmers don't think about: datastructures. When you are dealing with a list in Python for example, you just throw whatever you are working with into that list. Whereas Java Generics and C++ Templates are very ugly because you can't just say "this is a list of stuff" you have to say "this is a list of a set of lists of ints". Not only is it ugly to write and read, it gets worse whenever you have any errors involving it. Ever seen a C++ compiler error message with templates involved? Other static languages like C don't even really try to deal with datastructures and just leave it up to the programmer to manually access the memory.

In Haskell you can generate a parser to a typed structure using library combinators and code generation:

    data DataMessage = DataMessage { company :: Text
                                   }
      deriving (Show)
    $(deriveJSON defaultOptions ''DataMessage)

    data DataList = DataList { _data :: [DataMessage]
                             }
      deriving (Show)
    $(deriveJSON defaultOptions { fieldLabelModifier = drop 1 } ''DataList)

Which will fail properly when the data is malformed and in the real-world is even shorter, because you can set your data-type to protocol naming conventions and share them throughout.

Then there isn't much bloat. You wrote your types and generated your way to parse them.

You could test with:

    main = do
        print (encode (DataMessage "some-company"))
        print (decode "{\"company\":\"some-company\"}" :: Maybe DataMessage)

        print (encode (DataList [DataMessage "c1", DataMessage "c2", DataMessage "c3"]))
        print (decode "{\"data\":[{\"company\":\"c1\"},{\"company\":\"c2\"}]}" :: Maybe DataList)

https://gist.github.com/b30f6f09a737dcc980e052b0f3d2a39e

"This is sort of a subtle point: when programming in a static language, you always have a choice about what information you encode in the types, and how you encode things. ... In a static language, you do always have the option of building a less typeful API, where less is enforced by the types, but it is often tempting to spend more time encoding things statically (and then proving things to the typechecker) than would be saved by avoidance of potential future bugs. With experience, you develop a good sense for what is worth tracking statically and what to keep dynamic, but newcomers to static languages can make bad tradeoffs here, which in turn contributes to needless complexity in the language’s library ecosystem. "

This is a very important point that I've rarely seen talked about explicitly though I think all programmers develop a tacit sense of it.