Type Inference for Erlang Unions and Funs: eqWAlizer’s Approach

Erlang’s unions and funs pose interesting challenges for sound and expressive type checking. We’ll: - Tour some interesting cases and design considerations - See approaches employed in eqWAlizer (open source Erlang type checker used at WhatsApp) and other industrial type checkers - Point toward future work

Union Types

Union types in Erlang are non-discrimminated. Unlike algebraic data types, nothing prevents unions from overlapping. This poses challenges for type-checking.

Here are some interesting cases adapted from real-world code where industrial type-checkers struggle to be sound, expressive, and provide actionable error messages. Industrial type checkers can struggle with safely and fairly deciding which branch of a union an argument type should unify with:

-spec extract([T] | [[T]]) -> T.
extract([[T]]) -> T;
extract([T]) -> T.

-spec test07({T} | {T, T}) -> T.
test07({X}) -> X;
test07({X, X}) -> X.

Lambdas

Consider a call to lists:foldl:

-spec foldl(fun((T, Acc) -> Acc), Acc, [T]) -> Acc
....

Reversed = lists:foldl(fun (X, Acc) -> [X | Acc] end, [], [1, 2, 3])

Some things that make this kind of case tricky are that Acc is both an input and an output to the fun, and we don’t know that [] is a list of numbers until looking we look inside the lambda. We type-check such calls without requiring any annotations at call sites, and without giving up local type inference (Pierce and Turner, 2000).