A Simple Algorithm and Proof for Type Inference¹

Article type: Research Article

Authors: Wand, Mitchell

Affiliations: College of Computer Science, Northeastern University, 360 Huntington Avenue, 161CN Boston, MA 02115, U.S.A.

Note: [1] This Material is based on work supported by the National Science Foundation under grant numbers MCS 8303325, MCS 8304567, and DCR 8605218.

Abstract: We present a simple proof of Hindley’s Theorem: that it is decidable whether a term of the untyped lambda calculus is the image under type-erasing of a term of the simply typed lambda calculus. The proof proceeds by a direct reduction to the unification problem for simple terms. This arrangement of the proof allows for easy extensibility to other type inference problems.

DOI: 10.3233/FI-1987-10202

Journal: Fundamenta Informaticae, vol. 10, no. 2, pp. 115-121, 1987