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）的若干特性，例如函数的参数数量、守卫（guard）的使用、记录与字典的统一处理，以及一种新型可靠的渐进类型化机制的需求——该机制不依赖于在编译时插入特定的运行时类型检查，而是同时考虑虚拟机执行的类型检查以及程序员显式添加的类型检查。本文所描述的系统正在逐步实现并集成到 Elixir 中，但原型实现已可使用。本工作的目的是作为一份长期参考，用于向 Elixir 程序员介绍类型，同时暗示 Elixir 语言的未来方向与可能的演进。