From 2412596e703c1c9e85e036bacd654b5224610247 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Fri, 6 Nov 2026 21:01:39 +0100 Subject: [PATCH 1/4] Draft --- .../inference-narrowing-reverse-arrows.md | 299 ++++++++++++++++++ 1 file changed, 299 insertions(+) create mode 100644 src/content/blog/inference-narrowing-reverse-arrows.md diff --git a/src/content/blog/inference-narrowing-reverse-arrows.md b/src/content/blog/inference-narrowing-reverse-arrows.md new file mode 100644 index 000000000..6a8cf9099 --- /dev/null +++ b/src/content/blog/inference-narrowing-reverse-arrows.md @@ -0,0 +1,299 @@ +--- +title: "Type inference and narrowing with reverse arrows" +excerpt: "This article explains how Elixir implements type inference and type narrowing using reverse arrows." +date: 2026-11-10 +author: "José Valim, Guillaume Duboc" +category: "Internals" +tags: [] +--- + +This article explains how Elixir implements type inference and type narrowing +using reverse arrows. The upcoming Elixir release, v1.21, passes all tests in the +[If-T: Type Narrowing Benchmark by Guo et al.](https://github.com/utahplt/ifT-benchmark). +This means v1.21 can find even more bugs in existing Elixir programs and, when type +signatures are introduced, type narrowing will give us more precise types and avoid +false positives. + +> The type system was made possible thanks to a partnership between [CNRS](https://www.cnrs.fr/) +> and [Remote](https://remote.com/). The development work is currently sponsored by +> [Supermethod](https://www.supermethod.com/) and [Dashbit](https://dashbit.co/). + +## Type inference + +Elixir performs type inference by refining the dynamic type. This is quite different +from how inference and gradual typing is implemented in most type systems, so let's +break it down. + +In many gradual languages, the dynamic type, often known as `any`, is a "black-box" and +can be used in any context. For example, imagine this Elixir function, where `x` starts +with type `dynamic()`, as there is no type signature: + +```elixir +def using_x_as_number_and_binary(x) do + IO.puts x * 2 + IO.puts byte_size(x) + :ok +end +``` + +The program above uses `x` both as a number (more precisely, as `integer() or float()` +in `x * 2`) and as a bitstring in `byte_size(x)`. In some gradual type systems, the type +checker will accept the program above, even though it will crash at runtime, because +the dynamic type can be used in any context. + +However, in Elixir, the `dynamic()` type can be refined, and the above will report the +following typing violation: + +``` +warning: incompatible types given to Kernel.byte_size/1: + + byte_size(x) + +given types: + + dynamic(float() or integer()) + +but expected one of: + + bitstring() + +where "x" was given the type: + + # type: dynamic(float() or integer()) + # from: iex:3 + x * 2 + +└─ iex:4: Foo.using_x_as_number_and_binary/1 +``` + +As you can see in the error message, Elixir infers that the type of `x` after +`x * 2` is a `dynamic(float() or integer())`. This means that `x` can be given +to any function that accepts at least one of `float()` or `integer()`. However, +because `byte_size(x)` expects a bitstring, we have a typing violation. + +This is possible because `dynamic()` in Elixir actually means `dynamic(term())`, +where `term()` is the top type. Then, as a variable is used throughout a function, +its dynamic type is refined by intersecting its type with the domain of the invoked +functions. In other words, we go through the following steps: + +1. `x` starts as `dynamic(term())` + +2. `x` is given to `x * 2`. The left operand of `*` is `integer() or float()`, + which we then intersect with `term()`, and therefore `x` gains the type + `dynamic(integer() or float())` + +3. `x` is given to `byte_size(x)`, which expects a bitstring. The intersection + of `integer() or float()` with `bitstring()` is empty, which will lead to a + typing violation + +Now, let's take a look at this program: + +```elixir +def using_x_as_integer(x) do + IO.puts x * 2 + IO.puts rem(x, 2) + :ok +end +``` + +This time, we pass `x` to the remainder function, `rem`, which expects all of its +inputs to be integer. This means that, at the end of this function, Elixir will +correctly infer that `x` can only be an integer, because `x` was refined from +`dynamic(term())` to `dynamic(integer() or float())` and then only to `dynamic(integer())`. +The inferred type for `using_x_as_integer` is `dynamic(integer()) -> :ok`. + +The best part is that all dynamic types in Elixir are refined and therefore the type +system is always doing its best to find sure bug, even in the presence of dynamism. +And the refinement itself is often quite precise, thanks to reverse arrows, which we +will explore next. + +## Reverse arrows + +Functions in Elixir can be typed with multiple arrows. As an exercise, let's take the +unary negation operator. You could give it this type signature: + +```elixir +$ integer() or float() -> integer() or float() +def -number +``` + +However, this type says that, if you give it an integer, it may return a +float, which is never the case! This signature is too broad. Instead, we +could give it this signature: + +```elixir +$ integer() -> integer() +$ float() -> float() +def -number +``` + +This precisely captures that, if you give it an integer, it returns an integer. +If you give it a float, it returns a float. Multiple arrows are an excellent way +to type functions with multiple clauses, which are common in both Erlang and Elixir. + +With this in mind, what do you believe is the inferred type of `x` in the function below? + +```elixir +def negated_halt_remainder(x), do: rem(-x, 2) +``` + +You may think `x` is `dynamic(integer() or float())`, because that's the domain of +the unary negation operator, however, `x` will once again be inferred to be +`dynamic(integer())`, because Elixir reverse propagates types through the arrows. +Let's break it down. + +1. We start type checking the function and we find `rem(a, b)`, which has a type + signature of `integer(), integer() -> integer()`. Because we have a single arrow, + we know that `a` and `b` have to be `integer()` for this to type check + +2. Now we type check `-x`. We know that `-` has two arrows: `integer() -> integer()` + and `float() -> float()`. We also know that, because the result of `-x` is given to + `rem` which expects an integer, we can discard the `float() -> float()` arrow, + and the only valid type for the argument of `-` is `integer()` + +3. Now we type check `x` itself. `x` starts with type of `dynamic(term())`. We then + intersect it with `integer()`, resulting in `dynamic(integer())` + +In other words, as we give precise type signatures to our programs using multiple +arrows, the type system will use these same arrows to infer precise types. As we will +learn next, Elixir uses this technique to infers types from guards and performs type +narrowing (also known as occurence typing). + +## Guards + +Now we have the foundation to understand how Elixir performs type inference of guards. +Take this function clause + +```elixir +def something(x, y) when is_integer(x) and is_bitstring(y) do + ... +``` + +Both `x` and `y` start with type `dynamic(term())`. We also know that a guard only +succeeds if it returns `true` and we have the following type signatures (roughly): + +```elixir +$ true, true -> true +$ true, false -> false +$ false, true -> false +$ false, false -> false +def and(left, right) + +$ integer() -> true +$ not integer() -> false +def is_integer(value) + +$ bitstring() -> true +$ not bitstring() -> false +def is_bitstring(value) +``` + +Therefore, to infer the types of `when is_integer(x) and is_bitstring(y)`, +we start with `true`, which is the only condition a guard would be accepted, +and propagate it through the arrows in reverse: + +1. The only clause of `and` that can return `true` is `true, true -> true`, + therefore we know that both operands must be `true` + +2. The only clause of `is_integer` that can return `true` is `integer() -> true`, + therefore we know `x` must be an integer + +3. The only clause of `is_bitstring` that can return `true` is `bitstring() -> true`, + therefore we know `y` must be a bitstring + +If multiple clauses could return true, we would then simply union their domains. + +It is worth emphasizing that this behaviour is not hardcoded to a handful of +functions the type checker knows about. It works with any function, in any context. +Let's see more examples. + +## Type narrowing (also known as occurrence typing) + +Occurrence typing allows us to refine the type of variables and expressions +based on the different branches of a conditional. For example: + +```elixir +if is_bitstring(x) do + x #=> x has type: bitstring() +else + x #=> x has type: not bitstring() +end +``` + +The mechanism we use to perform occurrence typing is quite similar to the ones +from the previous sections. Within the `do`-branch, we consider the scenarios +where `is_bitstring(x)` will return `true`. Within the `else`-branch, where it +returns `false`. + +And since our foundation is built on reverse arrows, the narrowing applies to +patterns and `case`-expressions! For example: + +```elixir +def f(x) do + case parse(x) do + {:ok, _} -> ... # x is integer() + :error -> ... # x is bitstring() + end +end + +defp parse(x) when is_integer(x), do: {:ok, x} +defp parse(x) when is_bitstring(x), do: :error +``` + +The [If-T benchmarks](https://github.com/utahplt/ifT-benchmark) is a collection of +test scenarios designed to evaluate how well type checkers handle type narrowing. +Elixir v1.20 already handled 12 out of the 13 tests but it could not infer the +proper types for this example: + +```elixir +y = is_integer(x) + +if y do + # y is true, x remains dynamic +else + # y is false, x remains dynamic +end +``` + +In other words, Elixir could only narrow the types in the expressions given to +`if` and `case`. If the expression was moved to an assignment, we could not longer +narrow it. That would be quite harmful once we added type signatures, because it +meant trivial refactoring techniques, such as extracting an expression into a variable, +could lead to false positives. + +Elixir v1.21 solves it by narrowing even across assignments, as in the example below: + +```elixir +y = is_integer(x) +z = not y + +if z do + # z is true, y is false, x is not integer() +else + # z is false, y is true, x is integer() +end +``` + +Our implementation also performs the narrowing lazily, by cross references the variables +in the `if`-expression and `case`-expression with the variables used in each clause. +For example, if the clauses above do not access `z`, `y`, or `x`, then no narrowing is +performed. + +Finally, because Elixir defines reverse arrows for almost all operations, it can refine +expressions [which are not currently refined in TypeScript](https://www.typescriptlang.org/fr/play/?#code/PTAEHUFMBsGMHsC2lQBd5oBYoCoE8AHSAZVgCcBLA1UABWgEM8BzM+AVwDsATAGiwoBnUENANQAd0gAjQRVSQAUCEmYKsTKGYUAbpGF4OY0BoadYKdJMoL+gzAzIoz3UNEiPOofEVKVqAHSKigBmXLCoFPBeBGxEZKh4APoM0BQMgkmC7LAWgoIAFHgAXKCCqJSczKAAPqCc7IjSkGQAlKUNTS2gAN6KoCbR5aAAHqAAvL2gIfDwpXigAL4A3P0iIaAFiUTwGyMBMxjjx6AAROWVzKetvWsDTqjsZF54Ae5VqJirA4ugMIIoPoDe6QR7PUALADUoAAjN8lopFkA), +such as data constructors: + +```elixir +def f(foo) when is_bitstring(foo) or is_integer(foo) do + map = %{foo: foo} + + if is_bitstring(map.foo) do + byte_size(foo) + else + foo + 1 + end +end +``` + +In the program below, even though `foo` is set as the value of a map, +refining the map still refines the original variable. From 6b3707ed498f340fac492ef6b5a294c121e744a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Fri, 6 Nov 2026 21:06:29 +0100 Subject: [PATCH 2/4] Fix typos --- .../inference-narrowing-reverse-arrows.md | 62 +++++++++---------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/src/content/blog/inference-narrowing-reverse-arrows.md b/src/content/blog/inference-narrowing-reverse-arrows.md index 6a8cf9099..b2254363e 100644 --- a/src/content/blog/inference-narrowing-reverse-arrows.md +++ b/src/content/blog/inference-narrowing-reverse-arrows.md @@ -21,10 +21,10 @@ false positives. ## Type inference Elixir performs type inference by refining the dynamic type. This is quite different -from how inference and gradual typing is implemented in most type systems, so let's +from how inference and gradual typing are implemented in most type systems, so let's break it down. -In many gradual languages, the dynamic type, often known as `any`, is a "black-box" and +In many gradual languages, the dynamic type, often known as `any`, is a "black box" and can be used in any context. For example, imagine this Elixir function, where `x` starts with type `dynamic()`, as there is no type signature: @@ -33,7 +33,7 @@ def using_x_as_number_and_binary(x) do IO.puts x * 2 IO.puts byte_size(x) :ok -end +end ``` The program above uses `x` both as a number (more precisely, as `integer() or float()` @@ -79,12 +79,12 @@ functions. In other words, we go through the following steps: 1. `x` starts as `dynamic(term())` 2. `x` is given to `x * 2`. The left operand of `*` is `integer() or float()`, - which we then intersect with `term()`, and therefore `x` gains the type - `dynamic(integer() or float())` + which we then intersect with `term()`, and therefore `x` gains the type + `dynamic(integer() or float())` 3. `x` is given to `byte_size(x)`, which expects a bitstring. The intersection - of `integer() or float()` with `bitstring()` is empty, which will lead to a - typing violation + of `integer() or float()` with `bitstring()` is empty, which will lead to a + typing violation Now, let's take a look at this program: @@ -93,17 +93,17 @@ def using_x_as_integer(x) do IO.puts x * 2 IO.puts rem(x, 2) :ok -end +end ``` This time, we pass `x` to the remainder function, `rem`, which expects all of its -inputs to be integer. This means that, at the end of this function, Elixir will +inputs to be integers. This means that, at the end of this function, Elixir will correctly infer that `x` can only be an integer, because `x` was refined from `dynamic(term())` to `dynamic(integer() or float())` and then only to `dynamic(integer())`. The inferred type for `using_x_as_integer` is `dynamic(integer()) -> :ok`. The best part is that all dynamic types in Elixir are refined and therefore the type -system is always doing its best to find sure bug, even in the presence of dynamism. +system is always doing its best to find bugs, even in the presence of dynamism. And the refinement itself is often quite precise, thanks to reverse arrows, which we will explore next. @@ -134,11 +134,11 @@ to type functions with multiple clauses, which are common in both Erlang and Eli With this in mind, what do you believe is the inferred type of `x` in the function below? ```elixir -def negated_halt_remainder(x), do: rem(-x, 2) +def negated_half_remainder(x), do: rem(-x, 2) ``` You may think `x` is `dynamic(integer() or float())`, because that's the domain of -the unary negation operator, however, `x` will once again be inferred to be +the unary negation operator. However, `x` will once again be inferred to be `dynamic(integer())`, because Elixir reverse propagates types through the arrows. Let's break it down. @@ -151,18 +151,18 @@ Let's break it down. `rem` which expects an integer, we can discard the `float() -> float()` arrow, and the only valid type for the argument of `-` is `integer()` -3. Now we type check `x` itself. `x` starts with type of `dynamic(term())`. We then +3. Now we type check `x` itself. `x` starts with the type `dynamic(term())`. We then intersect it with `integer()`, resulting in `dynamic(integer())` In other words, as we give precise type signatures to our programs using multiple arrows, the type system will use these same arrows to infer precise types. As we will -learn next, Elixir uses this technique to infers types from guards and performs type -narrowing (also known as occurence typing). +learn next, Elixir uses this technique to infer types from guards and to perform type +narrowing (also known as occurrence typing). ## Guards Now we have the foundation to understand how Elixir performs type inference of guards. -Take this function clause +Take this function clause: ```elixir def something(x, y) when is_integer(x) and is_bitstring(y) do @@ -189,7 +189,7 @@ def is_bitstring(value) ``` Therefore, to infer the types of `when is_integer(x) and is_bitstring(y)`, -we start with `true`, which is the only condition a guard would be accepted, +we start with `true`, which is the only result for which a guard succeeds, and propagate it through the arrows in reverse: 1. The only clause of `and` that can return `true` is `true, true -> true`, @@ -201,7 +201,7 @@ and propagate it through the arrows in reverse: 3. The only clause of `is_bitstring` that can return `true` is `bitstring() -> true`, therefore we know `y` must be a bitstring -If multiple clauses could return true, we would then simply union their domains. +If multiple clauses could return `true`, we would then simply union their domains. It is worth emphasizing that this behaviour is not hardcoded to a handful of functions the type checker knows about. It works with any function, in any context. @@ -220,12 +220,12 @@ else end ``` -The mechanism we use to perform occurrence typing is quite similar to the ones +The mechanism we use to perform occurrence typing is quite similar to the one from the previous sections. Within the `do`-branch, we consider the scenarios -where `is_bitstring(x)` will return `true`. Within the `else`-branch, where it -returns `false`. +where `is_bitstring(x)` will return `true`. Within the `else`-branch, we consider +the ones where it returns `false`. -And since our foundation is built on reverse arrows, the narrowing applies to +And since our foundation is built on reverse arrows, the narrowing also applies to patterns and `case`-expressions! For example: ```elixir @@ -240,9 +240,9 @@ defp parse(x) when is_integer(x), do: {:ok, x} defp parse(x) when is_bitstring(x), do: :error ``` -The [If-T benchmarks](https://github.com/utahplt/ifT-benchmark) is a collection of +The [If-T benchmark](https://github.com/utahplt/ifT-benchmark) is a collection of test scenarios designed to evaluate how well type checkers handle type narrowing. -Elixir v1.20 already handled 12 out of the 13 tests but it could not infer the +Elixir v1.20 already handled 12 out of the 13 tests, but it could not infer the proper types for this example: ```elixir @@ -256,9 +256,9 @@ end ``` In other words, Elixir could only narrow the types in the expressions given to -`if` and `case`. If the expression was moved to an assignment, we could not longer -narrow it. That would be quite harmful once we added type signatures, because it -meant trivial refactoring techniques, such as extracting an expression into a variable, +`if` and `case`. If the expression was moved to an assignment, we could no longer +narrow it. That would be quite harmful once we add type signatures, because it +means trivial refactoring techniques, such as extracting an expression into a variable, could lead to false positives. Elixir v1.21 solves it by narrowing even across assignments, as in the example below: @@ -274,13 +274,13 @@ else end ``` -Our implementation also performs the narrowing lazily, by cross references the variables -in the `if`-expression and `case`-expression with the variables used in each clause. +Our implementation also performs the narrowing lazily, by cross-referencing the variables +in the `if` and `case` expressions with the variables used in each clause. For example, if the clauses above do not access `z`, `y`, or `x`, then no narrowing is performed. Finally, because Elixir defines reverse arrows for almost all operations, it can refine -expressions [which are not currently refined in TypeScript](https://www.typescriptlang.org/fr/play/?#code/PTAEHUFMBsGMHsC2lQBd5oBYoCoE8AHSAZVgCcBLA1UABWgEM8BzM+AVwDsATAGiwoBnUENANQAd0gAjQRVSQAUCEmYKsTKGYUAbpGF4OY0BoadYKdJMoL+gzAzIoz3UNEiPOofEVKVqAHSKigBmXLCoFPBeBGxEZKh4APoM0BQMgkmC7LAWgoIAFHgAXKCCqJSczKAAPqCc7IjSkGQAlKUNTS2gAN6KoCbR5aAAHqAAvL2gIfDwpXigAL4A3P0iIaAFiUTwGyMBMxjjx6AAROWVzKetvWsDTqjsZF54Ae5VqJirA4ugMIIoPoDe6QR7PUALADUoAAjN8lopFkA), +expressions [which are not currently refined in TypeScript](https://www.typescriptlang.org/play/?#code/PTAEHUFMBsGMHsC2lQBd5oBYoCoE8AHSAZVgCcBLA1UABWgEM8BzM+AVwDsATAGiwoBnUENANQAd0gAjQRVSQAUCEmYKsTKGYUAbpGF4OY0BoadYKdJMoL+gzAzIoz3UNEiPOofEVKVqAHSKigBmXLCoFPBeBGxEZKh4APoM0BQMgkmC7LAWgoIAFHgAXKCCqJSczKAAPqCc7IjSkGQAlKUNTS2gAN6KoCbR5aAAHqAAvL2gIfDwpXigAL4A3P0iIaAFiUTwGyMBMxjjx6AAROWVzKetvWsDTqjsZF54Ae5VqJirA4ugMIIoPoDe6QR7PUALADUoAAjN8lopFkA), such as data constructors: ```elixir @@ -295,5 +295,5 @@ def f(foo) when is_bitstring(foo) or is_integer(foo) do end ``` -In the program below, even though `foo` is set as the value of a map, +In the program above, even though `foo` is set as the value of a map, refining the map still refines the original variable. From cc37771754b13f031dec5620c852dec9e6924b38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Fri, 6 Nov 2026 21:17:26 +0100 Subject: [PATCH 3/4] Conclusion --- .../inference-narrowing-reverse-arrows.md | 45 +++++++++++++------ 1 file changed, 31 insertions(+), 14 deletions(-) diff --git a/src/content/blog/inference-narrowing-reverse-arrows.md b/src/content/blog/inference-narrowing-reverse-arrows.md index b2254363e..4352a6f65 100644 --- a/src/content/blog/inference-narrowing-reverse-arrows.md +++ b/src/content/blog/inference-narrowing-reverse-arrows.md @@ -8,10 +8,13 @@ tags: [] --- This article explains how Elixir implements type inference and type narrowing -using reverse arrows. The upcoming Elixir release, v1.21, passes all tests in the +using reverse arrows: a small set of composable ideas, rather than special cases +hardcoded into the type checker. + +Thanks to this work, the upcoming Elixir v1.21 passes all tests in the [If-T: Type Narrowing Benchmark by Guo et al.](https://github.com/utahplt/ifT-benchmark). -This means v1.21 can find even more bugs in existing Elixir programs and, when type -signatures are introduced, type narrowing will give us more precise types and avoid +This means v1.21 can find even more sure bugs in existing Elixir programs and, once +type signatures are introduced, narrowing will give us more precise types and fewer false positives. > The type system was made possible thanks to a partnership between [CNRS](https://www.cnrs.fr/) @@ -78,7 +81,7 @@ functions. In other words, we go through the following steps: 1. `x` starts as `dynamic(term())` -2. `x` is given to `x * 2`. The left operand of `*` is `integer() or float()`, +2. `x` is given to `x * 2`. The left operand of `*` expects `integer() or float()`, which we then intersect with `term()`, and therefore `x` gains the type `dynamic(integer() or float())` @@ -142,9 +145,9 @@ the unary negation operator. However, `x` will once again be inferred to be `dynamic(integer())`, because Elixir reverse propagates types through the arrows. Let's break it down. -1. We start type checking the function and we find `rem(a, b)`, which has a type - signature of `integer(), integer() -> integer()`. Because we have a single arrow, - we know that `a` and `b` have to be `integer()` for this to type check +1. We start type checking the function and we find `rem(-x, 2)`. `rem` has the type + signature `integer(), integer() -> integer()`. Because it has a single arrow, + we know that `-x` must be `integer()` for this to type check 2. Now we type check `-x`. We know that `-` has two arrows: `integer() -> integer()` and `float() -> float()`. We also know that, because the result of `-x` is given to @@ -192,16 +195,16 @@ Therefore, to infer the types of `when is_integer(x) and is_bitstring(y)`, we start with `true`, which is the only result for which a guard succeeds, and propagate it through the arrows in reverse: -1. The only clause of `and` that can return `true` is `true, true -> true`, +1. The only arrow of `and` that can return `true` is `true, true -> true`, therefore we know that both operands must be `true` -2. The only clause of `is_integer` that can return `true` is `integer() -> true`, +2. The only arrow of `is_integer` that can return `true` is `integer() -> true`, therefore we know `x` must be an integer -3. The only clause of `is_bitstring` that can return `true` is `bitstring() -> true`, +3. The only arrow of `is_bitstring` that can return `true` is `bitstring() -> true`, therefore we know `y` must be a bitstring -If multiple clauses could return `true`, we would then simply union their domains. +If multiple arrows could return `true`, we would then simply union their domains. It is worth emphasizing that this behaviour is not hardcoded to a handful of functions the type checker knows about. It works with any function, in any context. @@ -209,8 +212,9 @@ Let's see more examples. ## Type narrowing (also known as occurrence typing) -Occurrence typing allows us to refine the type of variables and expressions -based on the different branches of a conditional. For example: +Occurrence typing refines the type of variables and expressions based on +the branch taken in a conditional or pattern match, so the same variable may +have different types in different branches. For example: ```elixir if is_bitstring(x) do @@ -241,7 +245,7 @@ defp parse(x) when is_bitstring(x), do: :error ``` The [If-T benchmark](https://github.com/utahplt/ifT-benchmark) is a collection of -test scenarios designed to evaluate how well type checkers handle type narrowing. +test scenarios designed to evaluate both the precision and soundness of type narrowing. Elixir v1.20 already handled 12 out of the 13 tests, but it could not infer the proper types for this example: @@ -297,3 +301,16 @@ end In the program above, even though `foo` is set as the value of a map, refining the map still refines the original variable. + +## Summary + +Elixir's approach to type inference and narrowing is built on a few ideas that +compose well. Dynamic types are refined as variables are used, multiple arrows +give precise types to functions, and propagating types through those arrows in +reverse lets us infer and narrow types across conditionals, patterns, and assignments, +all without hardcoding knowledge about specific functions. + +In Elixir v1.21, we use these techniques to find sure bugs in existing Elixir programs, +without requiring any changes to your code. The same mechanisms will apply once type +signatures are introduced: the more precise the signatures, the more precise the +narrowing and the fewer false positives. From 0b642a32a66ae313096f06bf945c7f5e1882149b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Tue, 10 Nov 2026 08:59:45 +0100 Subject: [PATCH 4/4] Feedback --- .../inference-narrowing-reverse-arrows.md | 94 +++++++++++++------ 1 file changed, 63 insertions(+), 31 deletions(-) diff --git a/src/content/blog/inference-narrowing-reverse-arrows.md b/src/content/blog/inference-narrowing-reverse-arrows.md index 4352a6f65..9f53c0127 100644 --- a/src/content/blog/inference-narrowing-reverse-arrows.md +++ b/src/content/blog/inference-narrowing-reverse-arrows.md @@ -75,9 +75,9 @@ to any function that accepts at least one of `float()` or `integer()`. However, because `byte_size(x)` expects a bitstring, we have a typing violation. This is possible because `dynamic()` in Elixir actually means `dynamic(term())`, -where `term()` is the top type. Then, as a variable is used throughout a function, -its dynamic type is refined by intersecting its type with the domain of the invoked -functions. In other words, we go through the following steps: +where `term()` is the top type. Then, as a variable is used throughout the code, +its dynamic type is refined by intersecting its type with the arguments of the +functions the code invokes. In other words, we go through the following steps: 1. `x` starts as `dynamic(term())` @@ -103,7 +103,8 @@ This time, we pass `x` to the remainder function, `rem`, which expects all of it inputs to be integers. This means that, at the end of this function, Elixir will correctly infer that `x` can only be an integer, because `x` was refined from `dynamic(term())` to `dynamic(integer() or float())` and then only to `dynamic(integer())`. -The inferred type for `using_x_as_integer` is `dynamic(integer()) -> :ok`. +The inferred type for `using_x_as_integer` is a function, commonly written using +the arrow notation: `dynamic(integer()) -> :ok`. The best part is that all dynamic types in Elixir are refined and therefore the type system is always doing its best to find bugs, even in the presence of dynamism. @@ -112,52 +113,71 @@ will explore next. ## Reverse arrows -Functions in Elixir can be typed with multiple arrows. As an exercise, let's take the -unary negation operator. You could give it this type signature: +An arrow is the type of a function: `integer() -> boolean()` is an arrow that +says "given an integer, this function returns a boolean". The type on the left +of the arrow is its domain (what it accepts) and the type on the right is its +codomain (what it returns). Every function has arrows, whether they come from +a type signature you wrote or are inferred by Elixir from the function's clauses. + +Functions in Elixir can be typed with multiple arrows. As an exercise, let's take +a function that negates numbers, such as `negate(1)` returning `-1`: + +```elixir +def negate(number) when is_integer(number), do: 0 - number +def negate(number) when is_float(number), do: 0.0 - number +``` + +You could give it this type signature with a single arrow: ```elixir $ integer() or float() -> integer() or float() -def -number +def negate(number) ``` However, this type says that, if you give it an integer, it may return a float, which is never the case! This signature is too broad. Instead, we -could give it this signature: +could give it this signature with two arrows: ```elixir $ integer() -> integer() $ float() -> float() -def -number +def negate(number) ``` This precisely captures that, if you give it an integer, it returns an integer. If you give it a float, it returns a float. Multiple arrows are an excellent way to type functions with multiple clauses, which are common in both Erlang and Elixir. -With this in mind, what do you believe is the inferred type of `x` in the function below? +With this in mind, and remembering that `rem` only works on integers (its type is +`integer(), integer() -> integer()`), what do you believe is the inferred type of +`x` in the function below? ```elixir -def negated_half_remainder(x), do: rem(-x, 2) +def negated_remainder(x), do: rem(negate(x), 2) ``` You may think `x` is `dynamic(integer() or float())`, because that's the domain of -the unary negation operator. However, `x` will once again be inferred to be -`dynamic(integer())`, because Elixir reverse propagates types through the arrows. -Let's break it down. +`negate`. However, `x` will once again be inferred to be `dynamic(integer())`, +because Elixir propagates types through the arrows in reverse: it starts from +what the outermost call expects and walks inwards, from results to arguments, +until it reaches the variables. Let's break it down. -1. We start type checking the function and we find `rem(-x, 2)`. `rem` has the type - signature `integer(), integer() -> integer()`. Because it has a single arrow, - we know that `-x` must be `integer()` for this to type check +1. We start type checking the function and we find `rem(negate(x), 2)`. `rem` has + a single arrow, `integer(), integer() -> integer()`, so we know that `negate(x)` + must return an `integer()` for this to type check -2. Now we type check `-x`. We know that `-` has two arrows: `integer() -> integer()` - and `float() -> float()`. We also know that, because the result of `-x` is given to - `rem` which expects an integer, we can discard the `float() -> float()` arrow, - and the only valid type for the argument of `-` is `integer()` +2. Now we type check `negate(x)`. `negate` has two arrows: `integer() -> integer()` + and `float() -> float()`. Since its result must be an integer, we can discard + the `float() -> float()` arrow, as it never returns an integer. The only remaining + arrow is `integer() -> integer()`, so the argument of `negate` must be `integer()` 3. Now we type check `x` itself. `x` starts with the type `dynamic(term())`. We then intersect it with `integer()`, resulting in `dynamic(integer())` -In other words, as we give precise type signatures to our programs using multiple +In other words, inference goes in two directions. Going forward, from arguments to +results, arrows tell us what each call returns. Going in reverse, from results to +arguments, arrows tell us what each argument must have been for the call to produce +the expected result. As we give precise type signatures to our programs using multiple arrows, the type system will use these same arrows to infer precise types. As we will learn next, Elixir uses this technique to infer types from guards and to perform type narrowing (also known as occurrence typing). @@ -244,6 +264,11 @@ defp parse(x) when is_integer(x), do: {:ok, x} defp parse(x) when is_bitstring(x), do: :error ``` +Here, `parse` has no type signature, but Elixir infers its arrows from its clauses: +`integer() -> {:ok, integer()}` and `bitstring() -> :error`. Within the first branch, +we know `parse(x)` returned a tuple, and the only arrow that returns a tuple has +`integer()` as its domain, so `x` must be an integer. + The [If-T benchmark](https://github.com/utahplt/ifT-benchmark) is a collection of test scenarios designed to evaluate both the precision and soundness of type narrowing. Elixir v1.20 already handled 12 out of the 13 tests, but it could not infer the @@ -259,13 +284,20 @@ else end ``` -In other words, Elixir could only narrow the types in the expressions given to -`if` and `case`. If the expression was moved to an assignment, we could no longer -narrow it. That would be quite harmful once we add type signatures, because it -means trivial refactoring techniques, such as extracting an expression into a variable, -could lead to false positives. +To narrow `x`, we need to reverse the arrows of `is_integer(x)`. In Elixir v1.20, we +only did so for the expression given directly to `if` or `case`. Here, the expression +given to `if` is the variable `y`. All v1.20 knew about `y` is that it was a `boolean()`. +Inside the `do`-branch, `y` is `true`, but by then the connection between `y` and +`is_integer(x)` had been lost at the assignment, so there were no arrows to reverse. + +This would be quite harmful once we add type signatures, because it means trivial +refactoring techniques, such as extracting an expression into a variable, could lead +to false positives. -Elixir v1.21 solves it by narrowing even across assignments, as in the example below: +Elixir v1.21 solves this by keeping track of the expression each variable was assigned +to. Now, when `y` is narrowed to `true`, we know `y` came from `is_integer(x)`, so we +continue propagating `true` in reverse through the arrows of `is_integer`, narrowing `x` +to `integer()`. This works across any number of assignments: ```elixir y = is_integer(x) @@ -279,9 +311,9 @@ end ``` Our implementation also performs the narrowing lazily, by cross-referencing the variables -in the `if` and `case` expressions with the variables used in each clause. -For example, if the clauses above do not access `z`, `y`, or `x`, then no narrowing is -performed. +in the `if` and `case` expressions with the variables used in each clause, trying to find +any assignment they share with each other. If the clauses above do not access `z`, `y`, or +`x`, then no narrowing is performed. Finally, because Elixir defines reverse arrows for almost all operations, it can refine expressions [which are not currently refined in TypeScript](https://www.typescriptlang.org/play/?#code/PTAEHUFMBsGMHsC2lQBd5oBYoCoE8AHSAZVgCcBLA1UABWgEM8BzM+AVwDsATAGiwoBnUENANQAd0gAjQRVSQAUCEmYKsTKGYUAbpGF4OY0BoadYKdJMoL+gzAzIoz3UNEiPOofEVKVqAHSKigBmXLCoFPBeBGxEZKh4APoM0BQMgkmC7LAWgoIAFHgAXKCCqJSczKAAPqCc7IjSkGQAlKUNTS2gAN6KoCbR5aAAHqAAvL2gIfDwpXigAL4A3P0iIaAFiUTwGyMBMxjjx6AAROWVzKetvWsDTqjsZF54Ae5VqJirA4ugMIIoPoDe6QR7PUALADUoAAjN8lopFkA),