forall a. [a]和[forall a.a]有什么不同？

Question

标题和标签应该充分解释这个问题。

Answer 1

标题和标签应该能充分解释这个问题。

呃，不是很好。您使用了标记existential-type，但是您给出的两个类型都不是存在的。

系统F

这里已经有了一些很好的答案，所以我将采取一种不同的方法，并且更正式一些。多态值本质上是类型上的函数，但Haskell的语法使类型抽象和类型应用都是隐式的，这就掩盖了这个问题。我们将使用System F表示法，它具有显式的类型抽象和类型应用程序。

例如，熟悉的map函数将被编写为

map :: ∀a. ∀b. (a → b) → [a] → [b]
map = Λa. Λb. λ(f :: a → b). λ(xs :: [a]). case xs of
  [] → []
  (y:ys) → f y : map @a @b f ys

map现在是一个具有四个参数的函数:两种类型(a和b)、一个函数和一个列表。我们像往常一样使用Λ(大写的lambda)编写一个覆盖类型的函数，并使用λ编写一个覆盖值的函数。包含Λ的术语会导致包含∀的类型，正如包含λ的术语会导致包含→的类型一样。我使用符号@a (和GHC Core中一样)来表示类型参数的应用。

因此，多态类型的值就像一个从类型到值的函数。多态函数的调用者可以选择一个类型参数，并且该函数必须遵守。

∀a. a

那么，我们如何编写∀a. [a]类型的术语呢？我们知道包含∀的类型来自包含Λ的术语：

term1 :: ∀a. [a]
term1 = Λa. ?

在标记为?的主体中，我们必须提供一个[a]类型的术语。也就是说，类型为∀a. [a]的术语的意思是“给定任何类型的a，我将给您一个类型为[a]的列表”。

然而，我们对a一无所知，因为它是一个从外部传入的参数。所以我们可以返回一个空的列表

term1 = Λa. []

或未定义的值

term1 = Λa. undefined

或仅包含未定义值的列表

term1 = Λa. [undefined, undefined]

但除此之外就没什么了。

∀a. a

那[∀a. a]呢？如果∀表示类型上的一个函数，那么[∀a. a]就是一个函数列表。我们可以提供我们想要的数量：

term2 :: [∀a. a]
term2 = []

或相同数量的：

term2 = [f, g, h]

但是对于f、g和h，我们的选择是什么呢

f :: ∀a. a
f = Λa. ?

现在我们真的被卡住了。我们必须提供一个a类型的值，但是我们对a类型一无所知。所以我们唯一的选择就是

f = Λa. undefined

因此，我们的term2选项如下所示

term2 :: [∀a. a]
term2 = []
term2 = [Λa. undefined]
term2 = [Λa. undefined, Λa. undefined]

等等，让我们不要忘记

term2 = undefined

存在类型

通用(∀)类型的值是从类型到值的函数。存在(∃)类型的值是类型和值的一对。

更具体地说:类型为

∃x. T

是一对

(S, v)

其中S是一个类型，其中是v :: T，假设您将类型变量x绑定到T中的S。

下面是一个存在类型签名和该类型的一些术语：

term3 :: ∃a. a
term3 = (Int,         3)
term3 = (Char,        'x')
term3 = (∀a. a → Int, Λa. λ(x::a). 4)

换句话说，只要将该值与其类型配对，我们就可以将任何值放入∃a. a中。

类型为∀a. a的值的用户处于非常有利的地位；他们可以使用类型应用程序@T选择他们喜欢的任何特定类型，以获得类型为T的术语。类型为∀a. a的值的生产者的处境很糟糕:他们必须准备好生成所需的任何类型，因此(与上一节一样)唯一的选择就是Λa. undefined。

∃a. a类型的值的用户处于糟糕的境地；里面的值是某种未知的特定类型，而不是灵活的多态值。类型为∃a. a的值的生产者处于非常有利的位置；正如我们在上面看到的那样，他们可以将任何喜欢的值添加到这对值中。

那么，什么是不那么无用的存在主义呢？与二进制操作配对的值如何：

type Something = ∃a. (a, a → a → a, a → String)

