Partial polymorphic type inference and higher-order unification
Frank Pfenning · 1988
We show that the problem of partial type inference in the nth-order polymorphic λ-calculus is equivalent to nth-order unification. On the one hand, this means that partial type inference in polymorphic λ-calculi of order 2 or higher is undecidable. On the other hand, higher-order unification is often tractable in practice, and our translation entails a very useful algorithm for partial type inference in the ω-order polymorphic λ-calculus. We present an implementation in λProlog in full.