多态性的等级和（非）预测性之间有什么关系？

Question

多态性的等级和（非）预测性之间有什么关系？

1 级多态性可以是谓词还是非谓词？

rank-k 多态性k > 1可以是谓语还是非谓语？

我的困惑来自：

为什么https://en.wikipedia.org/wiki/Parametric_polymorphism提到等级 1 多态性下的预测性？（在我看来，rank-1 意味着可预测性）

Rank-1 (prenex) 多态性

在 prenex 多态系统中，类型变量可能无法用多态类型实例化。 [4] 这与所谓的“ML 风格”或“ Let-多态性”非常相似（从技术上讲，ML 的 Let-多态性还有一些其他语法限制）。这种限制使得多态和非多态类型之间的区别变得非常重要；因此，在谓词系统中，多态类型有时被称为类型模式，以区别于普通（单态）类型，后者有时被称为单类型。结果是所有类型都可以写成将所有量词放在最外面（前缀）位置的形式。例如，考虑上面描述的 append 函数，它具有类型

forall a. [a] × [a] -> [a]

为了将此函数应用于一对列表，必须用类型替换a函数类型中的变量，以便参数的类型与结果函数类型相匹配。

在非谓语系统中，被替换的类型可以是任何类型，包括本身是多态的类型；因此 append 可以应用于具有任何类型元素的列表对——甚至可以应用于多态函数列表，例如 append 本身。ML 语言中的多态性是预测性的。^{[需要引用]}这是因为预测性以及其他限制使类型系统足够简单，因此始终可以进行完整的类型推断。

作为一个实际示例，OCaml（ML 的后代或方言）执行类型推断并支持不可预测的多态性，但在某些情况下，当使用不可预测的多态性时，系统的类型推断是不完整的，除非程序员提供了一些显式的类型注释。

...

谓词多态性

在谓词参数多态系统中，不能以实例化为多态类型的方式使用?包含 类型变量的类型??。谓语类型理论包括 Martin-Löf 类型理论和 NuPRL。

https://wiki.haskell.org/Impredicative_types：

谓词类型是多态性的一种高级形式，与 rank-N 类型形成对比。

标准 Haskell 通过使用类型变量允许多态类型，类型变量被理解为普遍量化：id :: a -> a意味着“对于所有类型a，id可以接受一个参数并返回该类型的结果”。所有全称量词（“for all”）必须出现在类型的开头。

高阶多态性（例如，rank-N 类型）也允许通用量词出现在函数类型中。事实证明，出现在函数箭头的右侧并不有趣：Int -> forall a. a -> [a]实际上与forall a. Int -> a -> [a].

然而，高阶多态性也允许量词位于函数箭头的左侧，并且(forall a. [a] -> Int) -> Int确实与forall a. ([a] -> Int) -> Int.

Impredicative 类型将这个想法推向了它的自然结论：在类型中的任何地方都允许使用全称量词，甚至在普通数据类型（如列表或Maybe.

谢谢。

Answer 1

1 级多态性可以是谓词还是非谓词？

不，rank-1 多态性始终是谓词，因为任何forall量词都不会作为类型构造函数的参数出现，也就是说，量词是“prenex”。

k > 1 的 rank-k 多态性可以是谓语还是非谓语？

高阶多态性总是不可预测的；该RankNTypes扩展允许impredicative多态性仅用于(->)构造，即，给定一个类型a -> b，a或b可与含一种类型的被实例化forall秒。我们通常仅在a包含foralls时才将此类类型称为高阶类型，因为（除了TypeApplications）X -> forall t. Y等价于forall t. X -> Y。

ImpredicativeTypes不支持一般的谓词多态性（带有损坏的扩展）。例如，你不能写Maybe (forall a. [a] -> [a]). 这主要是因为很难自动确定何时泛化以及何时实例化该量词。幸运的是，您可以使用newtype包装器来“隐藏”不可预测性，或者更确切地说，让编译器清楚您想对量词做什么，例如：

{-# LANGUAGE RankNTypes #-}

newtype ListTransform = ListTransform { unLT :: forall a. [a] -> [a] }

f :: Maybe ListTransform -> [Int] -> [Char] -> ([Int], [Char])
f Nothing is cs = (is, cs)
f (Just (ListTransform t)) is cs = (t is, t cs)
-- or: f (Just lt) is cs = (unLT lt is, unLT lt cs)