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!).
A
and explode the stack eventually (in stack-based languages). $\endgroup$ – wvxvw Apr 7 '16 at 20:14