4

我刚从 F* 开始，我的意思是我已经写了几行连同教程。到目前为止，这真的很有趣，我想继续学习。

我自己尝试做的第一件事是编写一个表示非空列表的类型。这是我的尝试：

type nonEmptyList 'a = l : (list 'a) { l <> [] }

但我得到了错误

无法验证隐式参数：子类型检查失败；预期类型 (a#6468:Type{(hasEq a@0)}); 得到类型类型

我知道我走在正确的轨道上，因为如果我将列表类型限制为包含字符串，这确实有效：

type nonEmptyList = l : (list string) { l <> [] }

我假设这意味着l <> []在原始示例中无效，因为我没有指定'a应该支持平等。问题是我一生都无法弄清楚如何做到这一点。我猜这与更高的类型hasEq有关，但尝试诸如：

type nonEmptyList 'a = l : (list 'a) { hasEq 'a /\ l <> [] }

没有把我带到任何地方。该教程没有涵盖hasEq，我在 GitHub 存储库中的示例中找不到任何有用的东西，所以现在我被困住了。

4

2 回答 2

4

您在这里正确识别了问题。'a您在定义中使用的类型nonEmptyList未指定，因此不支持相等。您的直觉是正确的，您需要'a通过在其上添加改进来告诉 F* 这是一个具有相等性的类型：

为此，您可以编写以下内容：

type nonEmptyList (a:Type{hasEq a}) = l : (list a) { l <> [] }

请注意，我用于该类型的活页夹是a而不是'a. 它会导致语法错误，它更有意义，因为它不再是“任何”类型。另外，请注意，您可以更加精确并根据需要指定类型a的Type0全域。

于 2017-03-10T16:44:12.847 回答
3

您的分析确实是正确的，并且公认的答案通常给出了正确的解决方案。

但是，对于您的具体示例，您不需要列表元素上的可判定相等性：您可以只使用(list 'a){ ~ (List.isEmpty l) }.

作为参考，以下是 的定义isEmpty：

(** [isEmpty l] returns [true] if and only if [l] is empty  *)
val isEmpty: list 'a -> Tot bool
let isEmpty l = match l with
  | [] -> true
  | _ -> false
于 2017-05-17T17:56:48.173 回答