Trying to understand indexed types

Question

I'm trying to understand the vector type from the FStar tutorial:

type vector (a: Type) : nat -> Type =
   | Nil :  vector a 0
   | Cons : hd: a -> n: nat -> tl: vector a n -> vector a (n + 1)

Constructing a vector - similarly to constructing ordinary lists - by Cons nat 3 Nil fails, while Cons nat 3 is accepted. Could someone explain to me where I'm wrong by reading Cons as requiring a tail parameter? Furthermore, how vectors with actual elements are created - or is it an "empty vector" type?

Answer 1

There is quite a bit of confusion here, sorry :)

1. The type argument a of vector is (for reasons that are also unclear to me) implicit for Nil and Cons. So when you write Cons nat the nat argument is really the hd argument and F* infers a to be Type0 (the type of nat). So you're constructing a vector of types, which might not be what you intended.

2. The reason Cons nat 3 Nil fails is because the 3 argument is wrong and doesn't correspond to the length of the Nil list. Cons nat 0 Nil works and is the vector of size 1 containing the single type nat.

3. The reason Cons nat 3 works is because you didn't yet give it the tl argument, so this is a partially applied constructor, Cons applied to 2 of its 3 arguments. The type of Cons nat 3 is vector Type0 3 -> vector Type0 4, so a function that expects a vector of size 3 in order to produce a vector of type 4.

Hope this helps.