Input Parameter

programming type-theory

Contravariance

Let $\text{Cat}\le \text{Animal}$ (Cat is subtype of Animal). Consider two functions that consume input:

1. $f:\text{Cat}\to \text{void}$
2. $g:\text{Animal}\to \text{void}$

If a program expects $f$ (a handler that deals with cats), can we substitute $g$? Yes. The program intends to pass a Cat to the function. $g$ knows how to handle any Animal. Since $\text{Cat}\le \text{Animal}$, $g$ can safely handle the input.

However, the reverse is false. If a program expects $g$ (needs to handle any Animal, possibly a Dog), we cannot give it $f$, because $f$ crashes if given a Dog.

Therefore, the general function $g$ is a subtype of the specific function $f$:

$$\begin{array}{rl}(\text{Animal}\to \text{void})& \le (\text{Cat}\to \text{void})\\ K[\text{Animal}]& \le K[\text{Cat}]\end{array}$$

Thus, input parameters are contravariant.