On: Where Do Type Systems Come From?

[heavenlyblue]

    f(x) + g(x)

For any type of x is enumerable. What that means is that for this specific expression, you can enumerate all of the types that x may take, and then enumerate all of the types that a function would return, given the types (if you can). You can then decide whether this expression is true or not.

Now it depends on the implementation of f and g. And type systems, in most of the practical cases - would be able to deal with this.

    x = 1
    print_int(x)
    x="a"
    print_string(x)

The second example is always decidable, if we agree that semantics of '=' are generally a question of equivalence.