BEAM There, Done That with Annette Bieniusa & Guillaume Duboc - Typing Erlang & Elixir After 30 Years

Sharing a BEAM There, Done That episode that covers both efforts in the same conversation, which I haven’t seen discussed much here.

Annette Bieniusa (RPTU, Germany) is building etalizer, a type system for Erlang based on set-theoretic types - the same theoretical foundation that Guillaume Duboc (Dashbit, IRIF Paris) used for the type system shipping in Elixir 1.20. Both are grounded in semantic subtyping with union, intersection, and negation types. But the design choices diverge.

The most relevant distinction for Erlang developers: etalizer keeps existing Erlang type specs as the annotation language. The premise is that Erlang codebases already have specs written as documentation and Dialyzer hints. Etalizer takes those same annotations and enforces them strictly - which is a meaningful shift from what Dialyzer does with them today.

Dialyzer is bottom-up: it infers what it can and looks for inconsistencies, treating your specs as additional type information rather than as hard contracts. Etalizer is top-down when annotations are present: write a spec, and the body of that function is checked against it strictly, with the type checker propagating that assumption through pattern matches and branches.

A few things worth discussing from an Erlang perspective:

The episode addresses the concern that types might lead developers to write fewer supervision trees and less defensive code. Both guests are relatively unconvinced this is the primary risk on the BEAM - supervision trees handle a different failure class (concurrency, environment, distribution) that types can’t touch. Static types and OTP solve different problems and aren’t in tension in the way this concern implies.

There’s also a discussion of what types potentially unlock beyond bug detection: the possibility of using static type information to enable runtime optimizations in the JIT, something the BEAM already does with internally derived type information at the instruction level.

Annette’s paper “Same Same But Different” maps the broader landscape of type systems approaches for BEAM languages if you want the written version.