Type inference with recursive type equations

Abstract

This paper discusses decidability and existence of principal types in type assignment systems for λ-terms in which types are considered modulo an equivalence relation induced by a set of type equations. There are two interesting ways of defining such equivalence, an initial and a final one. A suitable transformation will allow to treat both in an uniform way.