RankNTypes и PolyKinds

В чем разница между 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 и области применения. Пример взят из руководства пользователя GHC по доброму полиморфизму.

Источник

3 ответа

Решение

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
Источник

Будем кровавыми. Мы должны все количественно определить и дать область количественного определения. Значения имеют типы; вещи на уровне типов имеют виды; виды живут в 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 упомянуто. Я не совсем уверен, что понимаю или готов защищать изложенную политику.

Орьян приводит хороший пример разницы в практике. Давай будем кровавыми об этом тоже. Я напишу /\ (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.

Как правило, чтобы разобраться с этими сверхполиморфными типами, хорошо выписать все квантификаторы, а затем выяснить, как это превратится в вашу игру против дьявола. Кто что выбирает и в каком порядке. Перемещение forall внутри аргумента тип меняет своего выбора, и часто может иметь значение между победой и поражением.

Источник

Тип 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 *
Источник
Другие вопросы по тегам