试图理解索引类型

Question

我正在尝试理解FStar教程中的向量类型：

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

通过Cons nat 3 Nil构造向量(类似于构造普通列表)失败，而Cons nat 3被接受。有人能向我解释我为什么要读Cons，因为它需要一个尾部参数吗？此外，如何创建带有实际元素的向量--或者是“空向量”类型？

Answer 1

这里有些混乱，对不起:)

1. a of vector (出于我也不清楚的原因)隐含在Nil和Cons中。因此，在编写Cons nat时，nat参数实际上是hd参数，F*推断a为Type0 (nat的类型)。因此，您正在构造一个类型向量，这可能不是intended.
2. The Cons nat 3 Nil失败的原因，因为3参数是错误的，并且与Nil列表的长度不相对应。nat.
3. The工作并且是1大小的向量，包含单个类型的Cons nat 3工作，因为您还没有给它tl参数，所以这是一个部分应用的构造函数，Cons应用于它的3个参数中的2个。Cons nat 3的类型是vector Type0 3 -> vector Type0 4，因此一个函数需要大小为3的向量才能生成类型4的向量。

希望这能有所帮助。