什么是困境？

Question

对于Haskell禁止的“impredicative”类型，我有相当不错的直觉：即forall出现在除->以外的类型构造函数的参数中。但是什么是困境？什么使它很重要？它与“谓词”这个词有什么关系？

Answer 1

让我刚刚添加一个关于“词源”问题的观点，因为@DanielWagner的其他答案涵盖了很多技术基础。

关于a之类的谓词是a -> Bool。现在一个谓词逻辑就是某种意义上的谓词 - 所以如果我们有一个谓词P，我们可以谈论，对于一个给定的a,P(a)，现在在一个“谓词逻辑”（比如一阶逻辑）我们也可以说∀a. P(a)。所以我们可以量化变量并讨论谓词在这些事情上的行为。

现在，反过来说，如果所有的谓词被应用到之前的之上，我们说一个陈述是可以预测的。因此，陈述是“已经存在”的东西。反过来，如果某种意义在某种意义上可以通过其“引导”来表达自己，那么这种表述是不确定的。

因此，在例如上面的例子id，我们发现，我们可以给一个类型id这样的，它需要的id的类型的东西，否则类型的id的东西。所以现在我们可以给一个函数一个类型，其中一个量化变量（由forall a.引入）可以“扩展”为与整个函数本身相同的类型！

因此impredicativity引入了某种“自我引用”的可能性。但是，等等，你可能会说，这种事情不会导致矛盾吗？答案是：“好的，有时候。”尤其是，多变lambda演算的“系统F”和GHC的“核心”语言的核心“核心”允许一种不确定性形式，但它有两个层次 - 价值层次和类型层次，允许量化自身。在这种两层次的分层中，我们可以具有不可预测性和不矛盾/悖论。

虽然注意到这一技巧是非常细腻且容易通过添加更多的功能搞砸了，因为这集由奥列格文章指出：http://okmij.org/ftp/Haskell/impredicativity-bites.html

Answer 2

这些类型系统的中心问题是：“你可以用一个多态类型替换类型变量吗？”。预测型系统是毫无意义的学校答案，“绝对不是”，而impandicative类型的系统是你的无忧无虑的伙伴谁认为这听起来像一个有趣的想法，可能会出错？

现在，Haskell把讨论混淆了一下，因为它认为多态性应该是有用的，但看不见。所以对于这篇文章的其余部分，我将用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。表语型系统是比较谨慎的说了一下：只有单态类型在允许

有一个类似的故事[] :: forall a. [a]和(:) :: forall a. a -> [a] -> [a]。（所以，如果我们有一个特别的b，我们可以写id :: b -> b）。虽然你的无忧无虑的伙伴可能会好起来[] :: [forall b. b]和(:) :: (forall b. b) -> [forall b. b] -> [forall b. b]，但是这个谓词的学校课程并不那么重要。实际上，正如你可以从列表的唯一两个构造函数中看到的那样，是没有办法生成包含多态值的列表，而没有将它们的构造函数中的类型变量实例化为多态值。因此，虽然[forall b. b]的允许用我们的Haskell方言，但它并不是真的明智的 - 这种类型的术语没有（终止）。这激发了GHC的决定，如果你甚至想到这种类型 - 这是编译器告诉你“不要打扰”的方式，抱怨。*

那么，什么使得学校学生如此严格？像往常一样，答案是关于保持类型检查和类型推断可行。猜测类型的类型推断是正确的。键入检查seems like it might be possible，但它很复杂，没有人想保持这一点。

在另一方面，有些人可能会反对说GHC与某些类型的出现，要求非直谓性非常开心：

> :set -Rank2Types 
> :t id :: (forall b. b) -> (forall b. b) 
{- no complaint, but very chatty -} 

事实证明，非直谓性的微微有些限制的版本都差不太多：专，类型检查更高等级的类型（允许类型变量被多态类型替代时，它们只是(->)的参数）相对简单。您确实会失去2级以上的类型推断，1级以上的主要类型，但有时候更高的排名类型正是医生所订购的。

不知道这个词的词源，但！

*你可能不知道你是否可以做这样的事情：

data FooTy a where 
    FooTm :: FooTy (forall a. a) 

然后你会得到一个术语（FooTm），其类型有东西多态作为参数传递给比(->)其他的东西（即FooTy），你不必跨越学校做这件事，所以“将非(->)东西应用于多态类型没有用，因为你不能使它们”将被取消。 GHC不会让你写FooTy，我承认我不确定是否存在限制的原则性原因。

Answer 3

我想做出评论词源问题，因为@ sclv的答案不完全正确（词源，而不是概念上）。

回到时间，回到罗素时代，当一切都是理论 - 包括逻辑。特别重要的逻辑概念之一是“理解原则”;也就是说，给定一些逻辑谓词φ:A→2我们希望有一些原则来确定满足该谓词的所有元素的集合，写作“{x | φ(x) }”或其上的一些变化。要牢记的关键点是，“集合”和“谓词”被看作是根本不同的东西：谓词是从对象到真值的映射，集合是对象。因此，例如，我们可以允许对集合进行量化，但不能对谓词进行量化。

现在，罗素很担心他的同名矛盾，并寻求一些方法来摆脱它。有许多修正，但这里的利益之一是限制理解的原则。但首先，该原则的正式定义：∃S.∀x.S x ↔︎ φ(x);也就是说，对于我们特定的φ，存在一些对象（即，设置）S，使得对于每个对象（也是一个集合，但被认为是一个元素）x，我们有那个S x（你可以把它看作是“x∈S “，虽然当时的逻辑学家给出了”∈“与仅仅并列的意思不同）是真实的，以防万一φ(x)为真。如果我们完全按照书面原则来采取这一原则，那么我们最终得出一个暗含的理论。但是，我们可以限制哪些φ允许我们理解。 （例如，如果我们说φ不能包含任何二阶量词）。因此，对于任何限制R，如果确定了一组S（即，通过理解生成）某些R -predicate，那么我们说S是“R -predicative”。如果我们语言中的每一组都是R -predicative，那么我们说我们的语言是“R -predicative”。然后，与带连字符的前缀事件通常情况一样，前缀会被丢弃并留下隐含的，从而产生“谓语”语言。而且，自然，不具有预测性的语言是“不确定的”。

这是旧学词源。自那时以来，这些条件已经消失，并获得了自己的生命。我们今天使用“预测性”和“impredicative”的方式完全不同，因为我们关心的事情已经改变了。所以有时可能有点难以看出我们的现代用法与这些东西有何联系。说实话，我并不认为词源学确实有助于理解这些词的真实含义（如今）。