Продуманная правильная перестановка менее чем O (n ^ 2)

Написанный в Haskell, вот тип данных, который доказывает, что один список является перестановкой другой:

data Belongs (x :: k) (ys :: [k]) (zs :: [k]) where
  BelongsHere :: Belongs x xs (x ': xs)
  BelongsThere :: Belongs x xs xys -> Belongs x (y ': xs) (y ': xys)

data Permutation (xs :: [k]) (ys :: [k]) where
  PermutationEmpty :: Permutation '[] '[]
  PermutationCons :: Belongs x ys xys -> Permutation xs ys -> Permutation (x ': xs) xys

С помощью Permutation мы можем переписать запись:

data Rec :: (u -> *) -> [u] -> * where
  RNil :: Rec f '[]
  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)

insertRecord :: Belongs x ys zs -> f x -> Rec f ys -> Rec f zs
insertRecord BelongsHere v rs = v :& rs
insertRecord (BelongsThere b) v (r :& rs) = r :& insertRecord b v rs

permute :: Permutation xs ys -> Rec f xs -> Rec f ys
permute PermutationEmpty RNil = RNil
permute (PermutationCons b pnext) (r :& rs) = insertRecord b r (permute pnext rs)

Это прекрасно работает. Тем не менее, permute O(n^2), где n - длина записи. Мне интересно, есть ли способ сделать это быстрее, используя другой тип данных для представления перестановки.

Для сравнения, в изменяемой и нетипизированной настройке (которая, как мне известно, действительно отличается от очень), мы могли бы применить перестановку к гетерогенной записи, подобной этой, в O(n) времени. Вы представляете запись как массив значений и перестановку в виде массива новых позиций (дубликаты не допускаются, а все цифры должны быть между 0 и n). Применение перестановки - это просто повторение этого массива и индексация в массив записей с этими позициями.

Я не ожидаю, что перестановка O(n) возможна в более строго типизированных настройках. Но похоже, что O(n*log(n)) возможно. Я ценю любую обратную связь, и дайте мне знать, если мне нужно что-то разъяснить. Кроме того, ответы на это могут использовать Haskell, Agda или Idris в зависимости от того, с чем легче общаться.