[Lens s t a b] -> Lens [s] [t] [a] [b]

LensList.hs

-- in response to https://twitter.com/_julesh_/status/1573281637378527232
--
-- The challenge is to implement a partial function of type
--
--     list :: [Lens s t a b]
--          -> Lens [s] [t] [a] [b]
--
-- while using the existential representation of lenses.
{-# LANGUAGE GADTs, ScopedTypeVariables #-}

-- Let's begin with the existential representation of lenses.
--
-- Informally, the idea is that if @s@ contains an @a@, then we should be able
-- to split @s@ into two parts, the @a@ and the rest, which we'll call @u@.
--
-- A bit more formally, there should be an isomorphism between @s@ and @(u,a)@
-- for some @u@.
--
-- Except that in order to allow the lens to change the type of the focus, we
-- use @s@ and @(u,a)@ in one direction of the isomorphism and @t@ and @(u,b)@
-- in the other direction.
data Lens s t a b where
  Lens
    :: (s -> (u, a))
    -> ((u, b) -> t)
    -> Lens s t a b


-- The challenge is to implement the following function. I simply fold over the
-- input list; not much of a challenge so far! The new challenges are now to
-- implement @nil@ and @cons@.
list
  :: forall s t a b
   . [Lens s t a b]
  -> Lens [s] [t] [a] [b]
list = foldr cons nil

-- Note that the @list@ function is partial: it assumes that the @[s]@ and
-- @[b]@ lists have the same length as the @[Lens s t a b]@ list. Thus, when
-- that list is empty and @list@ behaves like @nil@, it assumes that the @[s]@
-- and @[b]@ lists are empty. That's why we make the same assumption in @nil@,
-- by using the irrefutable pattern @[]@ to match on those lists.
nil
  :: Lens [s] [t] [a] [b]
nil
  = Lens
      (\[] -> ((), []))
      (\((),[]) -> [])

-- Only one function left, so this is where the heart of the challenge must
-- lie! The implementation does look more imposing, but it's actually really
-- simple: this time we can assume that the lists are non-empty, so we get a
-- head and a tail, and we process each using the corresponding function we
-- received from the input.
cons
  :: Lens s t a b
  -> Lens [s] [t] [a] [b]
  -> Lens [s] [t] [a] [b]
cons (Lens split1 join1)
     (Lens splitN joinN)
  = Lens
      ( \(s:ss)
     -> let (u,a) = split1 s
     in let (us,as) = splitN ss
     in ((u,us), a:as)
      )
      ( \((u,us), b:bs)
     -> let t = join1 (u,b)
     in let ts = joinN (us,bs)
     in t:ts
      )


-- We're done with the challenge, but in order to demonstrate that the
-- implementation works as intended, let's define a few more lenses and
-- operations:

_1 :: Lens (a,u) (b,u) a b
_1 = Lens
       (\(a,u) -> (u,a))
       (\(u,b) -> (b,u))

_2 :: Lens (u,a) (u,b) a b
_2 = Lens
       (\(u,a) -> (u,a))
       (\(u,b) -> (u,b))

view
  :: Lens s t a b
  -> (s -> a)
view (Lens split _)
  = snd . split

over
  :: Lens s t a b
  -> (a -> b)
  -> (s -> t)
over (Lens split join) f
  = join
  . (\(u, a) -> (u, f a))
  . split

-- We are now ready to demonstrate that @list@ behaves as intended:
main :: IO ()
main = do
  let ss = [ ("A","a")
           , ("B","b")
           , ("C","c")
           ]
  let ll = [_1, _2, _1]

  -- ["A","b","C"]
  print $ view (list ll) ss

  -- [("C","a"),("B","b"),("A","c")]
  print $ over (list ll) reverse ss