"f(x) + g(x)" This example is way too trivial to explain why type systems are generally undecidable. Let's imagine: def f/g(x): if isinstance(x, str

"f(x) + g(x)" This example is way too trivial to explain why type systems are generally undecidable. Let's imagine: def f/g(x): if isinstance(x, str): return 6 elif isinstance(x, int): return 'a' It is decidable for any type of x that is previously known. More importantly, type systems were essentially created to be able to prove whether a given expression is decidable or not. x = 1 print_int(x) x="a" print_string(x) This is solved by A-normal form (https://en.wikipedia.org/wiki/A-normal_form https://en.wikipedia.org/wiki/A-normal_form). Or by a more general concept that is available outside functional languages, SSA (https://en.wikipedia.org/wiki/Static_single_assignment_form https://en.wikipedia.org/wiki/Static_single_assignment_form). You can make a point that this code is hard to modify in dynamic languages, but it is an issue with the code style rather than type systems. For example - IntelliJ IDEA would highlight such Pythonic code as incorrectly typed, since you have changed the type and therefore the variable itself. I find the general argument against complexities in the type systems such as Haskell to be quite amusing, to be fair. Most of the time you are not dealing with code that is undecidable - and that's why type systems are interesting.