RankNTypes и область действия `forall '

В чем разница между ними?

{-# LANGUAGE RankNTypes #-}

f :: forall a. a -> Int
f _ = 1

g :: (forall a. a) -> Int
g _ = 1

В частности, почему я получаю сообщение об ошибке с g ()?

ghci> f ()
1
ghci> g ()
<interactive>:133:3:
    Couldn't match expected type `a' with actual type `()'
      `a' is a rigid type variable bound by
          a type expected by the context: a at <interactive>:133:1
    In the first argument of `g', namely `()'
    In the expression: g ()
    In an equation for `it': it = g ()

ghci> f undefined
1
ghci> g undefined
1

Ответ 1

f является просто обычной полиморфной функцией Haskell98, за исключением того, что forall выписывается явно. Таким образом, все переменные типа в сигнатуре являются параметрами, которые вызывающий получает для выбора (без каких-либо ограничений); в вашем случае он разрешил a ~ ().

g OTOH имеет тип ранга-2. Это требует, чтобы его аргумент имел полиморфный тип forall a . a. () не имеет такого типа, он мономорфен. Но undefined имеет этот тип (фактически, только undefined, и т.д.), Если мы снова добавим явный forall.

Возможно, он становится понятнее с менее тривиальной функцией Rank2:

h :: (forall a . (Show a, Num a) => a) -> String
h a = show a1 ++ " :: Double\n"
     ++ show a2 ++ " :: Int"
 where a1 :: Double; a2 :: Int
       a1 = a; a2 = a

GHCi > putStrLn $h 4
4.0:: Двойной
4:: Int

но я не могу сделать

GHCi > putStrLn $h (4:: Integer)

< интерактивная > : 4: 15:
Не удалось вывести (целое число)
из контекста (Показать a, Num a)
связанный типом, ожидаемым контекстом: (Показать a, Num a) = > a
at <interactive> : 4: 12-27
`a '- это жесткая переменная типа, связанная с тип, ожидаемый контекстом: (Показать a, Num a) = > a
at <interactive> : 4: 12
В первом аргументе `h ', а именно` (4:: Integer)'
Во втором аргументе `($) ', а именно` h (4:: Integer)'
В выражении: putStrLn $h (4:: Integer)

Ответ 2

Вспомните forall как функцию анонимного типа. Все типы данных в Haskell, которые имеют переменные типа в своей сигнатуре типа, неявно имеют forall. Например, рассмотрим:

f :: a -> Int
f _ = 1

Вышеупомянутая функция f принимает аргумент любого типа и возвращает Int. Откуда берется a? Он исходит из квантора forall. Следовательно, это эквивалентно:

f :: (forall a . a -> Int)
f _ = 1

Quatifier forall может использоваться для любого типа данных, а не только для функций. Например, рассмотрим типы следующих значений:

() :: ()
10 :: Int
pi :: Floating a => a

Здесь () и 10 являются мономорфными (т.е. они могут быть только одного конкретного типа). С другой стороны, pi является полиморфным с ограничением типа typeclass (то есть он может быть любого типа, если этот тип является экземпляром Floating). Выбранный тип pi явно выражается следующим образом:

pi :: (forall a . Floating a => a)

И снова квантор forall действует как функция типа. Он предоставляет вам переменную типа a. Теперь рассмотрим тип функции g:

g :: (forall a . a) -> Int
g _ = 1

Здесь g ожидает аргумент типа forall a . a и возвращает Int. По этой причине g () не работает: () имеет тип (), а не тип forall a . a. Фактически единственным значением типа forall a . a является undefined:

undefined :: a

Спрятать явно с помощью forall:

undefined :: (forall a . a)

Если вы заметили, что я всегда ставил круглые скобки вокруг квантов forall. Причина, по которой я это сделал, - показать вам, что, когда вы используете количественную оценку forall для функции, квантификация распространяется по всему пути вправо. Это похоже на лямбда: если вы не ставите круглые скобки вокруг лямбды, Haskell будет расширять лямбда-функцию до упора вправо. Следовательно, тип f равен (forall a . a -> Int), а не (forall a . a) -> Int.

Помните, что в первом случае Haskell ожидает, что тип аргумента будет a (т.е. что угодно). Однако во втором случае Haskell ожидает, что тип аргумента будет (forall a . a) (т.е. undefined). Конечно, если вы попытаетесь оценить undefined, ваша программа немедленно остановится с ошибкой. К счастью, вы не пытаетесь его оценить.