Md Jamilur Rahman

Posted on Jun 14

Elixir v1.20 Just Dropped — And It Changed Everything

The 4-year bet on types finally paid off.

For years, the Elixir community had one big question hanging over it: when are we getting types?

Today, the answer arrived. Elixir v1.20 is officially released, and it makes Elixir a gradually typed language. No more guessing. No more type annotations required. Your existing code just got smarter — for free.

Let's break down what this means and why it matters.

The Backstory

Elixir was created by José Valim, the same person who announced this release. The language launched in 2012 on the Erlang VM. For over a decade, Elixir stayed dynamically typed. No int, no string, no type signatures — just pattern matching and runtime checks.

That changed in 2022, when the Elixir team publicly announced their effort to add set-theoretic types to the language. A year later, in June 2023, they published an award-winning paper on the type system's design. The work transitioned "from research to development."

Fast forward to June 3, 2026: the first milestone is complete.

What v1.20 Actually Does

Here's the core idea:

Every Elixir program is now automatically type checked.

Not partially. Not with opt-in annotations. Every line of code you write gets analyzed. If the compiler finds a bug that is guaranteed to fail at runtime, it tells you. These are called "verified bugs" — they aren't warnings or suggestions. They're certainties.

And it works without any type annotations. You don't have to add @spec or @type to your functions. The compiler figures out the types on its own.

How It Passes the "If T" Benchmark

The team submitted Elixir's type system to the "If T: Benchmark for Type Narrowing", a standardized test for how well type systems can figure out the shape of values as your code runs.

Elixir passes 12 out of 13 categories.

For comparison, many established typed languages struggle with this benchmark. Elixir's type system can recover precise type information from ordinary, dynamically-written code — no annotations needed.

A Real Code Example

Let's see what a verified bug looks like. Here's a function that returns either a number or a string:

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

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

In a traditional typed language, this would trigger two false positives. The / operator expects only numbers, and String.upcase expects only strings. The variable value_or_error is both types, so both calls look wrong.

But the program is actually correct! The if checks guarantee that each branch uses the right type.

Elixir's type system handles this elegantly. It tags value_or_error as dynamic(integer() or binary()). When the types overlap with what's accepted, no violation is reported. Zero false positives.

Now imagine someone accidentally writes:

String.upcase(value_or_error)

without the if guard. The type checker knows integer() and String.upcase are disjoint — they share nothing. It flags a verified bug. This will fail at runtime, guaranteed.

That's the sweet spot: catch the real bugs, stay silent on the valid code.

Why `dynamic()` Is the Secret Weapon

Most gradual typed languages use an any() type. It basically says "I give up, anything goes." You turn off the type checker in those spots. Not great.

Elixir does something different. Its gradual type is called dynamic(). It has two key properties:

1. Compatibility

When you have a value of type dynamic(integer() or binary()), the type checker doesn't panic. It knows this value could be either type at runtime. So it only flags a violation if the types are completely disjoint — meaning there's zero overlap.

Example: You have a variable that might be a number or a string. You use it with / (which only takes numbers). If the variable could be a number at runtime, Elixir stays quiet. No false positive. But if you pass it to Kernel.halt() (which takes atoms), Elixir flags it — because numbers and atoms have no overlap.

2. Narrowing

This is the clever part. When you use if, case, or pattern matching on a dynamic() type, Elixir narrows the type. After an if value > 1 check, the variable is now known to be integer(). No false positives downstream.

This means your code gets more precise the more you branch. The type system follows your logic.

Binary Decision Diagrams Under the Hood

Here's a fun technical detail. Elixir's set-theoretic types are implemented using Binary Decision Diagrams (BDDs) — a data structure from computer science that efficiently represents Boolean functions. Types like integer() or binary() are encoded as BDD nodes, and set operations (unions, intersections, negations) become graph operations.

The team published multiple blog posts in 2025 about optimizing these BDDs. They used techniques called "Lazy BDDs with Eager Literal Intersections" and "Lazy BDDs with Eager Literal Differences" to make the type checker fast enough for real-world use.

This matters because type checking a large codebase needs to be fast. No one will use a type system that adds 30 seconds to every compile. The BDD optimizations keep Elixir's compile times reasonable.

Why Not Just Use a Type Annotation System?

You might wonder: why not just copy TypeScript's approach and require type annotations?

Elixir's team considered this. Their argument:

Annotations are overhead. Requiring @spec for every function slows down development. Many Elixir developers value the language's dynamic feel.
Most existing code has no annotations. If the type system only works with annotations, it's useless for legacy codebases. Elixir has thousands of packages with zero type specs.
Gradual typing bridges the gap. The dynamic() type lets you mix typed and untyped code seamlessly. You can add annotations later, at your own pace.

