This talk will report about our progress in adding static and gradual typing to Elixir. We will present set-theoretic types, and how they are suited to represent the behavior of Elixir programs. Then, we will showcase the potential benefits of the type system, such as detecting common bugs and providing direct feedback on code quality.

In addition to exploring the use of types to describe and enforce function interfaces, we will outline the techniques we use to analyze Elixir’s patterns and guards. We will also delve into the concept of gradual typing and its ability to mix typed and untyped code, as well as to ease the optional transition of existing codebases towards types.

We will conclude by presenting forthcoming work and some research challenges that lie ahead.