Skip to main content
added 432 characters in body
Source Link
chi
  • 14.7k
  • 1
  • 31
  • 40

Assume we have an occurrence of $t$ in a type formed by type constants, products, sums, and arrows/functions/exponentials. Count the number of arrows where such occurrence occurs in the left argument (possibly zero). If such number is even, the occurrence is positive, otherwise it is negative.

More precisely, the types types $P$ containing a positive occurrence of $t$ can be defined as those of the form $$ t, T \to P, N \to T, P \times P, P + P $$

where types $N$ containing a negative occurrence of $t$ are those of the form $$ P \to T $$ where $T$ is any type.

(The exact definition depends on the type system at hand, which might have more of fewer type constructors. Still, the overall idea holds.)

A more direct mnemonic is: an arrow $\to$ introduces a negation on its left argument, and double negations cancel out.

Assume we have an occurrence of $t$ in a type formed by type constants, products, sums, and arrows/functions/exponentials. Count the number of arrows where such occurrence occurs in the left argument (possibly zero). If such number is even, the occurrence is positive, otherwise it is negative.

Assume we have an occurrence of $t$ in a type formed by type constants, products, sums, and arrows/functions/exponentials. Count the number of arrows where such occurrence occurs in the left argument (possibly zero). If such number is even, the occurrence is positive, otherwise it is negative.

More precisely, the types types $P$ containing a positive occurrence of $t$ can be defined as those of the form $$ t, T \to P, N \to T, P \times P, P + P $$

where types $N$ containing a negative occurrence of $t$ are those of the form $$ P \to T $$ where $T$ is any type.

(The exact definition depends on the type system at hand, which might have more of fewer type constructors. Still, the overall idea holds.)

A more direct mnemonic is: an arrow $\to$ introduces a negation on its left argument, and double negations cancel out.

Source Link
chi
  • 14.7k
  • 1
  • 31
  • 40

Assume we have an occurrence of $t$ in a type formed by type constants, products, sums, and arrows/functions/exponentials. Count the number of arrows where such occurrence occurs in the left argument (possibly zero). If such number is even, the occurrence is positive, otherwise it is negative.