if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them.
Are you sure this is true in a meaningful way? You can always simply run the type checker at run-time, and this is indeed where statically typed languages are heading, but e.g. phantom types, and runST style tricks are areas where the embedding into a dynamically typed language is, at the very least, not trivial.
true, meaningful, yes; you'd still not be able to access ST references in the wrong thread, but in a purely dynamically typed language, you will only find out about problems in that area while the thread is already in the middle of its run. runST alone does not give transaction semantics. but it is also true that being able to isolate whole sub-programs at once, so that their type-checks are done before they are being run, and no type-checks are done while those sub-programs are run, is more than just an optimisation. it is a question of being able to express certain type-check-level transaction constraints: either the whole sub-program can be shown to run without type-errors or no part of the sub-program is permitted to run. (being able to fit a whole program into a single such type-level transaction is a special case, which we call static typing) see also apfelmus' message, which raised the same point, and my reply. that exchange reminded me that dynamic/typecase is not only a necessary addition to otherwise static typing, but also enables a very desirable addition to otherwise dynamic typing. the idea being that by default, all typing should be static, unless explicitly specified otherwise by use of dynamic/typecase. in other words, dynamic typing has to be made explicit, and is only used were static typing is not expressive enough; the majority of code consists of statically typed fragments enjoying the type-level transaction property; entry into such a fragment is protected by a dynamic type check, exit from such a fragment might reconstruct dynamic type information. claus