[Checkers] More Generics complications

[Michael Ernst]

> unify() is called for finding the least upper bound on  
> conditional expressions.  I just realized that unifying annotations on  
> the raw type is different from unifying ones on type argument.

This is related to the invariance of type arguments in Java:

  ArrayList<Integer> is a subtype of List<Integer>
  List<Integer> is unrelated to List<Number>

>    (true ? {@NonNull String} : {@Nullable String>}  --> {@Nullable String}     // Nullable is least restrictive here!
>    (true ? {@NonNull List<@NonNull String>} : {@Nullable List<@NonNull String}  --> {@Nullable List<@NonNull String}  // Nullable is least restrictive here!
> 
> Type Arguments:
>    (true ? {@NonNull List<@NonNull String>} : {@NonNull List<@Nullable  
> String>}  --> cannot really unify the types

Two supertypes that you could imagine using here are "@NonNull List" and
"@NonNull Object".  (Do these two types have any other supertypes?  Maybe
some superinterfaces?)  The former is raw, which is undesirable, and the
latter is very weak but is at least safe.

In Javari, the common supertype of List</*mutable*/ Date>} and
List<readonly Date> is List<? readonly Date>.  Our other type systems don't
express this type, however.

> For now, maybe we can simply issue a warning whenever the types of the  
> true expressions and false expressions are distinct un-unifiable types.

Yes, a warning is a very good idea if the unification has to throw away
type parameters.  Then type checking can proceed using some supertype, even
if not a very good one.

                    -Mike


I'll quote Mahmood's whole message for Jaime's benefit:

> From: Mahmood Ali <mahmood at MIT.EDU>
> To: checkers at lists.csail.mit.edu
> Subject: [Checkers] More Generics complications
> Date: Sat, 19 Apr 2008 01:54:58 -0400
> 
> Hi guys,
> 
> I am planning to work on AnnotatedTypeFactory.unify() and make it use  
> annoRelations.  unify() is called for finding the least upper bound on  
> conditional expressions.  I just realized that unifying annotations on  
> the raw type is different from unifying ones on type argument.  On raw  
> type, one need to take the super (least restrictive) annotation, while  
> on type arguments it is complicated.
> 
> Examples:
> Raw types:
>    (true ? {@NonNull String} : {@Nullable String>}  --> {@Nullable  
> String}     // Nullable is least restrictive here!
>    (true ? {@NonNull List<@NonNull String>} : {@Nullable List<@NonNull  
> String}  --> {@Nullable List<@NonNull String}  // Nullable is least  
> restrictive here!
> 
> Type Arguments:
>    (true ? {@NonNull List<@NonNull String>} : {@NonNull List<@Nullable  
> String>}  --> cannot really unify the types
> 
> Reason:
> - The iterator may have null elements, if the false expression is  
> returned
> - one cannot add a null item to resulting list, if the true expression  
> is returned
> 
> What do you think we should do?  We may want to include it in the  
> paper.  This may be the second item we have regarding generics.  Given  
> that none of the other type systems handle generics, it might be  
> worthy to write a section regarding the difficulties with it.
> 
> For now, maybe we can simply issue a warning whenever the types of the  
> true expressions and false expressions are distinct un-unifiable types.
> 
> Regards,
> Mahmood
> 
> _______________________________________________
> checkers mailing list
> checkers at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/checkers