Lazy BDDs with eager literal differences

José Valim details new optimizations to Elixir's set-theoretic type system targeting difference operations in lazy BDDs (Binary Decision Diagrams). With Elixir v1.20.0-rc.2 introducing clause-type propagation and redundant clause detection, the number of type difference computations increased significantly, causing compilation slowdowns in modules with 1000+ clauses. The post derives new mathematical formulas for eager literal differences — both when a literal appears on the left or right side of a difference — and introduces a 'one field difference' optimization for structs where only a single field type differs. These optimizations, shipping in v1.20.0-rc4, reduced compilation from dozens of seconds to milliseconds for affected projects. Claude Opus 4.6 is credited with suggesting a key algebraic simplification.