term() to something else

[FrankBro]

Is there a way to constrain term() to a more precise type via guards? I would expect this to work. If not, would love to contribute.

-module(test).

-export([int/1]).

-spec int(term()) -> integer() | undefined.
int(I) when is_integer(I) -> I;
int(_) -> undefined.

The variable on line 6 at column 30 is expected to have type integer() | undefined but it has type term()

-spec int(term()) -> integer() | undefined.
int(I) when is_integer(I) -> I;
                             ^

[FrankBro]

Interestingly, if term() is replaced with any(), the test passes. Is this normal?

[FrankBro]

Actually it's kind of also bad because this passes:

-module(test).

-export([int/1]).

-spec int(any()) -> integer() | undefined.
int(N) when is_list(N) -> N;
int(_) -> undefined.

[gomoripeti]

hi @FrankBro unfortunately guards in general are not really supported yet. Guards should be handled as constraints and that is the feature (constraint solving) that is not implemented yet.

So this is not specific to term(). The reason why the particular test is passing with any() because that is the "dynamic type", which is a subtype of every other type by definition. (You noticed this well in you last example, where the is_list/1 guard is also ignored in the sense that no type info on N is deduced from its presence)

So stay tuned for constraint solving to come, eventually. (Though don't hold you breath, it's a pretty big feature)

[zuiderkwast]

I don't believe collecting constraints and solving them after traversing the whole function is the way to go for refinements on guards.

Rather, just refining using is_integer(I) => I :: integer() and then combinting the types using intersection types: I :: term() & I & list() => I :: term() & integer() => I :: integer().

Then, for the following clauses we exclude I :: integer() using the equivalent of set difference I :: term() \ integer()...

[zuiderkwast]

Also note that currently, term() is the top of the type system and any() is the unknown type. That's why the results differ.

[FrankBro]

This is kind of what I'm doing right now. Nicely enough, there is check_guards. I'm currently adding support for the BIFs and very simple stuff. Hoping I can send a PR in a few days.

[zuiderkwast]

206 is related.

[FrankBro]

Looking at the code, it seems aligned with what I'm trying to do. Anything I could do to help?

[zuiderkwast]

Don't know... Multiple small PRs are always easier to review and merge than large ones.

The current problem seems to be that @josefs doesn't have much time at the moment and we have some disagreement about whether parameter name annotations in specs have any meaning in the type system or not and about the semantics of intersection and union types involving the unknown type (any()).

We also have some performance bottle-neck in the normalize and glb functions, something I think can be solved by representing the types on "gradual disjunctive normal form" using binary decision diagrams, as described in this paper: https://www.irif.fr/~gc/papers/icfp17.pdf (specifically the appendix). It allows for efficient union, intersection, difference and subtype checking, as well as computing the (gradual) types of domain and function application. These operations also make refinement straight-forward and other code can be simplified. It's a rather large change though...

[zuiderkwast]

Do we have your example (or equivalent) as a test case under test/known_problems? If not, a first PR can be to add it.

[FrankBro]

I can collaborate a few if needed. It's what I'm using right now to try and implement it.

[FrankBro]

In my situation, I'm not too concerned with any() as our product mostly deals with term().

[FrankBro]

Here are the tests I had in mind. https://github.com/josefs/Gradualizer/compare/master...FrankBro:guard-support

[FrankBro]

I'm having a tough time getting records to be of the right type. If I do {type, P, record, []}, I get the type record() but I want a specific record type. Should I put that information in var binds or constraints? I tried putting just the atom name of the record but it didn't work so well, tried putting all the fields and their types, didn't work either.

Basically, knowing the atom name of a record, how do I construct the type of a record?

[zuiderkwast]

#my_record{} is represented as {type,141,record,[{atom,141,my_record}]} (if the line is 141)

I have made examples for most of Erlang's abstract format here: https://github.com/zuiderkwast/erlang_abstract_format#types

[FrankBro]

Not sure what I was doing wrong but it works now. Will send a PR.

[FrankBro]

https://github.com/josefs/Gradualizer/pull/241

[zuiderkwast]

The topics in this issue are covered in other issues. Thus, I'm closing this.

The difference (not any more) between term() and any() is #217.

Refinement of any() and term() to more specific gradual types using guards is related to #232.