Haskell显式forall在lhs上有"缺失"类型参数

Question

我正在阅读haxl-Haxl的源代码.Core我发现了以下代码

data BlockedFetch r = forall a. BlockedFetch (r a) (ResultVar a)

并意识到我不完全理解ExplicitForall/ 的用法ExistentialQuantification.

上面的代码片段在哪些方面有所不同

data BlockedFetch r a = BlockedFetch (r a) (ResultVar a)

为什么我可以"省略"数据声明的lhs上的类型参数.

Answer 1

正如其他人所提到的,代码中的示例是存在量化的示例,因此与问题中的最终示例完全不同.

首先要注意的是,现在GADT符号通常是首选.GADT表示法中的类型是:

data BlockedFetch r where
    BlockedFetch :: r a -> ResultVar a -> BlockedFetch r

我们可以明确绑定a如下:

data BlockedFetch r where
    BlockedFetch :: forall a. r a -> ResultVar a -> BlockedFetch r

如果我们有免费的存在量化,这将与以下同构:

data BlockedFetch r where
    BlockedFetch :: (exists a. (r a, ResultVar a)) -> BlockedFetch r

这与不引入新关键字的愿望相结合,导致了旧的ExistentialQuantification语法.该BlockedFetch数据构造具有类型

BlockedFetch :: forall r a. r a -> ResultVar a -> BlockedFetch r

这就是尝试与语法沟通的内容:

data BlockedFetch r = forall a. BlockedFetch (r a) (ResultVar a)

从这个角度来看,与之相反的BlockedFetch r a是a,数据构造函数类型的结果会发生.forall a. F a -> G从逻辑上讲,它在概念上是等价的(exists a. F a) -> G,但显然不是forall a. F a -> G a等同于(exists a. F a) -> G a后者甚至没有良好范围的情况.

回到

BlockedFetch :: forall r a. r a -> ResultVar a -> BlockedFetch r

如果你不了解存在感,但你确实理解了普遍的量化,那么你就可以理解这是怎么回事.在这里,我们看到有人调用 BlockedFetch,即使用数据构造函数构建值,可以自由选择他们想要的任何类型a.有人消费,即模式匹配上,类型的值BlockedFetch R基本上是写一个函数forall a. R a -> ResultVar a -> X和函数必须连续工作任何的价值a,即调用该函数就可以选择的人a,这功能必须有这样的选择工作.