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

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

g OTOH имеет тип ранга 2. Требуется, чтобы его аргумент имел полиморфный тип forall a . a. () такого типа нет, он мономорфен. Но undefined имеет этот тип (фактически только undefined и error и т. Д.), Если мы снова добавим явный 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 :: Double
4 :: Int

но я не могу

GHCi> putStrLn $ h (4 :: Integer)

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

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

f :: a -> Int
f _ = 1

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

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

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

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