Total reversing for Traversable

ReverseTraversable.hs

{-# language
  TypeInType, ScopedTypeVariables, RankNTypes,
  GADTs, TypeOperators, TypeApplications, BangPatterns
#-}

-- requires ghc-typelits-natnormalise
{-# options_ghc -fplugin GHC.TypeLits.Normalise #-}

{-|
Tested with ghc-8.4.3

Challenge by dfeuer: https://stackoverflow.com/questions/51812947/how-to-write-reverset-without-using-list

Reversing any Traversable with a total well-typed function. Works the following way:
  1. Convert structure to size-indexed syntax tree.
  2. Build size-indexed reversed vector of elements from the tree by left folding.
  3. Fill tree with elements of the vector, then convert back to structure (we
     merge these two into one pass).

Although this operation should be linear, it doesn't seem to be very fast.

We use ghc-typelits-natnormalise to get rid of arithmetic proofs. It's
important for performance as well, because hand-written arithmetic
proofs are not erased and would definitely make the complexity at
least quadratic.
-}

import Data.Kind
import GHC.TypeLits

data Vec a n where
  Nil  :: Vec a 0
  (:>) :: a -> Vec a n -> Vec a (1 + n)
infixr 5 :>

data Exp a r n where
  One  :: a -> Exp a a 1
  Pure :: r -> Exp a r 0
  Ap   :: Exp a (r -> s) n -> Exp a r m -> Exp a s (n + m)

data Exp' a r where
  Exp' :: Exp a r n -> Exp' a r

instance Functor (Exp' a) where
  fmap f (Exp' e) = Exp' (Ap (Pure f) e)

instance Applicative (Exp' a) where
  pure = Exp' . Pure
  Exp' f <*> Exp' x = Exp' (Ap f x)

newtype AddN n f x = AddN {unAddN :: f (n + x)}

foldlExp ::
     forall (b :: Nat -> Type) a n r
   . (forall n. b n -> a -> b (1 + n))
  -> b 0
  -> Exp a r n -> b n
foldlExp f !z (One a)    = f z a
foldlExp f z  (Pure r)   = z
foldlExp f z  (Ap t u)   =
  unAddN (foldlExp (\(AddN b) a -> AddN (f b a))
                   (AddN (foldlExp f z t)) u)

runFill :: forall a r n. Vec a n -> Exp a r n -> r
runFill as e = fst (go @a @r @n @0 as e) where
  go :: forall a r n m. Vec a (n + m) -> Exp a r n -> (r, Vec a m)
  go (a :> as) (One _)    = (a, as)
  go as        (Pure r)   = (r, as)
  go as        (Ap t u)   = case go as t of
    (f, as') -> case go as' u of
      (a , as'') -> (f a, as'')

reverseT :: forall t a. Traversable t => t a -> t a
reverseT ta = case traverse (Exp' . One) ta of
  Exp' e -> runFill (foldlExp (flip (:>)) Nil e) e