ta0kira / zeolite

Zeolite is a statically-typed, general-purpose programming language.
Apache License 2.0
18 stars 0 forks source link

Sanity check handling of filters in type inference. #101

Closed ta0kira closed 3 years ago

ta0kira commented 3 years ago

The new algorithm for param inference (See #100) doesn't allow both upper and lower bounds for param guesses. This means that inference will almost always fail for requires filters.

On the other hand, I don't know if it's necessary to include the filters as guesses. For example, does success of the pattern match mean that any valid guess for the param will satisfy the filter?

Additionally, should it somehow account for defines filters? Perhaps a defines filter should be an automatic inference failure, since it can't be used in ranges and it requires a concrete type. On the other hand, you can still have variance with a concrete type.

ta0kira commented 3 years ago

Looking at TypeInstance.hs:

In other words, filters are treated as the meta-type of the param in the conversion check, and as a type template for the param during param assignment.

ta0kira commented 3 years ago

Actually, filters are explicitly converted to guesses in inferParamTypes. Without that, I don't think the inference algorithm would account for the filters at all.

But, since they're always going to be in a top-level "all" with the actual guesses, leaving them out during merging would result in a superset of guesses. This means that mergeInferredTypes could be updated to filter the final guesses before making a selection.

It would be straightforward to just filter the ranges by attempting to assign their bounds to the param:

Note that restricting the ranges in this manner shoudn't result in any new merge possibilities; therefore, the steps above can just be applied as post-processing before making the final selection.

Incidentally, inference will fail for params with no guesses, e.g., return types with allows filters. This is fine, because in such situations there really isn't anything to infer. (There would be if expected return types were accounted for in the inference process.)

ta0kira commented 3 years ago

Since filters in this context are type templates, they don't need to fall within any range constraints; the final guess just needs to match them. In other words, filters shouldn't be used as guesses.

This just means that whatever the guess was otherwise going to be needs to match the filters.

On the other hand, it's unclear if the filter should become the guess in some cases. For example, a requires filter could further restrict an upper bound, possibly making it compliant.

ta0kira commented 3 years ago

A few more thoughts:


So, maybe something like this:

  1. For each range [A,B]:

    1. If A and B both satisfy all filters, leave the range as it is.
    2. If A satisfies all filters, replace the range with [A,A].
    3. If B satisfies all filters, replace the range with [B,B].
    4. Otherwise, remove the range.
  2. Merge the remaining guesses with simplifyUnion.

  3. Use the existing approach for choosing the best guess.