Lazy BDDs with eager literal differences

Ina previous article, we discussed how we optimized intersections in Elixir set-theoretic types to improve performance.

In a nutshell, lazy BDDs allow us to represent set-theoretic operations at any depth. And while this is useful in many cases, 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-is in the BDD, from a quick glance it is clear that the above can only be equal to%Bar{}. To address this, we made intersections eager, removing the size of BDDs and drastically improving compilation times.

Lately, Elixir v1.20.0-rc.2 introduced new improvements to the type checker. Among them is the ability to propagate type information across clauses and check for redundant clauses. For example, take this code:

defexample(x)whenis_binary(x),do:...defexample(x)whenis_integer(x),do:...defexample(x),do:...

In the first clause, we know the argument is a binary. In the second, we know it is an integer. Therefore, in the third one, even though there are no guards, we knowxhas typenot binary() and not integer(). In other words, the type of a given clause is computed by the type of its patterns and guards,minusthe types of the previous clauses.

Furthermore, we can now check if a clause is redundant by checking if its type definition is a subset/subtype of the previous ones. For example, if you have three clauses, each with typeclause1,clause2, andclause3, you knowclause3is redundant if its type is contained in the union of the types ofclause1andclause2:

clause3 ⊆ (clause1 ∪ clause2)

In set-theoretic types, a type is a subtype of the other if it is a subset of said type, so we will use these terms interchangeably. Furthermore, checking if a type is a subset/subtype of another can be done by checking if the difference betweenclause3and the union of the clauses is empty. In Elixir terms:

empty?(difference(clause3,union(clause1,clause2)))

Long story short: with Elixir v1.20.0-rc.2, the type system is seeing an increase number of differences. Projects where modules had 1000+ of clauses were taking too long to compile, so it was time to derive new formulas and optimizations.

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.

A recap on lazy BDDs and literals

A lazy BDD has type:

typelazy_bdd()=:topor:bottomor{type(),constrained::lazy_bdd(),uncertain::lazy_bdd(),dual::lazy_bdd()}

wheretype()is the representation of the actual type. For example, if the type being represented is atuple,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}

whereBstands for BDD,ais the literal,Cis constrained,Uis uncertain, andDis dual. Semantically, the BDD above is the same as:

B=(aandC)orUor(notaandD)

Which means the following expression, wherefoo,bar,baz, andbatbelow represent types:

