Согласно учебнику. на объективах:
type Getting b a b = (b -> Const b b) -> (a -> Const b a)
-- ... equivalent to: (b -> b ) -> (a -> b )
-- ... equivalent to: (a -> b )
Вопрос. Почему (b -> b) -> (a -> b) эквивалентно (a -> b)?
Учебник не очень точен в этом. Вот полное определение Getting:
type Getting r s a = (a -> Const r a) -> s -> Const r s
Сняв шум newtype,
Getting r s a ~= (a -> r) -> s -> r
Интересный изоморфизм, который вы должны получить из этого, следующий:
(forall r. Getting r s a) ~= s -> a
В уже удаленном комментарии Чи указал, что это частный случай леммы Йонеды. .
Изоморфизм подтверждается
fromGetting :: Getting a s a -> (s -> a)
fromGetting g = getConst . g Const
-- ~= g id
-- Note that the type of fromGetting is a harmless generalization of
-- fromGetting :: (forall r. Getting r s a) -> (s -> a)
toGetting :: (s -> a) -> Getting r s a
toGetting f g = Const . getConst . g . f
-- ~= g . f
-- Note that you can read the signature of toGetting as
-- toGetting :: (s -> a) -> (forall r. Getting r s a)
Ни fromGetting, ни toGetting не имеют типа ранга 2, но для описания изоморфизма forall необходим. Почему это изоморфизм?
С одной стороны легко: игнорируя шум Const,
fromGetting (toGetting f)
= toGetting f id
= id . f
= f
Другая сторона сложнее.
toGetting (fromGetting f)
= toGetting (f id)
= \g -> toGetting (f id) g
= \g -> g . f id
Почему это эквивалентно f? forall является ключом здесь:
f :: forall r. Getting r s a
-- forall r. (a -> r) -> s -> r
f не может создать r, кроме как применив переданную функцию (назовем ее p) к значению типа a. Ему не дано ничего, кроме p и значения типа s. Таким образом, f ничего не может сделать, кроме как извлечь a из s и применить p к результату. То есть f p должен "факторироваться" в составе двух функций:
f p = p . h
So
g . f id = g . (id . h) = g . h = f g
Тип говорит: «Вы даете мне b -> b и a, а я дам вам b». Что может сделать функция этого типа со своим b -> b? Два варианта:
bКак получить b для применения функции? Вы используете a для его создания. Так или иначе, он должен выполнять работу a -> b.
Вот некоторый код, чтобы засвидетельствовать изоморфизм (редактировать: не совсем).
in :: ((b -> b) -> a -> b) -> (a -> b)
in f x = f id x
out :: (a -> b) -> ((b -> b) -> a -> b)
out f g x = g (f x)
((b -> b) -> a -> b) может применять первый аргумент не только один раз.
- person Li-yao Xia; 19.05.2017
in f x есть f :: b -> b и x :: a?
- person George; 19.05.2017
f это ((b -> b) -> a -> b), а x это a.
- person Benjamin Hodgson♦; 19.05.2017
zero f x = x; one f x = f x; two f x = f (f x). Тогда out (in zero) = out (in one) = out (in two) = one, но zero /= one и one /= two, так что это вовсе не изоморфизм!
- person Daniel Wagner; 19.05.2017
Lens, которая требует, чтобы аргумент использовался ровно один раз определенным образом, так что Getting является чрезмерным приближением фактической области для рассмотрения.
- person Li-yao Xia; 19.05.2017
(forall b. b -> b) -> (a -> b)гораздо более оправданно эквивалентен(a -> b)(вплоть до обычных предостережений по поводу определенности). Возможно, это то, что пытался передать учебник - или, возможно, это ошибка автора, и ее следует исправить, чтобы вообще не претендовать на эквивалентность. - person Daniel Wagner schedule 19.05.2017