Meaning of "positive position" and "negative position" in type theory?

Question

What does "in positive position" and "in negative position" mean in the context of type theory?

The only thing I understood from Bob Harper's blog post on the topic is that there is a connection between polarity in this sense in type theory and polarity in logic, but I don't know what that connection is.

Answer 1

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 Nats and includes zero. In line with this inductive construction we get an recursion principle across Nats 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

• d : (D -> D) -> D

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,

1. The argument starts in a positive position
2. 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.