Type refinement using comparison guards

[zuiderkwast]

Refinement using comparisons <, >, =<, >=, ==, /=, =:=, =/= in guard expressions on the form Var <op> Const and Const <op> Var.

%% Matching clause
-spec p1(integer()) -> pos_integer().
p1(N) when N > 0 -> N;
p1(_) -> 42;

%% Mismatching clause
-spec p2(integer()) -> pos_integer().
p2(N) when N =< 0 -> 42;
p2(N) -> N; %% Here the range neg_inf..0 is excluded, so N :: pos_integer().

%% More complex mismatching clause
-spec p3(integer() | undefined) -> pos_integer().
p2(N) when N < 1; is_atom(N) -> 42;
p2(N) -> N.

Erlang's term ordering

number < atom < reference < fun < port < pid < tuple < map < nil < list < bit string

can be used to turn an expression like X < 10 into the refined var binding X :: neg_integer() | 0..9 | float().

Likewise, from a guard like X > 2 we get X :: 3..pos_inf | float() | atom() | reference() | ... | bitstring().

Comma-separated guard expressions like when X > 2, X < 10 are combined using GLB to produce X :: 3..9 in the body of the matched clause.

I suggest dividing the work into 3 PRs:

1. Matching clauses

I think implementation is straight-forward.

2. Mismatching clauses with only one guard expression

We must be able to prove that the combination of guards is the reasons for the clause to mismatch, so I suggest the following limitations:

1. The patterns must be match-all (free vars and _)
2. Only one guard expression exists for the clause

3. Mismatching clauses with andalso/orelse

The 2nd limitation for mismatching clauses is replaced by these three:

• All guard expressions in the same clause must constrain the same variable
• Guards on the form is_TYPE(X) are also allowed
• Combinations of comma, semicolon, and, or, andalso, orelse allowed
  • comma, and, andalso => LUB
  • semicolon, or, orelse => GLB