Erlang is a functional programming language with dynamic typing. The language offers great flexibility for destructing values through pattern matching and dynamic type tests. Erlang also comes with a type language supporting parametric polymorphism, equi-recursive types, as well as union and a limited form of intersection types. However, type signatures only serve as documentation, there is no check that a function body conforms to its signature. Set-theoretic types and semantic subtyping fit Erlang's feature set very well. They allow expressing nearly all constructs of its type language and provide means for statically checking type signatures. This article brings set-theoretic types to Erlang and demonstrates how existing Erlang code can be statically typechecked without or with only minor modifications to the code. Further, the article formalizes the main ingredients of the type system in a small core calculus, reports on an implementation of the system, and compares it with other static typecheckers for Erlang.

翻译：Erlang是一种动态类型函数式编程语言，该语言通过模式匹配和动态类型测试为值解构提供了极大的灵活性。Erlang还配备了一种支持参数多态、等递归类型、联合类型以及有限形式交集类型的类型语言。然而，类型签名仅作为文档存在，函数体与其签名是否一致并未得到检查。集合论类型与语义子类型化非常契合Erlang的特性集，它们能够表达Erlang类型语言中的几乎所有构造，并为静态检查类型签名提供了手段。本文将集合论类型引入Erlang，并展示了如何对现有Erlang代码进行静态类型检查——而无需或仅需对代码进行微小修改。此外，本文在一个小型核心演算中形式化了该类型系统的主要组成部分，报告了系统的实现，并与其他Erlang静态类型检查器进行了比较。