Lazy BDDs with eager literal intersections

February 26, 2026 · by José Valim · in Internals

In a previous article, we discussed how Elixir changed its set-theoretic types representation from Disjunctive Normal Forms (DNFs) to Lazy Binary Decision Diagrams (Lazy BDDs).

In a nutshell, DNFs allow us to represent unions, intersections, and negations as a flat data structure:

(c1 and not d1) or (c2 and not d2) or (c3 and not d3) or ...

This meant that any operation between complex types was immediately flattened. For example, intersections of unions, such as (foo or bar) and (baz or bat), had to be immediately flatten into the cartesian production (foo and baz) or (foo and bat) or (bar and baz) or (bar and bat). Even worse, unions of differences could lead to exponential expansion.

Elixir v1.19 then introduced BDDs with lazy unions (in short, lazy BDDs). They are trees which allow us to represent set-theoretic operations of any arbitrary depth, without flattening them, while also detecting duplicate types. A lazy BDD has type

type lazy_bdd() = :top or :bottom or
  {type(), constrained :: lazy_bdd(), uncertain :: lazy_bdd(), dual :: lazy_bdd()}

where type() is the representation of the actual type. For example, if the type being represented is a tuple, type() would be a list of all elements in the tuple. In literature, type() is known as literal.

Throughout this article, we will use the following notation to represent lazy BDDs:

B = {a, C, U, D}

where B stands for BDD, a is the literal, C is constrained, U is uncertain, and D is dual. Semantically, the BDD above is the same as:

B = (a and C) or U or (not a and D)

Which means the following expression, where foo, bar, baz, and bat below represent types:

