# zbMATH — the first resource for mathematics

On the undecidability of partial polymorphic type reconstruction. (English) Zbl 0789.03017
Summary: We prove that partial type reconstruction for the pure polymorphic $$\lambda$$-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We show further that partial type reconstruction remains undecidable even in a very small predicative fragment of the polymorphic $$\lambda$$-calculus, which implies undecidability of partial type reconstruction for $$\lambda^{ML}$$ as introduced by Harper, Mitchell, and Moggi.

##### MSC:
 03B40 Combinatory logic and lambda calculus 03D35 Undecidability and degrees of sets of sentences