Hacker News new | ask | show | jobs
by tetha 1707 days ago
As I said, there are infinite possible programs that cannot be type checked statically. This is derived from the halting theorem trivially - lambda(p) = if p.halts() then A() else B().

However, the intersection of programs I encounter in practice with the number of programs that can be statically checked is rather large.
1 comments
phoneperson 1707 days ago
You are probably thinking of Gödel's incompleteness theorems. I do not think that you can trivially derive it from the halting problem.
link
tehnub 1707 days ago
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.
link
phoneperson 1707 days ago
The theorems predate Turing's theorem. As for the halting problem, it is solvable with an oracle, unlike the incompleteness theorems.
link
native_samples 1707 days ago
How does that follow? The input type would be vague, e.g. ByteArray or Program or something.
link
tehnub 1707 days ago
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.
link
native_samples 1707 days ago
No, but that isn't required for a static type system. Most languages would just unify to the top type.
link
tetha 1705 days ago
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.

link
tehnub 1706 days ago
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.
link