Type inference and narrowing with reverse arrows

Elixir v1.21, the upcoming release described by creators José Valim and Guillaume Duboc, passes all tests in the If-T: Type Narrowing Benchmark by Guo et al., using a type system that refines the dynamic type by intersecting it with function argument types rather than treating it as an unconstrained black box. The work, supported by a CNRS and Remote partnership and sponsored by Supermethod and Dashbit, lets the checker flag violations such as passing a value inferred as dynamic(float() or integer()) to byte_size/1, which expects a bitstring. Valim and Duboc say the approach will yield more precise types and fewer false positives once type signatures are introduced.

Type inference and narrowing with reverse arrows November 10, 2026 by José Valim, Guillaume Duboc in Internals https://elixir-lang.org/blog/?category=Internals This article explains how Elixir implements type inference and type narrowing 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 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/ 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 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 can be used in any context. For example, imagine this Elixir function, where x starts with type dynamic , as there is no type signature: python 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 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 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 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: python 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 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 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. And the refinement itself is often quite precise, thanks to reverse arrows, which we will explore next. Reverse arrows 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 : python 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: php $ integer or float - integer or float 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 with two arrows: php $ integer - integer $ float - float 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, 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? python def negated remainder x , do: rem negate x , 2 You may think x is dynamic integer or float , because that’s the domain of 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 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 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, 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 . Guards Now we have the foundation to understand how Elixir performs type inference of guards. Take this function clause: python 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 : php $ 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 result for which a guard succeeds, and propagate it through the arrows in reverse: 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 arrow of is integer that can return true is integer - true , therefore we know x must be an integer 3. The only arrow of is bitstring that can return true is bitstring - true , therefore we know y must be a bitstring 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. Let’s see more examples. Type narrowing also known as occurrence typing 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: js 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 one from the previous sections. Within the do -branch, we consider the scenarios 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 also applies to patterns and case -expressions For example: php 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 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 proper types for this example: y = is integer x if y do y is true, x remains dynamic else y is false, x remains dynamic end 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 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: 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-referencing the variables 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 , such as data constructors: python 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 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.