-
Notifications
You must be signed in to change notification settings - Fork 35
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
No errors are flagged for guarded function clauses #501
Comments
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:
Of these, -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.
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, 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:
This is an error which stems from 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 For example, refining 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 There are some more attempts at wrangling BTW, @duncanatt, what's you perspective on Gradualizer? Are you conducting some type system research? |
I am experimenting with Gradualizer on the code below, expecting it to complain.
However, no error is flagged. Similarly, no error is raised for this function:
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
, whereasinc_2
type checks). Is there something that I am missing, please?The text was updated successfully, but these errors were encountered: