forall a. [a] 和 [forall a. a] 有什么区别？（涉及IT技术）

Question

forall a. [a] 和 [forall a. a] 有什么区别？（涉及IT技术）

haskellpolymorphism

10

标题和标签应充分解释问题。

- Ollie Saunders

即使问题本身已经很明确，将一个小例子放在正文中也是很好的。 - JoshD

3

你有什么建议，Josh？ - Ollie Saunders

3个回答

6

类型forall a. [a]表示对于任何单一类型，它是一个包含该类型的列表。这也是仅使用[a]表示的意思，它是[]，空列表数据构造函数的类型。

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

因此，区别在于，虽然第一个可以用作任何类型的列表（基本上是按定义），但后者根本不能用作任何具体类型的列表，因为没有办法将其固定为任何单一类型。

要解释标签--存在类型是指在某些范围内将被实例化为某个未知具体类型的类型。它可以是任何东西，因此由上面的forall a. a表示。为了确保任何具有存在类型的内容仅在实际类型可用的范围内使用，编译器会防止存在类型“逃逸”。

可能有所帮助的是，将forall量词器视为类似于lambda表达式--它引入一个新的类型变量，并将该标识符绑定在某个范围内。在该范围之外，标识符没有意义，这就是为什么forall a. a非常无用的原因。

- C. A. McCann

我可以想到一个类型为 forall a. a 的值，即 ⊥。 - John L

1

@John：嗯，是的，但我有些犹豫称⊥为“值”。然而，作为学习的辅助，我认为“类型理论如何应用于Haskell”的问题最好在仅有全函数的虚构领域中考虑，⊥的存在大多数情况下只会分散注意力。此外，在彬彬有礼的场合讨论底部是不合适的。 ;) - C. A. McCann

1

我不同意。我认为最好一开始就提供完整的故事，而不是 "几乎正确 " 的陈述，因为当问题出现时，纠正比一开始就做到正确需要更多的工作。当然，这可能只是我的学习方式偏见。虽然有时候我也希望有一个没有 seq 的虚构 Haskell。 - John L

1

@John：我的想法是，如果你理解了一些类型理论，包括 ⊥，那么学习完整的故事会更容易；而如果你作为 Haskell 程序员忽略 ⊥，那么学习类型理论会更容易。在 Haskell 中使用的相当多的数学理论本来就只有在忽略 ⊥ 的情况下才能“正确”地工作... - C. A. McCann

4

在类型中使用forall意味着交集。因此forall a. a是所有类型的交集，或者类似于Int ∩ String ∩ ...，看起来会得到空集，但是每种类型都有一个额外的元素称为底部或⊥或Haskell中的undefined。从这里我们得到forall a. a = {⊥}。实际上，我们可以定义一个仅包含底部的类型：

data Zero

在这个设置之后，让我们来看看我们的类型，从[forall a. a]开始。它定义了一个底部列表或[Zero]，其中包含元素[], [undefined], [undefined, undefined], ...。让我们在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。

- Daniel

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- keegan · Accepted Answer

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

嗯，并不完全正确。您使用了标签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 的存在类型签名，假设您在 T 中绑定类型变量 x 为 S，则有 v :: T。

以下是几个具有该类型的术语：

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，因为它的类型（因此构造函数集）是未知的。这比面向对象编程更复杂。

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

将上述示例翻译如下：

{-# 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

进一步阅读

如果您想了解理论方面，我强烈推荐 Pierce 的 类型和编程语言。如果想了解 GHC 中存在类型的讨论，请参阅GHC 手册和Haskell 维基。