Что происходит с универсальными квантификациями и ограничениями класса типов при составлении функций?

Линзы могут быть составлены как любая обычная функция. У нас есть:

Lens' a b = forall f . Functor f => (b -> f b) -> a -> f a

Теперь рассмотрим этот пример:

(.) :: Lens' Config Foo -> Lens' Foo String -> Lens' Config String

Расширяя получаем:

(.) :: (forall f. Functor f => (Foo -> f Foo) -> Config -> f Config)
    -> (forall f. Functor f => (String -> f String) -> Foo -> f Foo)
    -> (forall f. Functor f => (String -> f String) -> Config -> f Config)

И тип функциональной композиции:

(.) :: (b -> c) -> (a -> b) -> (a -> c)

В котором отсутствуют какие-либо универсальные ограничения количественной оценки и класса типов. Теперь мой вопрос: как эти две функции обрабатываются компилятором/проверщиком типов, чтобы оператор композиции функций можно было использовать для составления линз?

Я предполагаю, что нормально иметь функции с универсальной количественной оценкой и ограничениями класса типов, если они соответствуют двум составляемым функциям.


haskell lenses rank-n-types
person Damian Nadales    schedule 02.09.2017    source источник
comment
Кроме того, a -> forall x. b = forall x. a -> b (если x не упоминается в a и, возможно, упоминается в b) и a -> c => b = c => a -> b (где c — ограничение). Обратите внимание, что (forall x. a) -> b, тип ранга 2, нельзя переписать таким образом, потому что forall-квантованный тип появляется в «отрицательной позиции» (слева от функциональной стрелки).   -  person Jon Purdy    schedule 02.09.2017
comment
Вы допустили ошибку во 2-й строке - тип Lens' X Y -> Lens' Y Z -> Lens' X Z никогда не будет выведен для (.). Этот тип является непредикативным, а GHC нет. поддержка непредикативного полиморфизма. У вас есть ответ, показывающий, что происходит на самом деле; короткая версия заключается в том, что каждый политип преобразуется в монотип при применении функции, если только эта функция явно не принимает политип в качестве аргумента (например, с RankNTypes).   -  person user2407038    schedule 03.09.2017
comment
О, привет, @Jon. Как твой котенок?   -  person Aadit M Shah    schedule 03.09.2017
comment
@AaditMShah: Хорошо, спасибо. :) Я занимаюсь реорганизацией кода, чтобы упростить реализацию нескольких последних основных функций перед выпуском. (Ограничения трейтов, универсальные экземпляры трейтов, неупакованные замыкания и массивы, кое-что еще.) Если я смогу найти/выкроить время, чтобы поработать над этим, я должен выпустить что-нибудь через пару месяцев. .   -  person Jon Purdy    schedule 03.09.2017

Ответы (1)


arrow_upward
3
arrow_downward

Почему мы не видим, что происходит? Рассмотрим следующие значения:

(.) :: (b -> c) -> (a -> b) -> a -> c

foo :: Lens' A B

bar :: Lens' B C

Тип foo и bar будет расширен до:

foo :: Functor f => (B -> f B) -> A -> f A

bar :: Functor g => (C -> g C) -> B -> g B

Обратите внимание, что я пропустил часть forall f., потому что она подразумевается. Кроме того, я изменил имя f на g для bar, чтобы показать, что оно отличается от f для foo.

В любом случае, мы сначала применим (.) к foo:

(.)     ::                 (b      ->    c)    -> (a ->    b)     -> a ->    c
                            |            |         |       |         |       |
                         --------     --------     |       |         |       |
                         |      |     |      |     |       |         |       |
foo     :: Functor f => (B -> f B) -> A -> f A     |    --------     |    --------
                                                   |    |      |     |    |      |
(.) foo :: Functor f =>                           (a -> B -> f B) -> a -> A -> f A

Таким образом, (.) foo имеет тип Functor f => (a -> B -> f B) -> a -> A -> f A. Как видите, ограничение Functor просто копируется как есть.

Теперь применим (.) foo к bar:

(.) foo     :: Functor f =>    (a      -> B -> f B) ->     a      -> A -> f A
                       |        |         |    | |         |         |    | |
                       |     --------     |    | |         |         |    | |
                       |     |      |     |    | |         |         |    | |
bar         :: Functor g => (C -> g C) -> B -> g B      --------     |    | |
                                                        |      |     |    | |
(.) foo bar :: Functor g =>                            (C -> g C) -> A -> g A

Таким образом, (.) foo bar имеет тип Functor g => (C -> g C) -> A -> g A, что означает, что это Lens' A C. Как видите, Functor f совпадает с Functor g, поэтому все работает.

person Aadit M Shah    schedule 02.09.2017