Каков тип 2, если на дворе полиморфизм высоких порядков
Общеизвестен способ выражения на чистой лямбде чисел Черча:
one = \f x -> f x
two = \f x -> f $ f x
three = \f x -> f $ f $ f x
four = \f x -> f $ f $ f $ f x
...
Для всех из них (кроме, разумеется, one) тайпчекер выводит тип (a->a)->(a->a). Ясно как он это делает. Пусть x::a, тогда
f x => f :: a -> a1
f $ f x => f :: a1 -> a2
f $ f $ f x => f :: a2 -> a3
...
где вывод о типе f берется из самого внешнего применения f и предыдущей строки; a1, a2, a3... вводятся как произвольные (пока) переменные типа. Сравнивая выведенные определения типов для f, получаем
a =a1 a1=a2
a1=a2 a2=a3
...
В результате имеем f :: a -> a, и, следовательно, лямбды типизируются так:
two :: (a -> a) -> a -> a
three :: (a -> a) -> a -> a
four :: (a -> a) -> a -> a
...
Эта типизация по Карри (выводимая, а не декларируемая) осуществляется "типовыводителем" по алгоритму Хиндли-Дамаса-Милнера. Но не является единственно возможной, даже в Хаскелле (не 98, конечно, а GHC-шном). Мы можем, включив поддержку полиморфных типов второго ранга (rank-2 types polymorphism) или более высокого (arbitrary-rank polymorphism), задать для нашей two другие типизации.
Зачем оно нам? Один из ответов таков: это расширяет класс типизируемых термов.
Действительно, рассмотрим, например, канцеллятор
k :: a -> b -> a
k = \x y -> x
известный также под именем const (в Хаскелле). В бестиповой лямбде выражение (two k) вполне осмысленно, фактически можно записать это так
two k x y z = k (k x) y z
При нормальном порядке редукций этот терм возвращает значение x отбрасывая y и z.
Однако в рамках Хиндли-Дамаса-Милнера (то есть стандартного Хаскелла) это не типизируется:
*Polymorph> :t two k
Occurs check: cannot construct the infinite type: a = b -> a
Probable cause: `k' is applied to too few arguments
In the first argument of `two', namely `k'
In the expression: two k
Понятно, в чем дело: тип k::a->(b->a), но two ждет в качестве первого аргумента a->a в соответствии со своим выведенным наиболее общим (principle) типом.
Включим теперь -XRankNTypes и укажем для функции two полиморфный тип второго ранга
two :: (forall t . t -> b -> t) -> a -> b -> b -> a
Обратите внимание на квантор общности внутри скобок, а не на верхнем уровне. Поработаем тайпчекером: проверим, что этот тип действительно подходит для терма
two = \f x -> f (f x)
Видим, что аргументов у лямбды два и для них предложены типы: первый f::(forall t . t -> b -> t), второй x::a. Таким образом, нам нужно проверить, что само тело лямбда-терма, f (f x), в этих предположениях имеет тип b->b->a.
Поехали! Из применения f x получаем отождествление t = a. То есть f в этом вызове имеет тип a->b->a, а (f x)::b->a. Из этого факта, а также применения f (f x) получаем отождествление t = b -> a. Во внешнем вызове f:: (b->a)->b->(b->a), a сам терм f (f x)::b->(b->a). ЧТД.
Проверяем
*Polymorph> :t two k
two k :: a -> b -> b -> a
*Polymorph> two k 42 "Answer" "Ultimate Question"
42
Можно замахнуться на типизацию two $ two k. У меня пока на Хаскелле не очень выходит
-- two $ two k :: ????
-- первое, неидеальное
two' :: (forall a . a -> b -> b -> a)
-> (a -> b -> b -> b -> b -> a)
two' = \f x -> f $ f x
-- тут жульничаем :)
--two' $ two k :: a -> b -> b -> b -> b -> a
-- второе, идеальное
two'' :: (forall a. a -> f a) -> b -> f (f b)
two'' = \f x -> f $ f x
-- к сожалению тайпчекер не справляется с
-- two'' $ two'' k
-- хотя cправляется с two'' k :: b1 -> b -> b -> b1
Хотя как-то должно получиться; общие идеи можно посмотреть
ftp://ftp.mimuw.edu.pl/People/urzy/karpacz-csl04.pdf стр. 26 и далее.
one = \f x -> f x
two = \f x -> f $ f x
three = \f x -> f $ f $ f x
four = \f x -> f $ f $ f $ f x
...
Для всех из них (кроме, разумеется, one) тайпчекер выводит тип (a->a)->(a->a). Ясно как он это делает. Пусть x::a, тогда
f x => f :: a -> a1
f $ f x => f :: a1 -> a2
f $ f $ f x => f :: a2 -> a3
...
где вывод о типе f берется из самого внешнего применения f и предыдущей строки; a1, a2, a3... вводятся как произвольные (пока) переменные типа. Сравнивая выведенные определения типов для f, получаем
a =a1 a1=a2
a1=a2 a2=a3
...
В результате имеем f :: a -> a, и, следовательно, лямбды типизируются так:
two :: (a -> a) -> a -> a
three :: (a -> a) -> a -> a
four :: (a -> a) -> a -> a
...
Эта типизация по Карри (выводимая, а не декларируемая) осуществляется "типовыводителем" по алгоритму Хиндли-Дамаса-Милнера. Но не является единственно возможной, даже в Хаскелле (не 98, конечно, а GHC-шном). Мы можем, включив поддержку полиморфных типов второго ранга (rank-2 types polymorphism) или более высокого (arbitrary-rank polymorphism), задать для нашей two другие типизации.
Зачем оно нам? Один из ответов таков: это расширяет класс типизируемых термов.
Действительно, рассмотрим, например, канцеллятор
k :: a -> b -> a
k = \x y -> x
известный также под именем const (в Хаскелле). В бестиповой лямбде выражение (two k) вполне осмысленно, фактически можно записать это так
two k x y z = k (k x) y z
При нормальном порядке редукций этот терм возвращает значение x отбрасывая y и z.
Однако в рамках Хиндли-Дамаса-Милнера (то есть стандартного Хаскелла) это не типизируется:
*Polymorph> :t two k
Occurs check: cannot construct the infinite type: a = b -> a
Probable cause: `k' is applied to too few arguments
In the first argument of `two', namely `k'
In the expression: two k
Понятно, в чем дело: тип k::a->(b->a), но two ждет в качестве первого аргумента a->a в соответствии со своим выведенным наиболее общим (principle) типом.
Включим теперь -XRankNTypes и укажем для функции two полиморфный тип второго ранга
two :: (forall t . t -> b -> t) -> a -> b -> b -> a
Обратите внимание на квантор общности внутри скобок, а не на верхнем уровне. Поработаем тайпчекером: проверим, что этот тип действительно подходит для терма
two = \f x -> f (f x)
Видим, что аргументов у лямбды два и для них предложены типы: первый f::(forall t . t -> b -> t), второй x::a. Таким образом, нам нужно проверить, что само тело лямбда-терма, f (f x), в этих предположениях имеет тип b->b->a.
Поехали! Из применения f x получаем отождествление t = a. То есть f в этом вызове имеет тип a->b->a, а (f x)::b->a. Из этого факта, а также применения f (f x) получаем отождествление t = b -> a. Во внешнем вызове f:: (b->a)->b->(b->a), a сам терм f (f x)::b->(b->a). ЧТД.
Проверяем
*Polymorph> :t two k
two k :: a -> b -> b -> a
*Polymorph> two k 42 "Answer" "Ultimate Question"
42
Можно замахнуться на типизацию two $ two k. У меня пока на Хаскелле не очень выходит
-- two $ two k :: ????
-- первое, неидеальное
two' :: (forall a . a -> b -> b -> a)
-> (a -> b -> b -> b -> b -> a)
two' = \f x -> f $ f x
-- тут жульничаем :)
--two' $ two k :: a -> b -> b -> b -> b -> a
-- второе, идеальное
two'' :: (forall a. a -> f a) -> b -> f (f b)
two'' = \f x -> f $ f x
-- к сожалению тайпчекер не справляется с
-- two'' $ two'' k
-- хотя cправляется с two'' k :: b1 -> b -> b -> b1
Хотя как-то должно получиться; общие идеи можно посмотреть
ftp://ftp.mimuw.edu.pl/People/urzy/karpacz-csl04.pdf стр. 26 и далее.