Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang

Florian Berger, Albert Schimpf, Annette Bieniusa, and Stefan Wehr

In Proc. of Erlang Workshop. Milan, Italy. ACM, 2024.

Abstract

Erlang is a dynamically typed language with support for optional type annotations. Though Erlang's type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang's type annotations, their results differ in ways that can be challenging for users to interpret.

In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer's success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang's type language remains challenging when it comes to develop a correct and efficient static type checker.

Bibtex

@INPROCEEDINGS{BergerSchimpfBieniusaWehr2024,
  author = {Florian Berger and Albert Schimpf and Annette Bieniusa and Stefan Wehr},
  title = {Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang},
  year = 2024,
  isbn = 9798400710988,
  publisher = {{ACM}},
  url = {https://doi.org/10.1145/3677995.3678189},
  doi = {10.1145/3677995.3678189},
  booktitle = {Proc. of Erlang Workshop},
  address = {Milan, Italy}
}

Resources

online version