(fooandnot(baror(bazandbat))

will be stored as:

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

Eager literal differences

The main insight of the previous article was, when intersecting two BDDs:

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

if the intersection betweena1 and a2is disjoint (i.e. it returns the empty type), we can likely build new formulas that eliminate many nodes from the BDD recursively.

The goal is to apply the same optimization for differences. In particular, there are two properties that we can leverage from differences. Take the difference betweena1anda2. If they are disjoint, they have nothing in common, and the result isa1. On the other hand, ifa1is a subtype ofa2, then the difference is empty.

Furthermore, for simplicity, we will only optimize the cases where at least one of the sides is exclusively a literal, which means thatC = :top,U = :bottom, andD = :bottom. Let’s get to work!

Literal on the right-hand side

We want to derive new formulas for difference whenB2is a literal. Let’s start with the base formula:

B1 and not B2

whereB1is(a1 and C1) or U1 or (not a1 and D1)andB2is simplya2. So we have:

((a1 and C1) or U1 or (not a1 and D1)) and not a2

Now let’s distributeand not a2:

(a1 and not a2 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

When they are disjoint,a1 and not a2is simplya1, so we have:

(a1 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

Whena1is a subtype ofa2,a1 and not a2is empty, plusnot a1 and not a2is the same asnot (a1 or a2), which is the same asnot a2. So we have:

(U1 and not a2) or (D1 and not a2)

In both formulas,and not a2is then applied using the same eager literal difference recursively.

Literal on the left-hand side

Now let’s derive new formulas for difference whenB1is a literal. This means we want to compute:

B1 and not B2

Which we can expand to:

a1 and not ((a2 and C2) or U2 or (not a2 and D2))

Now let’s distribute thenotover the right-hand side:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

Whena1anda2are disjoint, we know thata1 and (not a2 or not C2)isa1. This is because if we distribute the intersection, we end up with(a1 and not a2) or (a1 and not C2). And sincea1 and not a2isa1, we end up witha1unioned with a type that is a subset ofa1, hencea1.

So we end up with:

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

And ifa1anda2are disjoint, the intersection between them is empty, so we are left with the following disjoint formula:

a1 and not D2 and not U2

Whena1is a subtype ofa2, we can simplify two expressions in the initial formula. Let’s look at it again:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

First we distribute the intersection ina1 and (not a2 or not C2). We will have two parts,a1 and not a2, which is empty, unioned witha1 and not C2, resulting in:

a1 and (not C2) and (not U2) and (a2 or not D2)

Now we can distributea1 and (a2 or not D2). And becausea1 and a2isa1(sincea1is a subset), we end up witha1 or (a1 and not D2), which isa1. So our subset formula becomes:

a1 and not C2 and not U2

As you can see, these new formulas can reduce the amount of nodes in the BDD drastically, which lead to much better performance.

One last trick: one field difference

The optimizations above lead to excellent performance. Projects that would take dozens of seconds to compile could now do so in milliseconds. However, there were still some cases where the optimizations could not kick-in, leading to worse performance. In particular, with structs.

When working with a struct in Elixir, the fields will most often have the same type, except for one. For example:

def example(%MyStruct{x: x}) when is_binary(x)  def example(%MyStruct{x: x}) when is_integer(x)
def example(%MyStruct{x: x})

In the example above,xin the third clause starts with the value ofterm, so the last struct is a supertype of the other ones, and our optimizations do not apply. Therefore, the type of the third clause would be:

%MyStruct{x:term()}andnot%MyStruct{x:integer()}andnot%MyStruct{x:binary()}

However, whenever only one of the fields are different, we can translate the above as the difference of said field, so instead we could have:

%MyStruct{x:term()andnotinteger()andnotbinary()}

All we need to do is to compute new formulas. So let’s do it one last time. For our last batch of formulas, we will need three new types:a_diffwhich is a new literal where we compute the difference between the only different field (as done above), as well asa_intanda_union, which is respectively the intersection and union of the distinct field.

Literal on the right-hand side

Our formula forB1 and not B2with a literal on the right-hand side is:

(a1 and not a2 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

a1 and not a2isa_diff.not a1 and not a2is the same as(not (a1 or a2))which is the same asnot a_union, so we end up with:

(a_diff and C1) or (U1 and not a2) or (not a_union and D1)

Literal on the left-hand side

Our starting point is:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

By distributing the first intersection, we have:

((a1 and not a2) or (a1 and not C2)) and not U2 and (a2 or not D2)

We know thata1 and not a2isa_diff. So let’s slot that in and change the order of operations:

(a_diff or (a1 and not C2)) and (a2 or not D2) and not U2

We now distribute(a_diff or (a1 and not C2)) and (a2 or not D2):

((a_diff and (a2 or not D2)) or   ((a1 and not C2) and (a2 or not D2))) and not U2

a_diff and a2is empty, so the firstandbecomesa_diff and not D2. Then we distribute the secondandand, after replacinga1 and a2bya_int, we get the following:

((a_diff and not D2) or   (a_int and not C2) or
 (a1 and not C2 and not D2)) and not U2

At this point, I thought no further simplifications were possible. That’s when I reached to Claude Opus 4.6 to explore alternative variations and it suggested the following “obvious-only-in-hindsight” simplication. We know thata1 = a_diff or a_int, so let’s slot that in:

((a_diff and not D2) or   (a_int and not C2) or
 ((a_diff or a_int) and not C2 and not D2)) and not U2

Now if we distribute(a_diff or a_int) and not C2 and not D2), we get:

((a_diff and not D2) or   (a_int and not C2) or
 (a_diff and not C2 and not D2) or
 (a_int and not C2 and not D2)) and not U2

However, we know that(a_diff and not D2 and not C2)is a subtype of(a_diff and not D2)(as it is the same set minus C2), and the same applies to(a_int and not C2 and not D2). And then union of two typesa or b, whenbis a subset, is alwaysa. Therefore both terms can be fully discarded, so we end up with:

((a_diff and not D2) or (a_int and not C2)) and not U2

Summary

We implemented all simplifications above and they will be available in full as part of Elixir v1.20.0-rc4. At the moment, we have measured clear impact from the “literal on the left-hand side” optimizations, allowing us to drastically improve the type system performance when checking thousands of clauses or large structs. At the moment, we did not spot any scenarios where the right-hand side optimizations were useful, most likely because it does not show up in codebases (yet).

We will continue assessing the performance of the type system as we add more features based on community feedback.