[Drup]

This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.

[yogthos]

A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking.

There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system.

One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map.

[1] https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...

[aidenn0]

Static typing does not prevent this; the fact that static typed languages can parse freeform formats like JSON works as a simple example.

If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.

[yogthos]

You don't know what the keys are up front because each library is an independent module. Of course, you could just use Any type, but then you're not doing static typing.

[aidenn0]

Example:

Module X expects the "foo" key, then write a function that checks if it has the foo key and returns a type Maybe(HasFoo). It's less good than just treating the type as the union of HasFoo and HasBar or whatever, but if you fully decouple, then you have to be able to handle the case in which the mapping lacks a foo key anyways, and this will statically froce you to.

[yogthos]

But the point is that you don't know the totality of the keys up front. Module A might deal with keys X and Y, while module B deals with keys W and Z. These two modules know absolutely nothing about each other and they're developed by different people.

[aidenn0]

Right, so Module A defines a "TypeA" (which describes a map containing keys X and Y) and Module B defines a "TypeB" (which describes a map containing keys W and Z) and they each define their respective functions that return a (Maybe Type A) and (Maybe Type B). If the map has keys X and Y then you will get a (Just Type A) and if it does not you will get (Nothing). The type system will then enforce that you handle the possibility of (Nothing) which is something you would need to do in a dynamically typed language as well.

Remember, in the sense we are currently talking about[1], objects are untyped, it's variables that are typed. So there is no need to describe the type of this map that is passing around in concrete terms; it's perfectly cromulent to treat the map as a TypeA in one place and a TypeB in another place, so long as you ensure that the prerequisites for those types are satisfied by the object.

It is true that it is usually preferable in statically typed languages to demonstrate that the map satisfies the requirements for TypeA before type erasure (i.e. at compile time), but if you want total decoupling, then that is not possible (since the requirement that the map have keys X and Y would need to be enforced outside of Module A). This does not mean that a type system cannot help you though.

I think we are getting to the limits of what can be easily communicated via HN comments, so if you still don't understand, then perhaps I'll write a blog article explaining it more fully.