什么是预测性？
What is predicativity?
我对 Haskell 禁止的类型有相当不错的直觉，因为 "impredicative"：即 forall 出现在 -> 以外的类型构造函数的参数中。但究竟什么是预测性？是什么让它变得重要？它与 "predicate" 这个词有什么关系？
这些类型系统的核心问题是：“你能用多态类型代替类型变量吗？”。谓语类型系统是严肃的学生回答，“绝对不是”，而谓语类型系统是您无忧无虑的伙伴，他认为这听起来很有趣并且可能会出错？
现在，Haskell 使讨论有点混乱，因为它认为多态性应该有用但不可见。因此，对于此 post 的其余部分，我将使用 Haskell 的方言进行写作，其中 forall 的使用不仅是允许的，而且是必需的。这样我们就可以区分 a 类型，它是一种单态类型，它从我们稍后可以定义的类型环境中获取它的值，而 forall a. a 类型，它是一种更难的多态类型居住。我们还将允许 forall 在类型中的几乎所有位置——正如我们将看到的，GHC 将其类型语法限制为“快速失败”机制而不是技术要求。
假设我们已经告诉编译器id :: forall a. a -> a。我们以后可以要求使用 id 就好像它的类型是 (forall b. b) -> (forall b. b) 一样吗？谓词类型系统对此没有问题，因为我们可以将 id 类型中的量词实例化为 forall b. b，并在结果的任何地方用 forall b. b 代替 a。谓词类型系统对此更加谨慎：只允许单态类型。（所以如果我们有一个特定的 b，我们可以写成 id :: b -> b。）
关于 [] :: forall a. [a] 和 (:) :: forall a. a -> [a] -> [a] 也有类似的故事。虽然您无忧无虑的伙伴可能对 [] :: [forall b. b] 和 (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] 没意见，但谓词 schoolmarm 却不是这样。事实上，正如您从仅有的两个列表构造函数中看到的那样， 没有办法在不将构造函数中的类型变量实例化为多态值的情况下生成包含多态值的列表。因此，尽管类型 [forall b. b] 在我们的 Haskell 方言中是 allowed，但它并不是真正明智的——没有该类型的（终止）术语。这促使 GHC 决定在您考虑这种类型时进行投诉——这是编译器告诉您“别费心”的方式。*
嗯，是什么让女学生如此严格？像往常一样，答案是保持类型检查和类型推断可行。谓词类型的类型推断是正确的。类型检查 seems like it might be possible，但它太复杂了，没有人愿意维护它。
另一方面，有些人可能会反对 GHC 非常满意某些似乎需要预测性的类型：
> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}
事实证明，一些稍微受限的预测性版本并不太糟糕：具体来说，类型检查更高级别的类型（当类型变量只是 [=30 的参数时，它允许类型变量被多态类型替换） =]) 比较简单。你确实失去了 rank-2 以上的类型推断，以及 rank-1 以上的主要类型，但有时更高级别的类型正是医生所要求的。
不过我不知道这个词的词源。
* 你可能想知道你是否可以做这样的事情：
data FooTy a where
FooTm :: FooTy (forall a. a)
然后你会得到一个术语（FooTm），它的类型有一些多态的东西作为参数而不是(->)（即FooTy），你没有越过 schoolmarm 来做这件事，因此“将非 (->) 的东西应用于多态类型是没有用的，因为你不能制造它们”的信念将被推翻。 GHC 不允许你写 FooTy，我承认我不确定是否有原则性的限制原因。
（几年后的快速更新： 是 一个很好的原则性理由 FooTm 仍然不行。即，GADT 在 GHC 中的实现方式是通过类型等式，所以 FooTm 的扩展类型实际上是 FooTm :: forall a. (a ~ forall b. b) => FooTy a。因此要实际使用 FooTm，确实需要实例化一个具有多态类型的类型变量。感谢 Stephanie Weirich 向我指出了这一点。）
让我就 "etymology" 问题补充一点，因为@DanielWagner 的另一个回答涵盖了大部分技术基础。
像 a 这样的谓词是 a -> Bool。现在谓词逻辑是一种可以在某种意义上对谓词进行推理的逻辑——所以如果我们有一些谓词 P 并且我们可以讨论，对于给定的 a、P(a)，现在a"predicate logic"（比如一阶逻辑）我们也可以说∀a. P(a)。所以我们可以量化变量并讨论谓词对这些事物的行为。
现在，反过来，如果一个谓词所应用的所有事物都先于被引入，我们就说一个语句是谓语的。所以语句是 "predicated on" 已经存在的东西。反过来，如果一个陈述在某种意义上可以通过它的 "bootstraps".
来指代自己，那么这个陈述就是非谓语的。
因此，例如在上面的 id 示例中，我们发现我们可以给 id 一个类型，这样它就可以将 id 的 类型 的某些东西传递给其他东西id 的 类型 。所以现在我们可以给函数一个类型，其中量化变量（由 forall a. 引入）可以 "expand" 与整个函数本身的类型相同！
因此，不确定性引入了某种"self reference" 的可能性。但是等等，你可能会说，这样的事情不会导致矛盾吗？答案是："well, sometimes." 特别是，"System F" 是多态 lambda 演算和 GHC "core" 语言的基本 "core" 允许一种形式的非预测性，但它有两个层次 - - 价值水平和类型水平，允许对其自身进行量化。在这个两级分层中，我们可以有不确定性和不 contradiction/paradox.
虽然请注意，这个巧妙的技巧 非常 精致，并且很容易因添加更多功能而搞砸，正如 Oleg 的这篇文章集所示：http://okmij.org/ftp/Haskell/impredicativity-bites.html
我想对词源问题发表评论，因为@sclv 的回答不太正确（词源上，而不是概念上）。
回到过去，回到罗素的时代，那时一切都是集合论——包括逻辑。特定导入的逻辑概念之一是 "principle of comprehension"；也就是说，给定一些逻辑谓词 φ:A→2 我们希望有一些原则来确定满足该谓词的所有元素的集合，写为“{x | φ(x) }”或其一些变体。要记住的关键点是 "sets" 和 "predicates" 被视为根本不同的东西：谓词是从对象到真值的映射，而集合是对象。因此，例如，我们可能允许对集合进行量化但不允许对谓词进行量化。
现在，罗素非常关心他的同名悖论，并寻求某种方法来摆脱它。有许多修正，但这里感兴趣的一个是限制理解的原则。但首先，原则的正式定义：∃S.∀x.S x ↔︎ φ(x)；也就是说，对于我们特定的 φ 存在一些对象（即集合）S 这样对于每个对象（也是一个集合，但被认为是一个元素）x，我们有S x（你可以认为这意味着“x∈S”，尽管当时的逻辑学家赋予“∈”一个不同于单纯并列的含义）是正确的，以防万一φ(x) 是真的。如果我们完全按照所写的原则进行操作，那么我们最终会得到一个非谓语理论。但是，我们可以限制我们可以理解哪些 φ 。 （例如，如果我们说 φ 不能包含任何二阶量词。）因此，对于任何限制 R，如果确定了集合 S（即通过理解生成) 通过一些 R-谓词，那么我们说 S 是“R-谓词”。如果我们语言中的每个集合都是 R-谓语，那么我们说我们的语言是“R-谓语”。然后，就像带连字符的前缀事物经常出现的情况一样，前缀被删除并隐式保留，因此 "predicative" 语言。而且，自然地，非谓语的语言是 "impredicative".
这是老派词源。从那时起，条款已经取消并获得了自己的生命。我们今天使用 "predicative" 和 "impredicative" 的方式完全不同，因为我们关心的事情已经改变了。因此，有时很难看出我们的现代用法与这些东西有何关联。老实说，我不认为了解词源真的有助于弄清楚这些词的真正含义（如今）。
我对 Haskell 禁止的类型有相当不错的直觉，因为 "impredicative"：即 forall 出现在 -> 以外的类型构造函数的参数中。但究竟什么是预测性？是什么让它变得重要？它与 "predicate" 这个词有什么关系？
这些类型系统的核心问题是：“你能用多态类型代替类型变量吗？”。谓语类型系统是严肃的学生回答，“绝对不是”，而谓语类型系统是您无忧无虑的伙伴，他认为这听起来很有趣并且可能会出错？
现在，Haskell 使讨论有点混乱，因为它认为多态性应该有用但不可见。因此，对于此 post 的其余部分，我将使用 Haskell 的方言进行写作，其中 forall 的使用不仅是允许的，而且是必需的。这样我们就可以区分 a 类型，它是一种单态类型，它从我们稍后可以定义的类型环境中获取它的值，而 forall a. a 类型，它是一种更难的多态类型居住。我们还将允许 forall 在类型中的几乎所有位置——正如我们将看到的，GHC 将其类型语法限制为“快速失败”机制而不是技术要求。
假设我们已经告诉编译器id :: forall a. a -> a。我们以后可以要求使用 id 就好像它的类型是 (forall b. b) -> (forall b. b) 一样吗？谓词类型系统对此没有问题，因为我们可以将 id 类型中的量词实例化为 forall b. b，并在结果的任何地方用 forall b. b 代替 a。谓词类型系统对此更加谨慎：只允许单态类型。（所以如果我们有一个特定的 b，我们可以写成 id :: b -> b。）
关于 [] :: forall a. [a] 和 (:) :: forall a. a -> [a] -> [a] 也有类似的故事。虽然您无忧无虑的伙伴可能对 [] :: [forall b. b] 和 (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] 没意见，但谓词 schoolmarm 却不是这样。事实上，正如您从仅有的两个列表构造函数中看到的那样， 没有办法在不将构造函数中的类型变量实例化为多态值的情况下生成包含多态值的列表。因此，尽管类型 [forall b. b] 在我们的 Haskell 方言中是 allowed，但它并不是真正明智的——没有该类型的（终止）术语。这促使 GHC 决定在您考虑这种类型时进行投诉——这是编译器告诉您“别费心”的方式。*
嗯，是什么让女学生如此严格？像往常一样，答案是保持类型检查和类型推断可行。谓词类型的类型推断是正确的。类型检查 seems like it might be possible，但它太复杂了，没有人愿意维护它。
另一方面，有些人可能会反对 GHC 非常满意某些似乎需要预测性的类型：
> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}
事实证明，一些稍微受限的预测性版本并不太糟糕：具体来说，类型检查更高级别的类型（当类型变量只是 [=30 的参数时，它允许类型变量被多态类型替换） =]) 比较简单。你确实失去了 rank-2 以上的类型推断，以及 rank-1 以上的主要类型，但有时更高级别的类型正是医生所要求的。
不过我不知道这个词的词源。
* 你可能想知道你是否可以做这样的事情：
data FooTy a where
FooTm :: FooTy (forall a. a)
然后你会得到一个术语（FooTm），它的类型有一些多态的东西作为参数而不是(->)（即FooTy），你没有越过 schoolmarm 来做这件事，因此“将非 (->) 的东西应用于多态类型是没有用的，因为你不能制造它们”的信念将被推翻。 GHC 不允许你写 FooTy，我承认我不确定是否有原则性的限制原因。
（几年后的快速更新： 是 一个很好的原则性理由 FooTm 仍然不行。即，GADT 在 GHC 中的实现方式是通过类型等式，所以 FooTm 的扩展类型实际上是 FooTm :: forall a. (a ~ forall b. b) => FooTy a。因此要实际使用 FooTm，确实需要实例化一个具有多态类型的类型变量。感谢 Stephanie Weirich 向我指出了这一点。）
让我就 "etymology" 问题补充一点，因为@DanielWagner 的另一个回答涵盖了大部分技术基础。
像 a 这样的谓词是 a -> Bool。现在谓词逻辑是一种可以在某种意义上对谓词进行推理的逻辑——所以如果我们有一些谓词 P 并且我们可以讨论，对于给定的 a、P(a)，现在a"predicate logic"（比如一阶逻辑）我们也可以说∀a. P(a)。所以我们可以量化变量并讨论谓词对这些事物的行为。
现在，反过来，如果一个谓词所应用的所有事物都先于被引入，我们就说一个语句是谓语的。所以语句是 "predicated on" 已经存在的东西。反过来，如果一个陈述在某种意义上可以通过它的 "bootstraps".
来指代自己，那么这个陈述就是非谓语的。因此，例如在上面的 id 示例中，我们发现我们可以给 id 一个类型，这样它就可以将 id 的 类型 的某些东西传递给其他东西id 的 类型 。所以现在我们可以给函数一个类型，其中量化变量（由 forall a. 引入）可以 "expand" 与整个函数本身的类型相同！
因此，不确定性引入了某种"self reference" 的可能性。但是等等，你可能会说，这样的事情不会导致矛盾吗？答案是："well, sometimes." 特别是，"System F" 是多态 lambda 演算和 GHC "core" 语言的基本 "core" 允许一种形式的非预测性，但它有两个层次 - - 价值水平和类型水平，允许对其自身进行量化。在这个两级分层中，我们可以有不确定性和不 contradiction/paradox.
虽然请注意，这个巧妙的技巧 非常 精致，并且很容易因添加更多功能而搞砸，正如 Oleg 的这篇文章集所示：http://okmij.org/ftp/Haskell/impredicativity-bites.html
我想对词源问题发表评论，因为@sclv 的回答不太正确（词源上，而不是概念上）。
回到过去，回到罗素的时代，那时一切都是集合论——包括逻辑。特定导入的逻辑概念之一是 "principle of comprehension"；也就是说，给定一些逻辑谓词 φ:A→2 我们希望有一些原则来确定满足该谓词的所有元素的集合，写为“{x | φ(x) }”或其一些变体。要记住的关键点是 "sets" 和 "predicates" 被视为根本不同的东西：谓词是从对象到真值的映射，而集合是对象。因此，例如，我们可能允许对集合进行量化但不允许对谓词进行量化。
现在，罗素非常关心他的同名悖论，并寻求某种方法来摆脱它。有许多修正，但这里感兴趣的一个是限制理解的原则。但首先，原则的正式定义：∃S.∀x.S x ↔︎ φ(x)；也就是说，对于我们特定的 φ 存在一些对象（即集合）S 这样对于每个对象（也是一个集合，但被认为是一个元素）x，我们有S x（你可以认为这意味着“x∈S”，尽管当时的逻辑学家赋予“∈”一个不同于单纯并列的含义）是正确的，以防万一φ(x) 是真的。如果我们完全按照所写的原则进行操作，那么我们最终会得到一个非谓语理论。但是，我们可以限制我们可以理解哪些 φ 。 （例如，如果我们说 φ 不能包含任何二阶量词。）因此，对于任何限制 R，如果确定了集合 S（即通过理解生成) 通过一些 R-谓词，那么我们说 S 是“R-谓词”。如果我们语言中的每个集合都是 R-谓语，那么我们说我们的语言是“R-谓语”。然后，就像带连字符的前缀事物经常出现的情况一样，前缀被删除并隐式保留，因此 "predicative" 语言。而且，自然地，非谓语的语言是 "impredicative".
这是老派词源。从那时起，条款已经取消并获得了自己的生命。我们今天使用 "predicative" 和 "impredicative" 的方式完全不同，因为我们关心的事情已经改变了。因此，有时很难看出我们的现代用法与这些东西有何关联。老实说，我不认为了解词源真的有助于弄清楚这些词的真正含义（如今）。