鏡頭庫：有沒有這種鏡頭？

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