什么是困境？
对于Haskell所禁止的types，我有相当不错的直觉，就像“impandicative”一样：也就是说，除了->以外，类似于构造函数的参数出现在一个函数中。 但是什么是困境？ 什么使它重要？ 它与“谓词”有什么关系？
让我在“词源”问题上增加一点，因为@DanielWagner的其他答案涵盖了很多技术上的问题。
一个类似于a谓词是a -> Bool 。 现在一个谓词逻辑就是某种意义上的谓词，所以如果我们有一个谓词P ，那么对于一个给定的a ， P(a) ，现在可以用一个“谓词逻辑”（比如第一个顺序逻辑）我们也可以说∀a. P(a) ∀a. P(a) 。 所以我们可以对variables进行量化，并讨论谓词在这些事物上的行为。
现在，反过来说，如果一个谓词所应用的所有东西都在它之前被引入，那么我们说一个陈述是可以预测的。 因此，陈述是“已经存在”的东西。 反过来说，如果某种意义在某种意义上可以用“引导”来表示，那么这种表述就是不可预测的。
所以在例如上面的id例子中，我们发现我们可以给id一个types，使得它将某种types的id带到id types的其他types中。 所以现在我们可以给一个函数一个types，一个量化variables（由forall a.引入）可以“扩展”成与整个函数本身相同的types！
因此，不信任引入了某种“自我参照”的可能性。 但是，等等，你可能会说，这样的事情不会导致矛盾吗？ 答案是：“好的，有时候”。 特别是作为多态lambda演算的“系统F”和GHC的“核心”语言的核心“核心”允许一种不可预测性的forms，但它有两个层次 – 价值层次和types层次，允许量化自己。 在这个两层次的分层中，我们可以具有不可预测性，而不是矛盾/矛盾。
虽然请注意，这个巧妙的技巧是非常微妙的，通过添加更多的function很容易搞砸，因为这个由Oleg的文章集合表示： http : //okmij.org/ftp/Haskell/impredicativity-bites.html
这些types系统的中心问题是：“你可以用一个多态types来代替typesvariables吗？ 预测型系统是没有废话的学校答案，“绝对不是”，而impandicative型系统是你的无忧无虑的伙伴谁认为这听起来像一个有趣的想法，什么可能出问题？
现在，Haskell把讨论混淆了一下，因为它认为多态性应该是有用的，但是看不见的。 因此，对于这篇文章的其余部分，我将用Haskell的一个方言来写作，其中使用forall不仅是允许的，而且是必需的。 这样我们就可以区分typesa ，它是一个单types的types，它从我们稍后可以定义的打字环境中抽取它的值，以及typesforall a. a forall a. a ，这是一个更难的多态types居住。 我们也将允许forall在types的任何地方进行操作 – 正如我们将看到的那样，GHC将其types语法限制为“快速失败”机制，而不是技术要求。
假设我们已经告诉了编译器id :: forall a. a -> a id :: forall a. a -> a 。 我们稍后可以要求使用id ，就好像它有types一样(forall b. b) -> (forall b. b) ？ impandicativetypes的系统是可以的，因为我们可以实例化id的types的量词给所有的forall b. b forall b. b ，代替所有forall b. b forall b. b在结果中随处可见。 预测型系统有点更加谨慎：只允许单形types（所以如果我们有一个特定的b ，我们可以编写id :: b -> b 。
有关于[] :: forall a. [a]的类似故事[] :: forall a. [a] [] :: forall a. [a]和(:) :: forall a. a -> [a] -> [a] (:) :: forall a. a -> [a] -> [a] 。 虽然你的无忧无虑的朋友可以与[] :: [forall b. b] [] :: [forall b. b]和(:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] ，那么谓词的学校就不是这么多了。 实际上，从列表的唯一两个构造函数中可以看出，没有办法生成包含多态值的列表， 而没有在构造函数中将typesvariables实例化为多态值。 所以尽pipetypes[forall b. b] [forall b. b]在我们的Haskell方言中是允许的，这不是很明智的 – 这种types的术语没有（终止）。 这激发了GHC的决定，如果你甚至想到这样的types – 这是编译器告诉你“不要打扰”的方式。
那么学校学生如此严格呢？ 像往常一样，答案是保持types检查和types推断可行。 猜测types的types推断是正确的。 types检查似乎可能是可能的 ，但它是血腥的复杂，没有人想保持这一点。
另一方面，有人可能会反对GHC对某些似乎需要不可预知性的types感到满意：
> :set -Rank2Types > :t id :: (forall b. b) -> (forall b. b) {- no complaint, but very chatty -}
事实certificate，一些稍有限制的impredicativity版本并不算太糟糕：具体来说，types检查高级types（允许typesvariables被多态typesreplace时，它们只是(->)参数）相对简单。 你在2级以上的时候input推断types，1级以上的主要types，但是有时候更高的sortingtypes正是医生所订购的。
虽然不知道这个词的词源。
*您可能想知道您是否可以这样做：
data FooTy a where FooTm :: FooTy (forall a. a)
那么你会得到一个FooTm （ FooTm ），它的types有一些多态的东西作为(->) （即FooTy ）之外的其他东西的参数，你不必穿过学校做这件事，所以“应用非(->)东西多态types是没有用的，因为你不能让他们“将被无效。 GHC不会让你写FooTy ，我承认我不确定是否有限制的原则。
我想就词源问题发表评论，因为@ sclv的答案不是很正确（词源，而不是概念上）。
回到时代，到罗素时代，一切都是理论 – 包括逻辑。 特别重要的逻辑概念之一是“理解原则”; 也就是给定一个逻辑谓词φ:A→2我们希望有一些原则来确定满足该谓词的所有元素的集合，记为“ {x | φ(x) } ”或者其上的一些变化。 要牢记的是，“集合”和“谓词”被看作是根本不同的东西：谓词是从物体到真值的映射，集合是物体。 因此，例如，我们可以允许对多个集合进行量化，而不是对谓词进行量化。
现在，罗素很担心他的同名矛盾，并想方设法摆脱它。 有许多修复，但这里的利益是限制理解的原则。 但首先，原理的正式定义： ∃S.∀xS x ↔︎ φ(x) ; 也就是说，对于我们特定的φ ，存在一个对象（即集合） S ，使得对于每个对象（也是一个集合，但被认为是一个元素） x ，我们有这个S x （你可以把它看作是“ x∈S “，尽pipe当时的逻辑学家给出了” ∈ “一个不同于并置的含义），在φ(x)为真的情况下是正确的。 如果我们完全按照这个原则来采取这个原则，那么我们最终就会产生一个暗含的理论。 但是，我们可以限制我们允许理解哪个φ 。 （例如，如果我们说φ不能包含任何二阶量词）。因此，对于任何限制R ，如果集合S由某个R预测确定（即通过理解产生），那么我们说S是“ R预测”。 如果我们的语言中的每一组都是R -predicative，那么我们说我们的语言是“ R -predicative”。 然后，正如经常使用带连字符的前缀的情况一样，前缀会被丢弃并留下隐含的，因此“谓语”语言。 而且，自然地，不具有预测性的语言是“不确定的”。
这是旧的词源。 从那时起，这些条件已经消失，并得到了自己的生命。 今天我们使用“预测性”和“暗示性”的方式是完全不同的，因为我们所关心的事情已经改变了。 所以有时可能有点难以看出我们的现代用法与这个东西有什么联系。 老实说，我不认为这个词源学在确定这些词的真正含义方面真的有帮助（这几天）。
