Set-Theoretic Types for Erlang: Theory, Implementation, and Evaluation
This addresses runtime errors for Erlang developers, but it is incremental as it builds on existing type specification language features.
The authors tackled the problem of runtime errors in Erlang due to its dynamic typing by developing a set-theoretic type system that guarantees type soundness and decidability, with an implementation that successfully verified real-world Erlang code in a case study.
Erlang's dynamic typing discipline can lead to runtime errors that persist even after process restarts. Some of these runtime errors could be prevented through static type checking. While Erlang provides a type specification language, the compiler does not enforce these types, thereby limiting their role to documentation purposes. Type checking Erlang code is challenging due to language features such as dynamic type tests, subtyping, equi-recursive types, polymorphism, intersection types in signatures, and untagged union types. This work presents a set-theoretic type system for Erlang which captures the core features of Erlang's existing type language. The formal type system guarantees type soundness, and ensures that type checking remains decidable. Additionally, an implementation of a type checker is provided, supporting all features of the Erlang type language and most term-level language constructs. A case study with modules from Erlang's standard library, an external project, and the type checker itself demonstrates its effectiveness in verifying real-world Erlang code.