[多态性等级与（im）谓语之间的关系是什么？
等级1多态性可以是谓语性还是强制性？
具有k > 1的秩-k多态性可以是谓词性还是强制性的吗？
我的困惑来自：
为什么https://en.wikipedia.org/wiki/Parametric_polymorphism在等级1多态性下提到谓语？ （在我看来，等级1意味着谓语）
Rank-1（prenex）多态性
在prenex多态系统中，类型变量不能用多态类型实例化。[4]这与所谓的“ ML样式”或““让多态性”（从技术上讲，ML的让多态性还有其他一些语法限制）。此限制使区别在多态和非多态类型之间非常重要；因此在谓词系统多态类型有时也称为类型模式，以区别于普通（单态）类型，有时称为单型。结果是全部类型可以以将所有量词放在最外侧（前束）位置。例如，考虑附加上述功能，其类型为
forall a. [a] × [a] -> [a]为了将此功能应用于一对列表，类型必须为替换函数类型中的变量
a，使得参数的类型与结果函数类型匹配。在强制性系统中，被替换的类型可以是任何类型包括本身是多态的类型；因此追加可以应用于具有任何类型元素的列表对，甚至可以多态函数列表，例如追加自身。中的多态性语言ML是谓语。[[citation needed]]这是因为谓词加上其他限制，使类型系统非常简单，因此完全有可能进行类型推断。
作为一个实际例子，OCaml（ML的后代或方言）执行类型推断并支持强制性多态性，但在某些情况下使用强制性多态的情况下，系统的类型除非某些显式类型批注是由程序员提供。
...
谓语多态性
在谓词参数多态系统中，类型
τ包含类型变量α不能以α为实例化为多态类型。谓词类型理论包括Martin-Löf类型理论和NuPRL。
https://wiki.haskell.org/Impredicative_types：
表示类型是多态的高级形式，与排名为N的类型形成对比。
标准Haskell通过使用type允许多态类型变量，可以理解为普遍量化：
id :: a -> a的意思是“对于所有类型a，id都可以使用参数并返回该类型的结果”。所有通用量词（“全部”）必须出现在类型的开头。较高级别的多态性（例如N级类型）允许通用量词也出现在函数类型中。原来是出现在功能箭头右侧的按钮并不有趣：
Int -> forall a. a -> [a]实际上与forall a. Int -> a -> [a]相同。但是，较高级别的多态性允许量词位于功能箭头也是如此，
(forall a. [a] -> Int) -> Int确实是与forall a. ([a] -> Int) -> Int不同。暗示性类型将这个想法带入了自然的结论：通用量词允许在类型的任何位置（甚至在内部）常规数据类型，例如列表或
Maybe。
谢谢。
等级1多态性可以是谓语性还是强制性？
不，等级1多态性总是可预测的，因为任何forall量词都不作为类型构造函数的参数出现，也就是说，量词是“ prenex”。
k> 1的秩k多态性可以是谓语的还是命令的？
高级多态性总是强制性的； RankNTypes扩展启用了(->)构造函数的强制多态性[[only，也就是说，给定类型a -> b，可以用包含a的类型实例化b或forall。通常，仅当a包含forall时，才将此类类型称为高等级，因为（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)