Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study

Abstract

Erlang’s tooling ecosystem traditionally prioritizes flexibility over strict static guarantees, often leaving programming mistakes undetected until runtime. This is particularly acute in educational settings, where students accustomed to statically typed languages 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 student Erlang projects collected over five years to assess Etylizer’s behavior on novice-written code. Although only 14% of student functions carry type specifications, Etylizer still finds bugs in unannotated code. The study also revealed that Etylizer’s exhaustiveness check spuriously rejects a class of otherwise well-typed programs: if-expressions that encode exhaustiveness in complementary comparison guards instead of ending in Erlang’s idiomatic catch-all true clause—a shape that community style guides discourage, that is rare in production code, but that beginners use markedly more often. We refined Etylizer’s type system to properly handle such programs. Evaluation on student and open-source projects shows that this refinement addresses spurious exhaustiveness rejections of the shape observed in the corpus. Our findings demonstrate that educational code can reveal limitations hidden in expert-oriented codebases and provide valuable insights for improving practical static analysis tools.