This approach means the type system works today — not after everyone rewrites their code.

What Makes It Different from Other Typed Languages

Feature	Elixir	TypeScript	Python (mypy)
Annotations required?	No	Yes (mostly)	Yes
Gradual by design?	Yes (`dynamic()`)	Yes (`any`)	Yes (`Any`)
False positive control	Disjoint check	Inferred	Strict mode
Verified bugs	Yes	No	No
Underlying model	Set-theoretic (unions, intersections, negations)	Structural	Nominal

The big difference: Elixir's type system uses set-theoretic types. Types are built from unions, intersections, and negations — like sets in math. This makes the model both powerful and composable.

Who's Paying for This?

The type system was built through a partnership between:

CNRS (French National Centre for Scientific Research) — academic muscle
Remote (a global HR company) — real-world use cases

Current development is sponsored by:

Fresha (beauty industry platform)
Tidewave (a new Elixir-focused company)

This is one of the most significant open-source type system efforts funded by actual companies using the language in production.

The Journey: 4 Years from Idea to Release

Year	Milestone
2022	Set-theoretic types announced
2023	Award-winning paper published; transition to development
2024	Type checking of function calls, LSP listeners, built-in JSON
2025	Type checking of protocols, anonymous functions; 4x faster compilation
2026	Full gradual type inference on all programs

Each release added more capabilities. v1.18 checked function calls. v1.19 checked protocols. v1.20 checks everything.

What Other Languages Can Learn

TypeScript made gradual typing mainstream. Python followed with mypy and Pyright. Ruby has Sorbet. Go is slowly adding types.

But most of these bolted types onto existing languages with minimal redesign. Elixir took a different path: four years of academic research before writing a single line of production code.

The result is a type system that feels native to the language. It doesn't fight Elixir's dynamic nature. It works with pattern matching, guards, and the Erlang VM's process model.

Other language teams should study this approach. Types aren't just about adding annotations. They're about understanding your language's semantics deeply enough to make the type system fit.

What This Means for Elixir Developers

For existing codebases

Zero changes needed. The compiler now type checks your code automatically. You'll start seeing warnings about dead code and verified bugs you didn't know about.

For new projects

You get the flexibility of a dynamic language with the safety of a typed one. Pattern match on types without writing type specs. The compiler catches your mistakes.

For the ecosystem

Library authors can start adding @spec annotations to their public APIs. This doesn't change behavior — it just makes the type checker more precise.

The Bigger Picture

This is a huge deal for the Erlang VM ecosystem.

Erlang has always been about "let it crash" — fault tolerance through process isolation, not type safety. Adding types to Elixir doesn't replace that philosophy. It complements it. You get:

Process-level fault tolerance (from Erlang)
Compile-time bug detection (from the new type system)
Zero annotation overhead (from gradual typing)

This is exactly what José Valim described in his 2023 paper: types that are sound (they mean what they say), gradual (you can opt in over time), and developer friendly (clear errors, no noise).

The HN Reaction

The release hit Hacker News with 300 points and 90 comments within hours. The community reaction was overwhelmingly positive:

Many developers shared stories of bugs that would have been caught by the new type system
Questions about IDE support and editor integration came up frequently
Some wondered if this would finally push Elixir into mainstream adoption
Others asked about performance impact — the team confirmed compile times stay fast

The top comment summed it up: "Elixir's team did types the right way. Research first, implementation second."

My Take

This is one of the most thoughtfully executed type system rollouts I've seen.

Most languages bolt on types and immediately break half the ecosystem. Elixir's approach — four years of research, careful dynamic() semantics, verified bugs instead of fuzzy warnings — shows they learned from everyone else's mistakes.

The fact that it passes 12/13 categories on the "If T" benchmark on day one is remarkable. That's not a toy type system. That's production-grade inference.

If you've been on the fence about Elixir, this release is the sign you were waiting for.

What Comes Next

The Elixir team isn't done. Their roadmap includes:

More precise type inference — catching even more bugs without annotations
Better error messages — pointing you to exactly what went wrong and how to fix it
IDE integration — autocomplete, go-to-definition, inline type info
Optional type annotations — when you want to be more explicit about your API's contract

The v1.20 release is the foundation. The next releases will build on it.

If you're an Elixir developer, now is the time to update. Run mix deps.update --all and see what the type checker finds. You might be surprised.

If you're not an Elixir developer, this release is worth watching. Elixir just became one of the most type-safe dynamic languages in existence. That's a big claim, and they've got the benchmarks to back it up.

Elixir v1.20 is available now. Install it with asdf, mise, or from the official download page.

Written June 3, 2026.

DEV Community

Elixir v1.20 Just Dropped — And It Changed Everything

Elixir v1.20 Just Dropped — And It Changed Everything

The Backstory