haskell - 什么是预测性？

Question

我对 Haskell 禁止为“不可预测”的类型有相当不错的直觉:即 forall 的类型。出现在类型构造函数的参数中，而不是 -> .但什么是预测性？什么使它重要？它与“谓词”一词有何关系？

Answer 1

让我就“词源”问题补充一点，因为@DanielWagner 的另一个答案涵盖了大部分技术基础。

诸如 a 之类的谓词是 a -> Bool .现在，谓词逻辑可以在某种意义上对谓词进行推理——所以如果我们有一些谓词 P我们可以谈论，对于给定的 a , P(a) ，现在在“谓词逻辑”(例如一阶逻辑)中我们也可以说 ∀a. P(a) .因此，我们可以量化变量并讨论谓词对此类事物的行为。

现在，反过来，如果一个谓词所应用的所有事物都在它之前被引入，我们就说一个陈述是谓语的。所以陈述是“基于”已经存在的事物。反过来，如果一个语句在某种意义上可以通过它的“ bootstrap ”来引用它自己，那么它就是不可预测的。

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

因此，不可预测性引入了某种“自引用”的可能性。但是等等，你可能会说，这样的事情不会导致矛盾吗？答案是:“嗯，有时。”特别是，作为多态 lambda 演算和 GHC“核心”语言的基本“核心”的“系统 F”允许一种形式的不可预测性，尽管如此，它仍然具有两个级别——值级别和类型级别，允许对自身进行量化。在这个两级分层中，我们可以有不可预测性，而不是矛盾/悖论。

尽管请注意，这个巧妙的技巧非常精致，并且通过添加更多功能很容易搞砸，正如 Oleg 的这篇文章集所示:http://okmij.org/ftp/Haskell/impredicativity-bites.html