Fall 2021 CSE Departmental Seminar: Principal Type Inference for Object-Oriented Programming in a Boolean Algebra of Types
Abstract
What would TypeScript look like if it had been designed with type inference and soundness in mind? We provide one possible answer in MLscript, an object-oriented and functional programming language with records, generic classes, first-class unions and intersections, instance matching, and ML-style principal type inference. We define the constructs of our language using union, intersection, and complement (or negation) connectives, making sure they form a Boolean algebra, and add enough structure to derive a sound and complete type inference algorithm. With this work, we aim to disprove a long-held belief that principal type inference is not feasible for object- oriented programming languages with expressive subtyping systems. Thereby, we hope to encourage and help the implementation of better type inference for functional and object-oriented languages.
I gave a Departmental Seminar at the CSE department in November 2021 on the MLscript language developed by my group.
