Lazier Binary Decision Diagrams for set-theoretic types
9 days ago
- #Type Systems
- #BDDs
- #Elixir
- The Elixir team and CNRS are developing a set-theoretic type system for Elixir, utilizing unions, intersections, and negations.
- Disjunctive Normal Forms (DNFs) were initially used to represent types but led to exponential blow-ups in complexity, especially with negations.
- Binary Decision Diagrams (BDDs) were introduced to address DNF limitations, offering efficient representation of set-theoretic operations but introducing new slowdowns with unions.
- Lazy BDDs (or Ternary Decision Diagrams) were implemented to mitigate union-related slowdowns by introducing an 'uncertain' element for unions.
- Further optimizations led to 'Lazier BDDs,' preserving unions during intersections and differences, significantly improving performance.
- The new type system features in Elixir v1.19, including anonymous function type inference, now perform efficiently, with most projects type-checking faster than in v1.18.