fstar - 如何声明 hasEq 约束？

Question

我刚开始使用 F*，我的意思是我已经在教程中写了几行。到目前为止，它真的很有趣，我想继续学习。

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

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

但我得到了错误

Failed to verify implicit argument: Subtyping check failed; expected type (a#6468:Type{(hasEq a@0)}); got type Type

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

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

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

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

没有让我去任何地方。本教程不包括 hasEq我在 GitHub 存储库的示例中找不到任何有用的东西，所以现在我被卡住了。

Answer 1

您在此处正确识别了问题。型号'a您在 nonEmptyList 的定义中使用的未指定，因此无法支持平等。你的直觉是正确的，你需要告诉 F* 'a是一种具有相等性的类型，通过对其进行改进:

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

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

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