0

作为尝试熟悉 F* 的实验，我尝试实现一个应用函子。我陷入了一个看起来很奇怪的类型检查错误。我还不确定这是否是由于我不知道的类型检查中的某些功能/逻辑，或者这是否是由真正的错误引起的。

这是给我带来麻烦的代码部分：

module Test

noeq type test : Type -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

这是相应的错误：

Test(7,24-7,25): (Error 54) Test.test 'a is not a subtype of the expected type Test.test 'a (see also Test(7,12-7,13))
1 error was reported (see above)

有人可以向我指出我缺少什么吗？类型统一的行为是否受子类型化的影响？还是应该进行类型检查，这是编译器错误？

4

1 回答 1

1

我相信你没有强制执行的归纳有一个宇宙不平等约束。

以下代码将进行类型检查：

noeq type test : Type0 -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

注意0我在第一行添加的。

这是有效的，因为这表明第Type0一个宇宙比低于Type（我相信它本身意味着任何宇宙）。在您的情况下， F* 不知道如何比较这两种类型的宇宙，因此失败。

如果你写过noeq type test : Type -> Type0，你会看到一个稍微好一点的错误消息：“无法解决归纳法的宇宙不等式”。所以我在这里责怪错误信息。

如果解释不够精确，我深表歉意，我不是 PL 人... :)

于 2018-08-09T21:55:27.310 回答