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 Bottom, and I don't think it's commonly done.

What am I missing?


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.

  • $\begingroup$ Is it correct to say that for the RHS of an assignment, the useful information is the lower bound (it tells humans what they can assign that r-value to without violating the constraint); and for the LHS of an assignment, the useful information is the upper bound (it tells humans what they can put into that l-value without violating the constraint)? $\endgroup$ – max Apr 14 '17 at 8:49
  • $\begingroup$ @max: You may want to define "assignment" here. E.g. the C++ assignment is statically typed; it ignores upper and lower bounds and will slice subobjects. The rules for such an assignment will differ from that of Java, where assignments alter the binding between objects and variables. $\endgroup$ – MSalters Apr 14 '17 at 10:13
  • $\begingroup$ @MSalters I meant an assignment that creates binding between objects and variables (in the C++ assignment, the LHS variable doesn't care about subtyping at all, it has an exact static type). $\endgroup$ – max Apr 14 '17 at 10:26
  • $\begingroup$ I think it's better to think in terms of positive and negative occurrences of expressions. Assignments are just a very special case of that. You also need to pay attention to arguments to functions, etc. $\endgroup$ – Andrej Bauer Apr 14 '17 at 13:37
  • $\begingroup$ And I just realized that of course sometimes, no one equality stands out as being the most useful, since a type variable may appear in both covariant and contravariant positions. In that case, simplfying the constraints to an equality before displaying to the user would be somewhat misleading. $\endgroup$ – max Apr 15 '17 at 2:43

Depends on where the type appears.

On values (including return values), the lower bounds are the most interesting since it gives you more freedom on where to use them.

On parameters, the upper bounds are more relevant since they tell you what kinds of values you may pass into the function.

  • $\begingroup$ Let's say the value is a function. Then the lower bound on it would imply the upper bound on the type of its parameters. So in the (trivial) case of no constraints on a function of one argument, the reported type might be Top -> Bottom, i.e., argument of type Top and return type Bottom. When you mention "upper bounds for parameters", is that the context you meant? In that case, you seem to agree with my intuition that it's always best to show the lower bound overall (of course it might involve upper bounds for individual components of the type). $\endgroup$ – max Apr 14 '17 at 8:13
  • $\begingroup$ @max Good question. I'm not sure I can answer competently on that; I had not thought about function types. I think Top -> Top is the least informative function type; isn't Top -> Bottom an empty type? $\endgroup$ – Raphael Apr 14 '17 at 8:20
  • $\begingroup$ I guess the "lowest" function type (i.e., the subtype of all function types = a type of a function that would fit anywhere a function is expected) is Top -> Bot; it's empty, just like the regular Bot is empty. The "highest" function type (i.e., the supertype of all function types = the type of a variable that would accept any function) is Bot -> Top. For example, it's safe to pass your arbitrary function f to an argument of such type because your function will only be passed values of type Bot, and they can fit anywhere. (Of course, it also means f will never be called). $\endgroup$ – max Apr 14 '17 at 9:45
  • $\begingroup$ @max You are just saying that the arrow is contravariant in the first parameter and covariant in the second, i.e. if $A\supseteq A'$ and $B\subseteq B'$ then $(A\to B) \subseteq (A'\to B')$. So yeah, if you assume that for all $A$, $\bot \subseteq A \subseteq \top$, then for all $A,B$, $\top \to \bot \subseteq A \to B\subseteq \bot \to \top$. $\endgroup$ – xavierm02 Apr 14 '17 at 12:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.