Current state of polymorphism support

[xxdavid]

Hi, what is the current state of polymorphism support in Gradualizer? I get the impression that Gradualizer can deal with polymorphic types but it actually fails to catch obviously looking bugs when using lists:map.

Here are my two test files:

-module(test_a).
-export([bools/0]).

-spec is_three(integer()) -> boolean().
is_three(3) -> true;
is_three(N) -> false.

-spec nums() -> [integer()].
nums() -> [1, 2, 3, 4].

-spec bools() -> [integer()]. % the return type should be [boolean()]
bools() -> lists:map(fun is_three/1, nums()).

-module(test_b).
-export([bools/0]).

-spec negate(boolean()) -> boolean().
negate(true) -> false;
negate(false) -> true.

-spec nums() -> [integer()].
nums() -> [1, 2, 3, 4].

-spec bools() -> [boolean()].
bools() -> lists:map(fun negate/1, nums()). % negate does not take integers

Gradualizer's output is clean on both files.

[erszcz]

Hi, @xxdavid!

Indeed, polymorphism support in Gradualizer is currently limited. There's some work in progress on solving constraints on type variables in #284 and #450. The former is the original work by @josefs, whereas the latter is my rebase to a more recent commit of the master branch together with some tests showing what new bugs would actually be caught and some config details to enable/disable constraint solving.

However, the latter PR, apart from discovering issues similar to the ones you bring up, exhibits a number of new false positives and noise when running the Gradualizer self-check, so it's not ready for prime time yet. For example:

ebin/gradualizer_lib.beam: The variable on line 31 at column 21 is expected to have type fun((_TyVar-576460752303417503, _TyVar-576460752303417471,
               _TyVar-576460752303417439) ->
                  _TyVar-576460752303417407) but it has type fun((...) -> any())

merge_with(F, M1, M2) -> maps:merge_with(F, M1, M2).

These issues are caused due to (at least) the following reasons:

• some constraints not being generated everywhere where they should be,
• AFAIU constraint representation in the type checker doesn't allow for unions of constraints - I didn't yet grok completely why it's needed, but that's what I got from Constraint solver #284 and comments in the code.

Until recently we also had a more serious issue in the type checker implementation - #458. Personally, I'm trying to make Gradualizer as useful as possible as soon as possible, which in practice means minimising the number of crashes and false positives it generates. I'm gauging this by the number of errors it generates when checking itself, but also by dogfooding on other projects, or by running broader analyses like #464.

Following the above approach, my current target was #461, since it allows to shed a few lines of self-check errors. This is now on the last mile, but calendar-wise it might still be a while due to the amount of time I can spend on this project. If you, or anyone else, would like to work on the solver in the meantime, then go for it! If you're interested from the perspective of a user, then it's definitely on the roadmap ;)

[xxdavid]

Thank you for a detailed explanation!

I might actually be interested in contributing to the project but it's probably better to start with fixing more minor and easier issues. Do you have any tips on how to get some understanding of the codebase or where to start? I am interested in types but my formal knowledge is still lacking. I began to read Pierce's Types and Programming Languages a few months ago but I had to stop quite early on because I didn't have enough time for it (I would like to return to reading it soon though). I've also made a toy language with a simple type inference and type checking. I also had a course where the HM type system for lambda calculus was taught as a part of the course but it was years ago and unfortunately I don't remember much from that. So with that in mind, do you also have any recommendations on what to read before trying to get into the codebase or should I rather jump directly into the code and try to grasp it somehow without the formal background?

[erszcz]

It's a pretty similar story in my case. I'm already done with Types and Programming Languages and it was definitely the right foundation to enable grokking Gradualizer internals. On the way I've worked on Erlang implementations of the TaPL type checkers, to help me understand how the simple interpreters and type checkers look like in Erlang in relation with the more fully fledged implementation of Gradualizer. Bidirectional Typing by Dunfield and Krishnaswami helped me understand the idea of local type inference aka bidirectional type checking (the difference between type_check_expr and type_check_expr_in in Gradualizer's src/typechecker.erl), which is not covered in TaPL - the paper introduces the concept really well, but since it's a survey quite a lot of the details later on are not applicable to Gradualizer.

When starting, though, it might be good to focus on fixing small issues/bugs, to get a better understanding of the general structure of the code. I only got to the literature when it became apparent that digging deeper requires a better understanding of the prior art. Some of them are labelled as "Good first issues" if you want to give it a go.

When I'm puzzled with "what to do next" I usually look at the issues (not all of which are immediately actionable), test/known_problems, or results of make gradualize. So far make gradualize still doesn't pass (we have less than 100 lines of errors which is checked by CI, but that's more than 0), so thus far I haven't run out of things to improve :)

[xxdavid]

Okay, thank you for the pointers. :) I'll try to start with fixing some smaller bugs then and maybe also reading TaPL alongside (your Erlang version will surely be helpful!).