Особые случаи при обработке типов более высокого ранга в GHC?

Рассмотрим этот пример из сеанса GHCI:

Prelude> :set -XRankNTypes
Prelude> let bar :: (forall a.[a]->[a]) -> [Int]; bar f = f [1,2,3]

Это определяет функцию bar с типом ранга 2. Следовательно, вывод типа не должен быть в состоянии вывести правильный тип для:

Prelude> let foo f = bar f

И действительно,

<interactive>:7:17:
Couldn't match type `t' with `[a] -> [a]'
  `t' is a rigid type variable bound by
      the inferred type of foo :: t -> [Int] at <interactive>:7:5
In the first argument of `bar', namely `f'
In the expression: bar f
In an equation for `foo': foo f = bar f

Удивительно, но если мы напишем то же самое в свободном стиле, это сработает:

Prelude> let baz = bar
Prelude> :t baz
baz :: (forall a. [a] -> [a]) -> [Int]

Как получается, что вывод типа может вывести здесь тип более высокого ранга? Может ли кто-нибудь подтвердить, что это специально лечится в GHC, или указать, где я ошибаюсь.


functional-programming type-inference haskell higher-rank-types pointfree
person Ingo    schedule 24.07.2013    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Основной проблемой вывода типов при наличии типов более высокого ранга является вывод полиморфных типов для переменных с лямбда-связью. В вашем первом примере единственный правильный способ ввести foo — это присвоить полиморфный тип f. В вашем втором примере ничего подобного не требуется. Вместо этого baz — это просто (тривиальное) частичное применение bar. Простое применение полиморфной функции более высокого ранга без каких-либо лямбда-абстракций всегда должно быть возможно без дополнительных аннотаций типов.

См. также соответствующий раздел в Руководство пользователя GHC, а также различные исследовательские работы.

person kosmikus    schedule 24.07.2013
comment
Действительно, похоже, что программа проверки типов довольна, пока ей не нужно делать вывод о типе связанной лямбда-переменной, которая передается вместо аргумента с более высоким рейтингом. - person Ingo; 25.07.2013