Contravariant Functors Are Weird

Yes that is not bad, a good example.

I'm not a functional programmer, but I like reading about it to expand my horizon.

Some days I even think "hey functional programming looks fun, I should try it!"

Then I read articles like this and realize that ship has sailed...

I'll be sticking to my procedural code, now with a light sprinkling of functional-ish concepts.

The idea of polarity comes from the category theoretic notion of a universal property. Nice types have introduction and elimination rules but for negative types the introduction rule is "reversible" whereas for positive types the elimination rule is.

As an example, the function type `A -> B` is negative because the function introduction rule

G, x:A |- M : B ---------------- G |- lam x. M : A -> B

is a bijection: the inverse is

G |- N : A -> B ------------------- G , x:A |- N x : B

The beta and eta equations encode exactly the two properties of this being a bijection.

Positive types, like sums/alternatives/coproducts have their elimination rule as their reversible rule, i.e. "pattern matching". So the rule

G , x1 : A1 |- K1 : B G , x2 : A2 |- K2 : B --------------------- G , x : A1 + A1 |- case x of { in1 x1. K1 | n2 x2. K2 }

Has an inverse

G , x : A1 + A2 |- N : B --------------------------- G , x1 : A1 |- N[in1 x1/x] G , x2 : A2 |- N[in2 x2/x]

The reason people say the positive types are "defined in terms of their introduction rules" is that you say "here are all the ways to build a term of this type" (in1 and in2 for sums) and then the elimination rule is exactly "pattern match on all of those possibilities". There is a dual way to think of the negative types which is "here are all the ways to use a term of this type" and the introduction form is a "co-pattern match" where you say "inspect all of the ways I can be used and say what to do in each case".

If you know about category theory then the idea is that some types are defined by representing a functor C -> Set (positives) and others by representing a functor C^op -> Set (negatives).

Variance is I would say is an orthogonal concept, except that the only primitive contravariant type former in lambda calculus is function which is negative.

Honestly, concepts like functors are not that hard, they're way more intuitive than some of the OOP concepts when you get used to them a little bit.

Here's a description which is close to the way this arose in math. It's pretty simple. Maybe it will be helpful for some people to see it removed from programming issues. (Maybe not.)

From concreteness, let's suppose we're talking about sets and functions between sets. (The same thing works in an arbitrary category.) Thus, if X and Y are sets, Hom(X, Y) denotes the set of functions (morphisms) from X to Y. Suppose you have a fixed function f: A -> B. You can compose it with functions into A or out of B.

If g: C -> A maps into A, then f o g (using "o" to denote composition) gives a function from C to B: that is, f o g: C -> A -> B. We started with a function from C to A and wound up with a function from C to B. So we actually have a function (functor) Hom(C, A) -> Hom(C, B), which is often denoted Hom(C, f). We say that Hom(C, -) is covariant, because it respects the direction of arrows in the second slot. (f went from A to B, and Hom(C, f) goes from Hom(C, A) to Hom(C, B).)

If h: B -> D maps out of B, then h o f gives a function from A to D: that is, h o f: A -> B -> D. So we actually have a function from Hom(B, D) -> Hom(A, D) which is often denoted Hom(f, D). We say that Hom(-, D) is contravarient, because it reverses the direction of arrows in the first slot. (f went from A to B, but Hom(f, D) goes from Hom(B, D) to Hom(A, D).)

     g      f      h
  C ---> A ---> B ---> D

Thus, Hom(-, -) is actually a bifunctor which is covariant in one variable and contravariant in the other. Contravariant functors can be regarded as covariant functors on the opposite category. What is happening with Hom is a prototype for many of the ways that "covariance" and "contravariance" occur in math; for example, covariant and contravariant tensors. (The vector dual space function Hom(-, K) [where K is the ground field] is contravariant.)

One of the earliest descriptions of category theory (including variance) is in: Samuel Eilenberg and Saunders MacLane, "General Theory of Natural Equivalences". Transactions of the American Mathematical Society, Vol. 58, No. 2, (Sep., 1945), pp. 231-294

It's actually fairly readable. There have been many books and articles on category theory since then, and many specifically directed toward computer science (e.g. Michael Barr and Charles Wells, "Category Theory for Computer Science" - https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf).