Type refinement

Type refinement means that the type of a variable or another term becomes more specific in certain situations. This chapter describes when and where type checker is able to perform type refinement.

Type refinement for matching clauses

Variable refined using guard. Example:

-spec f1(atom() | integer()) -> atom().
f1(X) when is_atom(X) -> X; % here, X :: atom() because is_atom(X)
f1(_)                 -> some_atom.

Variable in a pattern like Var = ... or ... = Var. Example:

-spec f2(#my_record{} | undefined) -> integer().
f2(#my_record{} = R) -> R#my_record.some_field; % here, R :: #my_record{}
f2(undefined)        -> 42.

Type refinement for mismatching clauses

When checking a case clause, a function clause, a receive clause or a clause in try and catch, we make use of information from the previous clauses to make the type checking more exact. When the type checker knows exactly what must have mismatched in the previous clauses for the execution to be able to reach the following clauses, those types can be excluded when checking the the rest of the clauses.

Refinement of the term(s) subject to pattern matching

This form of refinement can only be applied when the type checker knows exactly why a clause mismatches and those values can be excluded from the types. That means that we can refine types that consist of unions of singleton types. Singleton types are single integers, atoms, the empty list, the empty tuple and tuples consisting of singletons. Empty maps and empty binaries are singleton types too, but currently Gradualizer is not capable of using these for refinement. Free variables and _ (match all) can also be part of pattern. We know that these can never cause a pattern to mismatch.

-spec foo(apa | hest | 42) -> 42.
foo(apa)  -> 42;  %% if this mismatches, apa is excuded
foo(hest) -> 42;  %% if this mismatches, hest is excluded
foo(X)    -> X.   %% here, X can only be 42, so no type error here

Refinement of bound variables after mismatching clauses

The type of a variable Var bound already before an if, case or other construct with clauses, can be refined using information about why the previous clauses have failed to match. The following conditions must be fulfilled for this refinement to happen:

1. The patterns of a clause must match all possible input (meaning that every pattern is either _ or a free variable)
   • Note: if clauses have no patterns, so this condition is automatically fulfilled
2. There is a single guard on the form is_TYPE(Var) for the clause and no other guards are present

If these conditions are fulfilled, the only reason for the clause to mismatch is the guard. Thus, for the following clauses within the same construct (if or case etc.), the type of Var can be refinement by excluding TYPE from the type of Var.

Example:

-spec f(integer() | atom()) -> atom().
f(Var) ->
    case Var of
        _ when is_integer(Var) -> hello;
        _                      -> Var       % here Var :: atom()
    end.

What prevents type refinement?

1. Guards. If there is any uncertainty to why a clause mismatches, such as a guard which depends on values unknown at compile time, we can not exclude any values. We cannot exclude the possibility that the clause mismatches just because of the guard. Any guards other than the ones mentioned above prevent Graudalizer from refining.

%% This gives a type error
-spec guard_prevents_refinement(apa | bepa) -> bepa.
guard_prevents_refinement(X) ->
    Y = receive Message -> Message end,
    case X of
        apa when Y /= yellow -> bepa;
        Other                -> Other  %% Here, Gradualizer cannot exclude apa
    end.

2. Imprecision. If a type or a part of a type in a clause is matched against a pattern that we cannot remove from the type, we cannot refine.

-spec imprecision_prevents_refinement(float(), a|b) -> b.
imprecision_prevents_refinement(3.14, a) -> b;
imprecision_prevents_refinement(_,    X) -> X. %% 'a' cannot be excluded