Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Erlang’s tooling ecosystem traditionally prioritizes flexibility over strict static guarantees, often leaving programming mistakes undetected—particularly in educational settings where students expect compiler-like feedback. Etylizer, a static type checker based on set-theoretic types, aims to provide stronger guarantees, but has mainly been evaluated on mature, idiomatic code. We present a retrospective study of approximately 2,700 student Erlang projects collected over five years to assess Etylizer’s behavior on novice-written code. Although only 14.9% of functions include type specifications, Etylizer identifies meaningful errors even in unannotated code.
The study also revealed that Etylizer’s exhaustiveness check for case/if expressions spuriously rejects a class of otherwise well-typed programs. We refined Etylizer’s type system to properly handle such programs. Evaluation on student and open-source projects shows that this refinement eliminates all observed spurious rejections without regressions.
Our findings demonstrate that educational code can reveal limitations hidden in expert-oriented codebases and provide valuable insights for improving practical static analysis tools.