13

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 user's guide on kind polymorphism。

4

3 回答 3

12

让我们血腥。我们必须量化一切，并给出量化的领域。值有类型；类型级别的事物有种类；种住在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 参数，但我们必须准备好忍受/\魔鬼可能选择的任何 -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。

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

于 2015-02-27T20:35:50.830 回答
11

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

{-# 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
于 2015-02-27T19:37:49.760 回答
3

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

即：类型 off1要求其定义在 kind 中是多态的k，而类型 off2要求其参数在 kind 中是多态的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 *
于 2015-02-27T21:59:24.690 回答