Какая история стоит за Геттером?

Question

Я наткнулся на определение Геттер, имеющий как Functor а также Contravariant ограничение на f,

Неудивительно, что "добытчик" мало что может сделать с "содержавшейся частью", но эта подпись выглядит как Призрак в "ван Лаарховене" (a -> f a) -> s -> f s, Является ли неявное ограничениеs знает о a"представлен таким образом в lens?

Как я могу найти исходный код некоторых конкретных экземпляров Getter чтобы я мог видеть map а также contramap использовался?

Answer 1

Идея Getter является то, что это объектив только для чтения. Учитывая Getter s a Вы можете потянуть a из s, но вы не можете вставить его. Тип определяется следующим образом:

type Getter s a = forall f. (Contravariant f, Functor f) => (a -> f a) -> s -> f s

Когда тип является Functor а также ContravariantНа самом деле, он не зависит от аргумента типа:

import Data.Void

change :: (Functor f, Contravariant f) => f a -> f b
change = fmap absurd . contramap absurd

Такой функтор всегда будет очень похож Const b для некоторых b,

Так что Getter s a по существу

type Getter s a = forall b . (a -> b) -> s -> b

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

Answer 2

Ну, геттер - это просто функция. Изоморфизм таков:

getter :: (Functor f, Contravariant f) => (s->a) -> (a->f a) -> s->f s
getter f q = contramap f . q . f

Здесь contramap в действительности ничего не будет делать, кроме как принуждать типы Functor а также Contravariant составляет требование, чтобы f x на самом деле не содержит x, По сути, обеспечение этого также является единственной причиной Functor ограничение есть.

Answer 3

Тип

Getter s a = forall f . (Contravariant f, Functor f) => (a -> f a) -> (s -> f s)

изоморфен типу s -> a, Две стороны изоморфизма определяются

toGetter :: (s -> a) -> Getter s a
toGetter h alpha = contramap h . alpha . h
fromGetter :: Getter s a -> (s -> a)
fromGetter getter = getConst . getter Const

Нетрудно понять, что fromGetter (toGetter h) равняется h,

До этого момента (т.е. для того, чтобы реализовать toGetter а также fromGetter и доказать это fromGetter . toGetter = id) мы не использовали Functor f ограничение. Однако это ограничение необходимо для того, чтобы доказать, что toGetter . fromGetter = id,

---

Сначала предположим, что f является одновременно ковариантным Functor и Contravariant функтор. Тогда любая функция g :: x -> y дает функции fmap g :: f x -> f y а также contramap g :: f y -> f x, Параметричность в сочетании с законами функторов предполагает, что они взаимно обратны, т.е. f x ≅ f y, Следовательно, f является (с точностью до изоморфизма) постоянным функтором, поэтому мы можем думать о Getter s a как определяется как

Getter s a = forall f0 . (a -> b) -> (s -> b)

(как указано в ответе dfeuer). По лемме Йонеды это изоморфно s -> a,

---

Примечательно, что если мы поднимем Functor f ограничение:

OddGetter s a = forall f . Contravariant f => (a -> f a) -> (s -> f s)

тогда мы получаем подтип Getter s a это больше не изоморфно s -> a, но вместо s -> Aux a s:

newtype Aux a x = Aux {aAux :: a, gAux :: x -> a}
instance Contravariant (Aux a) where
  contramap f (Aux a g) = Aux a (g . f)

toAux :: a -> Aux a a
toAux a = Aux a id

(Aux a, toAux) является инициалом всех пар (F, toF) где F является контравариантным функтором и toF :: a -> F a аналогично тому, как (Const a, Const) является инициалом всех пар (F, toF) где F является со-и контравариантным функтором и toF :: a -> F a ,

Две стороны изоморфизма могут быть реализованы следующим образом:

toOddGetter :: (s -> Aux a s) -> OddGetter s a
toOddGetter sigma alpha s1 =
    contramap (\s2 -> gAux (sigma s1) s2) $ alpha $ aAux (sigma s1)
fromOddGetter :: OddGetter s a -> (s -> Aux a s)
fromOddGetter getter = getter toAux

Опять же, это просто проверить, что fromOddGetter . toOddGetter = id что уже показывает, что OddGetter s a не изоморфен s -> a, Чтобы доказать это fromOddGetter . toOddGetter = id Нам снова нужен параметрический аргумент.

Параметричность влечет за собой то, что для любого естественного преобразования nu :: forall x . d x -> f x, любой getter :: OddGetter s a и любой alphaD :: a -> d a, у нас есть

nu . getter alphaD = getter (nu . alphaD) :: s -> f s

Теперь мы создаем d с Aux a, alphaD с toAux а также nu с factor alpha (для произвольной alpha : a -> f a):

factor :: (a -> f a) -> forall x . Aux a x -> f x
factor alpha (Aux a g) = contramap g $ alpha a

который имеет свойство, которое factor alpha . toAux = alpha, Тогда у нас есть

factor alpha . getter toAux = getter (factor alpha . toAux) = getter alpha :: s -> f s

Теперь, когда мы применяем это к некоторым s1 :: s мы находим, что getter alpha s1 (применяемая RHS) равна

factor alpha (getter toAux s1)
  = contramap (gAux $ getter toAux s1) $ alpha (aAux $ getter toAux s1)
    {-by definition of factor-}
  = contramap (\s2 -> gAux (getter toAux s1) s2) $ alpha $ aAux (getter toAux s1)
    {-by eta-expansion and regrouping-}
  = toOddGetter (getter toAux) alpha s1
    {-by definition of toOddGetter-}
  = toOddGetter (fromOddGetter getter) alpha s1
    {-by definition of fromOddGetter-}

т.е. getter = toOddGetter (fromOddGetter getter),

---

Учитывая изоморфизмы, возможно, замечательно, что тип

OddGetter s a ≅ s -> Aux a s

это подтип

Getter s a ≅ s -> a

Функция "принуждение"

\ getter -> getter :: OddGetter s a -> Getter s a

соответствует функции

\ sigma -> aAux . sigma :: (s -> Aux a s) -> (s -> a)

под этими изоморфизмами.