3 ms·

>On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting

>On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-) Any type system will reject some correct program. As a trivial example, consider: if( f() ): 1 + "a" else 1 This is a perfectly fine expression iff the result of f() is always false.

georgewsinger 9y ago
Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").
- gizmo686 9y ago
  Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case. Or consider a program like: x = 1 print_int(x) x="a" print_string(x) I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify. Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it). You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior. A completely different type of example, is C code such as: *0x01 = 0 which means "set the memory at address 1 to 0", but is poorly typed.
  - zem 9y ago
    for the case of x = 1 print_int(x) x="a" print_string(x) the type system could simply instantiate a new variable, x: string, that shadowed the old x: int. this is perfectly valid ocaml, for instance: let x = 1 in Printf.printf "%d\n" (x + 1); let x = "hello" in print_endline (x ^ " world")
    - gizmo686 9y ago
      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.
- rocqua 9y ago
  At this point, you start hitting a problem from fundamental computation. When are 2 programs equivalent? Is it when they behave equivalently in any implementation or is it when there is a chain of rewriting rules that change one to the other. The issue with the first definition is 2-fold. What set of implementations are you qualifying over, and what to do with weird programs that crash occasionally. This is similar to what happens in the given example. The program is equivalent to 'return 1' when f is always false. Otherwise, it might crash. In the second definition, 'return 1' and the given program are just different programs, until you actually substitute an f and continue reduction.
ufo 9y ago
I think the argument for untyped languages is their simplicity. There are lots of things that are trivial to express in a dynamic language but that require extra features on the type system to be able to write on a statically typed language (parametric polymorphism, subtype polymorphism, datatype introspection, and so on). Sure, there are type systems for all of these things but it is hard to have a single type system that does everything at once because things quickly become very complicated and type inference gets harder.

georgewsinger 9y ago

Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").

gizmo686 9y ago
Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case. Or consider a program like: x = 1 print_int(x) x="a" print_string(x) I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify. Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it). You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior. A completely different type of example, is C code such as: *0x01 = 0 which means "set the memory at address 1 to 0", but is poorly typed.
- zem 9y ago
  for the case of x = 1 print_int(x) x="a" print_string(x) the type system could simply instantiate a new variable, x: string, that shadowed the old x: int. this is perfectly valid ocaml, for instance: let x = 1 in Printf.printf "%d\n" (x + 1); let x = "hello" in print_endline (x ^ " world")
  - gizmo686 9y ago
    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.
rocqua 9y ago
At this point, you start hitting a problem from fundamental computation. When are 2 programs equivalent? Is it when they behave equivalently in any implementation or is it when there is a chain of rewriting rules that change one to the other. The issue with the first definition is 2-fold. What set of implementations are you qualifying over, and what to do with weird programs that crash occasionally. This is similar to what happens in the given example. The program is equivalent to 'return 1' when f is always false. Otherwise, it might crash. In the second definition, 'return 1' and the given program are just different programs, until you actually substitute an f and continue reduction.

ufo 9y ago

I think the argument for untyped languages is their simplicity. There are lots of things that are trivial to express in a dynamic language but that require extra features on the type system to be able to write on a statically typed language (parametric polymorphism, subtype polymorphism, datatype introspection, and so on). Sure, there are type systems for all of these things but it is hard to have a single type system that does everything at once because things quickly become very complicated and type inference gets harder.