Exhaustiveness checking and algebraic data types

Gradualizer, when checking the following code:

-type allergen() :: eggs
                  | chocolate
                  | pollen
                  | cats.

-spec allergic_to(allergen()) -> boolean().
allergic_to(Allergen) ->
  case Allergen of
    eggs -> true;
    chocolate -> false;
    cats -> true
  end.

Will report the following warning:

allergen.erl: Nonexhaustive patterns on line 11 at column 5
Example values which are not covered:
	pollen

This feature is called exhaustiveness checking.

In general, exhaustiveness checking detects unreachable clauses and non-exhaustive pattern matches. Gradualizer applies exhaustiveness checking to clause lists of functions, case expressions, and try ... of expressions. An exhaustiveness check will only be tried on fully typed parameters, i.e. any() disables the exhaustiveness check.

Algebraic data types

Thanks to exhaustiveness checking Gradualizer offers functionality similar to algebraic data types known from statically typed functional languages like ML (OCaml, Standard ML), Haskell, Elm, or PureScript.

We can define the following type and have it properly checked:

-record(record, {}).
-type record() :: #record{}.

-type complex_t() :: {string, string()}
                   | {list, list(allergen())}
                   | {atom, example_atom | another_atom}
                   | {binary, binary()}
                   | {record, record()}
                   | {map, #{non_empty := true}}
                   | {integer, integer()}
                   | {float, float()}
                   | {tuple, {integer(), string()}}.

-spec complex_match(complex_t()) -> ok.
complex_match({list, _}) -> ok.

There are a few important points to note:

• the list variant has to be fully typed, i.e. it cannot be just {list, list()}, as the latter translates to {list, list(any())}, and any() disables exhaustiveness checking
• string() is an alias for list(char())
• the map variant has to define a fully typed map, i.e. a map with all fields typed, since just map() will disable exhaustiveness checking; an empty map #{} is fine, though not very useful
• the tuple variant has to be fully typed, i.e. {tuple, {integer(), string()}} is fine, but {tuple, tuple()} is not, due to the size and element types of the tuple being unknown

This aspect of exhaustiveness checking, that is enabling the use of algebraic data types in Erlang, should be fully supported by Gradualizer.

Known limitations

Exhaustiveness checking, apart from enabling algebraic data types, also offers limited support for patterns on builtin types. However, in this application it is best effort, that is there are conditions under which Gradualizer will not try an exhaustiveness check. In general this stems from the complexity of patterns allowed by Erlang.

For example, matching on two initial elements of a list is not supported as it would require tracking the list length in the type:

%% NEGATIVE EXAMPLE - this will not be checked for exhaustiveness!

-spec too_complex(list(integer())) -> empty | exactly_one | at_least_two.
too_complex([]) -> empty;
too_complex([Cs]) -> exactly_one;
too_complex([C1, C2 | Cs]) -> at_least_two.

TODO: provide an example with binary matching