term4_a, term4_b :: Something
term4_a = (Int,    (1,     (+)  @Int , show @Int))
term4_b = (String, ("foo", (++) @Char, λ(x::String). x))

使用它：

triple :: Something → String
triple = λ(a, (x :: a, f :: a→a→a, out :: a→String)).
  out (f (f x x) x)

结果是：

triple term4_a  ⇒  "3"
triple term4_b  ⇒  "foofoofoo"

我们已经打包了一个类型和对该类型的一些操作。用户可以应用我们的操作，但不能检查具体的值-我们不能在triple中的x上进行模式匹配，因为它的类型(因此构造函数集)是未知的。这有点像面向对象编程。

使用实数的存在

使用∃和类型-值对的existentials的直接语法将非常方便。UHC部分支持这种直接语法。但GHC并非如此。为了在GHC中引入existentials，我们需要定义新的“包装器”类型。

翻译上面的例子：

{-# LANGUAGE ExistentialQuantification #-}

data Something = forall a. MkThing a (a -> a -> a) (a -> String)

term_a, term_b :: Something
term_a = MkThing 1 (+) show
term_b = MkThing "foo" (++) id

triple :: Something -> String
triple (MkThing x f out) =
  out (f (f x x) x)

与我们的理论处理方法有一些不同。类型应用程序、类型抽象和类型对也是隐式的。此外，包装器是用forall而不是exists编写的，这让人感到困惑。这引用了一个事实，即我们声明了一个存在类型，但数据构造函数具有通用类型：

MkThing :: forall a. a -> (a -> a -> a) -> (a -> String) -> Something

通常，我们使用存在量化来“捕获”类型类约束。我们可以在这里做一些类似的事情：

data SomeMonoid = forall a. (Monoid a, Show a) => MkMonoid a

进一步阅读

关于这个理论的介绍，我强烈推荐皮尔斯的。有关GHC中存在词类型的讨论，请参阅the GHC manual和the Haskell wiki。

Answer 2

类型forall a. [a]意味着对于任何单个类型，它都是包含该类型的列表。这也是普通[a]的含义，也是[]的类型，即空列表数据构造函数。

类型[forall a. a]意味着您有一个具有多态类型的值列表，也就是说，每个值都是任何可能类型的值，不一定与列表中的其他元素相同。任何可能的值都不能具有forall a. a类型，因此这也必须是一个空列表。

不同之处在于，虽然前者可以用作任何类型的列表(根据定义，基本上)，但后者根本不能用作任何具体类型的列表，因为无法将其固定到任何单个类型。

为了处理标记--存在类型是在某个范围内将被实例化为某个未知的具体类型的类型。它可以是任何东西，所以由上面的forall a. a表示。为了确保具有存在类型的任何内容仅在实际类型可用的作用域内使用，编译器会阻止存在类型“转义”。

将forall量词看作是一个λ表达式可能会有所帮助--它引入了一个新的类型变量，并将该标识符绑定在某个范围内。在这个作用域之外，标识符没有任何意义，这就是为什么forall a. a非常无用。

Answer 3

当用于类型时，forall表示交集。所以forall a. a是所有类型的交集，或者像Int ∩ String ∩ ...这样的东西，它似乎给出了空集，但每种类型都有一个额外的元素，在Haskell中称为undefined或⊥。从这里我们得到了forall a. a = {⊥}。实际上我们可以定义一个只包含bottom的类型：

data Zero

完成此设置后，让我们从[forall a. a]开始查看我们的类型。它定义的是一个包含[], [undefined], [undefined, undefined], ...元素的bottoms或[Zero]的列表。让我们在ghci中检查它：

> let l = [undefined, undefined]::[Zero]
> :t l
l :: [Zero]

以类似的方式，forall a. [a]是所有列表类型的交集，因为∩[a] = [∩a]，所以它也是[Zero]。

要进行最终检查，让我们定义：

type L = forall a. [a]
type U = [forall a. a]

在ghci中：

> let l2 = [undefined, undefined]::L
> let l3 = [undefined, undefined]::U
> :t l2
l2 :: [a]
> :t l3
l3 :: U

注意l2::[a]，解释是Haskell在所有多态类型前面放了一个隐式的forall。