Type refinement for extended numeric types about gradualizer HOT 11 CLOSED

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 neg_inf and pos_inf in ranges. That way all integer types are reducible to A..B and we some more types we didn't have before.

from gradualizer.

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:

-spec f(non_neg_integer()) -> pos_integer().
f(0) -> 1;
f(N) -> N.

=> The variable 'N' on line 7 has type non_neg_integer() but is expected to have type pos_integer()

In Gradualizer's type system non_neg_integer() is not a compatible subtype of pos_integer(). Gradualizer thinks based on the type spec that the argument N of the function has the type non_neg_integer() hence the return type of f/1 is also non_neg_integer(). It cannot infer that N cannot be zero because of pattern matching (at least in the current version). This sounds like a hard problem. @josefs what do you think?

from gradualizer.

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 non_neg_integer() and we've already pattern matched on 0 in the first branch, the second branch must then have type pos_integer(). Doing this kind of type refinement in general so that it works also for e.g. ranges, is a hard problem. Not insurmountable, but hard. But perhaps this particular special case in your example programs are important enough to warrant a hack which deals with only this specific situation.

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.

from gradualizer.

I've updated the title to accurately reflect the deeper issue here.

from gradualizer.

@josefs probably this is not very big issue - you always can specify just integer type like in normal static-typed languages like haskell. Problems will begin when Gradualizer will start to interact with OTP/Elixir core code that contains extended numeral types, but let's think about it later maybe

from gradualizer.

The simplest solution is just implicit conversion of extended numeral types to standard numeral types in Gradualizer code

from gradualizer.

I thought this might be fixed, so I just checked. The factorial example currently gives the error

The operator '-' on line 5 is expected to have type non_neg_integer() which is too precise to be statically checked

However, the return type pos_integer() is closed under multiplication, so no error for that.

from gradualizer.

@UlfNorell, @josefs What do you think about supporting integer range type minus with constants? E.g. N - Constant where N :: non_neg_integer()? Is it too strange of a typing rule?

If we handle that, this example would pass, since we already have N :: pos_integer() here, from refinement using the previous clause. I imagine this kind of recursions with minus one are common enough.

The example in Erlang syntax:

-spec factorial(non_neg_integer()) -> pos_integer().
factorial(0) -> 1;
factorial(N) -> N * factorial(N - 1).

from gradualizer.

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 non_neg_integer()?

It's easy to get the example to go through by pushing in pos_integer() and 1 (in arith_op_arg_types):

        _ 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

from gradualizer.

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. neg_inf..-2).

But apart from finite ranges, I guess pos_integer() - 1 :: non_neg_integer() is the only example with named types for which this works, so perhaps this single example is worth supporting. We can refer to the existence of non_neg_integer() to justify it, noting that there is no type named non_pos_integer().

from gradualizer.

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.

from gradualizer.