同构镜头

Question

我很感兴趣看到一个van Laarhoven的同构透镜的小例子，应用于像data BValue = BValue { π :: Float, σ :: Float, α :: Float } deriving Show这样的数据类型（特别是get/set/modify函数）。提前谢谢。

- Arets Paeglis

Answer 1

从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 的定义非常好，因为我们只需要检查同构律；通过他博客文章中的计算，镜头定律就会遵循。

因此我们的证明义务如下:

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

这两个证明都直接遵循 piFwd 和 piBwd 的定义以及关于组合的定律。

- Lambdageek

---

最后一件事：BValue没有get/set/modify函数。这些函数是为每个Lens a b类型定义的，只需一次定义即可（请参阅博客文章）。 唯一剩下的事情就是应用特定于您的数据类型的镜头，例如将get应用于piLens。 因此：get piLens是BValue中pi字段的getter。 - Lambdageek

如何在给定类型的特定变量上使用这些访问器，比如 bv :: BValue？镜头适用于类型，因此应该可以获取或设置属于该类型的变量的字段。 - Arets Paeglis

@mindbound 只需将 get/set/modify 函数应用于镜头和值：get piLens bv 或 modify piLens (+ 1.0) bv。 - Lambdageek

Answer 2

看看fclabels包中的Data.Label，它实现了记录类型的镜头。

To illustrate this package, let's take the following two example datatypes.

import Data.Label
import Prelude hiding ((.), id)

data Person = Person
 { _name   :: String
 , _age    :: Int
 , _isMale :: Bool
 , _place  :: Place
 }

data Place = Place
 { _city
 , _country
 , _continent :: String
 }

Both datatypes are record types with all the labels prefixed with an underscore. This underscore is an indication for our Template Haskell code to derive lenses for these fields. Deriving lenses can be done with this simple one-liner:

$(mkLabels [''Person, ''Place])

For all labels a lens will created.

Now let's look at this example. This 71 year old fellow, my neighbour called Jan, didn't mind using him as an example:

jan :: Person
jan = Person "Jan" 71 True (Place "Utrecht" "The Netherlands" "Europe")

When we want to be sure Jan is really as old as he claims we can use the get function to get the age out as an integer:

hisAge :: Int
hisAge = get age jan

Consider he now wants to move to Amsterdam: what better place to spend your old days. Using composition we can change the city value deep inside the structure:

moveToAmsterdam :: Person -> Person
moveToAmsterdam = set (city . place) "Amsterdam"

And now:

ghci> moveToAmsterdam jan
Person "Jan" 71 True (Place "Amsterdam" "The Netherlands" "Europe")

Composition is done using the (.) operator which is part of the Control.Category module. Make sure to import this module and hide the default (.), id function from the Haskell Prelude.

- rampion

---

fclabels 不使用等同镜头表示法。 - Ari Fordsham