This English version is an AI translation of my original article on Qiita (in Japanese).

About this article

On June 3, 2026, Elixir 1.20 shipped with a type system. But it aims at something a little different from the type systems we are used to, the ones where you write types to buy safety.

This article started from my own questions, which I worked through with an AI agent. We went to primary sources (the official blog, the docs, the paper), and in the end I installed Elixir 1.20 and checked how the type checker actually behaves. I may still have gotten things wrong, so if you notice anything, I would be glad to hear it in the comments.

What the type system aims for: soundness

First, the word sound. In type systems, a type system is sound when, if it says a value has some type, you will not get a type error of that kind at runtime. The opposite, unsound, means a program can type-check and still hit a type error when it runs.

Making a dynamic language fully sound is hard. TypeScript openly states that it is not sound (it lists "apply a sound or 'provably correct' type system" as a non-goal). Elixir, on the other hand, lists soundness as one of the goals of its type system. But it too admits it is best-effort ("we do not guarantee we will find every mistake"), so it does not claim to be fully sound either. Both projects talk about their type systems in terms of sound and unsound, so I will use the same words here.

There is room for different stances on how far, and how, to pursue soundness. The key question is how each one treats things it cannot be sure about.

Rust rejects what it cannot be sure about. Because it refuses to let those through, it is strongly sound about types and ownership. (The unsafe parts, and runtime errors like out-of-bounds array access, are outside that guarantee.)

TypeScript and Elixir both let unknowns through in the end. The difference is what happens before that. TypeScript is designed around writing types as much as you can, and where type information is missing (an any, or something made unknown by an as cast) it treats that as out of scope and lets it through without checking. Elixir, before letting a value through, traces the flow of the code (branches and guards) to work out the possible types, and rejects only what it can prove will always fail. Same "letting it through," but the question is whether it looks first. That difference is what separates unsound (TypeScript) from sound (Elixir).

Elixir 1.20's type system

Three things stand out.

1. dynamic() defers the judgment. Where type information is missing, TypeScript passes it without checking (by design: it assumes you write types, and treats what you did not as out of scope). Elixir instead assigns the unknown spot a type that literally means "unknown" (dynamic()) and holds off. As that value flows through the code it gets narrowed, and Elixir reports only the spots where every possible value is certain to fail. Where only some paths might fail, it stays quiet. It is built to say only what it is sure of, and to avoid false positives. If something stays gray to the end it is missed (the project itself admits this best-effort limit), but whatever it does report is certain.

2. You can express negation in a type. Elixir's types are built from set operations: union, intersection, and negation (set-theoretic types). So "not nil" is natural to write. TypeScript can also say "exclude this" via Exclude and narrowing, but Elixir has negation as a type operation itself. That is the difference.

3. It starts from writing no types. For now, you do not write type annotations; the compiler infers types from the code and checks them. The point is to make it work on huge existing codebases without adding anything. Later, the plan is to let you write type signatures at the boundaries where you want stronger guarantees (per the official roadmap), and 1.20 is the "inference first" milestone on that path. Note that the long-standing @spec is for documentation and Dialyzer; the new type system does not use it. The new type signatures are being designed as a separate thing.

Once you can write types explicitly, guarantees should reach places inference cannot follow today (struct fields, boundaries across modules). But the team itself is cautious ("we still need to assess the impact on how it feels to write code" and "it may turn out the type system is not practical"), and it is still being evaluated. The future where you write types should be better, but the people building it are still feeling their way.

How much it catches without a single type annotation (I ran it)

I installed Elixir 1.20 and tried, without writing a single type, to see what it catches.

For example, when every branch of a case returns an atom, the result is inferred to be an atom, and things stop when you hand that to a function that works on strings. Elixir calls strings "binaries," so the warning says binary().

def categorize(n) do
  label =
    case n do
      x when x < 0 -> :negative
      0 -> :zero
      _ -> :positive
    end
  String.length(label)
end

warning: incompatible types given to String.length/1:
    given types:     dynamic(:negative or :positive or :zero)
    but expected one of:     binary()

