Lens lib: Gibt es dafür eine Optik?

Question

Ich habe eine Familie mit fester Länge Vektoren:

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 

und zwei Funktionen zu erhalten und eine Scheibe eines Vektors als eine Liste gesetzt:

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. 

Ich dachte, ich diese Getter und Setter kombinieren könnte in eine Linse wie folgt aus:

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) 

aber gegen Linse Gesetze (http://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Lens.html#t:Lens

Also frage ich mich, ob es eine Struktur dafür gibt?

Answer 1

Ich denke nicht, dass Sie genau das bekommen können, was Sie suchen, aber Sie können einige verwandte Dinge bekommen. Diese Antwort wird einen ziemlich Umweg nehmen, um zu dem zu gelangen, von dem ich denke, dass Sie es am meisten wollen; Dies ist der Weg, den mein Verstand zu Ende gegangen ist, und ich denke, dass ich damit recht habe. Das allgemeine Thema ist, dass es ein paar verschiedene legitime Optiken gibt, die Sie auf Ihre Situation anwenden können und die auf verschiedene Arten nützlich sein können.

Zuerst schauen wir uns an, welche Art von Lens Sie können bekommen. Die i und lNat s markieren ein "Fenster" in der Vector n. Sie haben nicht angegeben, was Sie wollen, wenn das Fenster nicht vollständig innerhalb des Vektors liegt. Eine Möglichkeit besteht darin, sie einfach anzupassen. Eine weitere Option ist das Fenster auf die Größe des Vektors stutzen:

-- 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) 

Jetzt können Sie sicher definieren (für jeden n, eine Klasse mit, ich werde dieses Detail in dem Rest der Post ignorieren) ein legitimen

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

Oder, wenn Sie wollen nur die Fenster ermöglichen, die passen,

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

wir können nun durch eine dieser Linsen arbeiten, ohne jede Allgemeingültigkeit zu verlieren (obwohl wir eff verlieren iciency; mehr dazu, später herumzukommen). Dies bedeutet, dass wir alles außerhalb des Fensters vollständig ignorieren müssen, sodass wir die Proxies nicht mehr erwähnen müssen. Wenn wir eine Optik von Vector w a bis t haben, können wir eine Optik von Vector n a bis t herstellen.

Reduzieren Sie Ihre Slice-Manipulation Funktionen zum Fenster, erhalten Sie

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

diese keine Lens machen, wie Sie entdeckt. Aber wenn Sie reduzieren nur ein bisschen weiter, ersetzt setSliceWpartial mit

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

können Sie eine rechtmäßige Prism machen:

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

ein Vector w a gegeben, können Sie immer eine [a] produzieren, aber der andere Weg ist nur manchmal möglich.Sie können dies sicherlich mit vl oder vlCut (wenn das das Problem ist, das Sie lösen müssen, das ist eine gute Lösung), aber Sie können nicht mit ihnen komponieren, weil die Typen nicht richtig übereinstimmen. Sie können das Prisma mit re umkehren, aber das gibt Ihnen am Ende nur eine Getter.

---

Da Ihr Typ versuchen, scheint nicht so gut zu arbeiten, wollen sie sie zu ändern:

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

Jetzt sind wir mit Bass-Kochen! Dies hat die Art der Stücke von Lens' (Vector w a) [a], obwohl es nicht wirklich eine gesetzliche Linse ist. Es ist jedoch ein sehr guter Anhaltspunkt. Control.Lens.Traversal Angebote

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

, die Sie in diesem Zusammenhang lesen können, wie

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

So (durch das Fenster), was wir wirklich wollen, ist

traverseVMono :: Traversal' (Vector w a) a 

Natürlich das verallgemeinert sich sofort; Schreiben Sie einfach eine Traversable Instanz für Vector n und verwenden Sie traverse.

---

Ich erwähnte bereits, dass das Arbeiten durch ein Fenster Lens ineffizient ist. Wie können Sie damit umgehen? Nun, mach dir bloß keine Mühe, das Fenster zu bauen! Was Sie "von Ende zu Ende" gehen wollen, ist nur durchqueren das Fenster. Also, dass:

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) 

Sie können Ihre ursprüngliche Teil setSlice wiederherstellen, wenn Sie mögen; Sie müssen nur traverseWindow mit etwas verwenden wie 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