The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems hig

The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems highly plausible, but without a proof, it would not surprise me to learn that such is impossible. Without a constructivist proof, it would not suprise me to learn that the existence of such a system is irrelevent (to applied computer science).