Haskell详细的存在量化

Question

我对类型的存在量化是什么以及它可以在何处使用有一个大概的概念.然而,根据我迄今为止的经验,为了有效地使用这个概念,需要理解许多警告.

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

• 存在主义类型的统一如何运作 - 什么是统一的,什么不是？
• 按类型执行后续操作的顺序是什么？

我的目标是更好地理解GHC向我抛出的错误信息.消息通常会说些什么"this type using forall and this other type don't match",但是它们并没有解释为什么会如此.

Answer 1

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.当谈到使用数据构造函数可能会遇到的类型错误时,存在类型和通用类型之间没有太大区别.

二,请注意等级-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".