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?
There is quite a bit of confusion here, sorry :)
The type argument
a
ofvector
is (for reasons that are also unclear to me) implicit forNil
andCons
. So when you writeCons nat
thenat
argument is really thehd
argument and F* infersa
to beType0
(the type ofnat
). So you're constructing a vector of types, which might not be what you intended.The reason
Cons nat 3 Nil
fails is because the3
argument is wrong and doesn't correspond to the length of theNil
list.Cons nat 0 Nil
works and is the vector of size 1 containing the single typenat
.The reason
Cons nat 3
works is because you didn't yet give it thetl
argument, so this is a partially applied constructor,Cons
applied to 2 of its 3 arguments. The type ofCons nat 3
isvector 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.