我会对van Laarhoven的isomorphism lenses的一个小示例感兴趣，该示例适用于data BValue = BValue { π :: Float, σ :: Float, α :: Float } deriving Show这样的数据类型(特别是get/set/modify函数)。先感谢您。
最佳答案
在van Laarhoven的帖子中，Lens类型为
data Lens a b = forall r . Lens (Iso a (b, r))
因此，在我们的情况下，
a是BValue，我们想构造一些镜头来挑选一个或多个元素。因此，例如，让我们构建一个拾取π的镜头。piLens :: Lens BValue Float
因此，它将是一个从
BValue到Float(即三元组中的第一个，标签为pi)的镜头。piLens = Lens (Iso {fw = piFwd, bw = piBwd})
镜头有两件事:一个残差类型
r(在此省略，因为我们不必在haskell中明确指定一个存在性类型)，以及一个同构。同构又由前向和后向功能组成。piFwd :: BValue -> (Float, (Float, Float))
piFwd (BValue {pi, sigma, alpha}) = (pi, (sigma, alpha))
前向功能只是隔离我们想要的组件。请注意，这里的残差类型是“剩余的值”，即一对sigma和alpha浮点数。
piBwd :: (Float, (Float, Float)) -> BValue
piBwd (pi, (sigma, alpha)) = BValue { pi = pi, sigma = sigma, alpha = alpha }
向后功能是类似的。
因此，现在我们定义了一个用于操纵
BValue的pi分量的镜头。其他七个镜头相似。 (7个镜头:挑选sigma和alpha，挑选所有可能的对(不考虑顺序)，挑选所有
BValue和挑选())。我不确定的一点是严格性:我有点担心我写的fw和bw函数太严格了。没有把握。
我们尚未完成:
我们仍然需要检查
piLens是否确实遵守镜片法则。 van Laarhoven的Lens定义的好处在于，我们只需要检查同构定律即可；镜头定律遵循他博客文章中的计算方法。因此，我们的证明义务是:
fw piLens . bw piLens = id bw piLens . fw piLens = id 两种证明都直接遵循
piFwd和piBwd的定义以及有关组成的定律。