September 18, 2025
Recent research has demonstrated the effectiveness of extending the Hindley-Milner (HM) type system with Boolean kinds to support type inference for a wide variety of features. However, the means to support classic type system provisions such as local let generalization and polymorphic recursion is either limited or unknown for such extensions. This talk introduces procedures for equational generalization and semiunification in arbitrary varieties of primal algebras (including Boolean algebras, rings of prime characteristic, Post algebras, etc.), enabling complete and principal let generalization and polymorphic recursion in Boolean-kinded type systems and their generalizations. Additionally, a method to minimize the number of instantiated type variables in such kinds is developed. Boolean-kinded HM extensions are exemplified with a type system for nullable references, and the way in which said procedures are used to support let generalization and polymorphic recursion is outlined.
About Joseph Zullo
Joseph Zullo is a 5th year ECE PhD student at Purdue University, looking for a new advisor to guide his thesis research. He holds degrees in CS and ECE from Cornell University. As of late, he studies how equational unification and related symbolic techniques enable complete and principal type inference for various programming language features.