Elixir 1.20 ships gradual set-theoretic types, catches bugs without annotations

Elixir 1.20 marks the first development milestone of a multi-year effort to bolt a sound, gradual, set-theoretic type system onto the language. The release performs type inference and gradual type checking on every Elixir program without requiring annotations, surfacing dead code and verified bugs—violations guaranteed to fail at runtime—with a low false-positive rate. The work, backed by CNRS, Remote, Fresha, and Tidewave, builds on research first published in 2022 and a 2023 paper on the underlying design.

The distinguishing feature is how Elixir handles its dynamic() type. Unlike the permissive any() of most gradual systems, dynamic() carries compatibility and narrowing properties: a violation fires only when supplied and accepted types are disjoint, and the inferred type tightens as the value flows through operators, field accesses, and guards. A variable used as data.a + data.b, for example, is narrowed to a map with numeric a and b fields, so dropping the .b access produces a clean diagnostic.

Most of the release went into teaching the checker to read guards, pattern matches, tuple and map size checks, and case-clause refinements. The implementation passes 12 of 13 categories in the “If T” type-narrowing benchmark, suggesting precise inference is achievable on ordinary, unannotated Elixir code. User-facing type annotations are still to come; when they land, code that avoids dynamic() will behave like a fully static language, with sound transitions across the static-dynamic boundary and no extra runtime checks.