When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism

Explore a groundbreaking 22-minute conference talk from POPL 2024 that introduces a novel type inference approach for first-class polymorphism. Delve into the world of multi-bounded polymorphism and its application in resolving long-standing challenges in type inference for System F-like languages. Learn about F{≤}, a declarative type system derived from implicit coercions theory, and SuperF, a new algorithm for inferring polymorphic multi-bounded F{≤} types. Discover how this approach significantly advances the state of the art in type inference for general-purpose programming languages, offering solutions to problems that have puzzled researchers for decades. Gain insights into the recursion-avoiding heuristic used to guarantee termination of type inference and its practical implications. Presented by researchers from Hong Kong University of Science and Technology and EPFL, this talk showcases cutting-edge research in programming language theory and type systems.