We formalize a new type system for Elixir, a dynamically typed functional programming language of growing popularity that runs on the Erlang virtual machine. Our system combines gradual typing with semantic subtyping to enable precise, sound, and practical static type analysis, without requiring any changes to Elixir's compilation pipeline or runtime. Type soundness is ensured by leveraging runtime checks -- both implicit, from the Erlang VM, and explicit, via developer-written guards. Central to our approach are two key innovations: the notion of "strong functions", which can be assigned precise types even when applied to inputs that may fall outside their intended domain; and a fine-grained analysis of guards that enables accurate type refinement for case expressions and guarded function definitions. While type information is erased before execution and not used by the compiler, our "safe erasure" gradual typing strategy maintains soundness and expressiveness without compromising compatibility or performance. This work lays the theoretical foundation for Elixir's new type system, outlines its integration into recent versions of the language, and demonstrates its effectiveness on large-scale industrial codebases.

翻译：我们为 Elixir 形式化了一种新的类型系统，Elixir 是一种运行在 Erlang 虚拟机上的动态类型函数式编程语言，其流行度日益增长。本系统将渐进类型化与语义子类型化相结合，实现了精确、可靠且实用的静态类型分析，且无需对 Elixir 的编译管道或运行时进行任何修改。类型安全性通过利用运行时检查来保障——既包括来自 Erlang 虚拟机的隐式检查，也包括开发者编写的守卫所实现的显式检查。本方法的核心在于两项关键创新：“强函数”概念，即便在输入可能超出其预期域时，也能为其分配精确类型；以及一种细粒度的守卫分析，能够对 case 表达式和带守卫的函数定义实现精确的类型精化。尽管类型信息在执行前被擦除且编译器不加以利用，我们的“安全擦除”渐进类型化策略在维持兼容性与性能的同时，保障了类型系统的健全性和表达力。本工作为 Elixir 的新类型系统奠定了理论基础，概述了其与语言最新版本的集成，并在大规模工业代码库上验证了其有效性。