Mechanism for Inferring Template Variance

[DavePearce]

(see also #68)

Whiley supports automatic inference of declaration site variance for templates. For example, consider this simple type:

type List<T> is { int length, T[] items }

This template parameter T is inferred to be covariant. Thus, List<S> is a subtype of List<T> when S <: T. For example, List<int> is a subtype of List<int|null>.

Generally speaking, this approach to inference of variance works well. However, in the presence of traits, this starts to become problematic. For example, we might have something like this:

type List<T> is {
   int length,
   T[] items,
   function get(int)->T,
   function set(int,T)->List<T>,
   ...
}

At this point, we have a problem since T is now inferred as being invariant. Thus, List<int> is no longer a subtype of List<int|null>. This makes sense if we think about it as allowing this would mean the following incorrectly type checks:

List<int|null> nl = [1,2,null]
// Following shouldn't be permitted
List<int> l = nl
// Otherwise, following is allowed
int x = nl.get(2) 

This is pretty standard and well known stuff (see e.g. [1] below). The question is what we do about it. Well, there are some options. We could break it up like so:

type List<T> is {
   int length,
   T[] items,
   function get(int)->T,  
   ...
}

type WList<T> is {
   function set(int,T)->List<T>,
   ...
}

Then, the type List<T>&WList<T> would give us the original back, whilst just WList<T> gives us a "writeable" list, etc.

At this point, I'm not going to say any more. This is merely highlighting a potential issue which may need further thought.

References

1. Taming the Wildcards: Combining Definition- and Use-Site Variance. J. Altidor, S. Huang and Y. Smaragdakis. In PLDI'11.