RankNTypes и сфера действия `forall'

Question

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

{-# 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

Answer 1

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

g OTOH имеет тип ранга 2. Это требует, чтобы его аргумент имел полиморфный тип forall a . a, () не имеет такого типа, он мономорфен. Но 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:: Целое число)

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

Answer 2

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

f :: a -> Int
f _ = 1

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

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

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

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

Вот () а также 10 являются мономорфными (то есть они могут быть только одного конкретного типа). С другой стороны pi является полиморфным с ограничением класса типов (т. е. он может быть любого типа, если этот тип является экземпляром 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 тогда ваша программа немедленно остановится с ошибкой. К счастью, вы не пытаетесь это оценить.