Understanding Set-Theoretic Types and Strong Arrows in Elixir's Gradual Typing

In a recent article, José Valim discusses the efforts towards creating a type system for Elixir, revolving around set-theoretic types and strong arrows as a new approach for gradual typing. Such a system is founded on set operations like union, intersection, and negation, allowing the representation of Elixir's types in a more expressive and expansive manner. Examples of this typing approach involve typing atoms as themselves and leveraging bounded quantification (bounded polymorphism) using intersections for bounds, rather than introducing new constraints. Valim introduces the concept of strong arrows: statically provable functions that guarantee type consistency at runtime without the need for additional checks. This aligns well with Elixir's runtime type-checking behavior and Erlang VM optimizations. However, Valim acknowledges challenges and trade-offs when interfacing static and dynamic code within existing Elixir codebases. The article indicates that the shift from research to development of this type system is underway, with ongoing experimentation and reliance on community feedback. The work is supported by multiple organizations in the Elixir community.