It also follows types that change midway through a pipeline.

def pipeline(n) do
  n
  |> Integer.to_string()   # turn the integer into a string (Elixir calls strings "binaries")
  |> Kernel.+(1)           # warns: trying to add an integer to a string (binary)
end

warning: incompatible types given to Kernel.+/2:
    given types:     binary(), integer()
    but expected one of:     integer(), integer()   # and the other numeric combinations

Neither has any type annotations. It bundles the three case branches into :negative or :positive or :zero, follows the type change through the pipe, and points at the single spot where every value is bound to fail.

To be honest, I tried to build an example where TypeScript misses it but only Elixir catches it, and I could not make one work. TypeScript catches type mismatches too, and unsound cases like out-of-bounds array access are missed by Elixir as well (best-effort). The difference is not the range of what can be caught; it is that it catches this without my writing a single type for the example.

Pushed further: wouldn't a statically typed language be enough?

After running all this, a deeper question surfaced. If we have statically typed languages like Rust, then pushed to the limit, wouldn't those be enough? Why do dynamically typed languages need to exist at all? I wanted to find out, so I asked an AI agent. Here is the answer that came back.

First, let me split the question a little. Rust's heaviness comes less from static types themselves and more from ownership and lifetimes (the machinery for memory safety without a GC). A statically typed language with a GC gets type inference too, so you barely write annotations. So the real divide is not "Rust or dynamic" but "static or dynamic," with GC'd static languages sitting in between.

To be honest, the "static is enough" side has gotten stronger. Inference has narrowed the old "dynamic is faster to write" gap, and the trend of adding types to a dynamic language after the fact (TypeScript, Python, and now Elixir 1.20) is itself evidence that once code matters, people end up wanting static guarantees.

Even so, there are two reasons dynamic types will not disappear in principle.

1. A sound static type system must reject some programs that actually run correctly. Whether a program "never hits a type error at runtime" is undecidable in general (Rice's theorem), so if you prioritize never letting an unsafe program through, the price is that some "actually runs, but cannot be proven, so it is rejected" code always remains. This is not a flaw you fix by improving the type system; it is a hard ceiling. The proof is that every static language has an escape hatch (Rust's unsafe, the Any or dynamic casts in various languages). They admit there is a part static cannot cover, and quietly bring dynamic typing back in.

2. Some work has types that are only determined at runtime. Messy data coming from outside, a REPL you poke at interactively, macros that generate code, hot code reloading that swaps modules while the system runs. All of these are dynamic by nature, and clash with the premise of "check the whole thing up front."

In short, static and dynamic just differ in where you pay for type correctness. Static pays up front, at compile time, for every possible execution. Dynamic pays later, at runtime, for the one execution that actually happened. Because there are situations where you cannot pay up front, or where paying up front is not worth it, dynamic typing is needed. And the real answer is not "one or the other" but is heading toward "keep a dynamic base, and add static where it pays."

Reading that answer, I came to understand Elixir 1.20's reason for being, and its position, a little better.

Elixir is not trying to become Rust. It keeps a base you can run while still dynamic, statically stops only the certain mistakes, and plans to let you add types at the boundaries where you want guarantees later. It has chosen "a dynamic base, with static added where it pays" as a matter of language design.

And this overlaps with the era of having AI write code. AI can write a lot, fast, but it does not get everything completely right. So the type system points out, at the compiler level, the mistakes that are certain to be found, and assists with the parts AI does not quite finish. Elixir 1.20's type system looks like one form of that.

References

• Elixir v1.20 released: now a gradually typed language (official release blog)
• Gradual set-theoretic types (official docs: the note on soundness, best-effort, and phasing out typespecs)
• Typespecs reference (@spec is for documentation and Dialyzer)
• Type inference of all constructs and the next 15 months (roadmap)
• Giuseppe Castagna, Guillaume Duboc, José Valim, "The Design Principles of the Elixir Type System"
• TypeScript Design Goals (lists a sound type system as a non-goal)