Point Of No Local Return: The Continuing Story Of Erlang Type Systems

If you've written Erlang, you've probably annotated a function with a -spec or two to be typed-checked with Dialyzer. This static analysis tool allows for gradual typing and infers success typings, "a type signature that over-approximates the set of types for which the function can evaluate to a value[0]". Dialyzer aims to detect definite type errors instead of possible ones, focusing on being sound for defect detection[1] and not generating false positives.

Though Dialyzer is very familiar to Erlang programmers now, the history leading up to its inception and standardization within the Erlang ecosystem is less so. It's a fascinating tale, including type system papers and implementations going back to at least 1996, with a soft-typing system by Lindgren[2]. In 1997, an attempt was made at a subtyping system by well-known computer scientists Marlow and Wadler[3]. Unfortunately, this effort never covered the full breadth of the language, most notably missing support for checked inter-process messages[4]. Despite these limitations, however, it still has a visible legacy in our spec annotations of today.

Of course, this story doesn't end here. There's work extending Dialyzer's analyses to detect message passing errors[5] and, separately, differing implementations of session types, a formalism to model distributed communicating processes. The latter has been implemented in at-least two different research projects: one via a system atop just a minimal concurrent fragment of Erlang for binary sessions[6] and the other via runtime dynamic monitoring of types[7].

This talk will walk through some of the approaches, issues, motifs, and type theory for the various attempts, past and present, to add a viable type system to the Erlang language.

[0] Practical Type Inference Based on Success Typings - http://bit.ly/1MflvBj

[1] http://bit.ly/1NvlhI0

[2] A Prototype of a Soft Type System for Erlang - http://bit.ly/1QmzFZj

[3] A Practical Subtyping System For Erlang - http://bit.ly/1QmzKMG

[4] A History of Erlang - http://bit.ly/1TNUomk

[5] Detection of Asynchronous Message Passing Errors Using Static Analysis - http://bit.ly/1YidFhc

[6] Session Typing for a Featherweight Erlang - http://bit.ly/1NRHx2r [7] Monitoring Erlang/OTP Applications using Multiparty Session Types - http://bit.ly/1QqQy4W

Talk objectives:

- Survey the history of attempts made at implementing a type system atop (all/or parts of) Erlang.

- Explore the reasons why Dialyzer is a standard today, and how it came to be that way.

- Discuss contemporary approaches modeled on type-checking messages between processes and conforming to the communication patterns of Erlang's distributed actor-based system (i.e. session types).

Target audience:

This talk would appeal to anyone interested in type system implementations and static annotation tools, especially the history of what's failed, remained as an influence, and/or "succeeded", as well as what's oncoming.

Slides
Video

About Zeeshan

Zeeshan became a programmer by way of film and music recording/technology. Moving from science center to startup to labs to working on distributed systems at Basho, he has accrued tons of necessary and needless information, and is a polyglot who will dive into anything related to programming languages, particularly functional ones, machine learning, and math. Additionally, he is one of the lead organizers and founders of Papers We Love!

GitHub: zeeshanlakhani

Twitter: @zeeshanlakhani

Back to conference page