[tehnub]

He just did derive it from the halting problem. In words: It's impossible to statically check the type of a function that takes a program P as its input, and returns the integer 1 as its output if P halts, and returns the string "1" if it does not halt. It would require solving the halting problem, which is undecidable.

[phoneperson]

The theorems predate Turing's theorem. As for the halting problem, it is solvable with an oracle, unlike the incompleteness theorems.

[native_samples]

How does that follow? The input type would be vague, e.g. ByteArray or Program or something.

[tehnub]

It's the return type that isn't decidable. You can't statically check, in the arbitrary case, whether the function returns an int or a string.

[native_samples]

No, but that isn't required for a static type system. Most languages would just unify to the top type.

[tetha]

Yes, but it is not required that a type system has a singular top type. It is entirely valid for a type system to have any number of types which are not in any sub- or supertype relationship.

And once there are two types T1 and T2 which are neither subtypes, nor supertypes of each other, and 2 expressions A1 and A2 of types T1 and T2, and a statically undecideable expression p, then statically typing "if p then A else B" is a problem.

And yes, I agree: Most if not all practical type systems will not accept an if-else statement if they cannot unify both branches of the conditional into a single type. Which makes sense. Because you have to act on the result of the expression, and then it needs to have some common type.

But on a purely theoretical basis, it is entirely possible and valid to have an undecideable type system. Which, btw, happens for a lot of languages: https://3fx.ch/typing-is-hard.html . There are C++ programs which are provably impossible to type at compile time.

[tehnub]

Could you elaborate on that? It sounds like I may have an overly simplified understanding of the topic here—wouldn't be the first time.

[native_samples]

Static type systems don't imply fully dependent types. In Kotlin:

    sealed class Program
    class HaltingProgram : Program()
    class InfiniteProgram : Program()

    fun checkIsHalting(p: ByteArray) = if (halts(p)) HaltingProgram() else InfiniteProgram()

This program will type check just fine. The inferred return type will be Program because that's the nearest shared ancestor type of both possible return types. Good luck implementing the halts() function of course, but that's not the type system's problem.