Split View: Elixir 1.20의 점진 타입 시스템 — 어노테이션 없이 "검증된 버그"를 찾는다는 것의 실제

Elixir 1.20's Gradual Type System — The Reality of Finding 'Verified Bugs' Without Annotations

• Introduction — The First Milestone, Closed After Four Years
• Where dynamic() Differs From any()
• What 1.20 Actually Adds
• Checking "12 of 13" Against the Primary Source
• Compile Time — How Big Is the "Fastest" Claim, Really
• What Isn't Free
• What to Know Before Upgrading
• Why Type Signatures Are Still Far Off
• So What Should You Do Now
• Closing
• References

Introduction — The First Milestone, Closed After Four Years

The Elixir team announced it would bring set-theoretic types into the compiler back in 2022. In 2023, Giuseppe Castagna, Guillaume Duboc, and José Valim laid out the design in The Design Principles of the Elixir Type System, declaring that the project was moving "from research to development." Then on June 3, 2026, Elixir v1.20 shipped, closing out that first milestone.

The milestone can be summed up like this — perform type inference and gradual type checking on every Elixir program without introducing a single type annotation. That means the compiler finds dead code and "verified bugs" without you changing a line of code. Per the announcement's own definition, a verified bug is a typing violation guaranteed to fail at runtime if the code executes.

This post strips away the hype and looks at three things: (1) what 1.20 actually adds, (2) what survives once the announcement's numbers are checked against primary sources, and (3) tradeoffs documented in the docs but absent from the announcement. The broader ecosystem landscape around Elixir 1.18 and OTP 27/28 is already covered in Modern Elixir & Phoenix 2026 and Modern Erlang and BEAM 2026, so this post digs into the type system alone.

Where dynamic() Differs From any()

Per the official docs, the Elixir type system has three goals — soundness: the inferred and assigned types match what the program actually does at runtime. Graduality: there is a dynamic() type, and without it the system behaves like a static type system. Developer-friendliness: types are described with the basic set operations — union, intersection, negation (hence "set-theoretic").

The key piece here is dynamic(). In many gradual type systems, any() means "anything goes at all" from the type system's point of view, so it never reports violations. Elixir's dynamic() is different. In the announcement's own terms, it has two properties — compatibility and narrowing.

Start with compatibility. Here is the announcement's own example, carried over unchanged.

def percentage_or_error(value) when is_integer(value) do
  value_or_error =
    if value > 1 do
      value
    else
      "not well"
    end
  # ... more code ...
  if value > 1 do
    value_or_error / 100
  else
    String.upcase(value_or_error)
  end
end

value_or_error is either an integer or a binary. / only accepts numbers, and String.upcase only accepts binaries. A strict static type system would report two violations here. Yet this program never raises an exception at runtime. It's a false positive that arises because the type system fails to precisely capture the program's intent.

Elixir attaches the type dynamic(integer() or binary()) to this variable. And when a dynamic()-typed value is passed to a function, Elixir only raises a violation when the supplied type and the accepted type are disjoint. Even though / only accepts numbers, dynamic(integer() or binary()) could be an integer, so it's not disjoint — no violation. Now change the code to this:

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

Map.fetch!(value_or_error, :some_key)

Map.fetch! expects a map, but at runtime this value can only ever be an integer or a binary. That's disjoint, so it's a violation. This is the basis for Elixir's claim that it reports "only verified bugs."

But reporting only verified bugs while catching hardly any bugs wouldn't be useful. That's where narrowing comes in.

def add_a_and_b(data) do
  data.a + data.b
end

data starts as dynamic(), but seeing data.a and data.b used in an addition narrows it to %{..., a: number(), b: number()} (the leading ... means other keys are allowed). So if you drop .b and write data.a + data, data was already narrowed to a map, and then it's used as a number — that's a violation.

In one line — Elixir's dynamic() behaves like a range, narrows as it's traced through the code, and raises a violation only when a type check falls outside that range. That's the opposite direction of how other gradual type systems discard type information with their dynamic type.

