RankNTypes 和 PolyKinds

Question

f1和f2有什么区别？

$ ghci -XRankNTypes -XPolyKinds
Prelude> let f1 = undefined :: (forall a        m. m a -> Int) -> Int
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int
Prelude> :t f1
f1 :: (forall            (a :: k) (m :: k -> *). m a -> Int) -> Int
Prelude> :t f2
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) -> Int

与 RankNTypes and scope of forall. Example taken from the GHC user's guide on kind polymorphism 上的这个问题相关。

Answer 1

f2 要求它的参数是 k 类型的多态，而 f1 只是类型本身的多态。所以如果你定义

{-# LANGUAGE RankNTypes, PolyKinds #-}
f1 = undefined :: (forall a m. m a -> Int) -> Int
f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int
x = undefined :: forall (a :: *) m. m a -> Int

然后 :t f1 x 输入正常，而 :t f2 x 抱怨：

*Main> :t f2 x

<interactive>:1:4:
    Kind incompatibility when matching types:
      m0 :: * -> *
      m :: k -> *
    Expected type: m a -> Int
      Actual type: m0 a0 -> Int
    In the first argument of ‘f2’, namely ‘x’
    In the expression: f2 x

Answer 2

让我们热血沸腾。我们要把一切都量化，给量化的域。值有类型；类型级别的事物有种类；种生活在 BOX.

f1 :: forall (k :: BOX).
      (forall (a :: k) (m :: k -> *). m a -> Int)
      -> Int

f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int)
      -> Int

现在，在两个示例类型中都没有明确量化 k，因此 ghc 根据是否提及 k 以及在何处提及 k 来决定将 forall (k :: BOX) 放在哪里。我不确定我是否理解或愿意捍卫所述政策。

Ørjan 给出了实践中差异的一个很好的例子。让我们也为此而血腥。我会写/\ (a :: k). t来明确对应于forall的抽象，而f @ type则是对应的应用。游戏是我们可以选择 @-ed 论点，但我们必须准备好忍受魔鬼可能选择的任何 /\-ed 论点。

我们有

x :: forall (a :: *) (m :: * -> *). m a -> Int

并可能因此发现 f1 x 确实是

f1 @ * (/\ (a :: *) (m :: * -> *). x @ a @ m)

但是，如果我们尝试给予 f2 x 同样的待遇，我们会看到

f2 (/\ (k :: BOX) (a :: k) (m :: k -> *). x @ ?m0 @ ?a0)
?m0 :: *
?a0 :: * -> *
where  m a = m0 a0

Haskell 类型系统将类型应用视为纯粹的句法，因此求解等式的唯一方法是识别函数和识别参数

(?m0 :: * -> *) = (m :: k -> *)
(?a0 :: *)      = (a :: k)

但是这些方程式甚至都不是很好，因为 k 不是可以自由选择的：它是 /\-ed 而不是 @-ed。

一般来说，要掌握这些超级多态类型，最好写出所有量词，然后弄清楚它是如何变成你与魔鬼的游戏的。谁选择什么，以什么顺序。在参数类型中移动 forall 会改变其选择器，并且通常会决定胜负。

Answer 3

类型f1对其定义有更多限制，而f2类型对其参数有更多限制.

即：f1类型要求其定义在k类型中是多态的，而f2类型要求其参数是 k.

类型的多态

f1 :: forall (k::BOX). (forall          (a::k) (m::k->*). m a -> Int) -> Int
f2 ::                  (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int

-- Show restriction on *definition*
f1 g = g (Just True)  -- NOT OK. f1 must work for all k, but this assumes k is *
f2 g = g (Just True)  -- OK

-- Show restriction on *argument* (thanks to Ørjan)
x = undefined :: forall (a::*) (m::*->*). m a -> Int
f1 x  -- OK
f2 x  -- NOT OK. the argument for f2 must work for all k, but x only works for *

RankNTypes 和 PolyKinds

RankNTypes and PolyKinds

polymorphism

haskell

higher-rank-types

polykinds