Improvements to Set-Theoretic Types in Elixir Using Lazy BDDs

The Elixir team, in collaboration with CNRS, has been advancing a set-theoretic type system that utilizes unions, intersections, and negations. The article delves into the previous versions that used Disjunctive Normal Forms (DNFs) to represent types and the inefficiencies encountered as type complexities grew with the addition of features in Elixir v1.19, specifically regarding anonymous function type inference. To address these inefficiencies, the team shifted to Binary Decision Diagrams (BDDs), which optimize set-theoretic operations through a structured tree representation, helping to reduce exponential blow-ups in type checks. However, the transition to BDDs introduced new challenges, particularly with the expensiveness of union operations. The introduction of lazy BDDs was proposed to mitigate these issues, allowing for more efficient treatment of type intersections and differences without reverting to poor performance seen in earlier structures. Eventually, new formulas were designed for both intersections and differences that preserved type operations efficiently, leading to improved performance in type checking for projects in Elixir v1.19 and future releases. The collaboration and efforts highlight the evolving landscape of type systems within dynamic programming languages.