我偶然发现Getter定义在Functor上有Contravariant和f约束。
毫无疑问，“吸气剂”对“包含的部分”不起作用，但这个标志看起来像Phantom的“van Laarhoven”环境中的(a -> f a) -> s -> f s。隐含的约束“s知道a”在lens中以这种方式表示吗？
如何找到Getter的一些具体实例的源代码，以便我可以看到map和contramap被使用？
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
但为了使其与镜头生态系统的其余部分一起工作，它具有额外的多态性。
嗯，吸气剂基本上只是一个功能。同构是这样的：
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约束的唯一原因。
类型
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的答案所述）。通过Yoneda引理，这与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-}
即yaazkssvpoi。
鉴于同构，这种类型可能是非常值得注意的
getter = toOddGetter (fromOddGetter getter)是一个子类型
OddGetter s a ≅ s -> Aux a s
“强制”功能
Getter s a ≅ s -> a
对应于该功能
\ getter -> getter :: OddGetter s a -> Getter s a
在这些同构下。