Second-Order Unification and Type Inference for Church-Style Polymorphism

Abstract

We present a proof of the undecidability of type inference for the Church-style system F --- an abstraction of polymorphism. A natural reduction from the second-order unification problem to type inference leads to strong restriction on instances --- arguments of variables cannot contain variables. This requires another proof of the undecidability of the second-order unification since known results use variables in arguments of other variables. Moreover, our proof uses elementary techniques, which is important from the methodological point of view, because Goldfarb's proof [Gol81] highly relies on the undecidability of the tenth Hilbert's problem. 1 1 Introduction The Church-style system F was independently introduced by Girard [Gir72] and Reynolds [Rey74] as an extension of the simply-typed -calculus a type system introduced of H. B. Curry [Cur69]. As usual for type systems, the decidability of so called sequent decision problems was considered. A sequent decision problem in some ty...