Elixir v1.20 released: now a gradually typed language

In 2022,we announced the effort to add set-theoretic types to Elixir. In June 2023, wepublished an award winning paper on Elixir’s type system designand said our work was transitioningfrom 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 andverified 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 thedynamic()type means in Elixir, and how it findsverified 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 betweenCNRSandRemote. The development work is currently sponsored byFresha, andTidewave.

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 thedynamic()type, which can be used when the type of a variable or expression is checked at runtime. In the absence ofdynamic(), 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 thedynamic()type, which in Elixir is quite different from other gradually typed languages. Let’s break it down.

Thedynamic()type

Many gradual type systems have theany()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 calleddynamic()and it has two important properties: compatibility and narrowing.

In static type systems, when you have a type of shapeinteger() 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:

defpercentage_or_error(value)whenis_integer(value)dovalue_or_error=ifvalue>1dovalueelse"not well"end# ... more code ...ifvalue>1dovalue_or_error/100elseString.upcase(value_or_error)endend

Althoughvalue_or_errorhas typeinteger() or binary(), the operator/accepts only numbers, andString.upcaseaccepts 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/andString.upcaseare 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 thevalue_or_errorvariable above with the typedynamic(integer() or binary()), which means the type is eitherinteger() or binary()at runtime.

When calling a function with adynamic()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 aninteger()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=ifvalue>1dovalueelse"not well"endMap.fetch!(value_or_error,:some_key)

BecauseMap.fetch!expects a map data structure, andvalue_or_errorcan 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 onlyverified bugs.

However, reporting only verified bugs would not be useful if we can’t find many bugs in the first place. We addressed this problem by making sure Elixir’s dynamic type can be narrowed. Take this code:

defadd_a_and_b(data)dodata.a+data.bend

In the program above,datastarts as adynamic()type. We then use it asdata.aanddata.binside the plus operator, so Elixir will refine thedatavariable to have type%{..., a: number(), b: number()}, which implies it is a map with bothaandbfields with number values (and potentially any other field, hence the leading...). Therefore, if you were to forget to select the.bfield and write this:

defadd_a_and_b(data)dodata.a+dataend

datawould be first narrowed to a map of shape%{..., a: number()}, then attempted to be used as anumber(), which would emit a violation.

In other words, thedynamic()type in Elixir effectively works as a range, which can be refined as it is used throughout the program and reports violations whenever type checks fall outside of the range. This is a contrast to other gradual type systems, which use the dynamic type to discard all type information.

Behind the scenes, our type inference and type checking algorithms behave as if we annotated all argument types asdynamic(). Once we introduce user-supplied type annotations, Elixir’s type system will behave as any statically typed language as long asdynamic()is not used. And whenever you cross the static-dynamic boundary, wedeveloped new techniques that ensure our gradual typing is sound, without a need for additional runtime checks.

Typing guards, clauses, and more

Most of the work behind this release was to introduce type checking and narrowing to several constructs. Let’s see some of them.

When it comes to guards, we can infer unions, intersections, and negations:

defexample(x,y)whenis_list(x)andis_integer(y)

The code above correctly infersxis a list andyis an integer.

defexample({:ok,x}=y)whenis_binary(x)oris_integer(x)

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

defexample(x)whenis_map_key(x,:foo)

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

defexample(x)whennotis_map_key(x,:foo)

And the code above infersxis a map that does not have the:fookey, which has the type:%{..., foo: not_set()}. Hencex.foowithin the function body will raise a typing violation.

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

defexample(x)whentuple_size(x)<3

Elixir will correctly track the tuple has at most two elements, and therefore accessingelem(x, 3)will emit a typing violation. For maps and lists, we convert size checks into emptiness ones. In other words, Elixir can look at complex guards, infer types, and use this information to find bugs in our code.

When it comes to constructs such ascaseand conditionals, Elixir uses information from previous clauses to refine subsequent ones:

caseSystem.get_env("SOME_VAR")donil->:not_foundvalue->{:ok,String.upcase(value)}end

System.get_env("SOME_VAR")returns eithernilor abinary(). Because the first clause matches onnil, the type system knowsvaluecan no longer benil, and therefore it must only be abinary(), which allows the second clause to also type check without violations. Narrowing across clauses also helps the type system find redundant clauses and dead code in existing codebases.

Furthermore, we have typed many functions in the standard library that work with tuples and maps. You can find more details in therelease notes.

Compilation time improvements

Elixir v1.20 also improves compilation times once more, especially on applications running on machines with many cores.Even though BEAM languages are efficient to compile in general, our synthetic benchmarks now place Elixir’s build tool as the fastest among them. If you would like to contribute more examples and scenarios, please start a discussion so we can provide a transparent suite of benchmarks and results.

It also introduces a new compiler option called:module_definition, which specifies if the module definition should be:compiled(the default) or:interpreted. This may improve compilation times in large projects and it does not affect the.beamfiles written to disk, only how the contents insidedefmoduleare executed. You can enable it by settingelixirc_options: [module_definition: :interpreted]in yourmix.exs.Read the documentation to learn more.

What is next?

The biggest question ahead of us is: when will Elixir introduce new type signatures that leverage set-theoretic types? As recently discussedin my ElixirConf EU 2026 keynote, we still have both research and development work ahead of us. We will only introduce type signatures:

• if we are satisfied with the type system performance in Elixir v1.20 (and we have doneextensiveworkoptimizingit)
• if we can implement recursive types efficiently
• if we can implement parametric types efficiently
• if we can implement traversing key-value pairs of maps as an enumerable efficiently (we are still researching the possible solutions here)

Once those problems are tackled, we will start to explore and discuss typed struct definitions and finally type signatures. As usual, we will keep the community posted through news andin the Elixir Forum.

We appreciate everyone who tried the release candidates, ran benchmarks, and gave us feedback! Give Elixir v1.20 a try and remember to fix all of the bugs it will find for free!