[TheAsprngHacker]

One thing I've never understood is polarity. To my understanding, positive types are defined in terms of their introduction rules and negative types are defined in terms of their elimination rules. However, don't types both have introduction and elimination rules, making them positive or negative based on how you choose to define them?

Also, how does polarity (emphasis on introduction versus elimination rules) relate to variance, as this article presents?

[maxiepoo]

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.

[TheAsprngHacker]

Thank you for the explanation of polarity, I found it helpful.

I just remembered that people use the +/- notation to denote covariance and contravariance (such as in OCaml syntax and Scala syntax). I think it's possible that the author saw this and then related the +/- notation to polarity, even though variance is unrelated.