The Undecidability of System F Typability and Type Checking for Reductionists

摘要

The undecidability of both typability and type checking for System F (polymorphic lambda-calculus) was established by Wells in the 1990s. For type checking Wells gave an astonishingly simple reduction from semi-unification (first-order unification combined with first-order matching). For typability Wells developed an intricate calculus to control the shape of type assumptions across type derivations via term structure. This calculus of invariant type assumptions allows for a reduction from type checking to typability. Unfortunately, this approach relies on heavy machinery that complicates surveyability of the overall argument.The present work gives comparatively simple, direct reduction from semi-unification to System F typability. The key observation is as follows: in the existential setting of typability, it suffices to consider some specific (but not all, as for invariant type assumptions) type derivations. Additionally, the particular result requires only to consider closed types without nested quantification.The undecidability of type checking is obtained via a folklore reduction from typability.Profiting from its smaller footprint, correctness of the new approach is witnessed by a mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. For free, the library provides constructive, mechanically verified many-one reductions from Turing machine halting to both System F typability and System F type checking.