What 1.20 Actually Adds

Based on the CHANGELOG, here's what's new in 1.20.

Guard inference. This was the last missing piece for this release.

def example(x, y) when is_list(x) and is_integer(y)
# x is a list, y is an integer

def example({:ok, x} = y) when is_binary(x) or is_integer(x)
# x is a binary or an integer, y is a 2-element tuple starting with :ok

def example(x) when is_map_key(x, :foo)
# x is a map with the key :foo -> %{..., foo: dynamic()}

def example(x) when not is_map_key(x, :foo)
# x is a map without the key :foo -> %{..., foo: not_set()}
# so x.foo in the function body is a typing violation

def example(x) when tuple_size(x) < 3
# the tuple has at most 2 elements -> elem(x, 3) is a violation

The fact that negation (not is_map_key) is represented with a type called not_set() is exactly what you'd expect from a set-theoretic type system. Size checks on maps and lists get converted into "is it empty" checks.

Whole-function-body inference. Through 1.18, inference only happened on patterns. Now it looks at the body too.

def sum_to_string(a, b) do
  Integer.to_string(a + b)
end

+ accepts both integers and floats, but because the result flows into a function that requires an integer, both a and b are inferred to be integers. Information now flows backward.

Cross-clause inference and occurrence typing. case, cond, and with now have occurrence typing, where earlier clauses narrow later ones.

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

System.get_env/1 returns either nil or a binary. Since the first clause already caught nil, value can only be a binary, so String.upcase passes without a violation. As a bonus, this also produces redundant clause warnings.

Cross-dependency inference. This is the CHANGELOG's "Perform type inference across applications" item. Before 1.20-rc, types were only inferred from calls to standard library functions — calling into your own dependency modules only got type-checked, not inferred. Now, type information inferred from your dependencies flows into the inference for your own app. This change dramatically increases the volume of type information flowing through the compiler, and the Elixir team said in its January 2026 roadmap post that it dedicated an entire release candidate to this step alone.

In fact, 1.20 went through seven release candidates (rc.0 through rc.6). rc.0 landed January 9, 2026; rc.6 landed May 21; the final release landed June 3. The January roadmap post had projected the final release for "May," so it slipped by about a month — a fair result for a full rollout of a type system.

Checking "12 of 13" Against the Primary Source

The most eye-catching figure in the announcement is this:

our implementation performs well in the "If T: Benchmark for Type Narrowing" benchmark. Elixir passes 12 of the 13 categories

If-T is a real third-party benchmark. It was built by Hanwen Guo and Ben Greenman (arXiv:2508.03830) and lives in the University of Utah PLT group's utahplt/ifT-benchmark repository. It measures type narrowing (occurrence typing), pairing a program that "should pass type checking" with one that "should not" for every topic. There are exactly 13 categories — positive, negative, connectives, nesting_body, struct_fields, tuple_elements, tuple_length, alias, nesting_condition, merge_with_union, predicate_2way, predicate_1way, predicate_checked.

But the link the announcement attaches to this sentence points to the repository's Benchmark Results table. Open that table, and there is no Elixir column.

As of today (2026-07-16), here's what I confirmed: the upstream results table covers 11 type checkers — Typed Racket, TypeScript, Flow, mypy, Pyright, Sorbet, Luau, MLsem, Typed Clojure, ty, and Pyrefly. The repository tree (106 entries) has language directories for only those same 11 — no Elixir directory. A case-insensitive search of the full README for "elixir" returns zero hits, and there is no PR, open or closed, proposing to add Elixir.

