But what is strict positivity anyway?

My day job is to write things in lean. As far as theorem provers go, lean isn’t particularly strict; it lets you use classical reasoning whenever you want, for example. One restriction it does place upon you, however, is that all your data types must be strictly positive. In practise, when you first encounter lean, this means that it will sometimes just randomly reject certain inductive definitions. This is very frustrating, and at first it seems totally arcane. But unfortunately, it’s very necessary. Today I’m going to try and explain why.

An Evil Type

Consider the following data type, in haskell:

data Evil = Mk (Evil -> Int)

Evil has one constructor (Mk). To make an Evil, you need a function from Evil to an integer. Now let’s look at another function:

unpack :: Evil -> Int
unpack e@(Mk f) = f e

And please let me apologise for the horrible haskellianness of this example. What does unpack do? Well, it takes in an Evil and pulls out the function (f) from inside of it. Remember: f :: Evil -> Int. We can then take the original sin (e :: Evil) and pass it into f. This gives us an Int — and so unpack takes Evils to Ints.

Now there’s just one little example left to consider:

totally_real_integer :: Int
totally_real_integer = unpack (Mk unpack)

The key insight here is that unpack is a function Evil -> Int, and so we can use it to construct an evil object by passing it to Mk. We can then pass that Evil object to unpack, to get back an Int. Now riddle me this, dear reader: Which Int?

If you’re sitting there scratching your head, trying to work the answer out, let me give you a little hint first. I chose Int rather arbitrarily, because the example is much easier to understand with a concrete type. But we can change these definitions a bit to be parametric over the result type:

data Evil x = Mk (Evil x -> x)

unpack :: Evil x -> x
unpack e@(Mk f) = f e

totally_real_thing = unpack (Mk unpack)

And now we can ask a slightly different question: What is the type of totally_real_thing? There’s nothing actually in the program which restricts the type — it’s totally parametric. This single expression can be used in place of anything we could possibly want:

totally_real_integer :: Int
totally_real_integer = unpack (Mk unpack)

totally_real_char :: Char
totally_real_char = unpack (Mk unpack)

totally_real_bool :: Bool
totally_real_bool = unpack (Mk unpack)

This example typechecks. How is that possible? The answer here is that the spooky term unpack (Mk unpack) is divergent i.e. it never terminates. It’s a bit like a filibuster: you never have to give a concrete answer if you never stop talking. This is an example of Curry’s paradox, named after the logician Haskell Curry, who discussed it all the way back in the 40s [1].

Ok, who cares?

In a language like Haskell, divergent terms like this aren’t necessarily a problem. But in the world of theorem proving, they can be a bit more problematic. In a dependently typed theorem prover (like rocq, agda or lean), types are used to represent propositions. So for example, we cold have a statement:

def impl_self := ∀ a, a -> a

i.e. that every proposition implies itself. To prove this, we need to construct an object with this type, to act as a witness. This is called a constructive proof; we prove something is true by giving a concrete example. The specifics depend on the type of thing you are trying to prove. By the Curry-Howard correspondence (oh look, there he is again!), implication a -> b is the same thing as having a function a -> b. (Hence, the same symbol is used in both cases.) Therefore, we can prove the above by using:

def prf : impl_self := fun _ a' => a'

In this example, a' : a, so we have a function that takes a -> a. Just like that, we have proven that all things imply themselves.

And hopefully now you see why I descriptively named the type Evil. A divergent term like unpack (Mk unpack), whose type is totally parametric, can be used to prove anything at all. For example:

theorem oops : False = True := unpack (.Mk unpack)

Formally, our logical system becomes inconsistent. An inconsistent logic is one where all terms are provable — or equivalently, one where True = False. An inconsistent system is not sound — it means you can no longer trust your proofs. In a theorem prover, soundness is very important. Only true things ought to be provable.

Avoiding Evil Types

So why does this happen? And how can we prevent it? The root of all Evil lies in so called negative recursion. The standard definition is that the thing we are defining appears “on the left of an arrow”. Here are some examples in haskell:

-- OK:
data List a
  = Nil
  | Cons a (List a)
--          ^ Positive

-- Not OK:
data Tm -- Encode terms in the lambda calculus:
  = App Tm Tm
--      ^  ^ Both of these are positive
  | Abs (Tm -> Tm) Tm
--       ^ This is a "negative occurrence" of Tm
--         on the left of an arrow

In lean, the equivalent looks like this:

inductive List a where
  | Nil : List a
  | Cons : a -> List a -> List a

inductive Tm where
  | App : Tm -> Tm -> Tm
  | Abs : (Tm -> Tm) -> Tm

Here, because of how Lean’s syntax for inductive definitions work, the standard definition isn’t very helpful. Any time the type appears as an argument to one of it’s constructors, it’s to the left of an arrow. But, again, the first definition is strictly positive, where the second is negative. The intuition is that the thing being defined can’t appear “as an argument to an argument” to one of it’s constructors. That’s a bit of a mouthful, so a concrete example can help:

inductive Tm where
  | App : Tm -> Tm -> Tm
--        ^     ^ Both of these are positive
--                They are arguments themselves
  | Abs : (Tm -> Tm) -> Tm
--         ^ This is a "negative occurrence" of Tm
--           It's an argument to an argument

To preserve consistency, systems like lean disallow definitions that are not strictly positive. This is a little bit annoying, since lot’s of wonderful things are defined in a non-strictly-positive way. The Tm example is an instance of something called higher order abstract syntax (HOAS). HOAS is a very convenient way to avoid doing substitution by hand, and unfortunately it’s not allowed in lean. Neither are the modular data types of Data types à la carte [2]. Alas, this is the price we pay for a system where false is not true.

Non-Strict Positivity

Attentive readers may note that “strict positivity” implies the existence of “non-strict positivity” (or just “positivity”). And indeed there is. For this, we need to start counting arrows. An occurrence is positive if it appears on the left of an even number of arrows, and negative otherwise. A definition is strictly positive if it appears to the left of 0 arrows. Again, an example might help:

data Contrived
  = Mk1 ((Contrived -> Bool) -> Bool)
--        ^         ^        ^ two arrows
--        | so this is positive
  | Mk2 Contrived
--      ^ This is _strictly_ positive

Positive definitions are enough to avoid Curry’s paradox. So why does lean require definitions to be strictly positive? Well, it turns out that positive definitions that are not strictly positive can still lead to an inconsistent system, although the story is a bit more complex. There are three features, where having all three leads to an inconsistent system. Positive definitions, impredicativity and a universe type. A full explanation can be found on counterexamples.org [3]. Lean allows (certain) impredicative definitions, and has a universe type, so it has to ban positive types to stay consistent.