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和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 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不能自由选择:它/\没有被@用过了.

一般来说,为了掌握这些超级多态类型,最好写出所有量词,然后弄清楚它是如何变成你对抗魔鬼的游戏.谁选择什么,以什么顺序.移动一个forall参数类型会更改其选择器,并且通常可以区分胜利和失败.