haskell - forall 和 a. 有什么区别？ [a] 和 [forall a.一种]？

Question

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

Answer 1

Title and tags should explain the question adequately.

呃，不是真的。您使用了标签 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] 类型的术语?我们知道包含 ∀ 的类型来自包含 Λ 的项:

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]是一个函数列表。我们可以提供尽可能少的:

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 ，假设您绑定(bind)了类型变量 x至 S内 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 的值的生产者处于有利地位；正如我们在上面看到的那样，他们可以将他们喜欢的任何值(value)加入到货币对中。

那么什么是不那么无用的存在呢？与二元运算配对的值如何:

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"

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

真实地使用存在主义

使用 ∃ 和类型-值对的存在项的直接语法会非常方便。 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

进一步阅读

对于理论的介绍，我强烈推荐 Types and Programming Languages通过皮尔斯。有关 GHC 中存在类型的讨论，请参阅 the GHC manual和 the Haskell wiki .