The type system landing in Elixir 1.20 has been discussed in fragments across a lot of threads. A recent BEAM There, Done That episode brings the full picture together in one place, with Guillaume Duboc (PhD from IRIF Paris, now at Dashbit) and Annette Bieniusa (professor, RPTU Germany, building a parallel etalizer for Erlang) both on the same conversation.
What’s worth knowing for Elixir developers specifically:
The system is currently in warning mode, not rejection mode. When a warning fires, the design goal is that it reflects a definite bug 90% of the time, following the same philosophy as Dialyzer. Strict rejection - where a function with a type annotation must satisfy that contract at compile time or the program doesn’t compile - is a future step, not part of the initial release.
Message typing is explicitly out of scope for now. The current system types the functional core: functions, pattern matching, unions, intersections, negations. Processes and messages are handled through the gradual dynamic escape hatch until that feature is tackled separately.
The gradual design is not like TypeScript’s any. The dynamic type is part of the set-theoretic structure from the ground up, not bolted on. That means the type checker knows how to reason about gradual types structurally, which avoids some of the awkward interactions TypeScript has with any and unknown.
Francesco’s closing frame in the episode is worth sharing: Elixir 1.20’s type system isn’t the end of a 30-year argument. It’s the first moment that argument has both the theoretical foundations and the engineering pragmatism to actually move forward together.
Try the RC and report back. Both teams explicitly want feedback on where the current warnings are useful and where they’re generating noise.