undefined | Better HN

0 pointsgeorgewsinger8y ago0 comments

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

0 comments

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.

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

heavenlyblue8y ago

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

z3t48y ago

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.

wz10008y ago

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

zem8y 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")

gizmo6868y ago

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

1 more reply

j / k navigate · click thread line to collapse

0 comments

rocqua8y ago

In the second definition, 'return 1' and the given program are just different programs, until you actually substitute an f and continue reduction.

gizmo6868y ago

Or consider a program like:

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

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.

heavenlyblue8y ago

    "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)

z3t48y ago

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.

wz10008y ago

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

zem8y 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")

gizmo6868y ago

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

1 more reply

j / k navigate · click thread line to collapse