3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I'm not clear on what you're trying to construct. In the standard List definition, nil isn't exactly qualified by A, it has type "List A", so "nil A" isn't a thing it's just "nil" and it has type "List A" (for any A, because it's polymorphic). In essence the change you suggest is in fact what you already have. Or have I missed the point? $\endgroup$ – Luke Mathieson Feb 15 '14 at 5:01
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks. I have some misunderstood by W-type (I still do not understand...), and I have noticed that my version of nil is not uniquely typed... $\endgroup$ – molikto Feb 16 '14 at 11:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.