Same same but different: A Comparative Analysis of Static Type Checkers in Erlang
This program is tentative and subject to change.
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 that is 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 20% - 40% 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.
This program is tentative and subject to change.
Mon 2 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 30mTalk | Same same but different: A Comparative Analysis of Static Type Checkers in Erlang Erlang Florian Berger University of Kaiserslautern-Landau, Albert Schimpf University of Kaiserslautern-Landau, Annette Bieniusa University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences | ||
11:30 30mTalk | Nominal Types for Erlang Erlang Isabell Huang , John Högberg , Tobias Wrigstad Uppsala University, Kiko Fernandez-Reyes Ericsson, Sweden | ||
12:00 30mTalk | Modeling Erlang Compiler IR as SMT Formulas Erlang |