Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems

Explore a groundbreaking 18-minute conference talk from OOPSLA2 2023 that delves into a novel hybrid algorithm for solving Boolean unification queries in Hindley-Milner-style type and effect systems. Discover how researchers from Aarhus University and the University of Copenhagen have developed a fast and efficient approach based on Boole's Successive Variable Elimination (SVE) algorithm. Learn about key observations in Boolean unification queries encountered in practice and how they are exploited to implement various strategies for formula minimization. Examine the implementation of this new hybrid approach in the Flix programming language and its impressive results, including a 1.8x speed-up in compilation throughput and minimal overhead on type and effect inference time. Gain insights into the design choices that contribute to improved performance and understand the potential impact on more expressive type and effect systems.