Strict positivity

Question

From This reference : Strict positivity

The strict positivity condition rules out declarations such as

data Bad : Set where
 bad : (Bad → Bad) → Bad
         A      B       C
 -- A is in a negative position, B and C are OK

Why is A is negative ? Also Why B is allowed ? I understand why C is allowed.

Answer 1

First a terminological explanation: negative and positive positions come from logic. They are about an assymetry in logical connectives: in $A \Rightarrow B$ the $A$ behaves differently from $B$. A similar thing happens in category theory, where we say contravariant and covariant instead of negative and positive, respectively. In physics they speak of quantities that behave "covariantly" and "contravariantly, too. So this is a very general phenomenon. A programmer might think of them as "input" and "output".

Now onto inductive datatypes.

Think of an inductive datatype $T$ as a kind of algebraic structure: constructors are the operations which take elements of $T$ as arguments and produce new elements of $T$. This is very similar to ordinary algebra: addition takes two numbers and produces a number.

In algebra it is customary that an operation takes a finite number of arguments, and in most cases it takes zero (constant), one (unary) or two (binary) arguments. It is convenient to generalize this for constructors of datatypes. Suppose c is a constructor for a datatype T:

• if c is a constant we can think of it as a function unit -> T, or equivalently (empty -> T) -> T,
• if c is unary we can think of it as a function T -> T, or equivalently (unit -> T) -> T,
• if c is binary we can think of it as a function T -> T -> T, or equivalently T * T -> T, or equivalently (bool -> T) -> T,
• if we wanted a constructor c which takes seven arguments, we could view it as a function (seven -> T) -> T where seven is some previously defined type with seven elements.
• we can also have a constructor c which takes countably infinitely many arguments, that would be a function (nat -> T) -> T.

These examples show that the general form of a constructor should be

c : (A -> T) -> T

where we call A the arity of c and we think of c as a constructor that takes A-many arguments of type T to produce an element of T.

Here is something very important: the arities must be defined before we define T, or else we cannot tell what the constructors are supposed to be doing. If someone tries to have an constructor

broken: (T -> T) -> T

then the question "how many arguments does broken take?" has no good answer. You might try to answer it with "it takes T-many arguments", but that will not do, because T is not defined yet. We might try to get out of the cunundrum by using fancy fixed-point theory to find a type T and an injective function (T -> T) -> T, and would succeed, but we would also break the induction principle for T along the way. So, it's just a bad idea to try such a thing.

For the sake of completeness, let me explain the whole story. We need to generalize the above form of constructors a little bit. Sometimes we have operations or constructors that take parameters. For example, scalar multiplication takes a scalar $\lambda$ and a vector $v$ to produce a vector $\lambda \cdot v$. It is a unary operation on vectors, parameterized by a scalar. We could view scalar multiplication as infinitely many unary operations, one for each scalar, but that's annoying. So, the general form of a constructor c should allow a parameter of some type B:

c : B * (A -> T) -> T

Indeed, many constructors can be rewritten in this way, but not all, we need one more step, namely we should allow A to depend on B:

c : (∑ (x : B), A x -> T) -> T

This is the final form of a constructor for an inductive type. It is also precisely what W-types are. The form is so general that we only ever need a single constructor c! Indeed, if we have two of them

d' : (∑ (x : B'), A' x -> T) -> T
d'' : (∑ (x : B''), A'' x -> T) -> T

then we can combine them into one

d : (∑ (x : B), A x -> T) -> T

where

B := B' + B''
A(inl x) := A' x
A(inr x) := A'' x

By the way, if we curry the general form we see that it is equivalent to

c : ∏ (x : B), ((A x -> T) -> T)

which is closer to what people actually write down in proof assistants. The proof assistants allow us to write down the constructors in convenient ways, but those are equivalent to the general form above (exercise!).

Answer 2

The first occurrence of Bad is called 'negative' because it represents a function argument, i.e. is located to the left of the function arrow (see Recursive types for free by Philip Wadler). I guess the origin of the term 'negative position' stems from the notion of contravariance ('contra' means opposite).

It is not allowed to have the type being defined in negative position to because one can write non-terminating programs using it, i.e. strong normalization fails in its presence (more on this below). By the way, this is the reason for the name of the rule 'strict positivity': we don't allow negative positions.

We allow the second occurrence of Bad since it doesn't cause non-termination and we want use the type being defined (Bad) at some point in a recursive datatype (before the last arrow of its constructor).

It's important to understand that the following definition does not violate the strict positivity rule.

data Good : Set where
  good : Good → Good → Good

The rule applies only to constructor's arguments (which are both Good in this case) and not to a constructor itself (see also Adam Chlipala's "Certified Programming with Dependent Types").

Another example violating strict positivity:

data Strange : Set where
  strange : ((Bool → Strange) → (ℕ → Strange)) → Strange
                       ^^     ^
            this Strange is   ...this arrow
            to the left of... 

You might also want to check this answer about negative positions.

---

More on non-termination... The page your referenced contains some explanations (along with an example in Haskell):

Non strictly-positive declarations are rejected because one can write a non-terminating function using them. To see how one can write a looping definition using the Bad datatype from above, see BadInHaskell.

Here is an analogous example in Ocaml, which shows how to implement recursive behavior without (!) using recursion directly:

type boxed_fun =
  | Box of (boxed_fun -> boxed_fun)

(* (!) in Ocaml the 'let' construct does not permit recursion;
   one have to use the 'let rec' construct to bring 
   the name of the function under definition into scope
*)
let nonTerminating (bf:boxed_fun) : boxed_fun =
  match bf with
    Box f -> f bf

let loop = nonTerminating (Box nonTerminating)

The nonTerminating function "unpacks" a function from its argument and apples it to the original argument. What is important here is that most type systems do not permit passing functions to themselves, so a term like f f won't typecheck, since there is no type for f to satisfy the typechecker. One of the reasons type systems were introduced is to disable self-application (see here).

Wrapping datatypes like the one we introduced above can be used to circumvent this roadblock on the way to inconsistency.

I want to add that non-terminating computations introduce inconsistencies to logic systems. In case of Agda and Coq the False inductive datatype doesn't have any constructors, so you cannot ever build a proof term of type False. But if non-terminating computations were allowed, one could do it for example this way (in Coq):

Fixpoint loop (n : nat) : False = loop n

Then loop 0 would typecheck giving loop 0 : False, so under Curry-Howard correspondence it would mean we proved a false proposition.

Upshot: the strict positivity rule for inductive definitions prevents non-terminating computations which are disastrous for the logic.