镜头库：有没有这种镜头？

Question

我有一个家庭固定长度的载体：

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

所以我想知道是否有这样的结构？

Answer 1

我不认为你可以得到你正在寻找的东西，但你可以得到一些相关的东西。这个答案将采取一个相当迂回的路径来达到我认为你最可能想要的;这是我脑海中接近结论的道路，我认为我最终得到的结果是合理的。总的主题是，有几种不同的合法光学技术可以应用于您的情况，并且可以以不同的方式发挥作用。

首先，我们来看看你可以得到什么样的Lens。 i和lNat s在Vector 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) 

我们可以通过这些镜头中的一个，而不会丢失任何一般性（虽然我们将失去EFF现在的工作iciency;更多的是在稍后获得）。这样做意味着我们完全忽略了窗口外的所有内容，所以我们不必再提及代理。如果我们有从Vector w a到t的任何光学元件，那么我们可以生产从Vector n a到t的光学元件。

减少你的切片操作功能的窗口，你会得到

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

这些不作Lens，因为你发现了。但是，如果你减少只是有点此外，

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

更换setSliceWpartial你可以做一个合法的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 

现在我们正在与低音做饭！这有类型片段的Lens' (Vector w a) [a]，虽然它实际上不是一个合法的镜头。但是，这是一个非常好的线索。 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如果你喜欢;你只需要使用traverseWindow喜欢的东西MaybeT (State [a])：

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