Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
summary
Presents a hybrid solver that combines Boole’s SVE elimination with binary decision diagrams plus precomputed tabling and caching; implemented in the Flix compiler and tuned with special-case handlers and a QMC step to turn BDDs back into small formulas. Analysis of ~50,000 unification queries shows only 380 syntactic (89 semantic) forms, most with ≤4 vars. Result: compilation throughput rises from 8,580 to 15,917 lines/sec (1.8×) and Boolean unification costs fall to <7% of total compile time.
AI-written summary · about
chapters (12)
- 0:00Effect systems and BU unification
- 1:03Boolean formulas in Flix
- 2:26Performance in Boolean unification
- 3:51BU algorithms and complexity
- 5:35Query structure in Flix
- 7:40Optimization strategies
- 8:22Switching to BDDs
- 9:02Hybrid BDDs and tabling
- 11:33Lessons for compiler builders
- 12:57Open questions and future work
- 13:39Flix effect system
- 14:47Q&A
related talks
16mPolymorphic Types and Effects with Boolean Unification
15mQualified Types with Boolean Algebras
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
59mUnification Modulo Equational Theories in Languages with Binding Operators
21mVerifying term graph optimizations using Isabelle/HOL
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
30mA Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification