debugMinor
Which type compilers report if they cannot infer a precise type?
Viewed 0 times
cannotcompilerstypereportwhichpreciseinferthey
Problem
In the presence of subtyping, a type checker can usually infer only some inequality constraints on the type rather than the exact type. Of course, internally it will store the full constraints. But what is the common practice in case it needs to display the inferred type to the programmer?
I thought it might be reasonable to just display the lowest type that satisfies all the constraints (I guess it exists and unique if the types form a lattice). That would mean the programmer would know all the contexts where the name can be used. But then, if there's no constraint from below, the type checker would be displaying
What am I missing?
I thought it might be reasonable to just display the lowest type that satisfies all the constraints (I guess it exists and unique if the types form a lattice). That would mean the programmer would know all the contexts where the name can be used. But then, if there's no constraint from below, the type checker would be displaying
Bottom, and I don't think it's commonly done.What am I missing?
Solution
It is important to keep in mind that this is a question about human-computer interaction and not about compilers. As far as the machine is concerned, the constraints are the constraints, and the obvious thing to do is just to show all the constraints to the user. However, when the user is a human, they may find the constraints too complex to process, and so the machine needs to dumb down the information for the cognitively handicapped user. This is in fact what happens, see for instance Pretnar's paper on inference for effects where he discusses what to show the user (that's just the first paper that came to my mind, and is by no means the only one or the first one).
As you notice, showing just the lower bounds may be useless. Symetrically, showing just the upper bound may be useless as well. However, in many situations one has either useful lower bounds or useful upper bounds, in which case you just show the useful part (and you need to indicate whether you're showing the lower or the upper bound). Other than that, people try various strategies. A common one is to simplify the constraints in the hope that we won't lose much information, and then show those to the user. Simplification can also be useful to control the size of constraints, which can easily grow so much that the whole system becomes useless.
As you notice, showing just the lower bounds may be useless. Symetrically, showing just the upper bound may be useless as well. However, in many situations one has either useful lower bounds or useful upper bounds, in which case you just show the useful part (and you need to indicate whether you're showing the lower or the upper bound). Other than that, people try various strategies. A common one is to simplify the constraints in the hope that we won't lose much information, and then show those to the user. Simplification can also be useful to control the size of constraints, which can easily grow so much that the whole system becomes useless.
Context
StackExchange Computer Science Q#73927, answer score: 6
Revisions (0)
No revisions yet.