2013 IEEE 54th Annual Symposium on Foundations of Computer Science (1985)
Oct. 21, 1985 to Oct. 23, 1985
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SFCS.1985.44
Polymorphic type systems combine the reliability and efficiency of static type-checking with the flexibility of dynamic type checking. Unfortunately, such languages tend to be unwieldy unless they accommodate omission of much of the information necessary to perform type checking. The automatic inference of omitted type information has emerged as one of the fundamental new implementation problems of these languages. We show here that a natural formalization of the problem is undecidable. The proof is directly applicable to some practical situations, and provides a partial explanation of the difficulties encountered in other cases.
Hans-J. Boehm, "Partial polymorphic type inference is undecidable", 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, vol. 00, no. , pp. 339-345, 1985, doi:10.1109/SFCS.1985.44