什么是困境？

Question

我对Haskell禁止作为"impredicative"的类型有相当不同的直觉:即forall出现在除了类型构造函数的参数中的类型->.但究竟什么是困境？是什么让它变得重要？它与"谓词"这个词有什么关系？

Answer 1

这些类型系统的核心问题是:"你能用多态类型代替类型变量吗？".预测型系统是严肃的校园回答,"绝对不是",而不可思议的类型系统是你无忧无虑的伙伴谁认为这听起来像一个有趣的想法,可能会出错？

现在,Haskell讨论了一点,因为它认为多态性应该是有用但不可见的.因此,对于本文的其余部分,我将使用Haskell的方言进行编写,其中forall不仅允许使用而且需要使用.通过这种方式,我们可以区分类型a,它是从我们稍后可以定义的类型环境中获取其值的单态类型,以及类型forall a. a,它是更难以存储的多态类型之一.我们也允许forall在类型中的任何地方 - 我们将看到,GHC将其类型语法限制为"快速失败"机制而不是技术要求.

假设我们告诉了编译器id :: forall a. a -> a.我们以后可以要求使用id它好像有类型(forall b. b) -> (forall b. b)吗？Impredicative型系统都还好这一点,因为我们可以实例的量词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],预测的学校风格不是那么多.事实上,你可以从列表中唯一的两个构造看到的,是没有办法产生含有多态值列表,而在它们的构造类型变量实例化多态值.因此,尽管类型[forall b. b]被允许在我们的Haskell的话,它是不是真的明智的-有这种类型的无(终止)条款.如果你甚至考虑这种类型,这就会激发GHC的抱怨决定 - 这是编译器告诉你"不要打扰"的方式.*

是什么让校园如此严格？像往常一样,答案是关于保持类型检查和类型推断可行.对于impredicative类型的类型推断是正确的.类型检查似乎可能是可能的,但它很复杂,没有人愿意维护它.

另一方面,有些人可能反对GHC对某些看起来需要不可靠性的类型非常满意:

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

事实证明,一些稍微受限制的impredicativity版本并不是太糟糕:具体来说,类型检查更高级别的类型(当它们只是参数时允许类型变量被多态类型替换(->))相对简单.你确实失去了排名第2级以上的类型推断,以及排名第1级以上的主要类型,但有时更高级别的类型正是医生所要求的.

不过关于这个词的词源的Dunno!

*您可能想知道您是否可以这样做:

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

那么你会得到一个term(FooTm),其类型具有多态性作为参数,而不是(->)(即FooTy),你不必越过schoolmarm去做,所以相信"将非(->)东西应用于多态类型是没用的,因为你不能使它们"会失效.GHC不允许你写FooTy,我承认我不确定是否存在限制的原则性原因.

(快速更新一些年后:有是一个很好的,有原则的原因,FooTm仍然是不行的就是,任何GADTs在GHC实现的方式是通过式平等,所以扩大的类型.FooTm实际上是FooTm :: forall a. (a ~ forall b. b) => FooTy a因此实际使用.FooTm,一会确实需要实例化一个具有多态类型的类型变量.感谢Stephanie Weirich向我指出这一点.)

Answer 2

让我加上关于"词源"问题的一点,因为@DanielWagner的另一个答案涵盖了很多技术领域.

对类似的谓词a是a -> Bool.现在谓词逻辑是一种可以在某种意义上原因有关谓词-所以,如果我们有一些谓词P,我们可以谈论,对于一个给定的a,P(a)现在在"谓词逻辑"(比如一阶逻辑),我们可以也说?a. P(a).因此,我们可以量化变量并讨论谓词对这些事物的行为.

现在,反过来,我们说如果谓词所应用的所有内容都是在它之前引入的,那么语句是可预测的.因此,陈述是"基于"已经存在的事物.反过来,如果某种说法在某种意义上可以通过其"引导"来引用自己,那么它就是不可预测的.

因此,在如的情况下id上面的例子中,我们发现,我们可以给一个类型,id例如,它需要的东西类型的id,以其他的东西类型的id.所以现在我们可以给一个函数一个类型,其中量化变量(由...引入forall a.)可以"扩展"为与整个函数本身相同的类型!

因此,不确定性引入了某种"自我参照"的可能性.但是,等等,你可能会说,这样的事情不会导致矛盾吗？答案是:"好吧,有时候." 特别是,作为多态性lambda演算的"系统F"和GHC"核心"语言的基本"核心"允许一种不可信的形式,但仍然有两个层次 - 价值水平和类型水平,这是允许的量化自己.在这种两级分层中,我们可以产生不可预测性,而不是矛盾/矛盾.

虽然注意到这个巧妙的技巧非常精致,并且通过添加更多功能而容易搞砸,因为Oleg的这篇文章集合指出:http://okmij.org/ftp/Haskell/impredicativity-bites.html

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".然后,正如连字符前缀的情况一样,前缀被删除并且隐含了"谓词"语言.而且,自然而言,不具有预测性的语言是"不可预测的".

那是旧学派的词源.从那些日子开始,这些条款已经过去了,并获得了自己的生命.我们今天使用"预测性"和"不可预测性"的方式是完全不同的,因为我们关注的事情已经发生了变化.因此,有时候我们的现代用法与这些东西的关系有点难以理解.老实说,我不认为知道词源确实有助于弄清楚这些词的真正含义(如今).