How can I express foldr in terms of foldMap for type-aligned sequences?

Question

I'm playing around with type-aligned sequences, and in particular I'm messing around with the idea of folding them. A foldable type-aligned sequence looks something like this:

class FoldableTA fm where
  foldMapTA :: Category h =>
                (forall b c . a b c -> h b c) ->
                fm a b d -> h b d
  foldrTA :: (forall b c d . a c d -> h b c -> h b d) ->
             h p q -> fm a q r -> h p r
  foldlTA :: ...

It's pretty easy to implement foldrTA in terms of foldMapTA by first using foldMapTA to convert the sequence to a type-aligned list in the naive way (i.e., using the type-aligned list category) and then folding over that list. Unfortunately, this can be quite inefficient because long lists may be prepended to short ones. I've been trying to figure out a way to use a trick similar to the one used in Data.Foldable to define the right and left folds more efficiently, but the types are making me dizzy. Endo does not seem general enough to do the trick, and every step I take in other directions leads me to more type variables than I can keep track of.

Answer 1

I found that this typechecks:

{-# LANGUAGE RankNTypes #-}
module FoldableTA where

import Control.Category
import Prelude hiding (id, (.))

class FoldableTA fm where
  foldMapTA :: Category h => (forall b c . a b c -> h b c) -> fm a b d -> h b d
  foldrTA :: (forall b c d . a c d -> h b c -> h b d) -> h p q -> fm a q r -> h p r
  foldrTA f z t = appEndoTA (foldMapTA (\x -> TAEndo (f x)) t) z

newtype TAEndo h c d = TAEndo { appEndoTA :: forall b. h b c -> h b d  }

instance Category (TAEndo h) where
    id = TAEndo id
    TAEndo f1 . TAEndo f2 = TAEndo (f1 . f2)

No idea if it makes any sense, but with so many type indexes around, I doubt that there is much type-checking code that does not make sense.