Type inference with recursive types: Syntax and semantics

AbstractIn this paper we study type inference systems for λ-calculus with a recursion operator over types. The main syntactical properties, notably the existence of principal type schemes, are proved to hold when recursive types are viewed as finite notations for infinite (regular) type expressions representing their infinite unfoldings. Exploiting the approximation structure of a model for the untyped language of terms, types are interpreted as limits of sequences of their approximations. We show that the interpretation is essentially unique and that two types have equal interpretation if and only if their infinite unfoldings are identical. Finally, a completeness theorem is proved to hold w.r.t. the specific model we consider for a natural (infinitary) extension of the type inference system