Skip to content
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

Use Local Type Inference approach to typecheck polymorphic calls #564

Merged
merged 17 commits into from
May 30, 2024

Commits on Apr 19, 2024

  1. Allow subst_ty/2 to take empty substitutions

    The function allows it, only the spec didn't.
    xxdavid committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    16ad12e View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2024

  1. Merge intersection function types using inner unions

    Consider a function spec:
        -spec negate(bool()) -> bool();
                    (integer()) -> integer().
    
    Sometimes, we want to make a single function type out of these two clauses.
    Using an outer union like fun((bool()) -> bool()) | fun((integer()) -> integer())
    leads to a loss of precision, because this type says that we either have
    a function that can take a bool, or we have a function that can take an integer
    (and we do not know which case it is). This means that we cannot apply a function
    of this type to anything unless we assert type or something like that.
    
    But we know for sure that it can take both, bools and integers! Therefore, using
    an inner union like fun((bool() | integer()) -> bool() | integer()) seems better
    to me as this way we know that it can take both.
    
    Of course, an ideal solution would be to use intersection types like
    fun((bool()) -> bool()) & fun((integer()) -> integer()), but Erlang doesn't have
    them in its syntax and so don't we in Gradualizer.
    xxdavid committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    e9a0afa View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2024

  1. Document a known problem related to union function types

    Union function types (`fun_ty_union`) do not seem to work. These simple
    examples should be perfectly valid. I think it throws that error because
    `expect_fun_type/3` inputs a list of function types (i.e., a clause),
    containing only a single element (the union of two function types).
    This leads to expecting an intersection function type later on
    (which is wrong).
    
    Note that these union function types aren't that much useful in practice
    as when you want to call them, all your argument types must be subtypes
    of parameter types of all the possible function types. That is, when
    you have a function of the type
        fun((integer()) -> integer()) | fun((atom()) -> atom())
    then you can only call it with `none()` as we don't know whether the
    function will accept integers or bools and no other type is a subtype
    of `integer()` and `atom()`.
    xxdavid committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    e51f914 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    8d70850 View commit details
    Browse the repository at this point in the history

Commits on May 26, 2024

  1. Use Local Type Inference approach to typecheck polymorphic calls

    We use the Local Type Argument Synthesis algorithm from
    https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf
    (a bit extended for our use case).
    
    This replaces the global constraint generation and constraint
    solver. It should result in a much more precise type error
    messages (pinpointing the exact location, not just the
    function) and more streamlined code (refactor will be made
    in a subsequent commit).
    
    For more details, see the original paper or
    https://github.com/josefs/Gradualizer/wiki/Polymorphism#typechecking-polymorphic-calls
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    b8cfa76 View commit details
    Browse the repository at this point in the history
  2. Make rigid vars also from type vars in function constraints

    The following type spec from gradualizer_db uses a type variables (K)
    as a bound for another type variable (Key):
    
        -spec add_entries_to_map([{Key, Value}], #{K => V}) -> #{K => V}
                                                 when Key :: K, Value :: V.
    
    Until now, we converted all Ks and Vs to rigid vars, but then Key
    and Value got replaced to plain vars K and S in solve_bounds/2.
    
    We must therefore convert the type variables to rigid type variables
    *after* the call to solve_bounds/2, which is what this commit does.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    3210bce View commit details
    Browse the repository at this point in the history
  3. Remove constraints from where they are not needed

    Flexible type variables may now appear only when typechecking a polymorphic call,
    in which case they are only in the type of that polymorphic function. No other
    expression may of be a type that contains a flexible type variable. Constraints
    are thus needed only in the subtype_with_constraints/3 function that gets called
    only from type_check_poly_call/4. This means that nothing but the subtyping
    functions and the type_check_poly_call/4 function needs to deal with constraints.
    Therefore, I am removing constraints from all the other places.
    
    I believe this is a great simplification of the code. It also trivially solves
    all the TODOs like "Don't drop the constraints".
    
    In such a huge refactoring, Gradualizer has proved to be an invaluable help.
    Via self-gradualization, it discovered numerous errors that I didn't notice.
    Hopefully, there are no undetected errors left. All tests are passing, the
    self-gradualization does not crash and 100_000 proptests have also passed.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    6b6eddf View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    35ab4fe View commit details
    Browse the repository at this point in the history
  5. Fix type inference of try ... of expressions

    And also remove the assert_type uses that were needed because of this error.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    b10b5fb View commit details
    Browse the repository at this point in the history
  6. any_type/4: return constraints if exactly one supertype matches

    This quite a trivial change enables us to typecheck polymorphic
    functions like
    
        -spec generic_hd([A,...] | {A, any()}) -> A.
    
    or functions from Elixir's Enum module that use protocol
    polymorphism in addition to the parametric polymorphism:
    
        -spec enum_map([A] | map(), fun ((A) -> B)) -> [B].
    
    which is really handy for Gradient and other Elixir frontends!
    
    Support for intersection polymorphic functions like
    
        -spec generic_hd([A,...]) -> A;
                        ({A, any()}) -> A.
    
    is of course still missing. But at least some of these can now
    be typechecked when using a spec with the unions.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    4af8b2e View commit details
    Browse the repository at this point in the history
  7. Make type variables only atoms again

    Since now we do not generate type variables,
    they don't need to be strings anymore.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    7d45b1b View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    31caf2d View commit details
    Browse the repository at this point in the history
  9. Remove the remark on missing subtype polymorpism support

    It is already there since December 2022 (unless "subtype polymorphism"
    means bounded quantification).
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    a912cef View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    66bd8b5 View commit details
    Browse the repository at this point in the history
  11. Remove hyphens from flag descriptions

    They probably originate from the `fmt_location` description
    that uses hyphens to list possible values.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    cad1047 View commit details
    Browse the repository at this point in the history
  12. Update CLI synopsis in the README

    Removes the hyphens and add `--solve_constraints` flag.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    8efca04 View commit details
    Browse the repository at this point in the history
  13. Use lists:usort/1 instead of lists:uniq/1 on OTP < 25

    lists:uniq/1 was introduced in OTP 25.
    xxdavid committed May 26, 2024
    Configuration menu
    Copy the full SHA
    aac8000 View commit details
    Browse the repository at this point in the history