No errors are flagged for guarded function clauses
duncanatt opened this issue · 3 comments
I am experimenting with Gradualizer on the code below, expecting it to complain.
-spec inc_1(atom()) -> integer().
inc_1(X) when is_integer(X) -> X + 1.However, no error is flagged. Similarly, no error is raised for this function:
-spec inc_2(integer()) -> integer().
inc_2(X) when is_atom(X) -> X + 1.Once the guards are removed from the above functions, the expected behaviour is obtained (i.e. an error is flagged in the case of inc_1, whereas inc_2 type checks). Is there something that I am missing, please?
Hi, @duncanatt!
Thanks for raising this.
It's more complex than that, but a short answer is that Gradualizer is still experimental and just not complete. This means that there's some refinement happening, but not as much as there could be, and apparently obvious refinement failures are not signalled either.
Generally speaking refinement based on patterns (also known as exhaustiveness checking) is probably somewhat more advanced, but there's a little bit of refinement based on guard BIFs in place, too. The best way, though not necessarily the easiest, to know what's already supported is checking the tests. We have the following which somehow refer to type refinement:
19:19:14 erszcz @ x6 : ~/work/erszcz/gradualizer (master %)
$ fd refin test
test/known_problems/should_fail/refine_ty_vars.erl
test/known_problems/should_pass/refine_bound_var_on_mismatch.erl
test/known_problems/should_pass/refine_list_tail.erl
test/known_problems/should_pass/refine_mismatch_using_guard_bifs.erl
test/should_fail/exhaustive_refinable_map_variants.erl
test/should_fail/record_refinement_fail.erl
test/should_fail/tuple_union_refinement.erl
test/should_fail/type_refinement_fail.erl
test/should_fail/unreachable_after_refinement.erl
test/should_pass/record_refinement.erl
test/should_pass/refine_comparison.erl
test/should_pass/type_refinement_pass.erl
Of these, test/should_pass/type_refinement_pass.erl has some tests for type refinement based on guards:
-spec refine_bound_var_by_guard_bifs(ok | integer() | pid() |
#{x => y} | {x, y}) -> ok.
refine_bound_var_by_guard_bifs(X) ->
if
is_map(X) -> ok;
is_tuple(X) -> ok;
is_integer(X) -> ok;
is_pid(X) -> ok;
true -> X
end.
-spec refine_literals_by_guards(banana | 0 | {} | [] | pid()) -> pid().
refine_literals_by_guards(X) when is_atom(X) -> self();
refine_literals_by_guards(X) when is_integer(X) -> self();
refine_literals_by_guards(X) when is_tuple(X) -> self();
refine_literals_by_guards(X) when is_list(X) -> self();
refine_literals_by_guards(X) -> X.We can experiment by commenting out one of the clauses and running Gradualizer on the file:
-spec refine_bound_var_by_guard_bifs(ok | integer() | pid() |
#{x => y} | {x, y}) -> ok.
refine_bound_var_by_guard_bifs(X) ->
if
is_map(X) -> ok;
is_tuple(X) -> ok;
is_integer(X) -> ok;
%is_pid(X) -> ok;
true -> X
end.$ ./bin/gradualizer test/should_pass/type_refinement_pass.erl
test/should_pass/type_refinement_pass.erl: The variable on line 93 at column 26 is expected to have type ok but it has type ok | pid()
is_integer(X) -> ok;
%is_pid(X) -> ok;
true -> X
^
As we can see some refinement is actually taking place. I think a warning in case of obvious refinement failures would be a welcome addition.
In general, test/should_pass codify what should pass as valid code, test/should_fail what should fail type checking, and test/known_problems/should_{pass,fail} should respectively pass/fail, but lacks implementation in the type checker.
I hope this helps :)
Hi,
Thanks a lot for the information. It does help!
Hi Duncan,
Since you were interested in this topic and I bounced off a problem related to it last weekend I'll drop some notes here. Maybe they'll be useful - if not to you, then at the very least to a future me :)
One of the goals I have for Gradualizer is to make it capable of cleanly type checking itself. When there were no specs at all in the codebase there were few errors. Adding some specs unveiled a lof of inconsistencies and warnings to fix. The general pattern is that more specs lead to more warnings until we make the specs consistent. However, this is also a good source of feedback on how well Gradualizer is suited to type check real world code. The remaining 20 lines of warnings all lead to some issues in the logic of the type checker and not just sloppiness in the specs. The latest progress on this is in #504 and one of the issues I failed at solving so far was:
ebin/typelib.beam: The pattern {type, _, any} on line 113 at column 12 doesn't have the type af_constraint()
This is an error which stems from typelib:remove_pos/1 at ebin/typelib.erl:113 to work with type() - our representation of Erlang types. It's a complex type based on OTP's erl_parse and inheriting its idiosyncrasies. One of them being the fact that subnodes aren't of type type() itself, therefore typelib:remove_pos/1 called recursively on it has to have an intersection type.
Now, function intersection types (that is multiple-clause specs) have some support in Gradualizer, but it's based on type refinement via a set-theoretic difference. The intersection checking algorithm only proceeds to a subsequent spec clause if argument types of a previous spec clause are exhausted (i.e. reduced via refinement by the function's clauses to none()). However, type_diff (the set-theoretic difference refinement) is not complete, it doesn't cover all types/cases, which means that function intersection type checking is also limited to cases that refinement covers completely. This all hides behind just The pattern {type, _, any} on line 113 at column 12 doesn't have the type af_constraint() 🤔
For example, refining atom() ("any atom" type) with a singleton atom type (e.g. cat) is not possible, since that would require returning a negative type atom() \ cat. There's no support of negative types (yet?). Refining a finite union of atoms, on the other hand, is supported, so (cat | dog | wolf) \ cat gives dog | wolf. That's an example of how types might be refined to none(), which is used by the intersection type checking algorithm.
Currently, there are other type checking limitations on the programming style and flexibility offered by the Erlang syntax itself. For example, if we want Gradualizer to refine a type with multiple variants:
-type allergen() :: eggs | chocolate | pollen | cats.We have to match each of the variants explicitly:
match(eggs) -> ...
match(chocolate) -> ...
match(pollen) -> ...
match(cats) -> ...That is, it's not possible to use a guard expression, as you noticed in your original post:
match(Allergen) when Allergen =:= eggs; Allergen =:= chocolate -> ...Refinement on Allergen would not kick in in this last example - there's a specific check in the code not to even try refinement (or an exhaustiveness check), since we know guards are not handled yet.
There are some more attempts at wrangling typelib:remove_pos/1 to type check on https://github.com/erszcz/Gradualizer/tree/typelib-remove-pos-checking-issues.
BTW, @duncanatt, what's you perspective on Gradualizer? Are you conducting some type system research?