Post History

"Invariant" isn't really the right word to search, though that's clearly not obvious. The idea is that we have **covariant functors** where if we have `a -> b` we can make `f a -> f b`, and **contravariant functors** where if we have `a -> b` we can make `f b -> f a`. You can see that the "functor" `f a = a -> a` is neither covariant nor contravariant. The term "invariant" (which isn't really used this way by the math community) is meant to indicate that it's "not co- or contra-variant". (This notion of "invariant functors" also doesn't really come up that often in my experience. Mathematicians would be more likely to talk about functors out of the core of the category which would give you something like `imap` but only when the two provided functions are mutually inverse.) Another term, not widely used by the math community, is **free variant** for a functor that is both covariant and contravariant. The name comes from the fact a functor is usually free variant because it doesn't use the parameter at all. Chapter 2 of Hagino's [A Categorical Programming Language](https://arxiv.org/abs/2010.05167) gives a technical run-down of formulating these ideas in more generally and systematically.

So one way of defining "positive/negative position" is if we consider the functor that maps its argument to that position, is it covariant/contravariant? So, for example, for `a -> b`, as a functor of `a` (with `b` fixed) it's contravariant and as a functor of `b` (with `a` fixed). In practice, negative positions almost always directly or indirectly arise from being the domain of a function type.

One of the reasons for the "positive"/"negative" terminology is that a "negative of a negative is positive". Which is just to say that if you compose two contravariant functors the result is covariant, while if you compose two covariant functors the result is covariant. Of course, composing a covariant functor with a contravariant functor is contravariant. This is even clearer if you eliminate the notion of a contravariant functor, and instead replace them with (covariant) functors from the opposite category. In symbols, a contravariant functor from *A* to *B* is a covariant functor *A*<sup>op</sup> &rarr; *B*, and we have (*A*<sup>op</sup>)<sup>op</sup> = *A*. We also have for a functor *F* : *A* &rarr; *B* that it can also be viewed as a functor *F*<sup>op</sup> : *A*<sup>op</sup> &rarr; *B*<sup>op</sup>.

One intuition is "positive" positions are positions where a value of the type "provides" a value, where "negative" positions are positions where a value of the type "accepts" or "receives" a value. This is especially clear for the function type. A function of type `A -> B` accepts a value of type `A` and provides a value of type `B`. Less obvious is a type like `(A -> B) -> B`, where if the function wants to use its (function) argument it needs to provide a value of type `A`. The negative of a negative is positive makes sense in this context because if I accept something that accepts a type `A`, then I need to provide a type `A` if I want to use it.

Just for completeness, there's also the notion of a strictly positive type. This is usually applied to recursive types and here the idea is that we can define a recursive type *R* as a fixed point of a type constructor as *R* = &mu; *x*. *F x* (where &mu; is the traditional binding form for computing the least fixed point). *R* is strictly positive if not only is *F* a covariant functor, but the expression defining *F* doesn't have positive occurrences of the argument due to being a negative of a negative.

Polarity is something else entirely.