Lazier Binary Decision Diagrams (BDDs) for set-theoretic types

The Elixir team optimized their set-theoretic type system by evolving from Disjunctive Normal Forms (DNFs) to Binary Decision Diagrams (BDDs), and ultimately to "lazier BDDs" with improved union handling. The original DNF implementation suffered from exponential blow-up during intersections, which became problematic when Elixir v1.19 introduced type inference for anonymous functions requiring negations. While standard BDDs addressed intersection performance, they introduced slowdowns with unions. The team developed enhanced formulas that preserve union nodes during intersections and differences, eliminating redundant computations and achieving faster type checking than previous versions.