What defines negative and non-negative type operators?

Question

I'm working through some exercises in Robert Harper's "Practical Foundations for Programming Languages" and I'm not certain I understand what makes an occurrence of a type operator non-negative or negative in the general case.

I understand that positive type operators occur in the range of a function type, and that negative type operators occur in the domain of a function type, but I'm not sure how to generalize the additional category of non-negative based on the single given example t. (t -> bool) -> bool, which is only described as an occurrence in the domain of the domain without any mention of the interactions of further nesting. That also complicated my understanding of what makes an occurrence negative (must the occurrence on the left be positive, or just non-negative?), so now I'm just plain not sure what defines non-negative and negative type operators in the context of a function type.

For anybody who owns the book (second edition) this is chapter 14.

Answer 1

I can explain the mathematical background. Suppose we have a type operator $F$ that takes a type $A$ to a type $F(A)$, and we want to extend it so that it also maps functions. It should take a function $f : A \to B$ to a function $F(f) : F(A) \to F(B)$. This can often be done, for example if $$F(X) = X + (C \to X)$$ for a fixed $C$, then we may define $$F(f) : A + (C \to A) \to B + (C \to B)$$ in a natural way as \begin{align*} F(f)(\mathtt{inl}(a)) &= \mathtt{inl}(f(a)) \\ F(f)(\mathtt{inr}(g)) &= \mathtt{inr}(f \circ g) \end{align*} We say that $F$ acts covariantly on functions.

But sometimes the direction gets reversed! Consider $$F(X) = X \to C$$ for a fixed type $C$. Then $f : A \to B$ can be mapped to $$F(f) : (B \to C) \to (B \to A)$$ by $$F(f) = \lambda g . g \circ f.$$ This time the direction was reversed. We say that $F$ acts contravariantly on functions.

In some cases we are stuck, for instance if $F$ mixes things up. An example would be $F(X) = X + (X \to C)$.

If $F$ takes several arguments it may act covariantly on some of them and contravariantly on others.

Covariance and contravariance are important mathematical concepts which show up in many places: category theory, physics, analysis, you name it.

The positive and negative occurrences of a type variable in a type expression tell you whether the corresponding type constructor acts covariantly (positive) or contravariantly (negative) in that position.

For example, in $F(X) = (X \to C) \to C$ we have a positive occurrence of $X$, and indeed $F$ acts on $f : A \to B$ covariantly to give $F(f) : F(A) \to F(B)$ defined by $$F(f) = \lambda \phi : (A \to C) \to C . \lambda g : B \to C . \phi(g \circ f).$$

Answer 2

Assume we have an occurrence of $t$ in a type formed by type constants, products, sums, and arrows/functions/exponentials. Count the number of arrows where such occurrence occurs in the left argument (possibly zero). If such number is even, the occurrence is positive, otherwise it is negative.

More precisely, the types types $P$ containing a positive occurrence of $t$ can be defined as those of the form $$ t, T \to P, N \to T, P \times P, P + P $$

where types $N$ containing a negative occurrence of $t$ are those of the form $$ P \to T $$ where $T$ is any type.

(The exact definition depends on the type system at hand, which might have more of fewer type constructors. Still, the overall idea holds.)

A more direct mnemonic is: an arrow $\to$ introduces a negation on its left argument, and double negations cancel out.