[Vala] Generic Contravariance?

[Alan Manuel Gloria <almkglor gmail com>]

Greetings Vala world,

I've been researching about subtyping in the presence of type constructors,
and since generic types are type constructors, I was surprised at Vala's
subtyping behavior on generic type parameters.

Consider the following code:

public interface ReadS<T> {
  public abstract bool at_eof();
  public abstract T read()
    requires (!this.at_eof());
}
public interface WriteS<T> {
  public abstract bool is_closed();
  public abstract void close()
    ensures (this.is_closed());
  public abstract void write(T t)
    requires (!this.is_closed());
}

That is: A readable stream of T is anything that has an end-of-file
indication, and (if end-of-file is false) can produce a T.  A writable
stream of T is anything that can be closed, and (if it is not closed) can
consume a T.

Now given two types B and D:

if B supertypes D,

ReadS<B> supertypes ReadS<D>

and WriteS<D> supertypes WriteS<B>

Vala always assumes for any generic type G, if B supertypes D, then G<B>
supertypes G<D>.  But for writable streams, in fact a WriteS<D> supertypes
WriteS<B>, the inverse of this always-assumed Vala behavior!.  In other
words, writable streams are contravariant, but Vala assumes convariance.

--

Now let's introduce this interface:

public interface Pipe<T> : ReadS<T>, WriteS<T> { }

The correct type relations are:

forall T:

ReadS<T> supertypes Pipe<T>, and

WriteS<T> supertypes Pipe<T>.

if B supertypes D:

ReadS<B> supertypes ReadS<D>, and

ReadS<D> supertypes Pipe<D>, and

WriteS<D> supertypes WriteS<B>, and

WriteS<B> supertypes Pipe<B>.

How are Pipe<B> and Pipe<D> related?  They aren't: they are unrelated types
that cannot be converted to each other.  Pipe<B> cannot supertype Pipe<D>:
If so, then WriteS<B> would supertype Pipe<D>.  Now every Pipe<D> is also a
WriteS<D>, so that amounts to saying that WriteS<B> supertypes WriteS<D>:
which we already accepted as being incorrect.

Basically, a Pipe<D> cannot become a Pipe<B> because a Pipe<B> can accept
any B, but a Pipe<D> can only accept D, not B.

Pipe<D> cannot supertype Pipe<B> also because that would mean that every
ReadS<D> supertypes Pipe<B>, and a pipe of B may yield a B that is not a D.

Thus, not only must generics support contravariance, but also nonvariance.

--

Now one thing to notice is that ReadS has its type parameter as an output
of a method, while WriteS has its type parameter as an input of a method.
So we can indicate contravariance and nonvariance via keywords "in" and
"out", which are (conveniently enough) keywords in Vala:

public interface ReadS<out T> { // covariant
  public abstract bool at_eof();
  public abstract T read()
    requires (!this.at_eof());
}
public interface WriteS<in T> { // contravariant
  public abstract bool is_closed();
  public abstract void close()
    ensures (this.is_closed());
  public abstract void write(T t)
    requires (!this.is_closed());
}

How about Pipe<T>?  It is nonvariant, which is equivalent to saying that it
is both in and out variant:

public interface Pipe<in out T> : ReadS<T>, WriteS<T> { }

By default a generic parameter is out direction, because that's the
behavior of existing Vala.

--

In fact, we can infer the variance of generics.  Suppose a generic type G
has multiple type parameters, then for each type parameter T:

1.  If G<T> inherits from one or more bases B<T>, then get the union of the
directions of each base.  For example, the T in Pipe<T> is in and out
variant (nonvariant), because ReadS<T> has T as out variant (covariant)
while WriteS<T> has T as in variant (contravariant).

2.  If G<T> has methods, then get the union of the directions of T in each
return type and out argument, and union the *reversed* directions of each
non-out argument.  For example, if G<T> has a single method WriteS<T>
foo(ReadS<T>), then T is "in" variant (contravariant) because T is in
variant on WriteS<T>, and while T is out variant in ReadS<T>, we must
reverse the direction since it is used as a method argument.

3.  The inferred variance is the union of (1) and (2).

(in this view, properties are decomposed to their get and set methods; a
property might not have a set method if the property is construct-only.)

Sincerely,
AmkG