Reduce the amount of unification diagnostics #49

New issue

Open

opened 2023-06-05 14:42:05 +02:00 by samvv · 0 comments

samvv commented

2023-06-05 14:42:05 +02:00

(Migrated from github.com)

Problem

Consider the following program:

let foo k.
  let bar l = k == l
  bar True
  bar 1

foo 1

Right now, this program correctly produces two error diagnostics. One for bar 1 and one for foo 1. Both inform that Int and Bool do not match.

The two diagnostics didn't have to be. If we first had unified k with Int and only then inferred bar True and bar 1, we would find that bar True was wrong and bar 1 correctly related k with the Int type, as foo 1 does. This means one less diagnostic by just reversing some steps.

More generally, the problem is how we can unify constraints in such a way that the produced diagnostics are of a minimal amount.

Solution: Tracking Unified Types

For finding the minimal amount of diagnostics, one solution would be to keep track of all types that unified with each other instead of setting it to the first one. If a type unified with Int and Bool then an error is printed and both are added to a set. When another constraint requires this same type to be Bool, no diagnostic message is generated because it is already in the set. If, however, a new type String unifies with this type then String is added to the set and a diagnostic message is again generated.

We explicitly store the types in a set and not a list because the order of the types must not matter. In the above example, unifying k first with Int or first with Bool should not affect the outcome of the inference.

This method ensures that only really unexpected type combinations are reported, while types that are somewhat expected (because the source indicates that they are used like that) are ignored. At the same time, enough type errors are reported such that the user has to fix all (hidden) typing errors in the program before (s)he can continue.

## Problem Consider the following program: ``` let foo k. let bar l = k == l bar True bar 1 foo 1 ``` Right now, this program correctly produces two error diagnostics. One for `bar 1` and one for `foo 1`. Both inform that `Int` and `Bool` do not match. The two diagnostics didn't have to be. If we first had unified `k` with `Int` and only then inferred `bar True` and `bar 1`, we would find that `bar True` was wrong and `bar 1` correctly related `k` with the `Int` type, as `foo 1` does. This means one less diagnostic by just reversing some steps. More generally, the problem is how we can unify constraints in such a way that the produced diagnostics are of a **minimal** amount. ## Solution: Tracking Unified Types For finding the minimal amount of diagnostics, one solution would be to keep track of all types that unified with each other instead of setting it to the first one. If a type unified with `Int` and `Bool` then an error is printed and both are added to a set. When another constraint requires this same type to be `Bool`, no diagnostic message is generated because it is already in the set. If, however, a new type `String` unifies with this type then `String` is added to the set and a diagnostic message is again generated. We explicitly store the types in a set and not a list because the order of the types must not matter. In the above example, unifying `k` first with `Int` or first with `Bool` should not affect the outcome of the inference. This method ensures that only really unexpected type combinations are reported, while types that are somewhat expected (because the source indicates that they are used like that) are ignored. At the same time, enough type errors are reported such that the user has to fix all (hidden) typing errors in the program before (s)he can continue.

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: samvv/bolt#49

No description provided.