[chriswarbo]

PS: Static type inference, like your example of (symbol-name x) and (cos x), has been going on for at least 40 years, since ML. The article mentions, Ocaml, which is a descendent of ML and hence has full type inference (you can leave out all annotations and the type-checker will figure them out). Depending on the type system, this may or may not be possible. For example types in Agda, Coq and Idris are full programs, so inferring them is undecidable.

Since dynamic languages only have one static type, static type inference is trivial. So is type-safety: there's no way to cast a value of one type to an incompatible type, since there are no other types.

Inferring tags doesn't work in general: when I say `print x` it doesn't mean that `x` must be a string; I might want Python to raise a "TypeError" exception, so that I can jump to the handler where all the real work takes place. Of course that's bad practice, but exceptions are only "errors" by convention; in the same way that False is only a failure by convention.