Lens lib: Is there an optical system for this?
I have a family of fixed length vectors:
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
and two functions for getting and setting a slice of a vector as a list:
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.
I thought I could combine this getter and setter into a lens:
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)
but this violates the laws of lenses ( http://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Lens.html#t:Lens
So I wonder if there is a structure for this?
source to share
I don't think you can get exactly what you are looking for, but you can get some related stuff. This answer will have a pretty roundabout way to get to what you think you most likely want; this is the way my mind got closer to a conclusion, and I think it justifies what I did. The main theme is that there are several different legal options that you can apply to your situation and that can be useful in different ways.
First, let's see what type Lens
you can get. i
and l
Nat
mark the "window" in Vector n
. You haven't specified what you want unless the window is entirely inside the vector. One option is to simply require it to match. Another option is to click the window on the vector size:
-- 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)
Now you can definitely define (for everyone n
using the class, I will ignore this detail in the rest of the post) the legitimate
vlCut :: (KnownNat i, KnownNat l)
=> Proxy i -> Proxy l
-> Lens' (Vector n a) (Vector (ClippedLength i l n) a)
Or, if you only want to allow windows that match,
vl :: (KnownNat i, KnownNat j, i + l <= n)
=> Proxy i -> Proxy l
-> Lens' (Vector n a) (Vector l a)
We can now work through one of these lenses without losing any generality (although we will lose efficiency, more on that later). This means that we completely ignore everything outside the window, so we no longer need to mention the proxy. If we have any optical object from Vector w a
to t
, then we can create an optical disc from Vector n a
to t
.
By reducing your slice control functions to a window, you get
getSliceW :: Vector w a -> [a]
setSliceWpartial :: Vector w a -> [a] -> Maybe (Vector w a)
It doesn't Lens
, as you discovered. But if you decrease a little by replacing setSliceWpartial
with
fromList :: [a] -> Maybe (Vector w a)
you can do legal Prism
:
slicep :: Prism' [a] (Vector w a)
Considering Vector w a
, you can always create [a]
, but the other way is only possible sometimes. You can use this with vl
or vlCut
(if this is a problem you need to solve, this is a fine solution), but you cannot link to them because the types do not match correctly. You can rotate the prism with re
, but at the end you only get Getter
.
Since your types don't look that good, try changing them:
getSliceW :: Vector w a -> [a]
setSliceW :: Vector w a -> [a] -> Vector w a
Now we are preparing the bass! It has a type of parts Lens' (Vector w a) [a]
, although it is actually not a legal lens. This is, however, a very good hint. Control.Lens.Traversal
proposes
partsOf' :: ATraversal s t a a -> Lens s t [a] [a]
which you can read in this context as
partsOf' :: Traversal' (Vector w a) a -> Lens' (Vector w a) [a]
So (through the window) we really want
traverseVMono :: Traversal' (Vector w a) a
Of course, this is immediately generalized; just write an instance Traversable
for Vector n
and use it traverse
.
I mentioned earlier that working through a window is Lens
ineffective. So how can you handle this? Well, just don't bother actually creating a window! What you want to go "end-to-end" is just walk through the window. So do it:
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)
You can restore the original partial setSlice
if you like; you just need to use traverseWindow
with something like 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
source to share