标题： 守卫分析和安全擦除渐进类型系统：Elixir 的类型系统 显示英文标题

标题： Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir

摘要： 我们为Elixir定义了一种新的类型系统，Elixir是一种在Erlang虚拟机上运行的日益流行的动态类型函数式编程语言。 我们的系统结合了渐进类型和语义子类型，以实现精确、安全且实用的静态类型分析，而无需对Elixir的编译流程或运行时进行任何更改。 通过利用运行时检查来确保类型安全性——包括来自Erlang VM的隐式检查以及通过开发者编写的guards的显式检查。 我们方法的核心是两个关键创新： "强函数" 的概念，即使应用于可能超出其预期域的输入，也可以分配精确的类型；以及对guards的细粒度分析，这使得对case表达式和带guards的函数定义进行准确的类型细化成为可能。 虽然类型信息在执行前被擦除，并且编译器不使用它，但我们的“安全擦除”渐进类型策略在不损害兼容性或性能的情况下保持了安全性和表达性。 这项工作为Elixir的新类型系统奠定了理论基础，概述了其在最近版本语言中的集成，并在大规模工业代码库中证明了其有效性。 显示英文摘要

摘要： 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.