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". Dialyzer aims to detect definite type errors instead of possible ones, focusing on being sound for defect detection 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. In 1997, an attempt was made at a subtyping system by well-known computer scientists Marlow and Wadler. Unfortunately, this effort never covered the full breadth of the language, most notably missing support for checked inter-process messages. 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 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 and the other via runtime dynamic monitoring of types.
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.
 Practical Type Inference Based on Success Typings - http://bit.ly/1MflvBj
 A Prototype of a Soft Type System for Erlang - http://bit.ly/1QmzFZj
 A Practical Subtyping System For Erlang - http://bit.ly/1QmzKMG
 A History of Erlang - http://bit.ly/1TNUomk
 Detection of Asynchronous Message Passing Errors Using Static Analysis - http://bit.ly/1YidFhc
 Session Typing for a Featherweight Erlang - http://bit.ly/1NRHx2r  Monitoring Erlang/OTP Applications using Multiparty Session Types - http://bit.ly/1QqQy4W
- 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).
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
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:
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!