-
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
Type refinement for extended numeric types #11
Comments
It should but apparently it does not yet. After fixing the first minor issue actually your example highlights a bigger problem. Given the below simplified function:
In Gradualizer's type system |
Arithmetic operators can now have arguments of type e.g. pos_integer(). This addresses part of #11. Still todo: support for inferring types of arithmetic operators.
There is some support for the extended numerical types, but it clearly can be better. @tim2CF, the reason you got the error message was that I hadn't added support for the extended numerical types as arguments to arithmetic operators. That's fixed now. Instead you get an error akin to the one from the example of @gomoripeti. That is a much deeper issue. You're asking the Gradualizer to refine the types based on pattern matching. In particular, you're asking it to figure out that since the input type is Do you consider this to be an important use case? I'm interested in your opinions. I currently consider this a very low priority issue. If you disagree, please let me know. |
I've updated the title to accurately reflect the deeper issue here. |
@josefs probably this is not very big issue - you always can specify just |
The simplest solution is just implicit conversion of extended numeral types to standard numeral types in Gradualizer code |
I thought this might be fixed, so I just checked. The factorial example currently gives the error
However, the return type |
@UlfNorell, @josefs What do you think about supporting integer range type minus with constants? E.g. If we handle that, this example would pass, since we already have The example in Erlang syntax: -spec factorial(non_neg_integer()) -> pos_integer().
factorial(0) -> 1;
factorial(N) -> N * factorial(N - 1). |
The main problem I see is that we are pushing types in, not inferring types bottom up. That is, we are computing the expected argument types from the return type instead of the other way around. What types should we push in if the expected result is It's easy to get the example to go through by pushing in _ when Op == '-' -> {type(pos_integer), {integer, erl_anno:new(0), 1}}; That seems a little ad hoc though, but maybe natural number recursion is common enough to warrant it. It gives you very precise errors: -spec factorial(non_neg_integer()) -> pos_integer().
factorial(0) -> 1;
factorial(N) -> N * factorial(N - 2).
%% The integer 2 on line 5 does not have type 1 |
I thought we can peek at the right operand and if it's a constant, we can adjust what we push for the left operand. A bit sneaky perhaps; hard grasp by the user, especially as it doesn't always work (unless we extend the type language with e.g. But apart from finite ranges, I guess |
Fwiw, I'm in favor of the ad hoc solution @UlfNorell. It seems to me that people are already asking for this kind of very specific types so I think it makes sense to support them. |
I have no objections. Recursion on a natural number is pretty fundamental. I'd also be in favour of making the type language less ad hoc by allowing |
Arithmetic operators can now have arguments of type e.g. pos_integer(). This addresses part of josefs#11. Still todo: support for inferring types of arithmetic operators.
Special case for integer recursion, e.g. the factorial function. Fixes josefs#11.
Should Gradualizer support extended numeric types like
non_neg_integer()
,pos_integer()
and others? Currently Gradualizer returns:nok
in this example (Elixir)Error is
The text was updated successfully, but these errors were encountered: