Elixir is a dynamically-typed functional language running on the Erlang Virtual Machine, designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers. Static typing seems nowadays to be the most important request coming from the Elixir community. We present a gradual type system we plan to include in the Elixir compiler, outline its characteristics and design principles, and show by some short examples how to use it in practice. Developing a static type system suitable for Erlang's family of languages has been an open research problem for almost two decades. Our system transposes to this family of languages a polymorphic type system with set-theoretic types and semantic subtyping. To do that, we had to improve and extend both semantic subtyping and the typing techniques thereof, to account for several characteristics of these languages -- and of Elixir in particular -- such as the arity of functions, the use of guards, a uniform treatment of records and dictionaries, the need for a new sound gradual typing discipline that does not rely on the insertion at compile time of specific run-time type-tests but, rather, takes into account both the type tests performed by the virtual machine and those explicitly added by the programmer. The system presented here is "gradually" being implemented and integrated in Elixir, but a prototype implementation is already available. The aim of this work is to serve as a longstanding reference that will be used to introduce types to Elixir programmers, as well as to hint at some future directions and possible evolutions of the Elixir language.

翻译：Elixir是一种运行在Erlang虚拟机上的动态类型函数式语言，专为构建可扩展且易于维护的应用程序而设计。其特性使其被数百家工业机构和数万名开发者广泛采用。目前，静态类型似乎是Elixir社区最迫切的需求。我们提出了一种计划集成到Elixir编译器中的渐进类型系统，概述了其特性与设计原则，并通过简短示例展示了实际用法。为Erlang语言家族开发合适的静态类型系统，在过去近二十年中一直是一个开放的研究问题。我们的系统将具有集合论类型和语义子类型的多态类型系统移植到了该语言家族。为此，我们必须改进并扩展语义子类型及其相关的类型技术，以应对这些语言（尤其是Elixir）的若干特征，例如函数的元数、守卫的使用、记录与字典的统一处理，以及一种新的可靠渐进类型规则的需求——该规则不依赖于编译时插入特定的运行时类型检查，而是综合考虑虚拟机执行的类型检查与程序员显式添加的类型检查。此处提出的系统正在逐步实现并集成到Elixir中，且原型实现已可用。本工作旨在作为长期参考，用于向Elixir程序员介绍类型系统，同时指明Elixir语言的未来方向与可能的演进。