Is this a well founded inductive type? Can I express this in Coq?

Question

the standard List type in Coq can be expressed as:

Inductive List (A:Set) : Set :=
  nil : List A
| cons : A -> List A -> List A.

as I understand, W-type express a well-founded tree of elements of this type. so, what if nil is not qualified by A? i.e. we have:

for all A: Set nil : List A

instead of

for all A: Set nil A: List A

is this a correct W-type? can I express this in Coq?

Answer 1

You have misunderstood why A stands there in the definition of list.

Let us first look at how we might define lists of booleans:

Inductive ListBool : Set :=
  | nilBool : ListBool
  | consBool : bool -> ListBool -> ListBool.

And here is how we might define lists of natural numbers:

Inductive ListNat : Set :=
  | nilNat : ListNat
  | consNat : nat -> ListNat -> ListNat.

As you can see the nilBool and nilNat are constants that do not depend on any parameters. It is boring to define lists of booleans, lists of natural numbers, lists of lists of booleans, etc. Coq allows a parametrized definition of lists in which the List type itself takes a parameter A as input, to give lists of elements of type A. This is defined as you wrote:

Inductive List (A : Set) : Set :=
  | nil : List A
  | cons : A -> List A -> List A.

In the nil clause we have List A. Here A is the argument to List, it is not an argument to nil. If we wrote just List then Coq would ask "list of what"? For a similar reason the cons constructor has two occurences of List A.

Let me put it another way. The type of ListNat is Set. The type of List is Set -> Set. So we have to apply List to a set before we get a list.