Monday June 15 2026

Hacker Times

Elixir v1.20: Now a gradually typed language

Discussion

In 2022, we announced the effort to add set-theoretic types to Elixir. In June 2023, we published an award winning paper on Elixir’s type system design and said our work was transitioning from 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 and verified 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 the dynamic() type means in Elixir, and how it finds verified 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 between CNRS and Remote. The development work is currently sponsored by Fresha, and Tidewave.

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

The `dynamic()` type

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

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

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

Although value_or_error has type integer() or binary(), the operator / accepts only numbers, and String.upcase accepts 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 / and String.upcase are 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 the value_or_error variable above with the type dynamic(integer() or binary()), which means the type is either integer() or binary() at runtime.

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. In the program above, even though / expects only numbers, dynamic(integer() or binary()) can be an integer() 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 =
  if value > 1 do
    value
  else
    "not well"
  end

Map.fetch!(value_or_error, :some_key)

Because Map.fetch! expects a map data structure, and value_or_error can 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 only verified 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:

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

In the program above, data starts as a dynamic() type. We then use it as data.a and data.b inside the plus operator, so Elixir will refine the data variable to have type %{..., a: number(), b: number()}, which implies it is a map with both a and b fields with number values (and potentially any other field, hence the leading ...). Therefore, if you were to forget to select the .b field and write this:

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

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

In other words, the dynamic() 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 as dynamic(). Once we introduce user-supplied type annotations, Elixir’s type system will behave as any statically typed language as long as dynamic() is not used. And whenever you cross the static-dynamic boundary, we developed 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:

def example(x, y) when is_list(x) and is_integer(y)

The code above correctly infers x is a list and y is an integer.

def example({:ok, x} = y) when is_binary(x) or is_integer(x)

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

def example(x) when is_map_key(x, :foo)

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

def example(x) when not is_map_key(x, :foo)

And the code above infers x is a map that does not have the :foo key, which has the type: %{..., foo: not_set()}. Hence x.foo within the function body will raise a typing violation.

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

def example(x) when tuple_size(x) < 3

Elixir will correctly track the tuple has at most two elements, and therefore accessing elem(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 as case and conditionals, Elixir uses information from previous clauses to refine subsequent ones:

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

System.get_env("SOME_VAR") returns either nil or a binary(). Because the first clause matches on nil, the type system knows value can no longer be nil, and therefore it must only be a binary(), 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 the release 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 .beam files written to disk, only how the contents inside defmodule are executed. You can enable it by setting elixirc_options: [module_definition: :interpreted] in your mix.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 discussed in 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 done extensive work optimizing it)
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 and in 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!

Kaliboy•12 days ago

Honestly just build it using the tutorials and sound mind and you're like 80% there.

This may sound crazy but when any interpreter boots up, but I feel it especially with BEAM, that needs to be your "let there be Light" moment. That's your world, that state is yours and only your will decides what changes.

So yes you can call all functions in your module, that's indeed how it works. But that's your module and that function mutates your world.

Just like you filter what people tell you based on your knowledge, you do the same here.

Most of my methods start with guard clauses.

`return if condition_not_met`

Don't touch my state if I don't agree with what you want me to do.

In Ruby it's essential cause that's how we get RuntimeErrors all over the place. In Elixir it's way easier to do, with pattern matching. And easier since state is what enters the function and will be what leaves.

If you keep this in mind you should inherently write safe code, because in protecting your domain through guards you basically close the door for exploitation by unknown means.

I'll give you one example I just thought of. Where I work we run Rails since the time before time, and as such had a lot of technical debt.

Around Rails 5 or 6 what we call `ActionController::Parameters` had a breaking change. Basically this module processes parameters received from HTTP requests.

Beforehand it just wrapped all it got and handed it over to us. But now it expected us to tell it what to expect. And if didn't find what it expected it blew up with a bang!

Horrible for our hundreds of controllers with `controllers * 4` html templates where all the form keys were hidden.

We either had to add the conventiely available `permit!` call, or find the form keys for all the forms, and add `permit(:name, :address,...)`. A shitload of work before AI.

