fstar - 试图理解索引类型

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失败，whileCons nat 3被接受。Cons有人可以通过阅读需要尾部参数来向我解释我错在哪里吗？此外，如何创建具有实际元素的向量 - 还是“空向量”类型？

标签： fstar

Answer 1

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

1. 的类型参数a是vector（出于我也不清楚的原因）隐含的Niland Cons。因此，当您编写参数时Cons nat，nat实际上是hd参数，而 F* 推断a为Type0（的类型nat）。所以你正在构建一个类型的向量，这可能不是你想要的。

2. Cons nat 3 Nil失败的原因是因为3参数错误并且与列表的长度不对应Nil。Cons nat 0 Nil有效并且是包含单一类型的大小为 1 的向量nat。

3. 起作用的原因Cons nat 3是因为你还没有给它tl参数，所以这是一个部分应用的构造函数，Cons应用于它的 3 个参数中的 2 个。的类型Cons nat 3是vector Type0 3 -> vector Type0 4，所以一个函数需要一个大小为 3 的向量来生成一个类型为 4 的向量。

希望这可以帮助。