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语言的未来发展方向与可能的演变。