I ended up monkey patching Rails to generate the lists for us instead of crashing. And for the point of this entire story...

The defaults of most frameworks are very safe, but they require the most verbosity so the framework knows what to expect and to guard it. But there always exists easier and faster ways to the same goal, but it's generally a trade. You get ease, you sacrifice some security.

Don't get in that habit and you'll be fine. And spend a lot of time thinking what could go wrong and guard against them.

toast0•12 days ago

> "what if I have ghost processes",

I'm not sure what a ghost process is? I guess something that's living beyond its usefulness / isn't supervised, etc? ... I don't speak Elixir, but you can do the equivalent of this Erlang to see everything on the node:

    rp([{X, erlang:process_info(X)} || X <- erlang:processes()]).

Then you'll know what's going on. Caveat: if you have a lot of processes, that's going to use a bunch of memory; for production you probably don't want to use erlang:process_info/2 with specific items instead of the default items. And you might don't want to output something for all the processes if you have a lot of "normal" processes that won't need to be listed.

> "what if I spawn too many processes",

The default limit is 1,048,576, if you want to have more, you can add +P X to the erl command line with a bigger limit? Have your monitoring alert you when you're at ~ 80% of the limit.

> "what if this architecture is bad compared to...",

This probably addresses the real question of your too many process question. If your architecture is bad or if you spawn more processes than a good architecture would, your performance will be bad. If your architecture is really bad, you'll have a hard time solving the problems you're trying to solve. Future you will look upon your system and despair; you may also despair in the present...

Eh, you're going to make bad architecture. BEAM won't solve all your problems. But, if you've got problems it can solve, IMHO, it can be a very nice way to solve them.

> "when to kill processes",

Kill processes (or let them crash) when they misbehave. Kill them (or let them exit normally) when they've done their work and they don't have anything else to do or wait for. When you spawn a process, you'll often have a pretty good idea of the conditions that would lead to its death... Ex: if you spawn a process to handle a connection, it should probably die around the time that the connection ends. If you spawn a process to handle a request, it should probably die when the request is handled. If you spawn a process to listen for connections, it probably should die when you don't want to listen anymore. Etc.

> "whats the correct restart strategy for this"

Well... it depends. Almost never the default strategy. The default strategy is a big foot gun; at least it is for Erlang, maybe they changed it in Elixir. I need zero hands to count the number of times I actually wanted BEAM to stop because some supervised process failed 3 times in a small time frame; but it's happened to me a lot more times than that. For per connection or per request things, the appropriate strategy is not to restart at all; for other things, try to restart a few times quickly then maybe every minute or so is probably sufficient. You'll want some sort of alerting. And if the restart strategy isn't right, you can always console in and poke it.

toast0•12 days ago

> Errors are often simply swallowed.

That's a choice, but it's not idiomatic.

You're expected to write things like...

    ok = thing_that_might_not_work().

