1) It depends on the particular type system, for some of them (Standard ML) it is decidable, but the compiter does not terminate in any practically reasonable time/space, so it still "loops" in practice;
2) It is not clear whether one can covert a magic instant solver of the halting problem (a "Turing oracle") into a practical solver for the actual outcome of the type inference (since the termination can be of two types: "validated" and "error found").
***************************************
There is also the third type of possible eqiuvalence here, which is also not clear. The question is, given an oracle solving system F, can we obtain the solution of halting problem (without specific complexity constraints)? I don't know the answer to that either..
no subject
So what I wrote in my answer to Cema, is that
1) It depends on the particular type system, for some of them (Standard ML) it is decidable, but the compiter does not terminate in any practically reasonable time/space, so it still "loops" in practice;
2) It is not clear whether one can covert a magic instant solver of the halting problem (a "Turing oracle") into a practical solver for the actual outcome of the type inference (since the termination can be of two types: "validated" and "error found").
***************************************
There is also the third type of possible eqiuvalence here, which is also not clear. The question is, given an oracle solving system F, can we obtain the solution of halting problem (without specific complexity constraints)? I don't know the answer to that either..