Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer’s structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang’s opaque types, thereby improving Dialyzer’s performance and maintainability.
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 |