(newbie question) Covariance and contravariance

Firstly I don't have any theoretical background in Category Theory. My goal is just trying to understand the following:-

On wikipedia,
there is the following definition:

A covariant type operator in a type system preserves the ordering â‰¤ of types. 
A contravariant operator reverses â‰¤. If neither of these apply, the operator 
is invariant. These terms come from category theory.

What is type operator referring to in the context say Java ?
The entry goes on to say:

The array type is usually covariant on the base type.

Would I be right to say that the type operator is the assignment operator ?
e.g.

String[] a = new String[1];
Object[] b = a;

Thanks.

Covariance of Arrays

The covariance of arrays is a (mis)feature of Java spec.
It means that if B is a subclass of A, than B[] is a subclass of A[].
To see why it's bad:

public class Arrays {
	public static void main(String[] args) {
		A[] asorbs = new B[2]; // (1)
		asorbs[0] = new A(); // (2)
		asorbs[0] = new B(); // (3)
	}
}

class A {
}

class B extends A {
}

The code compiles without problems - line (1) is OK because B[] is a subtype of A[], and therefore assignable, line (2) is OK by even simpler reason.
However, at runtime, the line (2) throws a java.lang.ArrayStoreException, because you are trying to put an A into B[], which is invalid.
Thus, treating arrays as covariant makes compiler clueless, and means some checks must be done at runtime (JVM does that, and throws the exception).

Returning to your question about type operator - in this context it is anything which makes a type from a type - for example, array operator. It makes A[] from A, and B[] from B. In sound type systems this operator is usually invariant.

In Java with generics, any generic type is a type operator, e.g., List<> makes List from E. For similar reasons, List<> should be invariant as well.

To explore the idea of co(ntra)variance, I suggest you take a look at some language without uncontrolled side-effects (e.g., Haskell), as subtyping in them is much simpler than in Java or other languages with uncontrolled mutable state.

By Andris Birkmanis at Mon, 2008-01-07 10:25 | login or register to post comments

Array covariance can be safe...

...if the array isn't mutable. If you have a basket of apples; passing it to a function expecting a basket of fruit is only a problem if that function tries to insert an orange. In read-only contexts, a basket of apples is always a perfectly valid basekt of fruit.

Likewise, in a write-only environment, contravariance is safe but co-variance is not. Passing a basket of fruit into a routine that expects a basket of apples is safe unless the routine attempts to retrieve something from the basket, expecting it to be an apple.

More generally... if you have subtype polymorphism, then derived classes may safely modify a class feature covariantly if and only if it's a "read-only" feature, such as the return value of a method, or a non-mutable attribute. Contravariant modification is safe if and only if it's a write-only feature, such as the argument to a method. Features which are both read and written must have type preserved.

The case of arguments to overridden methods is interesting. Contravariant method arguments are safe, but almost entirely useless; few OO languages bother to support them. (Covariant return types, OTOH, are both safe and useful, several statically-typed OO languages support them, including C++). A few languages, most notably Eiffel, support covariant method arguments--even though the feature is type-unsafe--on the grounds that it is useful to do. Unfortunately, Eiffel doesn't do the sensible thing in this case and runtime-check the arguments, throwing an exception if a type error occurs. Early versions of the language simply crashed when covariant argument types were used incorrectly; later versions of the language employed a rather bizarre hack to prevent undefined behavior--but which had the unpleasant that the introduction of a new subclass into the system could break existing code.

[edited by author to fix error]

By Scott Johnson at Mon, 2008-01-07 17:45 | login or register to post comments

Not even then

The problem isn't mutability, but variance. A mutable array can be used covariantly if the only mutating methods don't mention the type parameter (e.g. clear(), remove(int index)).

By Daniel Yokomizo at Tue, 2008-01-08 04:01 | login or register to post comments

Any other languages doing the same thing.

You said

In sound type systems this operator is usually invariant.

.
Just out of curiosity, are there any other languages which behave the same way as Java with respects to the array type operator ?

By chihiro at Mon, 2008-01-14 04:39 | login or register to post comments

Eiffel

At least at one point Eiffel had variance issues with parametric types. See this paper and search for Eiffel. I haven't kept up with Eiffel and couldn't tell you if that's still true. The paper seems to say that they fixed it by making parametric types invariant.

By James Iry at Tue, 2008-01-15 21:00 | login or register to post comments

The type operator is the thing that creates array types.

In your example, the type operator is the array type operator, which that accepts a single type and returns a single type. For example, applying the array type operator to "String" yields "String[]".

Since (String â‰¤ Object), the array type operator would be covariant if (String[] â‰¤ Object[]). Interestingly, this is true in Java even though it's not really safe (which is why stores into arrays are checked by the VM at runtime).

An interesting type operator is the "arrow" type operator that yields function types. Applying the arrow type operator to two types X and Y yields the function type (X -> Y). The arrow type operator is covariant with respect to the return type and contravariant with respect to the argument type.

By Kannan Goundan at Mon, 2008-01-07 10:32 | login or register to post comments

Kannan, Thanks for the clear

Kannan,

Thanks for the clear explanation. I grok it totally.

Regards,

Gavin Bong

By chihiro at Mon, 2008-01-14 04:40 | login or register to post comments

Lambda the Ultimate

User login

Navigation