Traversing and Mapping on L1/M1/R1?

[Zemyla]

L1, M1, and R1 are Strong and Choice Categorys. That should mean that there is a Traversing instance for them. And the fact that they're Closed as well should mean there is a Mapping instance, too. But, while the Traversing instance seems like it can be done fairly mechanically, I can't figure out what the Mapping instance would be.

[sjoerdvisscher]

while the Traversing instance seems like it can be done fairly mechanically

Hmm, I don't see how, can you explain?

[Zemyla]

Every ArrowChoice is a Traversing, and it can be done by "freezing" the traversal into a list and then walking it.

-- This type represents a traversal "frozen" in a format that an ArrowChoice
-- can interact with.
newtype BazE a b t = BazE {
    unBazE :: Either t (a, BazE a b (b -> t))
  }

-- And this type represents a traversal as a difference list, in a way that
-- makes operations O(1). It's equivalent to
-- Backwards (Curried (Yoneda (BazE a b)) (Yoneda (BazE a b))).
newtype Bazaar a b t = Bazaar {
    unBazaar :: forall r y.
      (forall x. ((t -> r) -> x) -> BazE a b x) ->
      (r -> y) -> BazE a b y
  }

instance Functor (Bazaar a b) where
  fmap f (Bazaar m) = Bazaar $ \y -> m $ \c -> y $ \g -> c $ g . f
  {-# INLINE fmap #-}

instance Applicative (Bazaar a b) where
  pure a = Bazaar $ \y c -> y $ \g -> c $ g a
  {-# INLINE pure #-}

  Bazaar mf <*> Bazaar ma = Bazaar $
    \y -> mf $ ma $ \c -> y $ \g -> c $ \a f -> g $ f a
  {-# INLINE (<*>) #-}

-- This adds a value to the traversal.
bazaar :: a -> Bazaar a b b
bazaar a = Bazaar $ \y c -> BazE $ Right (a, y $ (.) c)
{-# INLINE bazaar #-}

-- And this turns a applicative Bazaar value into a dissectable BazE value.
runBazaar :: Bazaar a b t -> BazE a b t
runBazaar (Bazaar m) = m (\c -> BazE $ Left $ c id) id
{-# INLINE runBazaar #-}

-- This newtype is pretty much a hack so I don't have to use
-- ScopedTypeVariables.
newtype Debaz p a b = Debaz { unDebaz :: forall u. p (BazE a b u) u }

-- The Traversal type from Lens.
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

-- And now we implement wander.
wanderA :: ArrowChoice p => Traversal s t a b -> p a b -> p s t
wanderA tr p = arr (runBazaar . tr bazaar) >>> unDebaz go where
  go = Debaz $
    arr (either id $ uncurry $ flip id) . right (p *** unDebaz go) . arr unBazE
{-# INLINE wanderA #-}

There's probably a better way, specific to L1/M1/R1, that leverages the structure of the types rather than having to deconstruct the traversals.

[Zemyla]

And it turns out the naive way doesn't work, because in order to create go, it has to deconstruct go, and that makes a loop. However, I've got it figured out through manual expansion and ScopedTypeVariables:

instance Traversing M1 where
  wander tr (M1 k h m) = wand k (runBazaar . tr (bazaar . h)) m where
    wand :: forall s t m b. (m -> b) -> (s -> BazE m b t) -> (m -> m -> m) -> M1 s t
    wand k h' m = M1 k' h' m' where
      m' :: forall u. BazE m b u -> BazE m b u -> BazE m b u
      m' (BazE (Right (a, b))) (BazE (Right (c, d))) = BazE $ Right (m a c, m' b d)
      m' l@(BazE (Left _)) _ = l
      m' _ r@(BazE (Left _)) = r

      k' :: forall u. BazE m b u -> u
      k' (BazE (Left u)) = u
      k' (BazE (Right (a, b))) = k' b $ k a

The only law I'm not sure about whether it passes is

traverse' . traverse' = dimap Compose getCompose . traverse'

The first one is trivially satisfied by the default definition, and the second and fourth are obvious by inspection.

[sjoerdvisscher]

Nice! Would firstTraversing do the same thing as the currently implemented first?

[Zemyla]

It actually appears that it would do the reverse of the current first; namely, that the c produced is the first one given, not the last. You'd need to switch the last two lines of m' to make it properly right-biased.

[twhitehead]

Just ran into a need for a generalized fmap on these things. Fortunately I have an Applicative f instead of just a Functor f, and it would seem the obvious trivial definition (just lift all the values and functions) is solid.

[Zemyla]

And M1 isn't a Mapping because there's no way for it to support the operation

backclosed :: M1 a b -> M1 (b -> x) (a -> x)

which is necessary to map an M1 a b to an M1 (Cont r a) (Cont r b).