Haskell 存在量化详解

Question

我对类型的存在量化是什么以及它可以在哪里使用有一个大致的了解。然而，根据我迄今为止的经验，为了有效地使用这个概念，需要理解很多注意事项。

问题：是否有任何好的资源可以解释 GHC 中如何实施存在量化？即

• 存在类型的统一是如何运作的——什么是统一的，什么不是？
• 对类型的后续操作按什么顺序执行？

我的目标是更好地理解 GHC 向我抛出的错误消息。消息通常会说一些类似的内容“使用 forall 的此类型与其他类型不匹配”，但是它们没有解释为什么会这样。

Answer 1

西蒙·佩顿·琼斯 (Simon Peyton-Jones) 的论文涵盖了具体细节，但需要大量的技术专业知识才能理解它们。如果您想阅读有关 Haskell 类型推断如何工作的论文，您应该阅读广义代数数据类型 (GADT)，它将存在类型与其他几个功能相结合。我建议“GADT 的完整且可判定的类型推断”，位于 http://research.microsoft 的论文列表中.com/en-us/people/simonpj/。

存在量化实际上很像通用量化。这是一个突出两者之间相似之处的例子。函数useExis没有用，但它仍然是有效的代码。

data Univ a = Univ a
data Exis = forall a. Exis a

toUniv :: a -> Univ a
toUniv = Univ

toExis :: a -> Exis
toExis = Exis

useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x

useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x

首先，请注意 toUniv 和 toExis 几乎相同。它们都有一个自由类型参数a，因为两个数据构造函数都是多态的。但是，虽然 a 出现在 toUniv 的返回类型中，但它却没有出现在 toExis 的返回类型中。当谈到使用数据构造函数可能出现的类型错误时，存在类型和通用类型之间没有太大区别。

其次，注意所有 a 的 2 级类型 。一个-> useExis 中的 b。这是类型推断的巨大差异。从模式匹配 (Exis x) 中获取的存在类型就像传递到函数体的额外隐藏类型变量，并且不得与其他类型统一。为了更清楚地说明这一点，这里是最后两个函数的一些错误声明，我们试图统一不应该统一的类型。在这两种情况下，我们强制 x 的类型与不相关的类型变量统一。在useUniv中，类型变量是函数类型的一部分。在useExis中，它是数据结构中的存在类型。

useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
                          -- Variable 'a' is there in the function type

useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
                          -- Variable 'a' comes from the pattern "Exis x",
                          -- via the existential in "data Exis = forall a. Exis a".