>>40
yeah it was sloppy. Lemme try again.
Suppose for the sake of contradiction that we have the ability to always predict the type of a variable in a dynamic language. We will reach a contradiction by showing that the haling problem is decidable. Suppose that halts is a function that takes an algorithm as its input and will return true if A will halt, and false if A will not halt. Note that the halts function need not halt itself. Let A be an arbitrary algorithm. Define B to be the following:
function B()
if(halts(A))
a = "lol I'm a string"
else
a = 1337
end
print(a)
end
We can now implement a special Halts function, that will halt on all inputs:
function Halts(A)
function B()
if halts(A) then
a = "lol I'm a string"
else
a = 1337
end
print(a)
end
a_predicted_type = predict_type_when_printed(B, 'a')
if a_predicted_type == 'string' then
return true
else
return false
end
end
Halts will halt on all inputs, as the only routines it only calls the check_the_type function, which is assumed to be decidable. Halts correctly decides when algorithms will halt or not because halts correctly indicates when an algorithm will halt or not (or does it)***. So Halts is a solution to the halting problem which halts on all inputs, which implies that the halting problem is decidable, and we have reached a contradiction. Therefore the initial assumption that predicting a type of a variable in a language is decidable, must be false.
I think that would do it, although, *** what if halts(A) doesn't halt? Then its return value is not defined right? So what would be the behavior of the check_type function, when it is checking the type of a variable at a point in the algorithm that can never be reached? There's probably a better way of doing this.