RankNTypes and 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 和 forall 的范围。示例取自 GHC 用户指南中关于种类多态性。

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以及在哪里提及来决定将该forall (k :: BOX)放在哪里。我不完全确定我理解或是否愿意捍卫所述政策。

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

我们有

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 *