什么是困境？ [英] What is predicativity?

问题描述

我对Haskell禁止的impredicative类型有一个相当直观的直觉：也就是 forall 出现在除 - > 。但是什么是困境？什么使它很重要？它与predicate这个词有什么关系？

解决方案

让我仅仅添加关于词源问题的一点， @DanielWagner的其他答案涵盖了很多技术理由。

类似于 a 的谓词是 a - >布尔。现在谓词逻辑就是某种意义上的谓词，所以如果我们有一些谓词 P ，那么我们可以说，对于给定的 a ， P（a），现在在谓词逻辑（比如一阶逻辑）中，我们也可以说∀a。 P（A）。所以我们可以对变量进行量化并讨论谓词在这些事物上的行为。现在，反过来，我们说一个陈述是预测性的，如果所有的谓词都是适用于之前的介绍。因此，陈述是已经存在的东西。反过来说，如果某种说法在某种程度上可以用bootstraps来表示它本身，那么这种说法是不确定的。因此，在例如在上面的 id 例子中，我们发现我们可以给 id> 一个类型， >将 id 类型键入到 id 的类型的其他内容中。因此，现在我们可以给一个函数一个类型，其中一个量化变量（由引发的一个）可以扩展为与整个函数本身相同的类型！

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

尽管注意到这个巧妙的诀窍是非常由于添加了更多功能而变得细腻且容易混淆，因为Oleg的这篇文章集合指出： http://okmij.org/ftp/Haskell/impredicativity-bites.html

I have pretty decent intuition about types Haskell prohibits as "impredicative": namely ones where a forall appears in an argument to a type constructor other than ->. But just what is predicativity? What makes it important? How does it relate to the word "predicate"?

解决方案

Let me just add a point regarding the "etymology" issue, since the other answer by @DanielWagner covers much of the technical ground.

A predicate on something like a is a -> Bool. Now a predicate logic is one that can in some sense reason about predicates -- so if we have some predicate P and we can talk about, for a given a, P(a), now in a "predicate logic" (such as first-order logic) we can also say ∀a. P(a). So we can quantify over variables and discuss the behavior of predicates over such things.

Now, in turn, we say a statement is predicative if all of the things a predicate is applied to are introduced prior to it. So statements are "predicated on" things that already exist. In turn, a statement is impredicative if it can in some sense refer to itself by its "bootstraps".

So in the case of e.g. the id example above, we find that we can give a type to id such that it takes something of the type of id to something else of the type of id. So now we can give a function a type where an quantified variable (introduced by forall a.) can "expand" to be the same type as that of the entire function itself!

Hence impredicativity introduces a possibility of a certain "self reference". But wait, you might say, wouldn't such a thing lead to contradiction? The answer is: "well, sometimes." In particular, "System F" which is the polymorphic lambda calculus and the essential "core" of GHC's "core" language allows a form of impredicativity that nonetheless has two levels -- the value level, and the type level, which is allowed to quantify over itself. In this two-level stratification, we can have impredicativity and not contradiction/paradox.

Although note that this neat trick is very delicate and easy to screw up by the addition of more features, as this collection of articles by Oleg indicates: http://okmij.org/ftp/Haskell/impredicativity-bites.html

这篇关于什么是困境？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！