What is a constructor in Coq?

Question

I am having trouble understanding the principles of what a constructor is and how it works.

For example, in Coq, we have been taught to define the natural numbers like this:

Inductive nat : Type :=
   | O : nat
   | S : nat -> nat.

And have been told that S is a constructor, but what exactly does that mean?

If I then do:

Check (S (S (S (S O)))).

I get that it is 4 and of type nat.

How does this work, and how does Coq know that (S (S (S (S O)))) represents 4?

I guess the answer to this is some extremely clever background magic in Coq.

The pretty-printing of (S (S (S (S O)))) as 4 is just a convenience that you should not let distract you. If you are at the point where you want to get a feeling of what a constructor is, define your own type naturals with constructors Z (for zero) and N (for next). Then nothing magic will happen. — Pascal Cuoq

Pascal Cuoq Pascal Cuoq · Accepted Answer · 2011-02-23T12:18:50

Inductive naturals : Type :=
   | Z : naturals
   | N : naturals -> naturals.

says the following things:

Z is a term of type naturals
when e is a term of type naturals, N e is a term of type naturals.
Applying Z or N are the only two ways to create a natural. When given an arbitrary natural, you know that it was either made from one or from the other.
two terms e1 and e2 of type naturals are equal if and only if they are both Z or if they are respectively N t1 and N t2 with t1 equal to t2.

You can see how these rules would generalize to arbitrary inductive type definitions. In general, in an arbitrary inductive type definition for the type t:

applying a constructor to arguments of the correct types produces a term of type t;
any term of type t is the result of applying one of the constructors that were associated with the type t when it was defined; in other words, given a term of type t, one can assume that it is the result of applying one of the constructors of t;
two terms of type t are equal only if they result from applying the same constructors to the same arguments.

(Side note: when the type definition is for constructors of the shape of Z and N, these properties correspond more or less exactly Peano's axioms for natural numbers. This is why a type named nat is pre-defined in Coq with constructors of these shapes to be used to represent natural numbers. This type receives special treatment because it gets tiring very quickly to manipulate the raw form, but the special treatments are only there for convenience.)

What is a constructor in Coq?

2 Answers