1. 28
  1. 3

    I was curious what the practical implications of having an undecidable type system are. Apparently, it means you can make a program that makes the compiler crash during type checking: https://bugs.openjdk.java.net/browse/JDK-6558545

    1. 4

      I don’t think that’s a requirement. It can also mean that the type checker can go into an infinite loop (without crashing).

      1. 3

        The compiler crashing is rather a side-effect of the underlying undecidability.

        Concretely, undecidability means that there is no universal algorithm which, given a candidate Java program to compile, correctly terminates within some finite time (dependent on the input length), i.e. it may loop infinitely for some programs. It may also require infinite computing resources, such as stack space in this instance, which leads to the compiler crashing. But as @munksgaard correctly said, it can also “just” loop infintely.

        1. 3

          Practically, there is none. As soon as compilation takes too long, you’ll cancel it and rewrite the code anyway.

          1. 1

            I agree with @munksgaard and @bfieldler, crashing during type checking is just one way in which the undecidability can show.