Search code examples
haskellhaskell-lens

Lens lib: Is there an optic 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 to get and set 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 these getter and setter into a lens like this:

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 lens laws(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?

Solution

  • I don't think you can get exactly what you're looking for, but you can get some related things. This answer is going to take a rather roundabout path to get to what I think you most likely want; this is the path my mind took approaching a conclusion, and I think justifies what I ended up with. The general theme is that there are a few different legitimate optics you can apply to your situation and that can be useful in different ways.

    First, let's look at what sort of Lens you can get. The i and l Nats mark out a "window" in the Vector n. You haven't indicated what you want to happen if the window doesn't lie entirely within the vector. One option is to simply require it to fit. Another option is to clip the window to the size of the vector:

    -- 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 certainly define (for each n, using a class; I'll ignore this detail in the rest of the post) a 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 fit,

    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 getting around that later). Doing so means we get to completely ignore everything outside of the window, so we needn't mention the proxies anymore. If we have any optic from Vector w a to t, then we can produce an optic from Vector n a to t.

    Reducing your slice-manipulating functions to the window, you get

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

    These don't make a Lens, as you discovered. But if you reduce just a bit further, replacing setSliceWpartial with

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

    you can make a lawful Prism:

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

    Given a Vector w a, you can always produce a [a], but the other way is only sometimes possible. You can certainly use this with vl or vlCut (if that's the problem you need to solve, that's a fine solution), but you can't compose it with them, because the types don't match up right. You can reverse the prism with re, but that only gives you a Getter in the end.

    Since your types don't seem to work out so nicely, let's try changing them:

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

    Now we're cooking with bass! This has the type of the pieces of a Lens' (Vector w a) [a], although it's not actually a lawful lens. It is, however, a very good clue. Control.Lens.Traversal offers

    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), what we really want is

    traverseVMono :: Traversal' (Vector w a) a

    Of course, that generalizes immediately; just write a Traversable instance for Vector n and use its traverse.

    I mentioned earlier that working through a window Lens is inefficient. So how can you deal with that? Well, just don't bother actually constructing the window! What you want to go "from end to end" is just to traverse the window. So do that:

    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 recover your original partial setSlice if you like; you just have 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