Lazy BDDs with eager literal intersections

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.

Permalink

From Minimum Viable Product to Mission Critical - Camjar Djoweini | Erlang Solutions Webinar

Permalink

The Picture They Paint of You

Permalink

Erlang/OTP 29.0 Release Candidate 1

OTP 29.0-rc1

Erlang/OTP 29.0-rc1 is the first release candidate of three before the OTP 29.0 release.

The intention with this release is to get feedback from our users. All feedback is welcome, even if it is only to say that it works for you. We encourage users to try it out and give us feedback either by creating an issue at https://github.com/erlang/otp/issues or by posting to Erlang Forums.

All artifacts for the release can be downloaded from the Erlang/OTP Github release and you can view the new documentation at https://erlang.org/documentation/doc-17.0-rc1/doc. You can also install the latest release using kerl like this:

kerl build 29.0-rc1 29.0-rc1.

Erlang/OTP 29 is a new major release with new features, improvements as well as a few incompatibilities. Some of the new features are highlighted below.

Many thanks to all contributors!

General

• In the default code path for the Erlang system, the current working directory (.) is now in the last position instead of the first.

• There is no longer a 32-bit Erlang/OTP build for Windows.

New language features

• Native records as described in EEP-79 has been implemented. A native record is a data structure similar to the traditional tuple-based records, except that is a true data type. Native records are considered experimental in Erlang/OTP 29 and possibly also in Erlang/OTP 30.

• The new is_integer/3 guard BIF makes it possible to easily verify that a value is both an integer and within a certain range. For example: is_integer(I, 0, 100)

• Multi-valued comprehensions according to EEP 78 are now supported. For example, [-I, I || I <- [1, 2, 3]] will produce [-1,1,-2,2,-3,3].

• By enabling the compr_assign feature, it is now possible to bind variables in a comprehensions. For example: [H || E <- List, H = erlang:phash2(E), H rem 10 =:= 0]

Compiler and JIT improvements

• In the documentation for the [compile] module, there is now a section with recommendations for implementors of languages running on the BEAM.

• The JIT now generates better code for matching or creating binaries with multiple little-endian segments.

• The compiler will generate more efficient code for map comprehensions with constant values that don’t depend on the generator. Example: #{K => 42 || K <- List}

Compiler warnings

There are several new compiler warnings enabled by default. For each such warning, there is an option to disable it.

• There will now be a warning when using the catch operator, which has been deprecated for a long time. It is recommended to instead use try…catch but is also possible to disable the warning by using the nowarn_deprecated_catch option.

• There will now be a warning when exporting variables out of a subexpression. For example: file:open(File, AllOpts = [write, {encoding,utf8}]). This warning can be disabled using the nowarn_export_var_subexpr compiler option.

• The compiler will now warn for uses of the and and or operators. This warning can be disabled using the nowarn_obsolete_bool_op compiler option.

• The compiler will now warn for matches such as {a,B} = {X,Y}, which is better written as {a=X,B=Y}. This warning can be disabled using the nowarn_match_alias_pats option.

