F-systems

A cow can eat something more than food

Most type theories have been phrased for extensions of lamda-calculus, which is initiated by Luca Cardelli in his record-based model where the loophole of covariance is examined and the concept of contravariance is proposed.

By contravariance, the type of an argument in a method interface in a subtype can be redefined into a supertype. That is, the food type of a cow can be redefined to something more general than a food.

Some languages, like Sather, have made contravariance in the type system.

In practice, however, many people believe that contravariance is less natural than covariance, and in many cases covariance is required and contravariance is useless.

I have not found a meaningful example that can illustrate a natural class hierarchy with contravariance. I cannot imagine that a cow should eat something which is not food.

To upgrade a software system, we might want to make an function interface more general by redefine the type of the argument into a supertype. But this is not an example of contravariance, because version upgrade cannot be contrasted contravarianly with a "super-typification".