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 .
最佳答案
让我们血腥。我们必须量化一切,并给出量化的领域。值有类型;类型级别的事物有种类;种生活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
在参数类型内部会更改其选择器,并且通常可以决定胜负。
关于haskell - RankNTypes 和 PolyKinds,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/28772695/