(foo and not (bar or (baz and bat))

will be stored as:

{foo,
 {bar, :bottom, :bottom,
  {baz, :bottom,
   {bat, :bottom, :bottom, :top}, :top}, :bottom, :bottom}

The conversion to lazy BDDs and a few optimizations we added to their formulation in literature allowed us to type check Elixir programs faster, despite Elixir v1.19 performing more type checks than v1.18!

However, when working on Elixir v1.20, which introduced type inference of all constructs, we noticed some of the downsides of lazy BDDs. This article explores these downsides and how we addressed them.

As with previous articles, we discuss implementation details of the type system. You don’t need to understand these internals to use the type system. Our goal is simply to document our progress and provide guidance for future maintainers and implementers. Let’s get started.

The trouble with laziness

As we described above, lazy BDDs allow us to represent set-theoretic operations at any depth. And while this is extremely useful for unions and differences, they offer a downside when it comes to intersections. For example, take this type:

(%Foo{} or %Bar{} or %Baz{} or %Bat{}) and %Bar{}

While we could store the above as a BDD, it is also clear that the above can only be equal to %Bar{}. In other words, if we resolve intersections eagerly, we will most likely reduce the tree size, speeding up all future operations! To do this, we need to compute the intersection between literal types (the first element of the BDD node), rather than intersections between BDDs. So we are naming these new optimizations eager literal intersections.

Eager literal intersections

Our goal is to apply intersections between literals as soon as possible as it helps us reduce the size of the tree whenever literal intersections are empty.

Take two BDDs:

B1 = {a1, C1, U1, D1}
B2 = {a2, C2, U2, D2}

And imagine there is a function that can compute the intersection between a1 and a2 (which is the intersection of literals, not BDDs). The optimization works as long as one of C1 or C2 are :top. In this case, let’s choose C2, so we have:

B1 = (a1 and C1) or U1 or (not a1 and D1)
B2 = a2 or U2 or (not a2 and D2)

The intersection of B1 and B2 can be computed as:

B1 and (a2 or U2 or (not a2 and D2))

Let’s distribute it:

(a2 and B1) or (U2 and B1) or ((not a2 and D2) and B1)

And expand the first B1:

(a2 and ((a1 and C1) or U1 or (not a1 and D1))) or
  (U2 and B1) or ((not a2 and D2) and B1)

And now let’s distribute a2 while reordering the arguments:

(((a1 and a2) and C1) or (a2 and U1) or ((a2 and D1) and not a1) or
  (U2 and B1) or ((not a2 and D2) and B1)

In the first term of the union, we have a1 and a2 as a literal intersection. If a1 and a2 is empty, then the whole C1 node can be eliminated.

Then we proceed recursively intersect a2 with every literal node in a2 and U1 and a2 and D1. And, if their literal nodes are empty, those subtrees are eliminated too. This allows us to dramatically cut down the size of tree! In our benchmarks, these optimizations allowed us to reduce type checking of a module from 10s to 25ms.

The remaining terms of the union are U2 and B1 and (not a2 and D2) and B1. If desired, we could apply the same eager literal intersection optimization to U2 and B1 (as long as the constrained part in either U2 or B1 are :top).

This optimization has worked quite well for us, but it is important to keep in mind since BDDs are ordered and the literal intersection may create a new literal value, this optimization must be applied semantically so we can recompute the position of intersected literals in the tree. We cannot apply it when we are already traversing the tree using the general lazy BDD formulas from the previous article.

Finally, note this optimization may eagerly reintroduce some of the complexity seen in DNFs if applied recursively. For instance, if you have (foo or bar) and (baz or bat), the recursive application of eager literal intersections will yield (foo and baz) or (foo and bat) or (bar and baz) or (bar and bat). If most of those intersections are eliminated, then applying eager literal intersections is still beneficial, but that may not always be the case.

To discuss exactly when these trade-offs may be problematic, let’s talk about open vs closed types.

Open vs closed types

Elixir’s type system can represent both open and closed maps. When you write:

user = %{name: "john", age: 42}

We are certain the map has keys :name and :age and only those keys. We say this map is closed, as it has no other keys, and it would have the type %{name: binary(), age: integer()}.

However, when you pattern match on it:

def can_drive?(%{age: age}) when is_integer(age) and age >= 18

Because pattern matching only validates the age key, a map given as argument may have other keys! Therefore, we say the map is open and it has the type %{..., age: integer()}. This type says the map may have any keys but we are sure the age is integer().

The trouble is that, when we are intersecting two maps, because the open map is very broad, their intersection rarely eliminate entries. For example, the intersection between %{..., age: integer()} and %{..., name: binary()} is the map %{..., name: binary(), age: integer()}.

So when we have to compute the intersection between (foo or bar) and (baz or bat) and foo, bar, baz, and bat are open maps with different keys, then it will generate a cartesian product of all combinations! However, if they were closed maps, the end result would be empty. For this reason, we recommend applying the eager literal intersection only when the intersection will often lead to empty types.

Optimizing differences

The difference between B1 \ B2 can always be expressed as the intersection between B1 and not B2, which is precisely how we write differences in Elixir.

Now take the following type:

{:ok, integer()} and not {:error, integer()}

Currently, both ok-type and error-type are stored as nodes in the BDD. However, it is clear in the example above the types are disjoint and the result is {:ok, integer()}.

If we know the literals a1 and a2 are disjoint (their intersection is empty), then it is likely we can avoid adding nodes to the tree.

Furthermore, imagine this type:

{:ok, integer()} and not (not {:error, integer()})

The difference will convert the negation into a positive, resulting in {:ok, integer()} and {:error, integer()}, which is empty. Therefore, if B2 contains negations (which means its D2 component is not bottom), then we can also apply the eager literal intersection optimization from the previous section.

We will explore both scenarios next, starting with the one where D2 is bottom.

When D2 is bottom

We start B1 and not B2:

B1 and not B2

Next let’s break B1 into (a1 and C1) or B1_no_C1, where B1_no_C1 is U1 or (not a1 and D1):

((a1 and C1) or B1_no_C1) and not B2

Now we distribute the difference:

((a1 and C1) and not B2) or (B1_no_C1 and not B2)

Let’s solve the left-hand side. We know B2 = (a2 and C2) or U2 (remember D2 is bottom), so let’s add that:

(a1 and C1 and not ((a2 and C2) or U2))
or (B1_no_C1 and not B2)

Now distribute the not and remove the parenthesis:

(a1 and C1 and not (a2 and C2) and not U2)
or (B1_no_C1 and not B2)

Now, if a1 and a2 are disjoint, then a1 and not (a2 and C2) is the same as a1. This happens because if a1 and a2 are disjoint, a2 and C2 is a subset of a2, which is then also disjoint with a1. So the first part simplifies to a1 and C1 and not U2:

(a1 and C1 and not U2) or (B1_no_C1 and not B2)

Now by expanding B1_no_C1 into U1 or (not a1 and D1) and distributed the union, we get:

(a1 and C1 and not U2) or (U1 and not B2) or (not a1 and D1 and not B2)

which is in the BDD format! So we can rewrite the difference of disjoint literals as:

{a1, C1 and not U2, U1 and not B2, D1 and not B2}

which completely avoids adding a2 to the BDD and can then continue recursively.

When D2 is not bottom

When D2 is not bottom, it means B2 has a negated component. Since B2 itself is negated when part of a difference, the D2 component of B2 becomes an intersection, and we can apply the same eager literal technique we applied to intersections.

Once again, we start B1 and not B2:

B1 and not B2

Now let’s break B2 into (B2_no_D2 or (not a2 and D2)), where B2_no_D2 is (a2 and C2) or U2:

(B1) and not (B2_no_D2 or (not a2 and D2))

Now we distribute the negation all the way through:

(B1) and (not B2_no_D2 and (a2 or not D2))

And distribute B1’s intersection with (a2 or not D2):

((B1 and a2) or (B1 and not D2)) and not B2_no_D2

B1 and a2 is an eager literal intersection from the previous section, which we can reuse!

Furthermore, notice at the end we compute the difference between ((B1 and a2) or (B1 and not D2)) and B2_no_D2. Given B2_no_D2 by definition has D2 = bottom, we can apply the optimized difference for when D2 is bottom.

At the moment, we are not applying this optimization in Elixir, as the difference with negations on the right-hand side are uncommon. We may revisit this in the future.

Results

We initially implemented eager literal intersections as part of Elixir v1.20 release, which reduced the type checking time of one of the pathological cases from 10 seconds to 25ms!

However, our initial implementation also caused a performance regression, as we did not distinguish between open and closed maps. This regression was addressed by applying the optimization only to closed maps, as discussed in the article.