haskell - 多态性的等级和(非)预测性之间有什么关系？

Question

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

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

可以用 k > 1 对 k 多态性进行排序是谓语还是非谓语？

我的困惑来自:

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

Rank-1 (prenex) polymorphism

In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] This is very similar to what is called "ML-style" or "Let-polymorphism" (technically ML's Let-polymorphism has a few other syntactic restrictions). This restriction makes the distinction between polymorphic and non-polymorphic types very important; thus in predicative systems polymorphic types are sometimes referred to as type schemas to distinguish them from ordinary (monomorphic) types, which are sometimes called monotypes. A consequence is that all types can be written in a form that places all quantifiers at the outermost (prenex) position. For example, consider the append function described above, which has type

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

In order to apply this function to a pair of lists, a type must be substituted for the variable a in the type of the function such that the type of the arguments matches up with the resulting function type.

In an impredicative system, the type being substituted may be any type whatsoever, including a type that is itself polymorphic; thus append can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as append itself. Polymorphism in the language ML is predicative.^{[citation needed]} This is because predicativity, together with other restrictions, makes the type system simple enough that full type inference is always possible.

As a practical example, OCaml (a descendant or dialect of ML) performs type inference and supports impredicative polymorphism, but in some cases when impredicative polymorphism is used, the system's type inference is incomplete unless some explicit type annotations are provided by the programmer.

...

Predicative polymorphism

In a predicative parametric polymorphic system, a type τ containing a type variable α may not be used in such a way that α is instantiated to a polymorphic type. Predicative type theories include Martin-Löf Type Theory and NuPRL.

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

Impredicative types are an advanced form of polymorphism, to be contrasted with rank-N types.

Standard Haskell allows polymorphic types via the use of type variables, which are understood to be universally quantified: id :: a -> a means "for all types a, id can take an argument and return a result of that type". All universal quantifiers ("for all"s) must appear at the beginning of a type.

Higher-rank polymorphism (e.g. rank-N types) allows universal quantifiers to appear inside function types as well. It turns out that appearing to the right of function arrows is not interesting: Int -> forall a. a -> [a] is actually the same as forall a. Int -> a -> [a].

However, higher-rank polymorphism allows quantifiers to the left of function arrows, too, and (forall a. [a] -> Int) -> Int really is different from forall a. ([a] -> Int) -> Int.

Impredicative types take this idea to its natural conclusion: universal quantifiers are allowed anywhere in a type, even inside normal datatypes like lists or Maybe.

谢谢。

Answer 1

Can rank-1 polymorphism be either predicative or impredicative?

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

Can rank-k polymorphism with k > 1 be either predicative or impredicative?

高阶多态性总是不可预测的； RankNTypes扩展只为 (->) 启用不可预测的多态性构造函数，即给定类型 a -> b , a或 b可以使用包含 forall 的类型实例化s。我们通常仅在 a 时才将此类类型称为更高等级包含 forall s，因为(除了 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)