镜头库：这个有适用的光学吗？

Question

镜头库：这个有适用的光学吗？

3

我有一个固定长度向量的家族：

data family Vector (n :: Nat) a
data instance Vector 2 a = Vector2 a a
data instance Vector 3 a = Vector3 a a a
-- and so on

还有两个函数用于将向量的一部分作为列表进行获取和设置：

getSlice :: Proxy i -> Proxy l -> Vector n a -> [a]
setSlice :: Proxy i -> Proxy l -> Vector n a -> [a] -> Maybe (Vector n a)
-- ^ setSlice is partial because list parameter may not have enough elements.

我认为我可以将这些 getter 和 setter 结合成一个类似于镜头的东西：

slice :: Proxy i -> Proxy l -> Lens (Vector n a) (Maybe (Vector n a)) [a] [a]
slice i l = lens (getSlice i l) (setSlice i l)

但是这违反了镜头定律(http://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Lens.html#t:Lens)。因此我想知道是否有一个结构可以解决这个问题？

- Alexey Vagarenko

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- dfeuer · Accepted Answer

我认为你可能无法获得完全符合你要求的内容，但你可以获得一些相关的东西。这个答案会采用一个比较迂回的方式来达到我认为你最有可能想要的东西；这是我的思维路径接近结论所采取的方式，我认为这证明了我最终得出的结论的合理性。总的主题是，你可以应用几种不同的合法视角来看待你的情况，并且在不同方面都能够有所帮助。

首先，让我们看看你可以获得哪种类型的“镜头”。i 和 l Nat 标记出了向量 n 中的一个“窗口”。你没有说明如果窗口不完全位于向量中，你希望发生什么。其中一种选择是要求它适合。另一种选择是将窗口剪裁到向量的大小：

-- Minimum
type Min m n = Min' (m <=? n) m n
type family Min' m_le_n (m :: Nat) (n :: Nat) where
  Min' 'True m _ = m
  Min' 'False _ n = n

-- Saturated subtraction
type SatMinus m n = SatMinus' (n <=? m) m n
type family SatMinus' n_le_m m n where
  SatMinus' 'True m n = m - n
  SatMinus' 'False _ _ = 0

-- Window clipping
type ClippedLength i l n = Min l (SatMinus n i)

现在你可以为每个n（使用类来定义，本文的其余部分将忽略此细节）定义一个合法的。

vlCut :: (KnownNat i, KnownNat l)
   => Proxy i -> Proxy l
   -> Lens' (Vector n a) (Vector (ClippedLength i l n) a)

或者，如果您只想允许适合的窗口，

vl :: (KnownNat i, KnownNat j, i + l <= n)
   => Proxy i -> Proxy l
   -> Lens' (Vector n a) (Vector l a)

我们现在可以通过其中一个透镜进行工作，而不失去任何一般性（尽管我们会失去效率；稍后再详细介绍如何解决这个问题）。这样做意味着我们完全可以忽略窗口外的所有内容，因此我们不需要再提到代理。如果我们有从 Vector w a 到 t 的光学器，则我们可以产生从 Vector n a 到 t 的光学器。

将您的切片操作函数缩小到窗口，您将获得

getSliceW :: Vector w a -> [a]
setSliceWpartial :: Vector w a -> [a] -> Maybe (Vector w a)

这些并不能组成一个Lens，正如你所发现的。但是如果你再进一步简化，将setSliceWpartial替换为...

fromList :: [a] -> Maybe (Vector w a)

你可以制作一个合法的 Prism:

slicep :: Prism' [a] (Vector w a)

给定一个类型为 Vector w a 的值，你总是可以生成一个类型为[a]的值，但反过来不一定成立。你当然可以在使用vl或vlCut时使用它（如果这是你需要解决的问题，那么这是一个好的解决方案），但是你不能与它们组合，因为类型不匹配。你可以使用re翻转棱镜，但最终只会得到一个Getter。

由于您的类型似乎无法很好地工作，让我们尝试更改它们：

getSliceW :: Vector w a -> [a]
setSliceW :: Vector w a -> [a] -> Vector w a

现在我们开始使用 bass 进行编程！这个东西的类型类似于一个 Lens' (Vector w a) [a]，虽然它实际上不是一个合法的 lens。但是，它是一个非常好的线索。Control.Lens.Traversal 提供了相关内容。

partsOf' :: ATraversal s t a a -> Lens s t [a] [a]

“在这个上下文中，你可以将其解读为”

partsOf' :: Traversal' (Vector w a) a -> Lens' (Vector w a) [a]

所以（透过窗户），我们真正想要的是：

traverseVMono :: Traversal' (Vector w a) a

当然，这可以立即概括；只需为Vector n编写一个Traversable实例并使用其traverse即可。

我之前提到，通过窗口Lens工作效率低下。那么你该如何处理呢？好吧，其实不需要真正构建窗口！你想要的是“从头到尾”地遍历窗口。所以就这样做：

traverseWindow :: (KnownNat i, KnownNat l, Applicative f)
               -- optionally require i + l <= n
               => proxy1 i
               -> proxy2 l
               -> (a -> f a)
               -> Vector n a
               -> f (Vector n a)

如果您愿意，您可以恢复原始的部分setSlice；您只需要使用类似于MaybeT（State [a]）的内容来使用traverseWindow：

foldMapWindow :: (KnownNat i, KnownNat l, Monoid m)
  => proxy1 i
  -> proxy2 l
  -> (a -> m)
  -> Vector n a
  -> m
foldMapWindow p1 p2 f = getConst . traverseWindow p1 p2 (Const . f)

windowToList :: (KnownNat i, KnownNat l)
  => proxy1 i
  -> proxy2 l
  -> Vector n a
  -> [a]
windowToList p1 p2 = foldMapWindow p1 p2 (:[])

setSlice :: (KnownNat i, KnownNat l)
         => proxy1 i -> proxy2 l
         -> Vector n a -> [a] -> Maybe (Vector n a)
setSlice p1 p2 v xs = flip evalState (windowToList p1 p2 v) . runMaybeT $ flip (traverseWindow p1 p2) v $ \_ -> do
  y : ys <- get
  put ys
  pure y