Haskell存在量化的详细信息

我对存在量化的类型是什么以及可以在哪里使用有一个大致的了解。但是，从我迄今为止的经验来看，为了有效地使用这个概念，需要了解许多警告。Haskell存在量化的详细信息

问题：有没有什么好的资源可以解释GHC中如何实现存在量化？即

如何统一存在类型的工作 - 什么是可以统一的，什么是不可以的？
按什么顺序对类型进行后续操作？

我的目标是更好地理解GHC向我发出的错误消息。消息通常沿线"this type using forall and this other type don't match"说，但是他们没有解释为什么是这样。

2012-02-13 julkiewicz

Simon Peyton-Jones的论文报道了细节的细节，尽管需要大量的技术专业知识才能理解它们。如果你想读一篇关于Haskell类型推断如何工作的论文，你应该阅读一下广义代数数据类型（GADTs），它将存在类型和其他几个特征结合在一起。我在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的返回类型中。当涉及到使用数据构造函数时可能遇到的那种类型错误时，存在类型和通用类型之间没有太大区别。

二，请注意排名第二的forall a. a -> buseExis。这是类型推断中的重大差异。从模式匹配(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".

来源

2012-02-13 16:39:49 Heatsink

Haskell存在量化的详细信息

回答

相关问题