Bidirectional Higher-Rank Polymorphism with Intersection and Union Types

Watch this 19-minute conference talk from POPL 2025 exploring bidirectional higher-rank polymorphic type inference with intersection and union types. Presented by researchers Shengyi Jiang, Chen Cui, and Bruno C. d. S. Oliveira from the University of Hong Kong, the talk addresses the theoretical foundations lacking in modern programming languages like TypeScript, Flow, and Scala when implementing bidirectional higher-rank polymorphic type inference with non-structural subtyping. Learn about their proposed type system with explicit type applications that demonstrates sound, complete, and decidable algorithms, helping identify which types can always be inferred. The presentation also covers practical variants for handling records and inferring a broader class of types, with all results formally verified using the Coq proof assistant. Access the full paper and supplementary artifacts, which have been evaluated as reusable, to deepen your understanding of type inference implementations.