📎 Webclip
Type inference and narrowing with reverse arrows
Elixir infers types by refining dynamic() as values are used. Instead of treating the dynamic type as a black box, it intersects it with the types expected by the functions a variable reaches, which can expose violations such as using the same value as both a number and a bitstring.
Reading notes#
dynamic()in Elixir meansdynamic(term()), andterm()is the top type, so inference starts broad and becomes more specific as code uses the value.- Multiple arrows make function types precise when a function has several clauses, as in
integer() -> integer()andfloat() -> float()fornegate/1. - Elixir propagates arrows in reverse, starting from the expected result and walking back to the arguments, which can narrow
xinrem(negate(x), 2)tointeger(). - Guards are inferred the same way: if a guard must succeed, Elixir reverses the arrows of
and,is_integer/1, andis_bitstring/1to infer the variable types that make the guard true. - Occurrence typing narrows variables differently in each branch of
ifandcase, using the return value of the tested expression to recover the input types that could have produced it. - In v1.20, narrowing could fail after assigning a guard expression to a variable, because the connection between the variable and the original expression was lost.
- Elixir v1.21 keeps track of the expression assigned to each variable, so narrowing can continue through assignments such as
y = is_integer(x)and even across more than one assignment. - The implementation is lazy: it only narrows when the variables involved are actually used in the branch.
- Reverse arrows also let Elixir refine expressions such as map values and other data constructors, so narrowing can flow back from
map.footo the original variablefoo. - The article links this approach to the If-T benchmark and says v1.21 passes all its tests, improving bug detection and reducing false positives once type signatures are added.