[zem]

the point is that just because two variables have the same name doesn't mean they are the same variable; you need a (name, scope) pair to fully disambiguate them. some languages have the scope of a name be the enclosing function, so that all references to x within a function body are the same x, and the type therefore attaches to (x, function). however that is not the only way to do it; in ocaml the let statement rebinding x introduces a new scope, so that (x, line 1..) is a genuinely different variable from (x, line 3..), and has a new type. you can even say something like

let x = string-of-int(x)

and the rhs will take the value of x (a well-typed integer variable from the previous scope, and the lhs will introduce a new x (a well-typed string variable) in the newly created scope.

this is an orthogonal thing to static/dynamic typing, incidentally; for instance in ruby you can say

    a = 10
    (3..5).each do |a|
      puts a
    end
    puts a

and you will get

  3
  4
  5
  10

the a within the do loop being a new variable that happened to have the same name as the a in the outer scope, but referring to a different actual variable.

[gizmo686]

Yes, my point is that the fact that "x" refers to two different variables is a feature of the language, not the type system.

[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.