Elixir v1.20 released: now a gradually typed language - The Elixir programming language

Home

Install

Learning

Docs

Guides

Cases

Blog

Elixir v1.20 released: now a gradually typed language

June 03, 2026 · by José Valim · in

Announcements

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.

With Elixir v1.20, we have completed our first development milestone which is to perform type inference and gradually type check every Elixir program, without introducing type annotations. This means Elixir increasingly reports dead code and verified bugs: typing violations that are guaranteed to fail at runtime if executed. Elixir can find verified bugs in existing programs efficiently, without introducing developer overhead, and with an extremely low false positives rate.

In this announcement, we will break down the type system goals, what the dynamic() type means in Elixir, and how it finds verified bugs. In particular, our implementation performs well in the “If T: Benchmark for Type Narrowing” benchmark. Elixir passes 12 of the 13 categories, showing that it can recover precise type information from ordinary Elixir code, which we use to find verified bugs in dynamically typed programs.

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

Types, in my Elixir?

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), with clear error messages

Introducing a type system into an existing language is a complex change. For this reason, our first milestone was to implement the type system without introducing typing annotations but still have it provide value to developers by finding dead code and verified bugs. This is done through the dynamic() type, which in Elixir is quite different from other gradually typed languages. Let’s break it down.

The dynamic() type

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 has two important properties: compatibility and narrowing.

In static type systems, when you have a type of shape integer() or binary() and you invoke a function, said function must accept both types. However, because type systems cannot capture the intention of all of our programs with precision, this may lead to false positives. For example, take the simple code below:

def percentage_or_error(value) when is_integer(value) do<br>value_or_error =<br>if value > 1 do<br>value<br>else<br>"not well"<br>end

# ... more code ...

if value > 1 do<br>value_or_error / 100<br>else<br>String.upcase(value_or_error)<br>end<br>end

Although value_or_error has type integer() or binary(), the operator / accepts only numbers, and String.upcase accepts only binaries/strings, the program above is valid and emits no exceptions at runtime. However, a type system would still report two violations, because the types supplied to / and String.upcase are not a subtype of the accepted types.

While the program above could be better written to have no typing violations, type systems will always reject valid programs, and if Elixir were to introduce too many false positives in existing codebases, it would quickly erode the trust in the type system. Therefore, Elixir’s gradual type system tags the value_or_error variable above with the type dynamic(integer() or binary()), which means the type is either integer() or binary() at runtime.

When calling a function with a dynamic() type, Elixir will only emit a typing violation if the supplied types and the accepted types are disjoint. In the program above, even though / expects only numbers, dynamic(integer() or binary()) can be an integer() and given the accepted and supplied types are not disjoint, there are no typing violations. However, if we were to change the program to this:

value_or_error =<br>if value > 1 do<br>value<br>else<br>"not well"<br>end

Map.fetch!(value_or_error, :some_key)

Because Map.fetch! expects a map data structure, and value_or_error can only be integer or binary at runtime, the accepted and supplied types are disjoint, which turns into a violation. This is known as the compatibility property and it explains how Elixir reports only verified bugs.

However, reporting only...