It's perfectly possible to write a statically-typed language that looks exactly like Python or Perl or Ruby. It's just that nobody's done it yet.

So in the mean time, you have to pick between expressiveness and ease of development versus safety and speed. There's no concept in computer science that prevents us from having all four other than "it's hard and people are lazy".

Haskell and Go are good examples of good progress in this direction, though.

Really? You should definitely show us how.

I've been thinking about the issues of dynamic/static languages for a long time, and haven't yet thought of a unifying design (maybe I'm just stupid).

The big difference isn't type inference/dynamic type system, it's the difference between compile-time and run-time. In Go and Haskell, classes are compiled. In Python, classes are created at runtime, so if you wanted type-inference in such a language, it would have to be performed at runtime... Also, proper typing of OO languages is very complicated, see Scala (e.g. sometimes you want the function to return the type of this object, even when it is inherited...).

To be a statically type language you would need to throw the error at compile time.

How do you raise (or not raise) error of this code at compile time and still make it feel like dynamic type language?

    x = (rand() > 0.5) ? 42 : "42"
    y = x + 1;

The type of (+ 1) is Int -> Int

The type of y is Int

Because x is of type Int|String and it's passed to a function that can only operate on Int, the program fails to compile.

Python 3 added optional type annotations for function parameters and return types. Unfortunately, Python does not use these annotations for compile-time or run-time type checking. The annotations are just for documentation or tools that want to analyze the type attributes.