Security and the BEAM Ecosystem - Jonatan Männchen & Dali Khechine | Erlang Solutions Webinar

Permalink

How To Build Platforms That do Not Let Audiences Down - Lee Siguake | Erlang Solutions Webinar

Permalink

Lazy BDDs with eager literal differences

In a 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:

def example(x) when is_binary(x), do: ...
def example(x) when is_integer(x), do: ...
def example(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 know x has type not binary() and not integer(). In other words, the type of a given clause is computed by the type of its patterns and guards, minus the 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 type clause1, clause2, and clause3, you know clause3 is redundant if its type is contained in the union of the types of clause1 and clause2:

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 between clause3 and 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 increasing 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:

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}

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 between a1 and a2 is 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 between a1 and a2. If they are disjoint, they have nothing in common, and the result is a1. On the other hand, if a1 is a subtype of a2, 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 that C = :top, U = :bottom, and D = :bottom. Let’s get to work!

Literal on the right-hand side

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

B1 and not B2

where B1 is (a1 and C1) or U1 or (not a1 and D1) and B2 is simply a2. So we have:

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

Now let’s distribute and 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 a2 is simply a1, so we have:

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

When a1 is a subtype of a2, a1 and not a2 is empty, plus not a1 and not a2 is the same as not (a1 or a2), which is the same as not a2. So we have:

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

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

Literal on the left-hand side

Now let’s derive new formulas for the difference when B1 is 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 the not over the right-hand side:

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

When a1 and a2 are disjoint, we know that a1 and (not a2 or not C2) is a1. This is because if we distribute the intersection, we end up with (a1 and not a2) or (a1 and not C2). And since a1 and not a2 is a1, we end up with a1 unioned with a type that is a subset of a1, hence a1.

So we end up with:

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

And if a1 and a2 are disjoint, the intersection between them is empty, so we are left with the following disjoint formula:

a1 and not D2 and not U2

When a1 is a subtype of a2, 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 in a1 and (not a2 or not C2). We will have two parts, a1 and not a2, which is empty, unioned with a1 and not C2, resulting in:

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

Now we can distribute a1 and (a2 or not D2). And because a1 and a2 is a1 (since a1 is a subset), we end up with a1 or (a1 and not D2), which is a1. 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, x in the third clause starts with the value of term, 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()} and not %MyStruct{x: integer()} and not %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() and not integer() and not binary()}

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_diff which is a new literal where we compute the difference between the only different field (as done above), as well as a_int and a_union, which is respectively the intersection and union of the distinct field.

Literal on the right-hand side

Our formula for B1 and not B2 with 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 a2 is a_diff. not a1 and not a2 is the same as (not (a1 or a2)) which is the same as not 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 that a1 and not a2 is a_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 a2 is empty, so the first and becomes a_diff and not D2. Then we distribute the second and and, after replacing a1 and a2 by a_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 that a1 = 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 types a or b, when b is a subset, is always a. 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.

Permalink

Erlang/OTP 29.0 Release Candidate 2

OTP 29.0-rc2

Erlang/OTP 29.0-rc2 is the second 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-rc2/doc. You can also install the latest release using kerl like this:

kerl build 29.0-rc2 29.0-rc2.

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!

Highlights for RC2

• The module io_ansi allows the user to emit Virtual Terminal Sequences (also known as ANSI sequences) to the terminal in order to add colors/styling to text or to create fully fledged terminal applications.

• The new ct_doctest module allows the user to test documentation examples in Erlang module docs and documentation files.

• The ignore_xref attribute has been handled as a post-analysis filter by build tools such as Rebar3. In this release, [xref] itself does the filtering, ensuring that all tooling that calls xref for any purpose can rely on these declarations to just work.

Highlights for RC1

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

Erlang/OTP 28.4 Release

OTP 28.4

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

HIGHLIGHTS

ssh

• Added support for the PQC key exchange (kex) algorithm mlkem768x25519-sha256, a hybrid quantum-resistant algorithm combining ML-KEM-768 with X25519.

  erts

• Added persistent_term:put_new/2 that will quickly do nothing if a term with the given name and value already exists, and raise a badarg exception if the term exists with a different value.

POTENTIAL INCOMPATIBILITIES

• Added a new HttpOption {autoretry, timeout()} to httpc:request/4,5. This option allows the client to decide how to act upon receiving a Retry-After response header. The default behavior changes, as now only one retry is made before returning the error code, instead of retrying infinitely.

For details about bugfixes and potential incompatibilities see the Erlang 28.4 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

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 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 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.

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

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