For a long time, there has been a warning for using the obsolete guard tests (such as list(L) instead of is_list(L). In Erlang/OTP 30, the old guards will be removed from the language.

STDLIB

• There are new functions for randomly permutating a list: rand:shuffle/1 and rand:shuffle_s/2.

SSH

• The default key exchange algorithm is now mlkem768x25519-sha256, a hybrid quantum-resistant algorithm combining ML-KEM-768 with X25519. This provides protection against both classical and quantum computer attacks while maintaining backward compatibility through automatic fallback to other algorithms when peers don’t support it.

For more details about new features and potential incompatibilities see the README.

Permalink

Making your System Debuggable - Lessons from Erlang Doctor | Paweł Chrząszcz

Permalink

Instrumenting Erlang and Elixir code with open telemetry - Part 2 | Denys Gonchar

Permalink

Type inference of all constructs and the next 15 months

Today we celebrate 15 years since Elixir’s first commit! To mark the occasion, we are glad to announce the first release candidate for Elixir v1.20, which performs type inference of all language constructs, with increasing precision.

In this blog post, we will break down exactly what this means, and what to expect in the short and medium term of the language evolution (roughly the next 15 months).

Types, in my Elixir?

In 2022, we announced the effort to add set-theoretic types to Elixir. In June 2023, we published an award winning paper on Elixir’s type system design and said our work was transitioning from research to development.

Our goal is to introduce a type system which is:

• sound - the types inferred and assigned by the type system align with the behaviour of the program

• gradual - Elixir’s type system includes the dynamic() type, which can be used when the type of a variable or expression is checked at runtime. In the absence of dynamic(), Elixir’s type system behaves as a static one

• developer friendly - the types are described, implemented, and composed using basic set operations: unions, intersections, and negations (hence it is a set-theoretic type system)

However, I want to emphasize what the gradual typing means in Elixir. Many gradual type systems have the any() type, which, from the point of view of the type system, often means “anything goes” and no type violations are reported.

On the other hand, Elixir’s gradual type is called dynamic() and it works as a range. For example, you can say dynamic(integer() or float()), which means the type is either integer() or float() at runtime. Then if you proceed to pass it to a function that expects a binary(), you will get a typing violation. This allows the type system to emit warnings even in the presence of dynamism. Even if you declare a type as dynamic() and then proceed to use as integer() and then binary(), a type violation is still reported. We have also developed new techniques that ensure our gradual typing is sound, without a need for additional runtime checks.

The type system was made possible thanks to a partnership between CNRS and Remote. The development work is currently sponsored by Fresha, and Tidewave.

Let’s see how this is turning out in practice.

Inference across Elixir releases

Elixir v1.17 was the first release to introduce set-theoretic types into the compiler. Elixir v1.18 added inference of patterns and return types. Therefore, if you wrote this code:

defmodule User do
  defstruct [:age, :car_choice]

  def drive(%User{age: age, car_choice: car}, car_choices) when age >= 18 do
    if car in car_choices do
      {:ok, car}
    else
      {:error, :no_choice}
    end
  end

  def drive(%User{}, _car_choices) do
    {:error, :not_allowed}
  end
end

Elixir’s type system will infer the drive function expects a User struct as input and returns either {:ok, dynamic()} or {:error, :no_choice} or {:error, :not_allowed}. Therefore, the following code

User.drive({:ok, %User{}}, car_choices)

will emit a warning stating that we are passing an invalid argument, both in your IDE and the shell:

Now consider the expression below. We are expecting the User.drive/2 call to return :error, which cannot possibly be true:

case User.drive(user, car_choices) do
  {:ok, car} -> car
  :error -> Logger.error("User cannot drive")
end

Therefore the code above would emit the following warning:

However, Elixir v1.18 could only infer types from patterns. If you wrote this code:

def user_age_to_string(user) do
  Integer.to_string(user.age)
end

Elixir would not infer anything about the function arguments. As of Elixir v1.20-rc, Elixir correctly infers the function to be %{..., age: integer()} -> binary(), which means it expects a map with at least the age field (the leading ... indicates other keys may be present) and it returns a binary().

Or let’s see another example:

def add_rem(a, b) do
  rem(a + b, 8)
end

While a + b works with both integers and floats, because the rem (remainder) function works exclusively with integers, Elixir correctly infers that a and b must also both be integers. If you try calling the function above with a float, you will also get a type violation.

In a nutshell, we have been steadily increasing the amount of inference in Elixir programs. Our goal is to find typing violations in Elixir programs for free, without a need for developers to change existing code. And, in the last few days, we finally wrapped up the last missing piece.

Inference of guards

Elixir v1.20-rc also performs inference of guards! Let’s see some examples:

def example(x, y) when is_list(x) and is_integer(y)

The code above correctly infers x is a list and y is an integer.

def example({:ok, x} = y) when is_binary(x) or is_integer(x)

The one above infers x is a binary or an integer, and y is a two element tuple with :ok as first element and a binary or integer as second.

def example(x) when is_map_key(x, :foo)

The code above infers x is a map which has the :foo key, represented as %{..., foo: dynamic()}. Remember the leading ... indicates the map may have other keys.

def example(x) when not is_map_key(x, :foo)

And the code above infers x does not have the :foo key (hence x.foo will raise a typing violation), which has the type: %{..., foo: not_set()}.

You can also have expressions that assert on the size of data structures:

def example(x) when tuple_size(x) < 3

Elixir will correctly track that the tuple has at most two elements, and therefore accessing elem(x, 3) will emit a typing violation. In other words, Elixir can look at complex guards, infer types, and use this information to find bugs in our code!

The next ~15 weeks

As we work on the type system, we have been carefully monitoring the compiler performance. And while we have been able to develop new techniques to keep everything running smoothly, the next weeks will dramatically ramp up the amount of type information flowing through the compiler, and therefore we need your feedback.

The next Elixir release is scheduled for May. We are shipping this release candidate earlier than usual for validation. We also plan to launch at least two additional release candidates with increased type checking.

Jan/2026: inference of all constructs

The first release candidate is out right now, with type inference of all Elixir constructs. Please give it a try. However, at this stage, we expect some false positives: the type system will report warnings which are not actual violations. We will explain exactly why in the next paragraphs. So don’t change your programs yet. The most valuable feedback we want from you is performance! If everything compiles at roughly the same speed as before, then hooray!

Feb-Mar/2026: inference across clauses

The second release candidate will add type inference across clauses. Let’s see some examples. Take this code:

case some_function_call() do
  %{name: name} = user -> ...
  %{first_name: first, last_name: last} = user -> 
end

Today, we know user in the first clause has the name field (and potentially other fields). We know that user in the second clause has first_name and last_name. The code above also implies that user in the second clause does not have the name field (after all, if it had the name field, the first clause would have matched). In other words, pattern matching order becomes a source of negative type information. In the first release candidate, the type system cannot infer this information yet, but it will be implemented in the following release candidate.

Besides giving us more precise types, the above will also allow us to perform exhaustiveness checks as well as find redundant clauses (note we already warn for clauses that won’t ever match since Elixir v1.18).

However, it is worth keeping in mind the work is a bit more complex than one might think. For example, take this code:

case some_function_call() do
  %{age: age} = user when age >= 21 -> ...
  %{name: name} = user -> 
end

Can we say the user in the second clause does not have the age field? No, we can’t, because the first clause only matches if age is greater than or equal to 21. So the second clause will still match users with a lower age. This means we must distinguish between “surely accepted clauses” and “potentially accepted clauses”.

Apr-May/2026: inference across dependencies

Finally, we will ship a third release candidate, which enables type inference for function calls across your dependencies. In the current release candidate, Elixir can infer types from function calls, but such inference only applies to modules from Elixir’s standard library. Take the following code:

def integer_to_string(x) do
  Integer.to_string(x)
end

In the code above, we will infer x is an integer(), but if instead you call MyInteger.to_string(x) from a dependency, we only perform type checking, we won’t infer the integer_to_string function expects an integer. Once implemented, this step will drastically increase the amount of types flowing through the compiler, hence we are dedicating a release candidate for it.

The next ~15 months

At this point, you may be wondering: when can we officially claim Elixir is statically typed?

When we first announced the type system effort, we broke it into three distinct milestones:

1. Type inference of patterns and guards: this is our current milestone which has, since then, been extended to type inference of all language constructs

2. Introduction of typed structs, allowing struct types to propagate throughout the system, as we pattern match on structs throughout the codebase

3. Introduction of type signatures, including for parametric and protocol polymorphism

Assuming all release candidates above go according to plan, we will officially conclude the first milestone as part of Elixir v1.20 and start working on the subsequent ones. However, there are still challenges ahead that may prove the type system to be impractical:

• Ergonomics: all of our improvements so far have happened behind the scenes, without changes to the language. While this has been very valuable to validate the feasibility and performance of the type system, we still need to assess its impact on the developer experience

• Performance: our current implementation does not yet support recursive and parametric types and those may also directly impact performance and make the type system unfeasible

Our goal is to explore these problems and their solutions in the future Elixir v1.21 (Nov/2026) and v1.22 (May/2027) releases, by implementing these operations in the compiler and using it to internally type complex Elixir modules, such as the Enum module. So while we don’t have a precise date for when we will conclude these upcoming milestones, we will likely continue to see gradual improvements on every release for the next 15 months.

Wrapping up

The first release candidate for Elixir v1.20 is out and includes type inference of all constructs. We will have multiple release candidates before the final release in May/2026, and your feedback is very important:

• Jan/2026: inference of all constructs, may have many false positives, assess performance!
• Feb-Mar/2026: inference across clauses, few or none false positives, assess performance!
• Apr-May/2026: inference across dependencies, assess performance!

Every release will have a thread in the Elixir Forum for discussion.

Check our documentation to learn more about our overall work on set-theoretic types. This release also includes our official types cheatsheet.

The complete CHANGELOG for this release is on GitHub.

Happy coding!

Permalink

Software Acceleration and Desynchronization

Permalink

Erlang/OTP 28.3 Release

OTP 28.3

Erlang/OTP 28.3 is the second maintenance patch package for OTP 28, with mostly bug fixes as well as improvements.

POTENTIAL INCOMPATIBILITIES

• Adjustment in ssh_file module allowing inclusion of Erlang/OTP license in test files containing keys.

HIGHLIGHTS

ssl

• Support for MLKEM hybrid algorithms x25519mlkem768, secp384r1mlkem1024, secp256r1mlkem768 in TLS-1.3

  ssl, public_key

• Added support in public_key and ssl for post quantum algorithm SLH-DSA.

erts, kernel

• Support for the socket options TCP_KEEPCNT, TCP_KEEPIDLE, and TCP_KEEPINTVL have been implemented for gen_tcp, as well as TCP_USER_TIMEOUT for both gen_tcp and socket.

OTP

• Publish OpenVEX statements in https://erlang.org/download/vex/

  OpenVEX statements contain the same information as the OTP advisories, with the addition of vendor CVEs for which Erlang/OTP is not affected. This is important to silence vulnerability scanners that may claim Erlang/OTP to be vulnerable to vendor dependency projects, e.g., openssl.

  OpenVEX statements will be published in https://erlang.org/download/vex/ where there will be an OTP file per release, e.g., https://erlang.org/download/vex/otp-28.openvex.json.

  Erlang/OTP publishes OpenVEX statements for all supported releases, that is, as of today, OTP-26, OTP-27, and OTP-28.

  The source SBOM tooling (oss-review-toolkit) has been updated to produce source SBOM in SPDX v2.3 format, and the source SBOM now links OpenVEX statements to a security external reference. This means that by simply analyzing the source SBOM, everyone can further read the location of the OpenVEX statements and further process them.

For details about bugfixes and potential incompatibilities see the Erlang 28.3 README

The Erlang/OTP source can also be found at GitHub on the official Erlang repository, https://github.com/erlang/otp

Download links for this and previous versions are found here:

• https://www.erlang.org/downloads

Permalink

Lazier Binary Decision Diagrams (BDDs) for set-theoretic types

The Elixir team and the CNRS are working on a set-theoretic type system for Elixir which, simply put, is a type-system powered by unions, intersections, and negations. As part of the implementation of said type systems, we need an efficient way of representing said operations. This article discusses the existing approaches found in theory and practice, as well as the improvements we have introduced as part of Elixir v1.19.

This article covers the implementation details of the type system. You don’t need to understand these internals to use the type system, just as you don’t need to know virtual machine bytecodes or compiler passes to use a programming language. Our goal is to document our progress and provide guidance for future maintainers and implementers. Let’s get started.

DNFs - Disjunctive Normal Forms

A Disjunctive Normal Form (DNF) is a standardized way of expressing logical formulas using only disjunctions (unions) of conjunctions (intersections). In the context of set-theoretic type systems, DNFs provide a canonical representation for union and intersection types, represented respectively as or and and in Elixir.

In Elixir, we would represent those as lists of lists. Consider a type expression like (A and B) or (C and D). This is already in DNF, it’s a union of intersections, and it would be represented as: [[A, B], [C, D]]. This means performing unions between two DNFs is a simple list concatenation:

def union(dnf1, dnf2), do: dnf1 ++ dnf2

However, more complex expressions like A and (B or C) need to be converted. Using distributive laws, this becomes (A and B) or (A and C), which is now in DNF. In other words, the intersection of DNFs is a Cartesian product:

def intersection(dnf1, dnf2) do
  for intersections1 <- dnf1,
      intersections2 <- dnf2 do
    intersections1 ++ intersections2
  end
end

The advantage of DNFs is their simple structure. Every type can be represented as unions of intersecting terms, making operations like checking if a type is empty simply a matter of checking if all unions have at least one intersection that is empty:

def empty?(dnf) do
  Enum.all?(dnf, fn intersections ->
    Enum.any?(intersections, &empty_component?/1)
  end)
end

On the other hand, the snippets above already help us build an intuition on the drawbacks of DNFs.

First, we have seen how intersections are Cartesian products, which can lead to exponential blow ups when performing the intersection of unions. For example, (A₁ or A₂) and (B₁ or B₂) and (C₁ or C₂) leads to (A₁ and B₁ and C₁) or (A₁ and B₁ and C₂) or (A₁ and B₂ and C₁) or ..., with 8 distinct unions.

Furthermore, if we implement unions as simple list concatenations, those unions can end up with duplicated entries, which exacerbates the exponential blow up when we perform intersections of these unions. This forces us to aggressively remove duplicates in unions, making it more complex and expensive than a concatenation.

Despite their limitations, DNFs served us well and were the data structure used as part of Elixir v1.17 and v1.18. However, since Elixir v1.19 introduced type inference of anonymous functions, negations became more prevalent in the type system, making exponential growth more frequent. Let’s understand why.

Inferring anonymous functions

Imagine the following anonymous function:

fn
  %{full_name: full} -> "#{full}"
  %{first_name: first, last_name: last} -> "#{last}, #{first}"
end

We can say the first clause accepts any map with the key full_name. The second clause accepts any map with the keys first_name and last_name which DO NOT have the key full_name (otherwise they would have matched the first clause). Therefore, the inferred type should be:

$ %{full_name: String.Chars.t()} -> String.t()
$ %{first_name: String.Chars.t(), last_name: String.Chars.t()} and not
    %{full_name: String.Chars.t()} -> String.t()

As you can see, in order to express this type, we need a negation (not). Or, more precisely, a difference since A and not B is the same as A - B.

Implementing negations/differences in DNFs is relatively straightforward. Instead of lists of lists, we now use lists of two-element tuples, where the first element is a list of positive types, and the second is a list of negative types. For example, previously we said (A and B) or (C and D) would be represented as [[A, B], [C, D]], now it will be represented as:

[{[A, B], []}, {[C, D], []}]

While (A and not B) or C or D is represented as:

[{[A], [B]}, {[C], []}, {[D], []}]

The difference between two DNFs is implemented similarly to intersections, except we now need to perform the Cartesian product over the positive and negative parts of each conjunction. And given anonymous functions have differences, inferring the types of anonymous functions are now exponentially expensive, which caused some projects to take minutes to compile. Not good!

BDDs - Binary Decision Diagrams

Luckily, those exact issues are well documented in literature and are addressed by Binary Decision Diagrams (BDDs), introduced by Alain Frisch (2004) and later recalled and expanded by Giuseppe Castagna (2016).

BDDs represent set-theoretic operations as an ordered tree. This requires us to provide an order, any order, across all types. Given all Elixir values have a total order, that’s quite straightforward. Furthermore, by ordering it, we can detect duplicates as we introduce nodes in the tree. The tree can have three distinct node types:

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

:top represents the top type (where the intersection type and :top returns type) and :bottom represents the bottom type (where the intersection type and :bottom returns :bottom). Non-leaf nodes are represented via a three-element tuple, where the first element is the type (what we have been calling A, B… so far), the second element is called in literature the constrained branch, and the third element is the dual branch.

In order to compute the actual type of a non-leaf node, we need to compute (type() and constrained()) or (not type() and dual()) (hence the names constrained and dual). Let’s see some examples.

The type A is represented as {A, :top, :bottom}. This is because, if we compute (A and :top) or (not A and :bottom), we get A or :bottom, which is equivalent to A.

The type not A is represented as {A, :bottom, :top}, and it gives us (A and :bottom) or (not A and :top), which yields :bottom or not A, which is equivalent to not A.

The type A and B, assuming A < B according to a total order, is represented as {A, {B, :top, :bottom}, :bottom}. Expanding it node by node gives us:

(A and ((B and :top) or (not B and :bottom))) or (not A and :bottom)
(A and (B or :bottom)) or (not A and :bottom)
(A and B) or :bottom
(A and B)

While the difference A and not B is represented as {A, {B, :bottom, :top}, :bottom}, which we also expand node by node:

(A and ((B and :bottom) or (not B and :top))) or (not A and :bottom)
(A and (:bottom or not B)) or (not A and :bottom)
(A and not B) or :bottom
(A and not B)

Finally, the union A or B is implemented as {A, :top, {B, :top, :bottom}}. Let’s expand it:

(A and :top) or (not A and ((B and :top) or (not B and :bottom)))
(A and :top) or (not A and (B or :bottom))
A or (not A and B)
(A or not A) and (A or B)
:top and (A or B)
A or B

In other words, Binary Decision Diagrams allow us to represent unions, intersections, and differences efficiently, removing the exponential blow up. Guillaume Duboc implemented them as part of Elixir v1.19, addressing the bottlenecks introduced as part of the new type system features… but unfortunately BDDs introduced new slow downs.

The issue with BDDs comes when applying unions to intersections and differences. Take the following type (A and B) or C. Since we need to preserve the order A < B < C, it would be represented as:

{A, {B, :top, {C, :top, :bottom}}, {C, :top, :bottom}}

which can be expanded as:

(A and ((B and :top) or (not B and ((C and :top) or (not C and :bottom))))) or (not A and ((C and :top) or (not C and :bottom)))
(A and (B or (not B and C))) or (not A and C)
(A and (B or C)) or (not A and C)
(A and B) or (A and C) or (not A and C)
(A and B) or C

As you can see, although the representation is correct, its expansion ends-up generating too many disjunctions. And while we can simplify them back to (A and B) or C symbolically, doing such simplications in practice are too expensive.

In other words, the BDD expansion grows exponentially in size on consecutive unions, which is particularly troublesome because we must expand the BDD every time we check for emptiness or subtyping.

At the end of the day, it seems we traded faster intersections/differences for slower unions. Perhaps we can have our cake and eat it too?

BDDs with lazy unions (or ternary decision diagrams)

Luckily, the issue above was also forecast by Alain Frisch (2004), where he suggests an additional representation, called BDDs with lazy unions.

In a nutshell, we introduce a new element, called uncertain, to each non-leaf node to represent unions:

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

We’ll refer to the uncertain as unions going forward.

The type of each non-leaf node can be computed by (type() and constrained()) or uncertain() or (not type() and dual()). Here are some examples:

A = {A, :top, :bottom, :bottom}
A and B = {A, {B, :top, :bottom, :bottom}, :bottom, :bottom}
A or B = {A, :top, {B, :top, :bottom, :bottom}, :bottom}

And, going back to (A and B) or C, it can be represented as:

{A, {B, :top, :bottom, :bottom}, {C, :top, :bottom, :bottom}, :bottom}

The duplication of C is fully removed. With our new representation in hand, the next step is to implement union, intersection, and difference of lazy BDDs, using the formulas found in literature and described below.

Assuming that a lazy BDD B is represented as {a, C, U, D}, and therefore B1 = {a1, C1, U1, D2} and B2 = {a2, C2, U2, D2}, the union of the lazy BDDs B1 or B2 can be computed as:

{a1, C1 or C2, U1 or U2, D1 or D2} when a1 == a2
{a1, C1, U1 or B2, D1} when a1 < a2
{a2, C2, B1 or U2, D2} when a1 > a2

The intersection B1 and B2 is:

{a1, (C1 or U1) and (C2 or U2), :bottom, (D1 or U1) and (D2 or U2)} when a1 == a2
{a1, C1 and B2, U1 and B2, D1 and B2} when a1 < a2
{a2, B1 and C2, B1 and U2, B1 and D2} when a1 > a2

The difference B1 and not B2 is:

{a1, (C1 or U1) and not (C2 or U2), :bottom, (D1 or U1) and not (D2 or U2)} when a1 == a2
{a1, (C1 or U1) and not B2, :bottom, (D1 or U1) and not B2} when a1 < a2
{a2, B1 and not (C2 or U2), :bottom, B1 and not (D2 or U2)} when a1 > a2

Guillaume Duboc first implemented lazy BDDs to represent our function types, addressing some of the bottlenecks introduced alongside BDDs. Afterwards, we attempted to convert all types to use lazy BDDs, hoping they would address the remaining bottlenecks, but that was not the case. There were still some projects that type checked instantaneously in Elixir v1.18 (which used DNFs) but took minutes on v1.19 release candidates, which could only point to large unions still being the root cause. However, weren’t lazy BDDs meant to address the issue with unions?

That was the question ringing in Guillaume’s head and in mine after an hours-long conversation, when we decided to call it a day. Unbeknownst to each other, we both continued working on the problem that night and the following morning. Separately, we were both able to spot the issue and converge on the same solution.

Lazier BDDs (for intersections)

If you carefully look at the formulas above, you can see that intersections and differences of equal nodes cause a distribution of unions. Here is the intersection:

{a1, (C1 or U1) and (C2 or U2), :bottom, (D1 or U1) and (D2 or U2)} when a1 == a2

Notice how U1 and U2 now appear on both constrained and dual parts and the whole union part of the node disappeared, now listed simply as :bottom.

In addition, considering the common case where C1 = C2 = :top and D1 = D2 = :bottom, the node above becomes {a1, :top, :bottom, U1 and U2}, which effectively moves the unions to the dual part. If you play close attention to it, since the uncertain is now :bottom, we reverted back to the original BDD representation. Any further union on those nodes will behave exactly as in the non-lazy BDDs, which we know to be problematic.

In other words, certain operations on lazy BDDs cause unions to revert to the previous BDD representation. So it seems lazy BDDs are not lazy enough? Could we stop this from happening?

Guillaume and I arrived at a new formula using different approaches. Given Guillaume’s approach can also be used to optimize differences, that’s the one I will show below. In particular, we know the intersection of equal nodes is implemented as:

{a1, (C1 or U1) and (C2 or U2), :bottom, (D1 or U1) and (D2 or U2)} when a1 == a2

If we distribute the intersection in the constrained part, we get:

(C1 and C2) or (C1 and U2) or (U1 and C2) or (U1 and U2)

If we distribute the intersection in the dual part, we get:

(D1 and D2) or (D1 and U2) or (U1 and D2) or (U1 and U2)

We can clearly see both parts have U1 and U2, which we can then move to the union! Leaving us with:

{a1,
 (C1 and C2) or (C1 and U2) or (U1 and C2),
 (U1 and U2),
 (D1 and D2) or (D1 and U2) or (U1 and D2)} when a1 == a2

We can then factor out C1 in the constrained and D1 in the dual (or C2 and D2 respectively), resulting in:

{a1,
 (C1 and (C2 or U2)) or (U1 and C2),
 (U1 and U2),
 (D1 and (D2 or U2)) or (U1 and D2)} when a1 == a2

While this new formula requires more operations, if we consider the common case C1 = C2 = :top and D1 = D2 = :bottom, we now have {a1, :top, U1 and U2, :bottom}, with the unions perfectly preserved in the middle. We independently implemented this formula and noticed it addressed all remaining bottlenecks!

Lazier BDDs (for differences)

The issues we outlined above for intersections are even worse for differences. Let’s check the difference formula:

{a1, (C1 or U1) and not (C2 or U2), :bottom, (D1 or U1) and not (D2 or U2)} when a1 == a2
{a1, (C1 or U1) and not B2, :bottom, (D1 or U1) and not B2} when a1 < a2
{a2, B1 and not (C2 or U2), :bottom, B1 and not (D2 or U2)} when a1 > a2

As you can see, all operations shuffle the union nodes and return :bottom. But this time, we know how to improve it! Let’s start with a1 == a2. If we expand the difference in the constrained part, we get:

(C1 and not C2 and not U2) or (U1 and not C2 and not U2)

If we do the same in the dual part, we have:

(D1 and not D2 and not U2) or (U1 and not D2 and not U2)

Unfortunately, there are no shared union terms between the constrained and dual parts, unless C2 and D2 are :bottom. Therefore, instead of fully rewriting the difference of equal nodes, we add the following special case:

{a1, C1 and not U2, U1 and not U2, D1 and not U2}
when a1 == a2 and C2 == :bottom and D2 == :bottom

We can apply a similar optimization when a1 < a2. The current formula:

{a1, (C1 or U1) and not B2, :bottom, (D1 or U1) and not B2} when a1 < a2

The constrained part can be written as (C1 and not B2) or (U1 and not B2) and the dual part as (D1 and not B2) or (U1 and not B2). Given (U1 and not B2) is shared on both parts, we can also convert it to a union, resulting in:

{a1, C1 and not B2, U1 and not B2, D1 and not B2} when a1 < a2

Unfortunately, we can’t apply this for a2 > a1, as differences are asymmetric and do not distribute over unions on the right side. Therefore, the updated formula for difference is:

{a1, C1 and not U2, U1 and not U2, D1 and not U2} when a1 == a2 and C2 == :bottom and D2 == :bottom
{a1, (C1 or U1) and not (C2 or U2), :bottom, (D1 or U1) and not (D2 or U2)} when a1 == a2
{a1, C1 and not B2, U1 and not B2, D1 and not B2} when a1 < a2
{a2, B1 and not (C2 or U2), :bottom, B1 and not (D2 or U2)} when a1 > a2

With these new formulas, all new typing features in Elixir v1.19 perform efficiently and most projects now type check faster than in Elixir v1.18. You can derive similar properties when a1 == a2 and (U1 == :bottom) or (U1 == U2). Give it a try!

Acknowledgements

As there is an increasing interest in implementing set-theoretic types for other dynamic languages, we hope this article shines a brief light on the journey and advancements made by the research and Elixir teams when it comes to representing set-theoretic types.

The type system was made possible thanks to a partnership between CNRS and Remote. The development work is currently sponsored by Fresha and Tidewave.

Permalink