同构镜头

Question

我会对van Laarhoven的同构镜头的一个小例子感兴趣,应用于数据类型data BValue = BValue { ? :: Float, ? :: Float, ? :: Float } deriving Show(特别是get/set/modify函数).先感谢您.

Answer 1

从van Laarhoven的帖子来看,Lens类型是

data Lens a b = forall r . Lens (Iso a (b, r))

所以在我们的例子a中BValue,我们想构建一些选择一个或多个元素的leneses.例如,让我们构建一个能够挑出π的镜头.

piLens :: Lens BValue Float

所以它将是一个从a BValue到a 的镜头Float(即三个中的第一个镜头,标签为pi.)

piLens = Lens (Iso {fw = piFwd, bw = piBwd})

一个镜头挑选出两个东西:一个残留类型r(这里省略,因为我们不必在haskell中明确指定一个存在类型),以及一个同构.同构又由前向和后向函数组成.

piFwd :: BValue ->  (Float, (Float, Float))
piFwd (BValue {pi, sigma, alpha}) = (pi, (sigma, alpha))

forward函数只是隔离了我们想要的组件.请注意,我的剩余类型是"值的其余部分",即一对sigma和alpha浮点数.

piBwd :: (Float, (Float, Float)) -> BValue
piBwd (pi, (sigma, alpha)) = BValue { pi = pi, sigma = sigma, alpha = alpha }

后向功能类似.

所以现在我们已经定义了一个镜头来操纵a的pi组件BValue.

其他七个镜头是相似的.(7个镜头:选择西格玛和阿尔法,挑出所有可能的对(无视顺序),挑出所有BValue并挑选出来()).

我不确定的一点是严格:我有点担心我写的fw和bw函数太严格了.不确定.

我们还没有完成:

我们仍然需要检查piLens实际上是否尊重镜头规律.van Laarhoven定义的好处Lens是我们只需要检查同构定律; 透镜法则通过他博客文章中的计算得出.

所以我们的证明义务是:

1. fw piLens . bw piLens = id
2. bw piLens . fw piLens = id

这两种证明直接的定义遵循piFwd和piBwd有关组成和法律.