(Well, that's what it looks like in Erlang anyway). If there's an error, it doesn't match, so it crashes. You don't have to check for success, but it's easy to, and 'let it crash' is the mantra, so yeah. Then you watch for crashes, and fix them with hot loading, and pretty soon you have a reliable system.

Let it crash ends up not quite working, so you end up catching a lot of errors, but you should be logging them, not swallowing them...

solid_fuel•12 days ago

I find the optional parentheses, and the way that keyword lists are defined to be the two biggest stumbling blocks when I come back to Elixir after a while way.

Coming from other languages, I find that

    example("with", 3, extra: "arguments", as: "a", keyword: "list")

being equivalent to

    example("with", 3, [extra: "arguments", as: "a", keyword: "list"])

and

    example "with", 3, extra: "arguments", as: "a", keyword: "list"

always takes some extra mental effort to get through, especially when there's no parenthesis. But I appreciate not having to write all the extra brackets and parens when I get going, so I think it's a fair tradeoff.

Loading replies...

teleforce•11 days ago

>Type systems restrict which programs can be expressed and increasing expressiveness often requires increasing type-system complexity (which, speaking from experience, both humans and agents will struggle with).

I used to hold similar opinion but D language, and this article by Patrick Li (HN JITX co-founder) who's the original author of little known but very powerful language Stanza changed my mind [1],[2].

He argued that Ruby has enabled a very expressive language that enabled RoR, and when it was originally written other languages are less capable, and accordingly the proof is in the pudding.

In his new language Stanza for his PhD thesis he has designed an optional typed system supporting both typed and untyped, it seems very similar in concept to the OP article that you've written on Elixir. Groovy also deserved a special mention, and the pudding is Grails.

Interestingly both Elixir and Stanza have GC, but Stanza also support non-GC namely LoStanza in which Stanza GC is written.

Interestingly, D language pioneered this combination both GC (by default) and non-GC more seamlessly, even before Stanza.

In addition to Ruby, these four languages namely Elixir, Groovy, Stanza and D all have similar to or better expressive power than Ruby. Notably both Stanza and D are compiled languages. Above all D is an anomaly in a good way since it's a fully type programming language. Kudos to Walter and the team for giving birth to a highly expressive fully typed modern language, very fast in compilation and runtime, truly one of a kind [3].

Regarding the issue of comparatively smaller corpus for these languages as mentioned by others, I think the new self-distillation technique for LLM and code generation as proposed by Apple, MIT-ETH and UCLA can overcome this limitation [4].

[1] “Stop Designing Languages. Write Libraries Instead” (2016) (278 comments):

https://news.ycombinator.com/item?id=46525640

[2] Stanza: People:

https://lbstanza.org/people.html

[3] Origins of the D programming language:

https://dl.acm.org/doi/10.1145/3386323

[4] Embarrassingly simple self-distillation improves code generation (201 comments):

https://news.ycombinator.com/item?id=47637757

awepofiwaop•12 days ago

The issue with TS is that it's not really a type system, it's mostly just comments with a linter bolted on. It tries, but it's fundamentally broken in too many ways.

Here's just one very simple example, there are many more. I've checked all the strict mode options and this appears to still "typecheck".

  var x: {a: number} = {a: 1};
  var y: {a: number|string} = x;
  y.a = 'FAIL';
  var n: number = x.a; // not actually a number

Source: https://www.typescriptlang.org/play/?noUncheckedIndexedAcces...

Loading replies...

dqv•12 days ago

one more ;)

    example("with", 3, [{:extra, "arguments"}, {:as, "a"}, {:keyword, "list"}])

    iex> [{:extra, "arguments"}, {:as, "a"}, {:keyword, "list"}] = [extra: "arguments", as: "a", keyword: "list"]
    [extra: "arguments", as: "a", keyword: "list"]

josevalim•11 days ago

I don't think these articles fully cover (pun intended) the claims being made.

First of all, we need to separate "types" from "static type checking". Elixir always had types and types by themselves won't eliminate tests. You can combine types with type checkers, as well as tests themselves (as described in the first article), to aid software verification. Plus many of the techniques discussed in the article (property-based testing, static analysis, etc) are available to dynamically typed languages too.

Some notes on the first article:

> For example, there is no test we could write that would show that our function never throws an exception or never goes in to an infinite loop, or contains no invalid references. Only static analysis can do this.

Static analysis is doing a lot of heavy lifting here. When applied to type checking, where it can prove absence of exceptions depends entirely on how expressive the type system and checker are.

For example, this Haskell function can fail at runtime even though it type checks:

    maxPosInteger :: (Ord a, Num a) => [a] -> a
    maxPosInteger xs = maximum (filter (> 0) xs)

If `xs` contains no positive elements, maximum fails. The type system does not rule this out.

As the article itself later discusses, proving stronger properties requires more expressive type systems, such as dependent types. Those systems can prove the absence of additional classes of failures, but they come with their own costs in complexity, ergonomics, inference, compile times, and so on. My recent ElixirConf talk touched on these trade-offs: https://www.youtube.com/watch?v=Ay-gnCqDw9o

But overall the article does not discuss coverage. Under some of the scenarios it presents, such as finite domains, exhaustive testing guided by coverage can prove the absence of bugs too. Additionally, some of the concerns the article has about Python, such as runtime redefinition and excessive polymorphism, do not really apply to dynamic languages like Elixir and Clojure.