So, stated precisely — "12 of 13" is the Elixir team's own self-reported measurement, and the results table the announcement links to does not back that number. That doesn't mean it's wrong. It means there is no reproducible implementation posted upstream, so a third party can't verify it. Which single category failed has also never been disclosed (some search summaries float a specific category, but since no primary source confirms it, this post won't cite one).

For context, here are the actual upstream numbers, which help calibrate where the self-reported figure sits.

Upstream If-T results table (utahplt/ifT-benchmark, v1.1) — out of 13 categories
  Typed Clojure : 13/13  (passes every category)
  Typed Racket  : 12/13  (fails tuple_length)
  MLsem         : 12/13  (fails connectives)
  Flow          : 11/13
  Pyright       : 11/13
  TypeScript    : 10/13  (fails nesting_condition, predicate_1way, predicate_checked)
  mypy          :  9/13

  Elixir        : not in the table (announcement's self-reported 12/13)

If 12/13 holds up, it puts Elixir on par with Typed Racket and ahead of TypeScript. Getting that level of narrowing precision out of code with zero annotations would genuinely be impressive. But as things stand, the accurate label is: self-reported by the authors, with conditions and the failing category undisclosed, and unverifiable against the linked table.

Compile Time — How Big Is the "Fastest" Claim, Really

The announcement makes one more claim: "in our synthetic benchmark, Elixir's build tooling is now the fastest among BEAM languages."

The basis is José Valim's own repository, josevalim/langcompilebench. It's a self-reported measurement, and the repository itself states these are "synthetic benchmarks." What's measured is the time to compile 100 independent modules, each with 100 hello-world functions, boot the application, and run a minimal test suite. Conditions: a MacStudio M1, averaged over 5 runs.

On Erlang/OTP 28
  Elixir v1.19                        ~0.73s
  Elixir v1.20                        ~0.63s
  Elixir v1.20 (interpreted defmodule) ~0.58s
  Erlang (rebar3)                     ~0.72s
  Gleam v1.14                         ~0.71s

On Erlang/OTP 29
  Elixir v1.19                            ~0.65s
  Elixir v1.20-rc.2                       ~0.55s
  Elixir v1.20-rc.2 (interpreted defmodule) ~0.50s
  Erlang (rebar3)                         ~0.64s
  Gleam v1.14                             ~0.67s

Read the numbers at face value: going from 1.19 to 1.20, 0.73s became 0.63s, ahead of Erlang's 0.72s and Gleam's 0.71s. That's true. It's equally true that the whole job takes roughly 0.7 seconds and the gap is around 0.1 seconds. And this workload is a pile of hello-world functions, not real code — there's nothing here substantial enough to put real weight on the type checker.

The most honest thing to do is carry over, unchanged, the caveat the author himself attached to the repository.

Of course, this doesn't mean that an Elixir project of the same size will compile faster than an equivalent Gleam or Erlang project — there are more variables than raw compiler performance. (…) In theory, rebar3 should be the best performer of the three.

Switch to incremental compilation, and the ranking flips entirely. Per the same repository's own analysis, what matters is whether a language can separate inter-module dependencies into compile-time versus runtime. Erlang — aside from the rarely-used parse transform — has only runtime dependencies, which makes it the best performer here on incremental builds. Change one file, and only that file gets recompiled. Gleam treats every dependency as compile-time, making it the worst. Elixir sits in between.

langcompilebench summary table
  Language | Dependency kind         | Cycles allowed | Expected recompilation per change
  Erlang   | Runtime only            | Yes             | Lowest
  Elixir   | Runtime + compile-time  | Yes             | Medium
  Gleam    | Compile-time only       | No              | Highest

So the "fastest" claim is scoped to clean-build synthetic benchmarks — and the same repository's own conclusion is that Erlang is ahead on the incremental builds you actually feel day to day during development. That's context you'd miss reading the announcement alone.

What Isn't Free

These are tradeoffs written into the docs but absent from the announcement.

dynamic always sits at the root. As the official docs explain, if you write a tuple like {:ok, dynamic()}, Elixir rewrites it as dynamic({:ok, term()}). The docs state the downside explicitly — you can't make part of a tuple, map, or list gradual; the whole thing becomes gradual. In exchange, dynamic is always explicitly visible at the root, which is presented as a benefit — it stops dynamic from silently creeping into a statically-typed program. It's a deliberate design decision, but it clearly trades away precision.

Struct updates raise violations by design. Here's the docs' own example.

user = find_user_by_id(42)
%User{user | name: "John Doe"}

Even if find_user_by_id always returns a User struct at runtime, if the type system can't prove that statically, it raises a typing violation. In the docs' own words, "this is how struct updates are designed to work." The fix is to match the variable when you define it.

%User{} = user = find_user_by_id(42)
%User{user | name: "John Doe"}

The announcement's claim of "an extremely low false-positive rate" is a vendor self-assessment with no number attached, and it should be read alongside the fact that spots like this still require you to reshape your code.

Interpreted defmodule has a cost. The module_definition: :interpreted option, which produced the fastest numbers in the benchmark above, only gets its upside mentioned in the announcement — the CHANGELOG lists the downsides.

• Stack traces for errors raised during compilation can become less precise
• Anonymous functions inside defmodule can take at most 20 arguments (functions defined with def and friends still support up to 255)

The default is :compiled; to turn this on, add elixirc_options: [module_definition: :interpreted] to mix.exs. The .beam file itself doesn't change — only the way the inside of defmodule gets executed.

What to Know Before Upgrading

OTP requirement. 1.20 requires Erlang/OTP 27 or later and is compatible with OTP 29. If you're stuck on OTP 26 or earlier, 1.20 isn't an option at all.

The security patch only exists in 1.20. 1.20.1 (June 9, 2026) fixed CVE-2026-49762 (GHSA-w2h8-8x3g-278p, severity medium, published by the Erlang Ecosystem Foundation). The issue is unbounded integer parsing in the Version module. Numeric components of a version string were converted to integers with no length limit, so a single, all-numeric, sufficiently large component triggers a superlinear, non-yielding conversion that pins down a BEAM scheduler — and larger still, kills the process with a SystemLimitError. Per the OSV entry, a single string of about 1 megabyte is enough, and no authentication is required. The reachable paths are Version.parse/1, Version.parse!/1, Version.match?/3, Version.compare/2, and Version.parse_requirement/1 — any app that calls these on untrusted input, like HTTP parameters or package metadata, is affected. The fix caps the numeric component at 14 decimal bytes.

The important part here — the affected range is everything from 1.5.0 up to, but not including, 1.20.1. But checking the releases, everything shipped after June 9, 2026 is only 1.20.1 and 1.20.2 — there's no v1.19.6 or v1.18.5 tag. In other words, the only way to get the fix for this vulnerability is to move up to 1.20.1 or later. If you plan to stay on 1.19 or below, the Elixir team's own recommendation is to cap the size of data you pass to the Version module yourself.

Hard deprecations. These start actually emitting warnings in 1.20.

• File.stream!(path, modes, lines_or_bytes) → argument order changed to File.stream!(path, lines_or_bytes, modes)
• Matching a size inside a bit pattern now requires the pin operator: <<x::size(^existing_var)>>
• Kernel.ParallelCompiler.async/1 → Kernel.ParallelCompiler.pmap/2
• The Logger.*_backend functions → the handler-based approach (keep using backends via the :logger_backends package)
• Logger.enable/1, Logger.disable/1 → Logger.put_process_level/2, Logger.delete_process_level/1
• xref: [exclude: ...] in mix.exs → elixirc_options: [no_warn_undefined: ...]

Two potentially breaking changes. Raw CR line breaks after ? inside strings and comments are now disallowed for security reasons, and require SomeModule no longer expands to that module at compile time (it still returns the module at runtime, unchanged). The CHANGELOG specifically calls out the latter because code like require(SomeMod).some_macro() can break.

Why Type Signatures Are Still Far Off

The question everyone actually wants answered — when can you use compiler-enforced type signatures instead of @spec?

The announcement sets four conditions. Type signatures ship only once all of these are met:

1. The team is satisfied with 1.20's type-system performance
2. Recursive types can be implemented efficiently
3. Parametric types can be implemented efficiently
4. Iterating over a map's key-value pairs as an enumerable can be implemented efficiently — the announcement explicitly states this one is still an open research problem

So what's left isn't just engineering — it's unsolved research. The January roadmap post said these problems would be explored in v1.21 (November 2026) and v1.22 (May 2027), and it laid out, in its own words, two risks that could make the type system turn out impractical — ergonomics (every improvement so far has happened behind the scenes with no language changes, and the impact on developer experience hasn't been evaluated yet) and performance (the current implementation doesn't support recursive or parametric types, and they could directly hurt performance).

Here's the order of the remaining milestones. Second is typed structs — natively defining types for struct fields and propagating them across the codebase. Third is set-theoretic type signatures.

And there's a quietly big piece of news here. Stated explicitly in the official docs — existing Erlang Typespecs aren't precise enough for set-theoretic types, so once this phase wraps up, they'll be phased out of the language, with post-processing moved into a separate library. If your codebase has invested heavily in @spec, a migration is coming eventually. No timeline has been set.

So What Should You Do Now

When it's fine to upgrade. If you're on OTP 27+ and the deprecation list above is manageable, there's plenty of reason to move up. Type checking isn't opt-in — it's just on, and you don't have to touch your code. What you get is close to free. And since the Version CVE fix only exists in 1.20.1+, if your app passes external input into the Version module, upgrading is effectively a security matter.

When there's no rush. If you've been waiting to use type signatures, 1.20 isn't that. It's at least v1.21 (November 2026), realistically later, and it could slip further if the research problems don't get solved. Typed structs aren't here yet either. And if you're stuck on OTP 26 or earlier, you can't upgrade at all.

Set your expectations correctly. What 1.20 finds is violations that are "guaranteed to blow up if executed" and dead code. It doesn't prove your types are correct. With no annotations, the compiler only knows what it can infer from the code, and ambiguous spots stay dynamic(), flagged only when disjoint. If you've used Dialyzer, this territory will feel familiar — the difference is that Elixir 1.20 is built into the compiler, with no separate run or PLT build.

If warnings pour in after you upgrade, most of them are probably real bugs. That's what the announcement's closing line means — "give Elixir v1.20 a try, and don't forget to fix all the bugs it finds you for free."

Closing

To sum up: Elixir 1.20 really did close out the first milestone of the type-system work that began in 2022, and it's genuine — every program gets gradually type-checked with no annotations, dynamic() narrows through the code instead of discarding type information, and inference now flows across guards, function bodies, clauses, and dependencies. The cost is basically just the upgrade itself.

At the same time, two of the announcement's numbers shrink once checked against the source. If-T's "12 of 13" is a self-reported figure with no Elixir column at all in the linked upstream table, and the "fastest compiler" claim is a 0.1-second gap on a 0.7-second hello-world synthetic benchmark from the author himself — and on incremental builds, that same repository puts Erlang ahead. Neither claim is false, but both are smaller than the impression you'd get from the announcement alone.

And the thing people actually want — type signatures and typed structs — is still more than a year out, sitting behind unsolved research problems that the Elixir team itself admits "could turn out to be impractical." That honesty is part of why this project has kept people's trust for four years running.

References

• Elixir v1.20 released: now a gradually typed language (2026-06-03, José Valim)
• Elixir v1.20 CHANGELOG (primary source)
• Type inference of all constructs and the next 15 months (2026-01-09) — roadmap and RC schedule
• Gradual set-theoretic types — official docs (v1.20.2)
• The Design Principles of the Elixir Type System — Castagna, Duboc, Valim (Programming journal, 2024, Vol. 8, Issue 2, Article 4)
• If-T: A Benchmark for Type Narrowing — Guo, Greenman (arXiv:2508.03830)
• utahplt/ifT-benchmark — upstream benchmark and results table
• josevalim/langcompilebench — synthetic compile-time benchmark for BEAM languages
• CVE-2026-49762 / GHSA-w2h8-8x3g-278p — unbounded integer parsing in the Version module
• Modern Elixir & Phoenix 2026 — ecosystem landscape (related post)
• Modern Erlang and BEAM 2026 — OTP and runtime (related post)