我对 有一个大概的了解存在量化 类型是和可以使用的地方。然而,根据我迄今为止的经验,为了有效地使用这个概念,需要理解很多警告。
问题:是否有任何好的资源来解释如何在 GHC 中实现存在量化? IE。
我的目标是更好地理解 GHC 向我抛出的错误信息。消息通常会说
"this type using forall and this other type don't match"
,但是他们没有解释为什么会这样。
最佳答案
Simon Peyton-Jones 的论文中涵盖了细节,尽管需要大量的技术专业知识才能理解它们。如果你想阅读一篇关于 Haskell 类型推断如何工作的论文,你应该阅读广义代数数据类型 (GADT),它结合了存在类型和其他几个特性。我建议在 http://research.microsoft.com/en-us/people/simonpj/ 的论文列表中使用“用于 GADT 的完整和可判定类型推断”。 .
存在量化实际上很像全称量化。这是一个突出两者之间相似之处的示例。函数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
的返回类型中.当谈到使用数据构造函数可能会遇到的类型错误时,存在类型和通用类型之间没有太大区别。二、注意rank-2类型
forall a. a -> b
在 useExis
.这是类型推断的最大区别。从模式匹配中获取的存在类型 (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".
关于Haskell 存在量化详解,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/9259921/