Unfortunately "polarity" is a somewhat overloaded concept in type theory. "Positive position" and "negative position" refer to a different notion of polarity than what Bob's talking about with focusing/polarization.
Your Meaning
When you're defining an inductive type you give a series of rules which correspond to operations for the type you're defining. For example you might say a Nat
is something with
- a value
zero : Nat
- a function
suc : Nat -> Nat
And then expect that Nat
contains all the values that can be generated from repeatedly applying suc
to other Nat
s and includes zero
. In line with this inductive construction we get an recursion principle across Nat
s which works based on the fact that any Nat
is generated by those constructors.
rec : A -> (A -> A) -> Nat -> A
so that
rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)
However, there are some restrictions on what we can write as rules. Otherwise, we can write down a series of rules for which the recursion principle cannot be justified. Consider the "inductive type" D
with one constructor
Here there isn't a sane recursion principle here. and for good reason! If we had some recursion principle, we could use it to encode a version of self application and with it, nontermination. This means D
can't be called "inductive" because inductive types are finite constructions generated from repeatedly applying constructors!
In order to deal with this we restrict how inductive types can be recursive in type theory. Specifically, we stop them from appearing in "negative places". This is that notion of polarity you were talking about. The polarity of a position is determined thusly,
- The argument starts in a positive position
- Everytime we go to the left an arrow, the polarity flips
So X
is positive in the first two and negative in the second two
X
Int -> X
X -> Int
(Unit -> X) -> Int
This idea is justified with a recourse to category theory where an inductive type with whose only recurrences are positive gives rise to a covariant functor. The details of how this works and why its interesting a a bit long.
Bob Harper's Meaning
In his blogpost Harper was talking about a different meaning of polarity. This polarity is reference to how various connectives in logic are given meaning. In particular, we can classify connectives in two ways
- Positive connectives can be defined by defining how to introduce them (their introduction rules)
- Negative connectives can be defined by defining how to use them (their elimination rules)
In programming language terms, this nicely captures the distinction between lazy and strict types. A strict type is defined by its values. A lazy one is defined by how can pattern match on them. In order to handle this properly, we define a language with 2 main constructs, ways to build up positive types and "spines" to decompose negative types. We can use this to incorporate both strict and lazy computation into one language.
In order to understand this better, I refer you to chapter 38 of Bob Harper's book.