Elixir is now gradually typed. Nobody wrote a single annotation.

On June 3, Jose Valim published a release announcement with a headline most language maintainers would not dare to write: "Elixir v1.20 released: now a gradually typed language." The claim is precise. From v1.20, the compiler infers types for every Elixir program and gradually type checks it, and the amount of code anyone had to change to make that true is zero. No annotations. No new syntax. No strict-mode flag, no pragma at the top of the file, no migration guide.

Compare that to how every other dynamic language got types. TypeScript asked the JavaScript ecosystem to rewrite itself in annotations, and the ecosystem spent a decade doing it. Python standardized type hints with PEP 484 back in 2015 and is still arguing about coverage. Ruby put its types in sidecar RBS files. Elixir looked at all of that and made a different bet: the types were already in the code. The compiler just had to learn to read them.

Four years of slow walking

The v1.20 release is the end of the first milestone in a project that started in 2022, when the Elixir team announced an effort to add set-theoretic types to the language. In June 2023 the design landed as a research paper, "The Design Principles of the Elixir Type System," written by Giuseppe Castagna and Guillaume Duboc of IRIF (Universite Paris Cite and CNRS) together with Valim. It was published in The Art, Science, and Engineering of Programming and picked up an award along the way. The work has been funded the whole time: a partnership between CNRS and Remote got it started, and Fresha and Tidewave sponsor development today.

What followed was a deliberately slow rollout, one inference capability per release.

The v1.17 release notes were almost apologetic about scope: "The Elixir typechecker only infers types from patterns within the same function at the moment." Eighteen months later, v1.18 still carried the caveat that "the current implementation does not perform type inference of guards yet," which mattered because guards are where Elixir code states its types most explicitly. v1.20 closes that gap. The checker now extracts types from every guard form, including compound ones:

def example(x, y) when is_list(x) and is_integer(y)
def example({:ok, x} = y) when is_binary(x) or is_integer(x)
def example(x) when is_map_key(x, :foo)
def example(x) when tuple_size(x) < 3

Each of those guards was always a runtime type test. The BEAM executed them on every call. What changed in v1.20 is that the compiler now reads them as type declarations too, which is the entire thesis of the project in miniature: Elixir code was full of type information before the type system existed.

The team has been explicit about why the rollout took four releases. In the v1.20 announcement, Valim writes that "if Elixir were to introduce too many false positives in existing codebases, it would quickly erode the trust in the type system." Each release shipped inference against the entire ecosystem's existing code and had to hold to what the team calls an extremely low false positive rate before the next capability landed.

How you type a program nobody annotated

The core trick is the dynamic() type, and it behaves differently from the escape hatches in other gradual systems. TypeScript's any switches type checking off: once a value is any, you can call anything on it and the compiler stays silent. Elixir's dynamic() stays on the record. The announcement describes the rule precisely: "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."

Disjointness is a high bar, and it is the load-bearing design decision. The checker does not complain when a value might be wrong. It complains when no possible runtime value could ever be right. The team calls the resulting findings verified bugs: "typing violations that are guaranteed to fail at runtime if executed." That framing inverts the usual gradual typing pitch. Instead of "we will catch most of your mistakes and occasionally cry wolf," it is "we will only speak when we can prove the crash."

A checker that only reports certainties would be useless if it could rarely be certain, so the second half of the design makes dynamic() narrowable. It behaves like a range that tightens as the program tests the value:

case System.get_env("SOME_VAR") do
  nil -> :not_found
  value -> {:ok, String.upcase(value)}
end

System.get_env/1 returns a string or nil. The first clause consumes nil, so in the second clause the checker knows value is a string and the String.upcase/1 call is safe. v1.20 extends this narrowing across clauses, through case, cond, and with, and into data structures. Map types now track key domains beyond atoms, so the checker can represent a map as %{integer() => binary(), float() => :ok}, and operations like Map.put/3 and Map.delete/2 propagate what they did to the keys into the inferred type downstream.

Multi-clause functions get intersection types rather than union types. A function with one clause for integers and one for booleans has the type (integer() -> integer()) and (boolean() -> boolean()): it is both functions at once, and call sites get checked against the clause they would actually hit. That is a direct payoff of building on set-theoretic types, where types are sets and unions, intersections, and negations are first-class operations.

The road TypeScript did not take

Hold Elixir's approach next to the annotation-first model and the trade becomes visible. TypeScript is the most successful gradual type system ever shipped, and it got there by making annotation the unit of adoption: you annotate a file, a function, a package boundary, and the checker trusts what you wrote. The ecosystem produced DefinitelyTyped, thousands of packages' worth of .d.ts files, and an entire job category of keeping them honest. The cost shows up at scale. We covered how the TypeScript compiler had to be rewritten in Go because checking all those annotations across large graphs stopped fitting in JavaScript's performance envelope, and migrating to TypeScript 7 is its own project precisely because so much tooling grew roots into the old compiler API.

TypeScript also chose unsoundness on purpose. Its design goals document lists, under non-goals, "apply a sound or 'provably correct' type system," opting instead to "strike a balance between correctness and productivity," because soundness would have rejected too much idiomatic JavaScript. Elixir went the other way: the system is sound, meaning the inferred types are guaranteed to describe what the program actually does. The catch is what soundness costs when you refuse annotations, and we will get to it.

