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

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 для соответствующего приложения. Игра состоит в том, что мы можем выбрать аргументы @, но мы должны быть готовы мириться с любыми /\ аргументами, которые может выбрать дьявол.

Мы

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) 

, но эти уравнения не даже хорошо kinded, потому что k не волен выбирать: это время /\ не -ed @ -ed.

Как правило, чтобы справиться с этими uber-полиморфными типами, хорошо написать все кванторы, а затем выяснить, как это превращается в вашу игру против дьявола. Кто выбирает то, что и в каком порядке. Перемещение 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 *