>>14,15
Wow, what a bunch of word-baloney that misses the one all-important point: (a) static typechecking is a must for practical programming because of error-checking, documentation and low-level optimization, (b) type declarations are an extremely useful form of metadata (both to the compiler and the programmer) independent of machine representations and (c) subtyping is a terrible killer of type inference and is actually largely unuseful because it creates unnecessary entanglement.
And what you call "disjoint" types is actually a necessary ingredient in type expressivity. Being able to declare that a certain type is to be used ONLY in certain places is no less useful than being able to declare what these certain places are. Dynamic type-checking is a sorry excuse for the language not being expressive enough to delineate the disjointness of the types of all terms clearly enough.