Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir

TL;DR

This paper introduces a formalized gradual type system for Elixir that combines semantic subtyping and runtime checks to enable precise, sound static analysis without altering the language's existing compilation or runtime environment.

Contribution

It presents a novel type system with strong functions and guard analysis, ensuring soundness and expressiveness while maintaining compatibility and performance in Elixir.

Findings

Type soundness achieved through runtime checks.

Precise type refinement via guard analysis.

Effective on large-scale industrial codebases.

Abstract

We formalize a new type system for Elixir, a dynamically typed functional programming language of growing popularity that runs on the Erlang virtual machine. Our system combines gradual typing with semantic subtyping to enable precise, sound, and practical static type analysis, without requiring any changes to Elixir's compilation pipeline or runtime. Type soundness is ensured by leveraging runtime checks -- both implicit, from the Erlang VM, and explicit, via developer-written guards. Central to our approach are two key innovations: the notion of "strong functions", which can be assigned precise types even when applied to inputs that may fall outside their intended domain; and a fine-grained analysis of guards that enables accurate type refinement for case expressions and guarded function definitions. While type information is erased before execution and not used by the compiler, our "safe erasure" gradual typing strategy maintains soundness and expressiveness without compromising compatibility or performance. This work lays the theoretical foundation for Elixir's new type system, outlines its integration into recent versions of the language, and demonstrates its effectiveness on large-scale industrial codebases.