The prior art objection comes from inside the BEAM house, and it is fair. Erlang already ships Dialyzer, and the official docs describe the same philosophy: it "bases its analysis on the concept of success typings, ensuring sound warnings without false positives." On paper that is exactly the v1.20 pitch. In practice, the Hacker News thread on the release filled with Elixir veterans reporting that Dialyzer cries wolf anyway, particularly around protocols and circular dependencies, and several said they had quietly dropped it from CI. Dialyzer also runs as a separate pass over compiled BEAM files, with its own cache to warm and its own error vocabulary. The new type checker lives inside the compiler, runs on every build, and reports in terms of the source you wrote. Same philosophy, different delivery, and delivery was most of the problem.

There is one independent yardstick. The If-T benchmark, published in 2025 by Hanwen Guo and Ben Greenman at the University of Utah, tests type narrowing behavior across thirteen categories of programs, from simple positive refinement through tuple lengths, aliases, and custom predicates. It has implementations for TypeScript, Flow, mypy, Pyright, and Typed Racket, among others. The Elixir team reports that v1.20 passes twelve of the thirteen categories. The announcement does not say which category fails, and self-reported scores deserve the usual discount, but the relevant point survives either way: a checker with zero annotations is competitive at narrowing with systems that have had annotations to lean on for a decade.

One more contrast worth drawing. In the TypeScript world, static types stop at the network boundary, which is why runtime validators grew into their own ecosystem with their own standards war. Elixir's types are extracted from constructs the VM actually executes: pattern matches and guards run at runtime whether or not the type checker exists. The boundary problem does not disappear, but the same mechanism that types the inside of the program is the one validating the outside.

What inference-first gives up

The honest version of the v1.20 story includes three real costs.

The first is detection power. The disjointness rule means the checker only flags a call when the supplied types and accepted types share no overlap at all. The documentation is candid that inference is best-effort: it finds bugs where every possible type combination fails, and it does not promise to find incompatibilities that annotations would have exposed. A function that accepts a string or an integer, called with a value that is a string or an atom, passes the check because the string case overlaps. An annotation-first system with a declared parameter type would have asked harder questions. Fewer false positives, bought with more false negatives. That is not a flaw in the implementation. It is the price of the design.

Intent is the second cost. Annotations are not just constraints for the checker; they are documentation, API contracts, and a way to say what a function is for rather than what its body happens to accept. Elixir cannot express that yet. Type signatures are the next phase of the project, and the announcement names the unsolved problems standing in the way: recursive types, parametric types, and efficiently traversing the key-value pairs of maps as enumerables. The January roadmap post puts typed structs around v1.21, expected near the end of 2026, and signatures around v1.22 in 2027. Until then, the inferred type of your public API is whatever your implementation implies, and refactoring the body can silently change the contract.

Scope is the third. The gradual guarantee is also bounded by where dynamic() is allowed to appear: only at the root of a type. Write {:ok, dynamic()} and the system rewrites it to dynamic({:ok, term()}), which keeps gradualness from leaking into the interior of otherwise static types. And the BEAM's defining feature sits outside the system entirely. Processes receive any message any sender throws at their mailbox, and commenters in the release thread were quick to note that typing message passing would require rethinking the architecture, not extending the checker. OTP behaviors paper over some of this in practice. None of it is typed today.

Whether all this matters is a live argument in the community rather than a settled question. Several long-time Elixir developers in the release discussion said they have run production systems for a decade without feeling the absence of static types, crediting immutability and pattern matching for keeping type errors rare. Valim himself pushed back on maximalist readings of the release, arguing in the thread that type systems restrict which programs you can express, are not the only mechanism for correctness, and do not replace tests. It is an unusual posture: a language author shipping a type system while talking down type systems. It is also consistent with a project that spent four years making sure nobody would be forced to care.

What you actually get on upgrade day

For a team running Elixir in production, v1.20 is a low-drama upgrade with a real payoff. The requirements: Erlang/OTP 27 or later, with support through OTP 29. The new checks arrive as compiler warnings, not errors, so CI does not break on day one; whether to promote them with --warnings-as-errors is your call after you have seen what they say about your codebase.

The typing work also rode alongside a multi-release compilation speed push. v1.19 introduced lazy module loading, which the team reported made compilation more than twice as fast on some large projects, and parallel dependency compilation behind the MIX_OS_DEPS_COMPILE_PARTITION_COUNT environment variable, where some users reported up to 4x improvements. v1.20 continues the trend and adds a :module_definition compiler option. The default, :compiled, behaves as before. Setting it to :interpreted via elixirc_options: [module_definition: :interpreted] speeds up compilation on machines with many cores, in exchange for less precise stacktraces in code executed during module definition and a 20-argument limit on anonymous functions inside defmodule. For most projects the default is right; the interpreted mode is for monorepos with build farms.

More important than the mechanics: v1.20 is the end of the free part. Everything the type system has delivered so far cost users nothing, and that was the point of the milestone. The next two phases, typed structs and then signatures, will ask developers to write types for the first time, and the team has scheduled roughly fifteen months to get there. That is when the design meets its real test: whether a community that just learned it never needed annotations will want to write them anyway, and whether signatures can land with the same restraint as inference did.

For everyone outside the BEAM, the experiment is worth watching for a different reason. Elixir just demonstrated that a dynamic language can become gradually typed without an annotation-shaped migration, given pattern matching, guards, immutability, and four years of research funding. Most dynamic languages have at most two of those. If the 2027 signature work sticks the landing, the inference-first path stops being an Elixir curiosity and becomes the standard against which every future "we are adding types" announcement gets judged.