3 ms·

You could, but that seems like a transformation of the program itself, not a feature of the type system.

zem 9y ago
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 9y ago
  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 9y ago
    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.

zem 9y ago

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 9y ago
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 9y ago
  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.