Set-Theoretic Types for Erlang in Practice (Experience Report)

Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting type solver remain tractable on real-world code? Can the type system reflect the programmer's intention even though no principal types exist? And does it actually detect or avoid errors in real codebases? This paper reports on our experience on applying Etylizer, a set-theoretic type checker for Erlang, to its own implementation. We test whether the type system can express the patterns arising in a non-trivial Erlang codebase. In addition, we examine the design tradeoffs that set-theoretic types present across exhaustiveness, function overloading, numeric precision, gradual typing, and occurrence typing, and relate them to how other type systems handle the same dimensions. Our findings suggest that set-theoretic types are expressive enough to capture Erlang programmers' intentions: intersection types and automatic exhaustiveness checking provide clear advantages, and the approach is not in conflict with Erlang's let-it-crash idiom. Although the type system lacks principal types, types can be refined as needed through annotations. Scalability for type checking is largely addressed, and in the cases where it remains an issue, less expressive tools face similar limitations.