Set-theoretic Types for Erlang

TL;DR

This paper introduces set-theoretic types for Erlang, enabling static type checking in a language with dynamic typing and complex type features, through formalization and implementation.

Contribution

It adapts set-theoretic types to Erlang, allowing static verification of type signatures and demonstrating practical applicability with minimal code modifications.

Findings

Erlang code can be statically typechecked using set-theoretic types.

The proposed system formalizes core type constructs and compares favorably with existing typecheckers.

Implementation shows practical feasibility with minor code changes.

Abstract

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.