haskell - 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 上的这个问题相关.示例取自 GHC 用户指南 kind polymorphism .

Answer 1

让我们血腥。我们必须量化一切，并给出量化的领域。值有类型；类型级别的事物有种类；种生活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 决定在哪里放置 forall (k :: BOX) , 基于是否和在哪里 k提到。我不完全确定我理解或愿意为所述政策辩护。

Ørjan 给出了一个很好的例子来说明实践中的差异。让我们也为此感到血腥。我会写 /\ (a :: k). t明确对应于 forall 的抽象, 和 f @ type为相应的应用程序。游戏是我们要选择 @ -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。

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