Что я делаю неправильно с этим подразумеваемым тривиальным упражнением по полиморфизму более высокого ранга?
Более года назад я задал вопрос Как использовать прокси-сервер в Haskell, и с тех пор у меня есть небольшое использование расширения RankNTypes GHC. Проблема в том, что каждый раз, когда я пытаюсь работать с ней, я получаю причудливые сообщения об ошибках и взламываю код, пока они не уйдут. Или я сдаюсь.
Очевидно, я действительно не понимаю полиморфизм более высокого ранга в Haskell. Чтобы попытаться это разрешить, я решил перейти к самым простым примерам, которые я мог бы проверить, проверить все мои предположения и посмотреть, могу ли я получить момент Эврика.
Первое предположение - причина, по которой полиморфизм более высокого ранга не является стандартной функцией Haskell 98 (или 2010?), заключается в том, что, если вы принимаете некоторые не-очевидные ограничения, которые многие программисты даже не заметили, это isn Не нужно. Я могу определить полиморфные функции ранга 1 и 2, которые на первый взгляд эквивалентны. Если я загружу их в GHCi и назову их теми же параметрами, они дадут те же результаты.
Итак - простые примерные функции...
{-# LANGUAGE RankNTypes #-}
rank0 :: [Int] -> Bool
rank0 x = null x
rank1a :: [a] -> Bool
rank1a x = null x
rank1b :: forall a. [a] -> Bool
rank1b x = null x
rank2 :: (forall a. [a]) -> Bool
rank2 x = null x
и сеанс GHCi...
GHCi, version 7.4.2: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load example01
[1 of 1] Compiling Main ( example01.hs, interpreted )
Ok, modules loaded: Main.
*Main>
Пока нет ошибок - хорошее начало. Затем проверьте каждую функцию с пустым параметром списка...
*Main> rank0 []
True
*Main> rank1a []
True
*Main> rank1b []
True
*Main> rank2 []
True
*Main>
Честно говоря, я немного удивился тем, что в этом случае работали функции rank1a и rank1b. Список не знает, какие элементы типа он содержит, функции тоже не знают, но наверняка тип должен быть решен, чтобы сделать этот вызов? Я ожидал, что вам нужно предоставить явную подпись.
Это не проблема ATM, и результаты кажутся многообещающими. Следующий, непустые списки...
*Main> rank0 [1,2,3]
False
*Main> rank1a [1,2,3]
False
*Main> rank1b [1,2,3]
False
*Main> rank2 [1,2,3]
<interactive>:10:8:
No instance for (Num a)
arising from the literal `1'
In the expression: 1
In the first argument of `rank2', namely `[1, 2, 3]'
In the expression: rank2 [1, 2, 3]
*Main>
О, дорогая, похоже, что версия ранга 2 не нравится, когда параметр знает немного больше об этом типе. Тем не менее, возможно, проблема в том, что литералы 1 и т.д. Являются полиморфными...
*Main> rank2 ([1,2,3] :: [Int])
<interactive>:11:8:
Couldn't match type `a' with `Int'
`a' is a rigid type variable bound by
a type expected by the context: [a] at <interactive>:11:1
Expected type: [a]
Actual type: [Int]
In the first argument of `rank2', namely `([1, 2, 3] :: [Int])'
In the expression: rank2 ([1, 2, 3] :: [Int])
*Main>
Ошибка отличается, но она по-прежнему не работает, и я до сих пор не понимаю эти сообщения об ошибках.
Беседу с различными теориями, одна идея у меня была, что, может быть, мне нужно сказать GHC, чтобы "забыть" некоторый статический тип списка. По этой теории я пробовал разные вещи, в том числе...
*Main> [1,2,3] :: [a]
<interactive>:12:2:
No instance for (Num a1)
arising from the literal `1'
In the expression: 1
In the expression: [1, 2, 3] :: [a]
In an equation for `it': it = [1, 2, 3] :: [a]
*Main>
ОК, GHCi не знает, о чем я говорю. В случае, если GHCi просто нужно было точно знать, какой тип забыть, я также пробовал...
*Main> ([1,2,3] :: [Int]) :: [a]
<interactive>:15:2:
Couldn't match type `a1' with `Int'
`a1' is a rigid type variable bound by
an expression type signature: [a1] at <interactive>:15:1
Expected type: [a]
Actual type: [Int]
In the expression: ([1, 2, 3] :: [Int]) :: [a]
In an equation for `it': it = ([1, 2, 3] :: [Int]) :: [a]
*Main>
Так много для моих надежд получить сообщение об ошибке, что GHCi не знает, как show значение с забытым типом. Я не знаю, как создать список со "забытым" статическим типом, и я даже не уверен, что это имеет смысл.
В этот момент я не пытаюсь ничего использовать с полиморфизмом более высокого ранга. Суть здесь состоит в том, чтобы просто вызвать функцию rank2 с непустым списком и понять, почему она не работает точно так же, как и другие функции. Я хочу продолжить это, шаг за шагом, но сейчас я просто полностью застрял.
Ответы
Ответ 1
Подумайте, что означает тип rank2.
rank2 :: (forall a. [a]) -> Bool
rank2 x = null x
Первый аргумент rank2 должен быть чем-то типа forall a. [a]. forall, являющийся внешним, означает, что тот, кто получает такое значение, может выбрать свой выбор a. Подумайте об этом, как о принятии типа в качестве дополнительного аргумента.
Итак, чтобы дать что-то как аргумент rank2, он должен быть списком, чьи элементы могут быть любого типа, который может потребоваться для внутренней реализации rank2. Поскольку нет способа вызвать значения такого произвольного типа, единственными возможными входами являются [] или списки, содержащие undefined.
Контрастируйте это с помощью rank1b:
rank1b :: forall a. [a] -> Bool
rank1b x = null x
Здесь forall уже является внешним, поэтому любой, кто использует rank1b, сам выбирает тип.
Вариант, который будет работать, будет примерно таким:
rank2b :: (forall a. Num a => [a]) -> Bool
rank2b x = null x
Теперь вы можете передать ему список числовых литералов, которые являются полиморфными во всех экземплярах Num. Другой альтернативой было бы что-то вроде этого:
rank2c :: (forall a. [a -> a]) -> Bool
rank2c x = null x
Это работает, потому что вы действительно можете вызвать значения типа forall a. a -> a, в частности функцию id.
Ответ 2
Давайте сравним эти явные подписи типа forall:
rank1b :: forall a. [a] -> Bool
rank1b x = null x
Это означает forall a.([a]->Bool), поэтому работает, как вы ожидаете, во всех списках, независимо от типа, и возвращает Bool.
rank2 может принимать только полиморфные списки:
rank2 :: (forall a. [a]) -> Bool
rank2 x = null x
Теперь это другое - это означает, что аргумент x должен быть полиморфным. [] является полиморфным, поскольку он может быть любого типа:
>:t []
[] :: [a]
который тайно означает forall a.[a], но rank2 не примет ['2'], поскольку имеет тип [Char].
rank2 будет принимать только списки, которые действительно относятся к типу forall a.[a].
Ответ 3
В этот момент я не пытаюсь делать ничего полезного с более высоким рангом полиморфизм. Дело здесь просто в том, чтобы иметь возможность назвать rank2 функции с непустым списком и понять, почему он не работает точно так же, как и другие функции. Я хочу продолжить вычисление это шаг за шагом сам, но сейчас я просто полностью застрял.
Я не уверен, что более высокий уровень полиморфизма - это то, что вы думаете.
Я думаю, что концепция имеет смысл только в отношении типов функций.
Например:
reverse :: forall a. [a] -> [a]
tail :: forall a. [a] -> [a]
сообщает нам, что reverse и tail работают независимо от типа элемента списка.
Теперь, учитывая эту функцию:
foo f = (f [1,2], f [True, False])
Каков тип foo?
Стандартный вывод HM не может найти тип. В частности, он не может вывести тип f. Мы должны помочь здесь проверить тип и обещать, что мы передаем только функции, которые не заботятся о типе элементов списка:
foo :: (forall a. [a] -> [a]) -> ([Int], [Bool])
Теперь мы можем
foo reverse
foo tail
и, следовательно, иметь полезный тип ранга-2.
Обратите внимание, что подпись типа запрещает передавать что-то вроде:
foo (map (1+))
потому что переданная функция не полностью независима от типа элемента: для нее требуются элементы Num.
