On: Where Do Type Systems Come From?

[gizmo686]

>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 → gizmo686]

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

[rocqua → georgewsinger]

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.

[gizmo686 → georgewsinger]

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.

[heavenlyblue → gizmo686]

    "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). Or by a more general concept that is available outside functional languages, SSA (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.

[z3t4 → heavenlyblue]

the real world is not strictly typed, i think types are for the compiler rather then humans. Im however a big fan of runtime bound checking so that the program always have a sane state.

[wz1000 → gizmo686]

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

You can encode this quite easily in a language with a dependent types.

[zem → gizmo686]

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 → zem]

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

[zem → gizmo686]

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 → zem]

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 → gizmo686]

    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.

[ufo → gizmo686]

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.