This talk introduces a type system for Erlang based on Gradual Typing. The principles of Gradual Typing has emerged in the type system research community over the last decade and has resulted in several successful type systems for dynamically typed languages. Gradual Typing is tailored to mix static and dynamic code. The type system provides pay-as-you-go static checking: the more type annotation in the program, the more static checking will be performed.Erlang provides a unique set of challenges for creating a type system. The language already has a widely used notation for types despite lacking a standardized type system. We will cover the design decisions we made to accommodate this notation and some of the other challenges.We have implemented the type system in a tool called Gradualizer. Type checking existing Erlang code has revealed a number of additional interesting challenges. In particular, it is common for Erlang programmers to write uninhabited types when mixing polymorphism and subtyping. Since our goal has been to be able to cover as much of the existing code as possible, we've come up with a new way of interpreting bounded polymorphism to handle these cases.
Dialyzer is currently the most popular tool for the static checking of Erlang. Gradualizer turns out to be somewhat complementary to Dialyzer. While Dialyzer aims to give no false positives, Gradualizer always reports an error whenever a type spec doesn't match the code. We'll provide an in-depth comparison of the two tools.
Cornwallis South West,
University of Kent,