> Correctness oracles abound. We have test suites, fuzzers and property-based testers, runtime sanitizers, static analyzers, linters, strong type systems, and formal verifiers. Any time such a tool can be made available to the LLM, we’ll reap the benefits in terms of not dealing with bugs the hard way, later on.

I completely agree with that framing. Static type systems are valuable tools, but they're one tool among many. My overall point is that I wouldn't draw the line at static typing as the "must have" mechanism for software quality, especially in the context of AI-assisted development where multiple correctness oracles can be composed together.

Thanks for sharing, those were great reads!

scythmic_waves•11 days ago

Anecdotally, it is very much different in Elixir land. I occasionally see bugs related to something being unexpectedly `nil` but it's pretty rare IME.

I'd love to evidence what I'm saying with specific numbers since this kind of discussion would benefit from being as objective as possible. Sadly I don't have them. But I still believe what I'm saying and I have a few guesses about some of the causes:

1. Immutable data - so, so many bugs are caused by data mutating out from under you in subtle ways. If you write `x = 1` in your Elixir function, nothing can change the value of `x` except an explicit rebinding. You can then write e.g. `y = f(x)` and know `x` remains unchanged after. Note: this is also true even if the variable is a composite type. `my_struct = blah()` will remain the same in it's entirety no matter what you do with `my_struct`. This is different than in JS where e.g. you can change the contents of an object even if it's declared `const`.

2. Assertive style - the Elixir community favors writing things in an "assertive" fashion [1]. Briefly, this a way of writing code that will fail the moment an assumption is broken rather than letting the issue propagate.

3. Pattern matching (somewhat like destructuring in JS) - Elixir code actually ends up feeling "typed" with pattern matching. E.g. `%Time{} = today = Date.utc_today()` will attempt to bind `today` to the result of `Date.utc_today()` and will raise a `MatchError` when the result, a `%Date{}` struct, fails to be a `%Time{}` struct. Or `[a, b] = [1, 2, 3]` will raise a `MatchError` because `[1, 2, 3]` isn't a list of length exactly 2. You can use pattern matching to write very assertive code quite tersely.

These reasons are all local properties of code. But when all its parts are written in this way, a program as a whole gains a level of correctness that's hard to achieve in a dynamically typed language without them.

Also these reasons aren't exhaustive, but they're top of mind when thinking about this topic.

[1]: https://dashbit.co/blog/writing-assertive-code-with-elixir

spider-mario•11 days ago

`let <var> = <expr> in <expr>` is an expression. Top-level bindings are just `let <var> = <expr>`. That’s pretty much all there is to it.

    let fac =
      let rec fac' acc = function
        | 0 -> acc
        | n -> fac' (n * acc) (n - 1)
      in
      fac' 1

    let seven =
      let four = 4 and three = 3 in
      four + three

https://ideone.com/HpTrI4

simoncion•12 days ago

Cool, cool.

  [W]hat happens when you run Dialyzer against BEAM files compiled from Elixir that has circular dependencies? Do its reports become more reliable, or does the reliability of those reports become irrelevant because the transformations the Elixir build system makes to your code make the structure of the BEAM code difficult to trace back to the Elixir source code?

OkayPhysicist•11 days ago

> (people writing dynamically typed languages eventually resort to type comments)

This has never been an issue in Elixir, because instead of a comment, you'd just improve the pattern matching in the function definition.

    def blah(%{students: [%{firstname: firstname, lastname: lastname}|[]], count: cnt}) when is_int(cnt):
      fullname = firstname <> lastname

Is a valid function declaration, which specifies that blah takes a dictionary that contains at least 2 keys, :count, who's value is an integer, and :students, who's value is a length-1 list who's first element is a dictionary that contains the keys :firstname and :lastname

Hacker Times

Hacker Times

Elixir v1.20: Now a gradually typed language

Discussion

Discussion

Types, in my Elixir?

The dynamic() type

Typing guards, clauses, and more

Compilation time improvements

What is next?

The `dynamic()` type