Set-Theoretic Types for Erlang: Theory, Implementation, and Evaluation

TL;DR

This paper introduces a set-theoretic type system for Erlang that enhances static type checking, ensuring type soundness and decidability, with an implementation that verifies real-world code to reduce runtime errors.

Contribution

It presents the first formal set-theoretic type system for Erlang, including a sound, decidable type checker supporting core language features and practical evaluation.

Findings

Type checker successfully verifies real-world Erlang modules.

The system guarantees type soundness and decidability.

Implementation supports all core Erlang type features.

Abstract

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.