Is it possible to reverse type-aligned traversals?

Question

There's a lot of setup here. If you've ever seen a type-aligned sequence before, you can skim everything up to the line.

A type-aligned sequence is anything that looks vaguely like

data ConsList c x y where
  CNil :: ConsList c x x     
  Cons :: c x y -> ConsList c y z -> ConsList c x z

Given a class for Atkey-style indexed functors and applicative functors

class IxFunctor f where
  ixmap :: (a -> b) -> f x y a -> f x y b
class IxFunctor f => IxApply f where
  ixap :: f i j (a -> b) -> f j k a -> f i k b
class IxApply f => IxApplicative f where
  ixpure :: a -> f i i a

and a two-index McBride-style functor class:

type (f :: q -> r -> *) ~~> (g :: q -> r -> *) =
  forall (i :: q) (j :: r) . f i j -> g i j

class TFunctor t where
  tmap :: (c ~~> d) -> (t c ~~> t d)

it's possible to describe maps, folds and traversals that will work for type-aligned sequences:

class TFoldable t where
  tfoldMap :: Category d => (c ~~> d) -> t c ~~> d
  tfoldMap f = tfoldr (\cij djk -> f cij >>> djk) id

class (TFunctor t, TFoldable t) => TTraversable t where
  ttraverse :: IxApplicative f
            => (forall x y . c x y -> f x y (d x y))
            -> (t c p q -> f p q (t d p q))

Now it turns out that it's possible to define a version of Data.Functor.Reverse for type-aligned sequences. Specifically

newtype Reverse t c x y = Reverse {unReverse :: t (Dual c) y x}

where

newtype Dual c x y = Dual {getDual :: c y x}

When the type t is actually a type-aligned sequence, it's straightforward to give Reverse t the full complement of type-aligned sequence operations.

---

The actual question

What's not clear to me is whether t being IxTraversable is sufficient to implement IxTraversable (Reverse t). Everything I've tried hits a brick wall. For standard Traversables, this can be done using a Backwards applicative. There is an IxBackwards available, but it doesn't seem to help. For standard Traversables, it's possible to dump the container contents into a list, then pull back in from the list. But that doesn't seem to be possible here, because there's no apparent way to record the types on the way out and ensure they'll match up on the way in. Have I missed something, or is this a no-go?

The barest start:

instance IxTraversable t => IxTraversable (Reverse t) where
  ttraverse f (Reverse xs) = Reverse `ixmap` _ xs

This gets me a hole of type

t (Dual c) q p -> f p q (t (Dual d) q p)

The obvious challenge is that we have t _ q p, but f p q _. So if there's a way to do this, we presumably need to somehow come up with an f that will flip things. As I said before, there's an IxBackwards

newtype IxBackwards f y x a = IxBackwards { ixforwards :: f x y a }

but I don't see how this helps.

Answer 1

Your setup is sound, and IxBackwards is useful (in fact, critical) - the issue you have run into is the fact that both Dual and Reverse swap positions of type variables, whereas the first argument of ttraverse requires the positions of the quantified type variables (x,y) to 'agree' in a sense. You must simultaneously 'flip' these variables in the recursive call to ttraverse using both Dual and IxBackwards:

instance TTraversable t => TTraversable (Reverse t) where

  ttraverse f = 
    ixmap Reverse . ixforwards . 
    ttraverse (IxBackwards . ixmap Dual . f . getDual) . 
    unReverse 

Writing the instances for TFunctor and TFoldable may give a hint as to how to find this implementation:

dualNat2 :: (c ~~> d) -> Dual c ~~> Dual d 
dualNat2 k (Dual x) = Dual $ k x 

instance TFunctor f => TFunctor (Reverse f) where 
  tmap f (Reverse q) = Reverse $ tmap (dualNat2 f) q 

instance TFoldable f => TFoldable (Reverse f) where 
  tfoldMap k (Reverse z) = getDual $ tfoldMap (dualNat2 k) z 

You essentially do the same in the case of TTraversable, except now there are two indices to flip:

f                                      :: forall x y . c x y -> f x y (d x y)   
ixmap Dual . f . getDual               :: forall x y . Dual c y x -> f x y (Dual d y x)
IxBackwards . f                        :: forall x y . c x y -> IxBackwards f y x (d x y)
IxBackwards . ixmap Dual . f . getDual :: forall x y . Dual c y x -> IxBackwards f y x (Dual d y x)

and note that if you only flip one of the indices, the type of the function doesn't even match the type of the argument to ttraverse.

---

I'll try to give a step-by-step derivation using Typed Holes.

Begin with this skeleton, which I think is trivial to derive:

  ttraverse f = 
    ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

This gives a type error:

Couldn't match type `q' with `p'
...
Expected type: Reverse t c p q -> f p q (Reverse t d p q)
Actual type: Reverse t c q p -> f p q (Reverse t d q p)
* In the expression: ixmap Reverse . ttraverse _trfun . unReverse

So add more holes until it compiles. My first instinct is to add another hole to the front (since the type error is for the whole expression, something has to be done to the whole expression to make it typecheck):

  ttraverse f = 
    _out . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

Now we get no type errors (ignoring 'ambiguous type' errors of the form C x where C is a class - there are erroneous) and the type reported is

 _out :: f0 q p (Reverse t c0 p q) -> f p q (Reverse t d p q)

where f0, c0 are (currently) free type variables, which we use to our advantage! If we let c0 ~ d and f0 ~ IxBackwards f then this is precisely the type of ixforwards - so let's try it:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

and now we get a nice monomorphic inferred type:

 _trfun :: Dual c x y -> IxBackwards f x y (Dual d x y)
 * Relevant bindings include
     f :: forall (x :: r) (y :: r). c x y -> f x y (d x y)

Now I also assume it is obvious that _trfun should somehow use f, so let's try that. We notice that both the domain and range of f are not exactly that of _trfun so we place a hole on both sides:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . f . _in) . 
    unReverse 

and get:

_out :: f x0 y0 (d x0 y0) -> IxBackwards f x y (Dual d x y)
_in :: Dual c x y -> c x0 y0

where x0, y0 are free variables. It is probably most obvious that with x0 ~ y, y0 ~ x, we have _in = getDual, so we try that, and get a new inferred type:

_out :: f y x (d y x) -> IxBackwards f x y (Dual d x y)

and now it is obvious to see that the type variables are 'flipped' in two different places; once by IxBackwards and once by Dual. The way to flip the first pair of indices is most obvious (probably):

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . IxBackwards . f . getDual) . 
    unReverse 

and get:

_out :: IxBackwards f x y (d y x) -> IxBackwards f x y (Dual d x y)

Now we have something of the form q A -> q B with IxFunctor q, so setting _out = ixmap _out we get

_out :: d y x -> Dual d x y

and there is a trivial function of this type - namely Dual - which completes the definition:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (ixmap Dual . IxBackwards . f . getDual) . 
    unReverse 

Note how some function compositions are flipped compared to the original version - I was pretending I didn't know the answer a priori and derived it in the 'most obvious' way, by filling in the things which are simplest first. The two definitions are equivalent (truly equivalent, since Dual and IxBackwards are both just newtypes).